Last active
March 14, 2020 19:06
-
-
Save hatsugai/d8253fc07a720deff290e91a4d33bb2d to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* Isabelle/HOL 2014 *) | |
theory "greedy_section" imports Main begin | |
definition sound :: "(nat * nat) set => bool" where | |
"sound X = (ALL p. p : X --> fst p < snd p)" | |
inductive_set greedy :: "(nat * nat) set => (nat * nat) list set" | |
for A :: "(nat * nat) set" | |
where | |
greedy_base: | |
"[| (a, b) : A; ALL c d. (c, d) : A --> b <= d |] | |
==> [(a, b)] : greedy A" | |
| greedy_step: | |
"[| (a1, b1)#ps : greedy A; | |
(a, b) : A; b1 <= a; | |
ALL x y. (x, y) : A --> b1 <= x --> b <= y |] | |
==> (a, b)#(a1, b1)#ps : greedy A" | |
inductive_set nowrap :: "(nat * nat) set => (nat * nat) list set" | |
for A :: "(nat * nat) set" | |
where | |
nowrap_base: "(a, b) : A ==> [(a, b)] : nowrap A" | |
| nowrap_step: | |
"[| (a1, b1)#ps : nowrap A; (a, b) : A; b1 <= a |] | |
==> (a, b)#(a1, b1)#ps : nowrap A" | |
lemma ex_min [rule_format]: | |
"finite (X::(nat * nat) set) ==> | |
X ~= {} --> | |
(EX m. m : X & (ALL x. x : X --> snd m <= snd x))" | |
apply(erule finite_induct) | |
apply(auto) | |
by (metis le_trans nat_le_linear) | |
lemma greedy_min: | |
"ps : nowrap A ==> | |
finite A --> | |
sound A --> | |
ps ~= [] --> | |
(EX ms. ms : greedy A & length ms = length ps & snd (hd ms) <= snd (hd ps))" | |
apply(erule nowrap.induct) | |
apply(auto) | |
apply(drule ex_min) | |
apply(clarsimp) | |
apply(clarsimp) | |
apply(rule_tac x="[(aa, ba)]" in exI) | |
apply(clarsimp) | |
apply(rule greedy_base) | |
apply(assumption) | |
apply(blast) | |
(**) | |
apply(subgoal_tac "finite {p. p : A & snd (hd ms) <= fst p}") | |
defer | |
apply(clarsimp) | |
apply(rotate_tac -1) | |
apply(drule_tac X="{p. p : A & snd (hd ms) <= fst p}" in ex_min) | |
apply(clarsimp) | |
apply (metis le_trans) | |
apply(clarsimp) | |
apply(rule_tac x="(aa, ba)#ms" in exI) | |
apply(clarsimp) | |
apply(rule) | |
apply(case_tac ms) | |
apply(clarsimp) | |
apply(clarsimp) | |
apply(rule greedy_step) | |
apply(clarsimp) | |
apply(clarsimp) | |
apply(clarsimp) | |
apply(clarsimp) | |
by (metis le_trans) | |
theorem greedy_max_count: | |
"[| ps : nowrap A; finite A; sound A; ps ~= [] |] ==> | |
EX ms. ms : greedy A & length ps <= length ms" | |
apply(drule greedy_min) | |
apply(clarsimp) | |
by (metis eq_iff) | |
end |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment