theory week04B_demo_sol imports Main begin \ \---------------------------------------------------\ text\A manual proof in set theory:\ thm equalityI subsetI UnI1 UnI2 UnE lemma "(A \ B) = (B \ A)" apply (rule equalityI) apply (rule subsetI) apply (erule UnE) apply (rule UnI2, assumption) apply (rule UnI1, assumption) apply (rule subsetI) apply (erule UnE) apply (erule UnI2) apply (erule UnI1) done (* try: find_theorems intro, find_theorems elim *) lemma "(A \ B) = (B \ A)" apply (rule equalityI) apply (rule subsetI) apply (rule IntI) apply (erule IntE, assumption) apply (erule IntE, assumption) apply (rule subsetI) apply (rule IntI) apply (erule IntE, assumption) apply (erule IntE, assumption) done text\Note that "by blast" works as well\ text \As an exercise, try the following one\ lemma "(A \ B \ C) = (A \ C \ B \ C)" apply (rule iffI) apply (rule conjI) apply (rule subsetI) apply (erule subsetD) apply (erule UnI1) apply (rule subsetI) apply (erule subsetD) apply (erule UnI2) apply (erule conjE) apply (rule subsetI) apply (erule UnE) apply (erule subsetD, assumption) apply (erule subsetD, assumption) done text\Note that "by blast" works as well\ text\Most simple proofs in set theory are automatic:\ lemma "{a, b} \ {b, c} = (if a=c then {a, b} else {b})" apply simp apply blast done lemma "-(A \ B) = (-A \ -B)" by blast lemma "{x. P x \ Q x} = {x. P x} \ {x. Q x}" by blast \ \--------------------------------------------\ text \Introducing new types\ \ \a new "undefined" type:\ typedecl names consts blah :: names \ \simple abbreviation:\ type_synonym 'a myrel = "'a \ 'a \ bool" definition eq :: "'a myrel" where "eq x y \ (x = y)" term "eq" \ \type definition: pairs\ typedef three = "{0::nat,1,2}" apply (rule_tac x=1 in exI) apply blast done print_theorems definition Prod :: "('a \ 'b \ bool) set" where "Prod \ {f. \a b. f = (\(x::'a) (y::'b). x=a \ y=b)}" typedef ('a, 'b) prod = "Prod::('a \ 'b \ bool) set" by (auto simp: Prod_def) (* To understand this proof, try: apply (simp add: Prod_def) -- "just need to exhibit *one* pair, any" apply (rule_tac x="\x y. x=blah1 \ y=blah2" in exI) apply (rule_tac x=blah1 in exI) apply (rule_tac x=blah2 in exI) apply (rule refl) *) print_theorems definition pair :: "'a \ 'b \ ('a,'b) prod" where "pair a b \ Abs_prod (\x y. x = a \ y = b)" definition fs :: "('a,'b) prod \ 'a" where "fs x \ SOME a. \b. x = pair a b" definition sn :: "('a,'b) prod \ 'b" where "sn x \ SOME b. \a. x = pair a b" lemma in_Prod: "(\x y. x = c \ y = d) \ Prod" apply (unfold Prod_def) apply blast done lemma pair_inject: "pair a b = pair a' b' \ a=a' \ b=b'" apply (unfold pair_def) apply (drule iffD1 [OF Abs_prod_inject[OF in_Prod in_Prod]]) apply (drule fun_cong)+ apply auto done (* apply (unfold pair_def) apply (subgoal_tac "(\x y. x = a \ y = b) \ Prod") apply (subgoal_tac "(\x y. x = a' \ y = b') \ Prod") prefer 2 apply (rule in_Prod) apply (simp add: Abs_prod_inject) apply (drule_tac x=a in fun_cong) apply (drule_tac x=b in fun_cong) apply simp apply (rule in_Prod) done *) (* apply (unfold pair_def) apply (simp add: Abs_prod_inject [OF in_Prod in_Prod]) apply (blast dest: fun_cong) done *) (* apply (unfold pair_def) apply (cut_tac c=a and d=b in in_Prod) apply (insert in_Prod[where c=a' and d=b']) apply (simp add: Abs_prod_inject) apply (drule_tac x=a in fun_cong) apply (drule_tac x=b in fun_cong) apply simp done *) (* apply (unfold pair_def) apply (insert in_Prod [of a b]) apply (insert in_Prod [of a' b']) apply (blast dest: Abs_prod_inject fun_cong) done *) (* apply (unfold pair_def) apply (simp add: Abs_prd_inject in_prd) apply (drule_tac x=a in fun_cong) apply (drule_tac x=b in fun_cong) apply auto done *) lemma pair_eq: "(pair a b = pair a' b') = (a=a' \ b=b')" by (blast dest: pair_inject) lemma fs: "fs (pair a b) = a" apply (unfold fs_def) apply (blast dest: pair_inject) done lemma sn: "sn (pair a b) = b" apply (unfold sn_def) apply (blast dest: pair_inject) done \ \--------------------------------------------\ section\Inductive definitions\ subsection\Inductive definition of finite sets\ inductive_set Fin :: "'a set set" where emptyI: "{} \ Fin" | insertI: "A \ Fin \ insert a A \ Fin" print_theorems subsection\Inductive definition of the even numbers\ inductive_set Ev :: "nat set" where ZeroI: "0 \ Ev" | Add2I: "n \ Ev \ Suc(Suc n) \ Ev" print_theorems text\Using the introduction rules:\ lemma "Suc(Suc(Suc(Suc 0))) \ Ev" thm ZeroI Add2I apply(rule Add2I) apply(rule Add2I) apply(rule ZeroI) done text\Using the case elimination rules:\ lemma "n \ Ev \ n = 0 \ (\n' \ Ev. n = Suc (Suc n'))" thm Ev.cases apply(blast elim: Ev.cases) done text\A simple inductive proof:\ lemma "n \ Ev \ n+n \ Ev" thm Ev.induct apply(erule Ev.induct) apply(simp) apply(rule ZeroI) apply(simp) apply(rule Add2I) apply(rule Add2I) apply assumption done 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.intros.\ thm Ev.intros declare Ev.intros[simp] text\A shorter proof:\ lemma "n \ Ev \ n+n \ Ev" apply(erule Ev.induct) apply(simp_all) done text\Nice example, but overkill: don't need assumption @{prop "n \Ev"} because @{prop"n+n \ Ev"} is true for all @{text n}.\ lemma "n+n \ Ev" apply(induct n) (* You'll learn about this proof method in week05B *) apply simp apply simp done text\However, here we really need the assumptions:\ lemma "\ m \ Ev; n \ Ev \ \ m+n \ Ev" apply(erule Ev.induct) apply(auto) done text\An inductive proof of @{prop "1 \ Ev"}:\ thm Ev.induct lemma "n \ Ev \ n \ 1" apply(erule Ev.induct) apply(simp)+ done text\The general case:\ lemma "n \ Ev \ \(\k. n = 2*k+1)" apply(erule Ev.induct) apply simp apply arith done subsection\Proofs about finite sets\ text\Above we declared @{text Ev.intros} as simplification rules. Now we declare @{text Fin.intros} as introduction rules (via attribute ``intro''). Then fast and blast use them automatically.\ declare Fin.intros [intro] thm Fin.intros lemma "\ A \ Fin; B \ Fin \ \ A \ B \ Fin" apply(erule Fin.induct) apply simp apply auto done lemma "\ A \ Fin; B \ A \ \ B \ Fin" apply(erule Fin.induct) txt\The base case looks funny: why is the premise not @{prop "B \ {}"}? Because @{prop "B \ A"} was not part of the conclusion we prove. Relief: pull @{prop "B \ A"} into the conclusion with the help of @{text"\"}. \ oops lemma "A \ Fin \ B \ A \ B \ Fin" apply(erule Fin.induct) apply auto[1] apply (clarsimp del: subsetI) txt\We need to strengthen the theorem: quantify @{text B}.\ oops lemma "A \ Fin \ \B. B \ A \ B \ Fin" apply(erule Fin.induct) apply(simp) apply(rule Fin.emptyI) apply(rule allI) apply(rule impI) apply simp thm subset_insert_iff insert_Diff apply (simp add:subset_insert_iff) apply(simp add:subset_insert_iff split:if_split_asm) apply(drule_tac A = B in insert_Diff) apply(erule subst) apply(blast) done \ \---------------------------------------------------\ section "Inductive Predicates" text \The whole thing also works for predicates directly:\ inductive even :: "nat \ bool" where 0: "even 0" | 2: "even n \ even (Suc (Suc n))" print_theorems lemma even_imp_Ev: "even x \ x \ Ev" apply(induct rule:even.induct) (* You'll learn about this proof method in week05B *) apply simp apply(erule even.cases) apply simp apply simp done lemma Ev_imp_even: "x \ Ev \ even x" apply(induct rule:Ev.induct) (* You'll learn about this proof method in week05B *) apply(rule 0) by (rule 2) lemma "even = Evp" unfolding Evp_Ev_eq apply(rule ext) apply(rule iffI) apply(rule even_imp_Ev) apply assumption by (rule Ev_imp_even) end