(*  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