Theory Examples

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