# Theory Examples

theory Examples
imports Main Eisbach_Tools
```(*  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
```