theory week04A_demo imports Main begin \ \------------------------------------------------------------------\ text \implicit backtracking\ lemma "\P \ Q; R \ S\ \ S" (* doesn't work -- picks the wrong assumption apply(erule conjE) apply assumption *) apply (erule conjE, assumption) done text \do (n) assumption steps\ lemma "\P \ Q\ \ P" apply (erule (1) conjE) done text \'by' does extra assumption steps implicitly\ lemma "\P \ Q\ \ P" by (erule conjE) text \more automation\ \ \clarsimp: repeated clarify and simp\ lemma "ys = [] \ \xs. xs @ ys = []" apply clarsimp oops \ \auto: simplification, classical reasoning, more\ lemma "(\u::nat. x=y+u) \ a*(b+c)+y \ x + a*b+a*c" thm add_mult_distrib2 apply (auto simp add: add_mult_distrib2) done \ \limit auto (and any other tactic) to first [n] goals\ lemma "(True \ True)" apply (rule conjI) apply (auto)[1] apply (rule TrueI) done \ \also try: - blast, fast (classical reasoners) - auto, force (simplifier + classical reasoner) - fastforce (proof method that "tries harder than auto") - arith (for linear arithmetic problems) \ print_simpset text \simplification with assumptions, more control:\ lemma "\x. f x = g x \ g x = f x \ f [] = f [] @ []" \ \would diverge:\ (* apply(simp) *) apply (simp (no_asm)) done \ \------------------------------------------------------\ \ \let expressions\ lemma "let a = f x in g a = x" apply (simp add: Let_def) oops thm Let_def term "let a = f x in g a" term "(let a = f x in g (a + a)) = (Let (f x) (\a. g (a + a)))" \ \------------------------------------------------------\ \ \splitting case: manually\ lemma "(case n of 0 \ x | Suc n' \ x) = x" apply (simp only: split: nat.splits) (* alternatively: apply (split nat.splits) *) apply simp done \ \splitting if: automatic in conclusion\ lemma "\ P; Q \ \ (if x then A else B) = z" (* this will fail: apply(simp split del: if_split) *) apply simp oops thm if_split thm if_split_asm thm if_splits (* both *) lemma "\ (if x then A else B) = z; Q \ \ P" apply (simp split: if_splits) (* apply (simp split: if_split_asm)*) oops lemma " ((if x then A else B) =z) \ (z=A\z=B)" apply simp done thm conj_cong lemma "A \ (A \ B)" apply (simp cong: conj_cong) oops thm if_cong lemma "\ (if x then x \ z else B) = z; Q \ \ P" apply (simp cong: if_cong) oops thm add_ac thm mult_ac lemmas all_ac = add_ac mult_ac print_theorems lemma fixes f :: "'a \ 'a \ 'a" (infix "\" 70) assumes A: "\x y z. (x \ y) \ z = x \ (y \ z)" assumes C: "\x y. x \ y = y \ x" assumes AC: "\x y z. x \ (y \ z) = y \ (x \ z)" shows "(z \ x) \ (y \ v) = something" apply (simp only: C) apply (simp only: A C) apply (simp only: AC) oops text \when all else fails: tracing the simplifier typing declare [[simp_trace]] turns tracing on, declare [[simp_trace=false]] turns tracing off (within a proof, write 'using' rather than 'declare') \ declare [[simp_trace]] declare [[simp_trace_depth_limit=100]] lemma "A \ (A \ B)" (* alternatively: using [[simp_trace]] using [[simp_trace_depth_limit=100]] *) apply (simp cong: conj_cong) oops declare [[simp_trace=false]] \ \single stepping: subst\ thm add.commute thm add.assoc declare add.assoc [simp] lemma "a + b = x + ((y::nat) + z)" thm add.assoc add.assoc[symmetric] apply (simp add: add.assoc [symmetric] del: add.assoc) thm add.commute apply (subst add.commute [where a=x]) oops end