src/HOL/Eisbach/Examples.thy

 begin
 
 
 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)
   apply assumption
   done
 
 
 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>
   back  -- \<open>Can backtrack over matches, exploring all bindings\<close>
   back

   back
   back  -- \<open>Found the other conjunction\<close>
   back
   back
   back
-  back
-  back
   oops
 
 text \<open>Use matching to avoid "improper" methods\<close>
 
 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"
   apply match_test'
   done

   apply match_test'
   oops
 
 
 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>
   oops
 

 
 
 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"
   shows "the x = a"
   by (higher_order_example x \<open>simp add: A\<close>)
 
 
 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)")
   oops
 

   done
 
 
 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
   impI
   disjCI

 lemma "((A \<or> B) \<and> (A \<longrightarrow> C) \<and> (B \<longrightarrow> C)) \<longrightarrow> C"
   apply prop_solver
   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
   apply prop_solver
   done

 lemma "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow>  P z \<Longrightarrow> P y \<Longrightarrow> Q y"
   apply (solve \<open>guess_all, prop_solver\<close>)  -- \<open>Try it without solve\<close>
   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
   apply prop_solver
   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]
   exE [elims]
   ex_simps [subst]