(* Title: HOL/Eisbach/Examples.thy Author: Daniel Matichuk, NICTA/UNSW *) section ‹Basic Eisbach examples› theory Examples imports Main Eisbach_Tools begin subsection ‹Basic methods› method my_intros = (rule conjI | rule impI) lemma "P ∧ Q ⟶ Z ∧ X" apply my_intros+ oops method my_intros' uses intros = (rule conjI | rule impI | rule intros) lemma "P ∧ Q ⟶ Z ∨ X" apply (my_intros' intros: disjI1)+ oops method my_spec for x :: 'a = (drule spec[where x="x"]) lemma "∀x. P x ⟹ P x" apply (my_spec x) apply assumption done subsection ‹Focusing and matching› method match_test = (match premises in U: "P x ∧ Q x" for P Q x ⇒ ‹print_term P, print_term Q, print_term x, print_fact U›) lemma "⋀x. P x ∧ Q x ⟹ A x ∧ B x ⟹ R x y ⟹ True" apply match_test ― ‹Valid match, but not quite what we were expecting..› back ― ‹Can backtrack over matches, exploring all bindings› back back back back back ― ‹Found the other conjunction› back back back oops text ‹Use matching to avoid "improper" methods› lemma focus_test: shows "⋀x. ∀x. P x ⟹ P x" apply (my_spec "x :: 'a", assumption)? ― ‹Wrong x› apply (match conclusion in "P x" for x ⇒ ‹my_spec x, assumption›) done text ‹Matches are exclusive. Backtracking will not occur past a match› method match_test' = (match conclusion in "P ∧ Q" for P Q ⇒ ‹print_term P, print_term Q, rule conjI[where P="P" and Q="Q"]; assumption› ¦ "H" for H ⇒ ‹print_term H›) text ‹Solves goal› lemma "P ⟹ Q ⟹ P ∧ Q" apply match_test' done text ‹Fall-through case never taken› lemma "P ∧ Q" apply match_test'? oops lemma "P" apply match_test' oops method my_spec_guess = (match conclusion in "P (x :: 'a)" for P x ⇒ ‹drule spec[where x=x], print_term P, print_term x›) lemma "∀x. P (x :: nat) ⟹ Q (x :: nat)" apply my_spec_guess oops method my_spec_guess2 = (match premises in U[thin]:"∀x. P x ⟶ Q x" and U':"P x" for P Q x ⇒ ‹insert spec[where x=x, OF U], print_term P, print_term Q›) lemma "∀x. P x ⟶ Q x ⟹ Q x ⟹ Q x" apply my_spec_guess2? ― ‹Fails. Note that both "P"s must match› oops lemma "∀x. P x ⟶ Q x ⟹ P x ⟹ Q x" apply my_spec_guess2 apply (erule mp) apply assumption done subsection ‹Higher-order methods› method higher_order_example for x methods meth = (cases x, meth, meth) lemma assumes A: "x = Some a" shows "the x = a" by (higher_order_example x ‹simp add: A›) subsection ‹Recursion› method recursion_example for x :: bool = (print_term x, match (x) in "A ∧ B" for A B ⇒ ‹print_term A, print_term B, recursion_example A, recursion_example B | -›) lemma "P" apply (recursion_example "(A ∧ D) ∧ (B ∧ C)") oops subsection ‹Solves combinator› lemma "A ⟹ B ⟹ A ∧ B" apply (solves ‹rule conjI›)? ― ‹Doesn't solve the goal!› apply (solves ‹rule conjI, assumption, assumption›) done subsection ‹Demo› named_theorems intros and elims and subst method prop_solver declares intros elims subst = (assumption | rule intros | erule elims | subst subst | subst (asm) subst | (erule notE; solves prop_solver))+ lemmas [intros] = conjI impI disjCI iffI notI lemmas [elims] = impCE conjE disjE lemma "((A ∨ B) ∧ (A ⟶ C) ∧ (B ⟶ C)) ⟶ C" apply prop_solver done method guess_all = (match premises in U[thin]:"∀x. P (x :: 'a)" for P ⇒ ‹match premises in "?H (y :: 'a)" for y ⇒ ‹rule allE[where P = P and x = y, OF U]› | match conclusion in "?H (y :: 'a)" for y ⇒ ‹rule allE[where P = P and x = y, OF U]››) lemma "(∀x. P x ⟶ Q x) ⟹ P y ⟹ Q y" apply guess_all apply prop_solver done lemma "(∀x. P x ⟶ Q x) ⟹ P z ⟹ P y ⟹ Q y" apply (solves ‹guess_all, prop_solver›) ― ‹Try it without solve› done method guess_ex = (match conclusion in "∃x. P (x :: 'a)" for P ⇒ ‹match premises in "?H (x :: 'a)" for x ⇒ ‹rule exI[where x=x]››) lemma "P x ⟹ ∃x. P x" apply guess_ex apply prop_solver done method fol_solver = ((guess_ex | guess_all | prop_solver); solves fol_solver) declare allI [intros] exE [elims] ex_simps [subst] all_simps [subst] lemma "(∀x. P x) ∧ (∀x. Q x) ⟹ (∀x. P x ∧ Q x)" and "∃x. P x ⟶ (∀x. P x)" and "(∃x. ∀y. R x y) ⟶ (∀y. ∃x. R x y)" by fol_solver+ text ‹ Eisbach_Tools provides the catch method, which catches run-time method errors. In this example the OF attribute throws an error when it can't compose H with A, forcing H to be re-bound to different members of imps until it succeeds. › lemma assumes imps: "A ⟹ B" "A ⟹ C" "B ⟹ D" assumes A: "A" shows "B ∧ C" apply (rule conjI) apply ((match imps in H:"_ ⟹ _" ⇒ ‹catch ‹rule H[OF A], print_fact H› ‹print_fact H, fail››)+) done text ‹ Eisbach_Tools provides the curry and uncurry attributes. This is useful when the number of premises of a thm isn't known statically. The pattern \<^term>‹P ⟹ Q› matches P against the major premise of a thm, and Q is the rest of the premises with the conclusion. If we first uncurry, then \<^term>‹P ⟹ Q› will match P with the conjunction of all the premises, and Q with the final conclusion of the rule. › lemma assumes imps: "A ⟹ B ⟹ C" "D ⟹ C" "E ⟹ D ⟹ A" shows "(A ⟶ B ⟶ C) ∧ (D ⟶ C)" by (match imps[uncurry] in H[curry]:"_ ⟹ C" (cut, multi) ⇒ ‹match H in "E ⟹ _" ⇒ fail ¦ _ ⇒ ‹simp add: H››) end