theory week05A_demo imports Main begin -- --------------------------------------------------- text{*A manual proof in set theory:*} thm equalityI subsetI UnI1 UnI2 UnE lemma "(A \ B) = (B \ A)" (*TODO*) sorry lemma "(A\B \ C) = (A\C \ B\C)" (*TODO*) sorry lemma "{a,b} \ {b,c} = TODO" (*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