--- a/src/HOL/Eisbach/Examples.thy Thu Apr 30 17:00:50 2015 +0200
+++ b/src/HOL/Eisbach/Examples.thy Thu Apr 30 17:02:57 2015 +0200
@@ -11,19 +11,19 @@
subsection \<open>Basic methods\<close>
-method my_intros = \<open>rule conjI | rule impI\<close>
+method my_intros = (rule conjI | rule impI)
lemma "P \<and> Q \<longrightarrow> Z \<and> X"
apply my_intros+
oops
-method my_intros' uses intros = \<open>rule conjI | rule impI | rule intros\<close>
+method my_intros' uses intros = (rule conjI | rule impI | rule intros)
lemma "P \<and> Q \<longrightarrow> Z \<or> X"
apply (my_intros' intros: disjI1)+
oops
-method my_spec for x :: 'a = \<open>drule spec[where x="x"]\<close>
+method my_spec for x :: 'a = (drule spec[where x="x"])
lemma "\<forall>x. P x \<Longrightarrow> P x"
apply (my_spec x)
@@ -34,11 +34,11 @@
subsection \<open>Focusing and matching\<close>
method match_test =
- \<open>match prems in U: "P x \<and> Q x" for P Q x \<Rightarrow>
+ (match premises in U: "P x \<and> Q x" for P Q x \<Rightarrow>
\<open>print_term P,
print_term Q,
print_term x,
- print_fact U\<close>\<close>
+ print_fact U\<close>)
lemma "\<And>x. P x \<and> Q x \<Longrightarrow> A x \<and> B x \<Longrightarrow> R x y \<Longrightarrow> True"
apply match_test -- \<open>Valid match, but not quite what we were expecting..\<close>
@@ -51,8 +51,6 @@
back
back
back
- back
- back
oops
text \<open>Use matching to avoid "improper" methods\<close>
@@ -60,18 +58,18 @@
lemma focus_test:
shows "\<And>x. \<forall>x. P x \<Longrightarrow> P x"
apply (my_spec "x :: 'a", assumption)? -- \<open>Wrong x\<close>
- apply (match concl in "P x" for x \<Rightarrow> \<open>my_spec x, assumption\<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' =
- \<open>match concl in
+ (match conclusion in
"P \<and> Q" for P Q \<Rightarrow>
\<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>
- \<close>
+ )
text \<open>Solves goal\<close>
lemma "P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q"
@@ -89,20 +87,20 @@
method my_spec_guess =
- \<open>match concl in "P (x :: 'a)" for P x \<Rightarrow>
+ (match conclusion in "P (x :: 'a)" for P x \<Rightarrow>
\<open>drule spec[where x=x],
print_term P,
- print_term x\<close>\<close>
+ print_term x\<close>)
lemma "\<forall>x. P (x :: nat) \<Longrightarrow> Q (x :: nat)"
apply my_spec_guess
oops
method my_spec_guess2 =
- \<open>match prems in U[thin]:"\<forall>x. P x \<longrightarrow> Q x" and U':"P x" for P Q x \<Rightarrow>
+ (match premises in U[thin]:"\<forall>x. P x \<longrightarrow> Q x" and U':"P x" for P Q x \<Rightarrow>
\<open>insert spec[where x=x, OF U],
print_term P,
- print_term Q\<close>\<close>
+ print_term Q\<close>)
lemma "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> Q x \<Longrightarrow> Q x"
apply my_spec_guess2? -- \<open>Fails. Note that both "P"s must match\<close>
@@ -118,7 +116,7 @@
subsection \<open>Higher-order methods\<close>
method higher_order_example for x methods meth =
- \<open>cases x, meth, meth\<close>
+ (cases x, meth, meth)
lemma
assumes A: "x = Some a"
@@ -129,12 +127,12 @@
subsection \<open>Recursion\<close>
method recursion_example for x :: bool =
- \<open>print_term x,
+ (print_term x,
match (x) in "A \<and> B" for A B \<Rightarrow>
- \<open>(print_term A,
+ \<open>print_term A,
print_term B,
recursion_example A,
- recursion_example B) | -\<close>\<close>
+ recursion_example B | -\<close>)
lemma "P"
apply (recursion_example "(A \<and> D) \<and> (B \<and> C)")
@@ -151,15 +149,15 @@
subsection \<open>Demo\<close>
-method solve methods m = \<open>m;fail\<close>
+method solve methods m = (m; fail)
named_theorems intros and elims and subst
method prop_solver declares intros elims subst =
- \<open>(assumption |
+ (assumption |
rule intros | erule elims |
subst subst | subst (asm) subst |
- (erule notE; solve \<open>prop_solver\<close>))+\<close>
+ (erule notE; solve \<open>prop_solver\<close>))+
lemmas [intros] =
conjI
@@ -177,11 +175,11 @@
done
method guess_all =
- \<open>match prems in U[thin]:"\<forall>x. P (x :: 'a)" for P \<Rightarrow>
- \<open>match prems in "?H (y :: 'a)" for y \<Rightarrow>
+ (match premises in U[thin]:"\<forall>x. P (x :: 'a)" for P \<Rightarrow>
+ \<open>match premises in "?H (y :: 'a)" for y \<Rightarrow>
\<open>rule allE[where P = P and x = y, OF U]\<close>
- | match concl in "?H (y :: 'a)" for y \<Rightarrow>
- \<open>rule allE[where P = P and x = y, OF U]\<close>\<close>\<close>
+ | match conclusion in "?H (y :: 'a)" for y \<Rightarrow>
+ \<open>rule allE[where P = P and x = y, OF U]\<close>\<close>)
lemma "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> P y \<Longrightarrow> Q y"
apply guess_all
@@ -193,10 +191,10 @@
done
method guess_ex =
- \<open>match concl in
+ (match conclusion in
"\<exists>x. P (x :: 'a)" for P \<Rightarrow>
- \<open>match prems in "?H (x :: 'a)" for x \<Rightarrow>
- \<open>rule exI[where x=x]\<close>\<close>\<close>
+ \<open>match premises in "?H (x :: 'a)" for x \<Rightarrow>
+ \<open>rule exI[where x=x]\<close>\<close>)
lemma "P x \<Longrightarrow> \<exists>x. P x"
apply guess_ex
@@ -204,7 +202,7 @@
done
method fol_solver =
- \<open>(guess_ex | guess_all | prop_solver) ; solve \<open>fol_solver\<close>\<close>
+ ((guess_ex | guess_all | prop_solver) ; solve \<open>fol_solver\<close>)
declare
allI [intros]