theory Sets imports Main begin text{*A manual proof in set theory:*} thm equalityI subsetI thm UnI1 UnI2 UnE lemma "A Un B = B Un A" apply(rule equalityI) apply(rule subsetI) apply(erule UnE) apply(rule UnI2) apply(assumption) apply(rule UnI1) apply(assumption) apply(rule subsetI) apply(erule UnE) apply(rule UnI2) apply(assumption) apply(rule UnI1) apply(assumption) done text{* Most simple proofs in set theory are automatic: *} lemma "-(A \ B) = (-A \ -B)" by(blast) lemma "{x . P x \ Q x} = {x . P x} \ {x. Q x}" by(blast) lemma "((A:: 'a set) \ -B) = (B \ -A)" by blast lemma "A Int B = B Int A" by blast lemma "A Int (B - A) = {}" by blast lemma "{a,b} Un {a,d} = {a,b,d}" by blast lemma "{a,b} Int {b,c} = (if a = c then {a,b} else {b})" apply simp by blast text{*set comprehension*} lemma "{p*q | p q. p \ prime \ q \ prime}= {z. \p q. z = p*q \ p \ prime \ q \ prime}" oops subsection{*Inductive definition of the even numbers*} inductive_set Ev :: "nat set" where ZeroI: "0 : Ev" | Add2I: "n : Ev \ Suc(Suc n) : Ev" inductive_set even :: "nat set" where zero[intro!]: "0 \ even" | step[intro!]: "n \ even \ (Suc(Suc n)) \ even" text{* Using the introduction rules: *} lemma "Suc(Suc(Suc(Suc 0))) \ Ev" apply(rule Add2I) apply(rule Add2I) apply(rule ZeroI) done text{*A simple inductive proof: *} lemma "Suc(Suc(Suc(Suc 0))) \ even" apply(rule step) apply(rule step) apply auto done lemma "Suc(Suc 0) : even" apply auto done text{*lemma "\ Suc 0 \ even"*} lemma "n:Ev \ n+n : Ev" apply(induct rule: Ev.induct) apply(simp) apply(rule Ev.ZeroI) apply(simp) apply(rule Ev.Add2I) apply(rule Ev.Add2I) apply(assumption) done lemma two_times_even[intro!]: "2*n \ even" apply(induct_tac n) apply auto done lemma two_times_ev[intro!]: "2*n \ Ev" apply(induct_tac n) apply auto apply(rule Ev.ZeroI) apply(rule Ev.Add2I) apply(assumption) done declare Ev.intros[simp] text{*lemma "n \ Ev \ n \ even" apply(erule Ev.induct) apply auto apply(assumption) declare Ev.intros[simp]*} lemma "n \ Ev \ n+n \ Ev" apply (induct_tac n) apply(auto) oops lemma dvd_imp_even: "2 dvd n \ n \ even" by (auto simp add: dvd_def) lemma "2 dvd n \ n \ Ev" by (auto simp add: dvd_def) text{* You can also use the rules for Ev as conditional simplification rules. This can shorten proofs considerably. \emph{Warning}: conditional rules can lead to nontermination of the simplifier. The rules for Ev are OK because the premises are always smaller than the conclusion. The list of rules for Ev is contained in Ev.intrs. *} declare Ev.intros[simp] text{* A shorter proof: *} lemma "n:Ev \ n+n : Ev" apply(induct rule: Ev.induct) apply(auto) done text{* Nice example, but overkill: don't need assumption @{prop"n \ Ev"} because @{prop"n+n \ Ev"} is true for all @{text n}. However, here we really need the assumptions: *} lemma "2*n : Ev" apply (induct_tac n) apply simp apply auto done lemma double: "n+n = (2::nat)*n" apply (induct_tac n) apply auto done lemma "\ m:Ev; n:Ev \ \ m+n : Ev" apply(induct rule: Ev.induct) apply(auto) done text{* An inductive proof of @{prop"1 \ Ev"}: *} lemma "n \ Ev \ n \ 1" apply(induct rule: Ev.induct) apply(auto) done text{* The general case: *} lemma "n \ Ev \ \(\k. n = 2*k+1)" apply(induct rule: Ev.induct) apply(simp) apply arith done lemma even_imp_dvd: "n \ even \ 2 dvd n" apply (erule even.induct) apply (simp_all add: dvd_def) apply clarify apply (rule_tac x = "Suc k" in exI, simp) done theorem even_iff_dvd: "(n \ even) = (2 dvd n)" by (blast intro: dvd_imp_even even_imp_dvd) theorem even_iff_Ev: "(n \ even) = (n \ Ev)" apply(induct_tac n) apply auto oops lemma even_in_Ev: "n \ even \ n \ Ev" apply(induct rule: even.induct) apply auto done lemma Ev_in_even: "n \ Ev \ n \ even" apply(induct rule: Ev.induct) apply auto done theorem even_iff_Ev: "(n \ even) = (n \ Ev)" by (blast intro: even_in_Ev Ev_in_even) lemma "Suc (Suc n) \ even \ n \ even" apply (erule even.induct) oops lemma "(0::nat) - 2 = 0" apply(rule Nat.diff_0_eq_0) done lemma "(Suc (Suc n)) - 2 = n" apply(induct_tac n) apply auto done lemma even_imp_even_minus_2: "n \ even \ n - 2 \ even" apply (erule even.induct) apply auto done lemma Suc_Suc_even_imp_even: "Suc (Suc n) \ even \ n \ even" by (drule even_imp_even_minus_2, simp) lemma [iff]: "((Suc (Suc n)) \ even) = (n \ even)" by (blast dest: Suc_Suc_even_imp_even) inductive_cases Suc_Suc_cases [elim!]: "Suc(Suc n) \ even" inductive_set Even :: "nat set" and Odd :: "nat set" where zero: "0 \ Even" | EvenI: "n \ Odd \ Suc n \ Even" | OddI: "n \ Even \ Suc n \ Odd" lemma "(m \ Even \ 2 dvd m) \ (n \ Odd \ 2 dvd (Suc n))" apply(rule Even_Odd.induct) apply simp apply simp apply (simp_all add: dvd_def) apply clarify apply (rule_tac x = "Suc k" in exI) apply simp done subsection{*Reflexive Transitive closure*} inductive_set rtc :: "('a * 'a)set \ ('a * 'a)set" ("_*" [1000] 999) for r :: "('a * 'a)set" where rtc_ref1[iff]: "(x,x) \ r*" | rtc_step: "\ (x,y) \ r; (y,z) \ r* \ \ (x,z) \ r*" lemma [intro]: "(x,y)\ r \ (x,y) \ r*" by(blast intro: rtc_step) lemma rtc_trans: "\ (x,y) \ r*; (y,z) \ r* \ \ (x,z) \ r*" apply(erule rtc.induct) oops text{*unifikation mit erster Premisse von rtc.induct zu allgemein. Heuristik.Abhängigkeit von y nicht auf rechter Seite, verschiebe y Prämissen*} lemma rtc_trans[rule_format]: "(x,y) \ r* \ (y,z) \ r* \ (x,z) \ r*" apply(erule rtc.induct) apply(blast) apply(blast intro:rtc_step) done inductive_set rtc2 :: "('a * 'a)set \ ('a * 'a)set" for r :: "('a * 'a)set" where "(x,y) \ r \ (x,y) \ rtc2 r" | "(x,x) \ rtc2 r" | "\ (x,y) \ rtc2 r; (y,z) \ rtc2 r \ \ (x,z) \ rtc2 r" lemma "(x,y) \ rtc2 r \ (x,y) \ r*" apply(erule rtc2.induct) apply(blast) apply(blast) apply(blast intro: rtc_trans) done lemma "(x,y) \ r* \ (x,y) \ rtc2 r" apply(erule rtc.induct) apply(blast intro: rtc2.intros) apply(blast intro: rtc2.intros) done lemma "\(x,y) \ r*; (y,z) \ r \ \ (x,z) \ r*" apply(erule rtc.induct) oops lemma rtc_inv: "(x,y) \ r* \ (y,z) \ r \ (x,z) \ r*" apply(erule rtc.induct) apply(blast) apply(blast intro: rtc_step) done lemma "\(x,y) \ r*; (y,z) \ r \ \ (x,z) \ r*" apply (drule rtc_inv) apply (drule mp) apply(auto) done inductive_set rtc1 :: "('a * 'a)set \ ('a * 'a)set" for r :: "('a * 'a)set" where rtc1_ref1[iff]: "(x,x) \ rtc1 r" | rtc1_step: "\ (x,y) \ rtc1 r; (y,z) \ r \ \ (x,z) \ rtc1 r" lemma "\ (x,x) \ rtc1 r; (x,y) \ r \ \ (x,y) \ rtc1 r" apply(erule rtc1_step) apply(assumption) done lemma [intro]: "(x,y)\ r \ (x,y) \ rtc1 r" by(blast intro: rtc1_step) lemma "\ (x,y) \ rtc1 r; (y,z) \ r \ \ (x,z) \ rtc1 r" apply(erule rtc1_step) apply (assumption) done lemma "(x,y) \ rtc1 r \ (y,z) \ r \ (x,z) \ rtc1 r" by(blast intro: rtc1_step) lemma "(y,z) \ r \ (x,y) \ rtc1 r \ (x,z) \ rtc1 r" by(blast intro: rtc1_step) lemma rtc1_trans: "\ (x,y) \ rtc1 r; (y,z) \ rtc1 r \ \ (x,z) \ rtc1 r" apply(erule rtc1.induct) oops text{*unifikation mit erster Premisse von rtc.induct zu allgemein. Heuristik.Abhängigkeit von y nicht auf rechter Seite, verschiebe y Prämissen*} lemma rtc1_trans [rule_format]: "(y,z) \ rtc1 r \ \x. (x,y) \ rtc1 r \ (x,z) \ rtc1 r" --"apply(rule_tac ?x1.0=x and ?x2.0=z in rtc1.induct)" apply (erule rtc1.induct) apply blast apply clarify apply (drule_tac x=xa in spec) apply (blast intro: rtc1.intros) done lemma "(x,y) \ rtc2 r \ (x,y) \ rtc1 r" apply(erule rtc2.induct) apply(blast) apply(blast) apply(blast intro: rtc1_trans) done lemma "(x,y) \ rtc1 r \ (x,y) \ rtc2 r" apply(erule rtc1.induct) apply(blast intro: rtc2.intros) apply(blast intro: rtc2.intros) done subsection{*Universal quantifiers in intro rules*} datatype 'f gterm = Apply 'f "'f gterm list" datatype integer_op = Number int | UnaryMinus | Plus --"type integer_op gterm denotes the ground terms build over those symbols" inductive_set gterms :: "'f set \ 'f gterm set" for F :: "'f set" where step[intro!]: " \\ t \ set args. t \ gterms F; f \ F\ \ (Apply f args) \ gterms F" lemma gterms_mono: "F \ G \ gterms F \ gterms G" apply clarify apply (erule gterms.induct) apply blast done inductive_set well_formed_gterm :: "('f \ nat) \ 'f gterm set" for arity :: "'f \ nat" where step[intro!]: "\\ t \ set args. t \ well_formed_gterm arity; length args = arity f\ \ (Apply f args) \ well_formed_gterm arity" --"alternative definition using a monotone function" inductive_set well_formed_gterm' :: "('f \ nat) \ 'f gterm set" for arity :: "'f \ nat" where step[intro!]: "\args \ lists (well_formed_gterm' arity); length args = arity f\ \ (Apply f args) \ well_formed_gterm' arity" monos lists_mono --"notice all references to an inductively defined set must be positive" --"proving the equivalende of the definitions" lemma "well_formed_gterm arity \ well_formed_gterm' arity" apply clarify apply (erule well_formed_gterm.induct) apply auto done lemma "well_formed_gterm' arity \ well_formed_gterm arity" apply clarify apply (erule well_formed_gterm'.induct) apply auto done inductive_cases gterm_Apply_elim [elim!]: "Apply f args \ gterms F" lemma gterms_IntI [rule_format, intro!]:"t \ gterms F \ t \ gterms G \ t \ gterms (F \ G)" apply (erule gterms.induct) apply blast done lemma gterms_Int_eq [simp]: "gterms (F \ G) = gterms F \ gterms G" by (blast intro!: mono_Int monoI gterms_mono) inductive_set well_typed_gterm :: "('f \ 't list * 't) \ ('f gterm * 't)set" for sig :: "'f \ 't list * 't" where step[intro!]:"\argsp \ lists (well_typed_gterm sig); map (snd) argsp = fst (sig f) \ \ (Apply f (map (fst) argsp), snd (sig f)) \ well_typed_gterm sig" monos lists_mono --"Context free grammar S\ eps| bA | aB A \ aS | bAA B \ bS | aBB " datatype alfa = a | b lemma [simp]: "(x \ a) = (x = b) \ (x \ b) = (x = a)" by (case_tac x, auto) inductive_set S :: "alfa list set" and A :: "alfa list set" and B :: "alfa list set" where "[] \ S" | "w \ A \ b#w \ S" | "w \ B \ a#w \ S" | "w \ S \ a#w \ A" | "\ v \ A; w \ A \ \ b#v@w \ A" | "w \ S \ b#w \ B" | "\ v \ B; w \ B \ \ a#v@w \ B" lemma correctness: "(w \ S \ size[x \ w. x=a] = size[x \ w. x=b]) \ (w \ A \ size[x \ w. x=a] = size[x \ w. x=b]+ 1) \ (w \ B \ size[x \ w. x=b] = size[x \ w. x=a]+ 1)" by (rule S_A_B.induct, auto) lemma step1: "\ i < size w. \ (int(size[x\take (i + 1) w. P x]) - int(size[x\ take (i + 1) w. \ P x])) - (int(size[x\ take i w. P x]) - int(size[x\ take i w. \ P x])) \ \ 1" apply(induct_tac w) apply(auto simp add: abs_if take_Cons split: nat.split) done lemma part1: "size[x\w. P x] = size[x\w. \ P x] + 2 \ \ i \ size w. size[x\take i w. P x] = size[x\take i w. \ P x] + 1" apply(insert nat0_intermed_int_val[OF step1, of "P" "w" "1"]) by force --"suffix part" lemma part2: "\size[x\ take i w @ drop i w. P x] = size[x\ take i w @ drop i w. \ P x] + 2; size[x\ take i w . P x] = size[x\ take i w . \ P x] + 1\ \ size[x\ drop i w . P x] = size[x\ drop i w . \ P x] +1" by(simp del: append_take_drop_id) declare S_A_B.intros[simp] theorem completeness: "(size[x\w . x=a] = size[x\w . x=b] \ w \ S) \ (size[x\w . x=a] = size[x\w . x=b] + 1 \ w \ A) \ (size[x\w . x=b] = size[x\w . x=a] + 1 \ w \ B)" apply(induct_tac w rule: length_induct) apply(rename_tac w) apply(case_tac w) apply(simp_all) apply(rule conjI) apply(clarify) apply(frule part1[of "\ x. x = a", simplified]) apply(clarify) apply(drule part2[of "\ x. x = a", simplified]) apply(assumption) apply(rule_tac n1 = i and t=list in subst[OF append_take_drop_id]) apply(rule S_A_B.intros) apply(force simp add: min_less_iff_disj) apply(force split add: nat_diff_split) apply(clarify) apply(frule part1[of "\ x. x = b", simplified]) apply(clarify) apply(drule part2[of "\ x. x = b", simplified]) apply(assumption) apply(rule_tac n1 = i and t=list in subst[OF append_take_drop_id]) apply(rule S_A_B.intros) apply(force simp add: min_less_iff_disj) apply(force split add: nat_diff_split) done --"last line can be also done with by(force simp add: min_less_iff_disj split add: nat_diff_split)" subsection{*Inductive definition of AVL trees*} datatype tree = Tip | Br tree tree --"AVL trees come with their height (t,h)" inductive_set AVL :: "(tree * nat)set" where "(Tip,0) : AVL" | "\ (t,m) : AVL; (u,n) : AVL; m=n | m = n+1 | n = m+1 \ \ (Br t u, max m n + 1) : AVL" text{* We prove a lower bound for the number of internal nodes in an AVL tree of height h. *} fun fib1 :: "nat => nat" where "fib1 0 = 0" | "fib1 (Suc 0) = 1" | "fib1 (Suc (Suc x)) = fib1 x + fib1 (Suc x) + 1" lemma fib1_Suc: "fib1(Suc n) \ 2*fib1(n) + 1" apply(induct n rule: fib1.induct) apply auto done --"where is size defined? Every datatype has such a function: Here Number of internal nodes" lemma "(t,h) : AVL \ fib1 h \ size t" apply(induct rule:AVL.induct) apply simp apply(erule disjE) apply simp apply(cut_tac n=n in fib1_Suc) apply arith apply(erule disjE) apply (simp add:max_def) apply (simp add:max_def) done end