theory week04B_demo imports Main begin \ \---------------------------------------------------\ text\A manual proof in set theory:\ thm equalityI subsetI UnI1 UnI2 UnE lemma "(A \ B) = (B \ A)" sorry lemma "(A\B \ C) = (A\C \ B\C)" sorry lemma "{a,b} \ {b,c} = TODO" sorry 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 \ \--------------------------------------------\ 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 prd :: "('a \ 'b \ bool) set" where "prd \ {f. \a b. f = (\x y. x=a \ y=b)}" typedef ('a, 'b) prd = "prd::('a \ 'b \ bool) set" by (auto simp: prd_def) (* To understand this proof, try: apply (simp add: prd_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) done *) print_theorems definition pair :: "'a \ 'b \ ('a,'b) prd" where "pair a b \ Abs_prd (\x y. x = a \ y = b)" definition fs :: "('a,'b) prd \ 'a" where "fs x \ SOME a. \b. x = pair a b" definition sn :: "('a,'b) prd \ 'b" where "sn x \ SOME b. \a. x = pair a b" lemma in_prd: "(\x y. x = c \ y = d) \ prd" apply (unfold prd_def) apply blast done lemma pair_inject: "pair a b = pair a' b' \ a=a' \ b=b'" (*TODO*) sorry 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" sorry 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 sorry 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}. 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 end