Quelle  Examples.thy   Sprache: Isabelle

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