greedy_section.thy

(* 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