(* Title: HOL/Eisbach/Examples.thy
Author: Daniel Matichuk, NICTA/UNSW
*)
section \<open>Basic Eisbach examples\<close>
theory Examples
imports Main Eisbach_Tools
begin
subsection \<open>Basic methods\<close>
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 \<open>Focusing and matching\<close>
method match_test =
(match premises in U: "P x \ Q x" for P Q x \
\<open>print_term P,
print_term Q,
print_term x,
print_fact U\<close>)
lemma "\x. P x \ Q x \ A x \ B x \ R x y \ True"
apply match_test \<comment> \<open>Valid match, but not quite what we were expecting..\<close>
back \<comment> \<open>Can backtrack over matches, exploring all bindings\<close>
back
back
back
back
back \<comment> \<open>Found the other conjunction\<close>
back
back
back
oops
text \<open>Use matching to avoid "improper" methods\<close>
lemma focus_test:
shows "\x. \x. P x \ P x"
apply (my_spec "x :: 'a", assumption)? \<comment> \<open>Wrong x\<close>
apply (match conclusion in "P x" for x \<Rightarrow> \<open>my_spec x, assumption\<close>)
done
text \<open>Matches are exclusive. Backtracking will not occur past a match\<close>
method match_test' =
(match conclusion in
"P \ Q" for P Q \
\<open>print_term P, print_term Q, rule conjI[where P="P" and Q="Q"]; assumption\<close>
\<bar> "H" for H \<Rightarrow> \<open>print_term H\<close>)
text \<open>Solves goal\<close>
lemma "P \ Q \ P \ Q"
apply match_test'
done
text \<open>Fall-through case never taken\<close>
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 \<Rightarrow>
\<open>drule spec[where x=x],
print_term P,
print_term x\<close>)
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 \
\<open>insert spec[where x=x, OF U],
print_term P,
print_term Q\<close>)
lemma "\x. P x \ Q x \ Q x \ Q x"
apply my_spec_guess2? \<comment> \<open>Fails. Note that both "P"s must match\<close>
oops
lemma "\x. P x \ Q x \ P x \ Q x"
apply my_spec_guess2
apply (erule mp)
apply assumption
done
subsection \<open>Higher-order methods\<close>
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 \<open>simp add: A\<close>)
subsection \<open>Recursion\<close>
method recursion_example for x :: bool =
(print_term x,
match (x) in "A \ B" for A B \
\<open>print_term A,
print_term B,
recursion_example A,
recursion_example B | -\<close>)
lemma "P"
apply (recursion_example "(A \ D) \ (B \ C)")
oops
subsection \<open>Solves combinator\<close>
lemma "A \ B \ A \ B"
apply (solves \<open>rule conjI\<close>)? \<comment> \<open>Doesn't solve the goal!\<close>
apply (solves \<open>rule conjI, assumption, assumption\<close>)
done
subsection \<open>Demo\<close>
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 \
\<open>match premises in "?H (y :: 'a)" for y \<Rightarrow>
\<open>rule allE[where P = P and x = y, OF U]\<close>
| match conclusion in "?H (y :: 'a)" for y \<Rightarrow>
\<open>rule allE[where P = P and x = y, OF U]\<close>\<close>)
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 \<open>guess_all, prop_solver\<close>) \<comment> \<open>Try it without solve\<close>
done
method guess_ex =
(match conclusion in
"\x. P (x :: 'a)" for P \
\<open>match premises in "?H (x :: 'a)" for x \<Rightarrow>
\<open>rule exI[where x=x]\<close>\<close>)
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 \<open>
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.
\<close>
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 \<open>
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>\<open>P \<Longrightarrow> Q\<close> 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>\<open>P \<Longrightarrow> Q\<close> will match P with the conjunction of all the premises, and Q with
the final conclusion of the rule.
\<close>
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) \
\<open>match H in "E \<Longrightarrow> _" \<Rightarrow> fail
\<bar> _ \<Rightarrow> \<open>simp add: H\<close>\<close>)
end
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
