src/HOL/Eisbach/Tests.thy
author wenzelm
Fri Oct 27 13:50:08 2017 +0200 (23 months ago)
changeset 66924 b4d4027f743b
parent 63186 dc221b8945f2
child 69216 1a52baa70aed
permissions -rw-r--r--
more permissive;
     1 (*  Title:      HOL/Eisbach/Tests.thy
     2     Author:     Daniel Matichuk, NICTA/UNSW
     3 *)
     4 
     5 section \<open>Miscellaneous Eisbach tests\<close>
     6 
     7 theory Tests
     8 imports Main Eisbach_Tools
     9 begin
    10 
    11 
    12 subsection \<open>Named Theorems Tests\<close>
    13 
    14 named_theorems foo
    15 
    16 method foo declares foo = (rule foo)
    17 
    18 lemma
    19   assumes A [foo]: A
    20   shows A
    21   apply foo
    22   done
    23 
    24 method abs_used for P = (match (P) in "\<lambda>a. ?Q" \<Rightarrow> fail \<bar> _ \<Rightarrow> -)
    25 
    26 
    27 subsection \<open>Match Tests\<close>
    28 
    29 notepad
    30 begin
    31   have dup: "\<And>A. A \<Longrightarrow> A \<Longrightarrow> A" by simp
    32 
    33   fix A y
    34   have "(\<And>x. A x) \<Longrightarrow> A y"
    35     apply (rule dup, match premises in Y: "\<And>B. P B" for P \<Rightarrow> \<open>match (P) in A \<Rightarrow> \<open>print_fact Y, rule Y\<close>\<close>)
    36     apply (rule dup, match premises in Y: "\<And>B :: 'a. P B" for P \<Rightarrow> \<open>match (P) in A \<Rightarrow> \<open>print_fact Y, rule Y\<close>\<close>)
    37     apply (rule dup, match premises in Y: "\<And>B :: 'a. P B" for P \<Rightarrow> \<open>match conclusion in "P y" for y \<Rightarrow> \<open>print_fact Y, print_term y, rule Y[where B=y]\<close>\<close>)
    38     apply (rule dup, match premises in Y: "\<And>B :: 'a. P B" for P \<Rightarrow> \<open>match conclusion in "P z" for z \<Rightarrow> \<open>print_fact Y, print_term y, rule Y[where B=z]\<close>\<close>)
    39     apply (rule dup, match conclusion in "P y" for P \<Rightarrow> \<open>match premises in Y: "\<And>z. P z" \<Rightarrow> \<open>print_fact Y, rule Y[where z=y]\<close>\<close>)
    40     apply (match premises in Y: "\<And>z :: 'a. P z" for P \<Rightarrow> \<open>match conclusion in "P y" \<Rightarrow> \<open>print_fact Y, rule Y[where z=y]\<close>\<close>)
    41     done
    42 
    43   assume X: "\<And>x. A x" "A y"
    44   have "A y"
    45     apply (match X in Y:"\<And>B. A B" and Y':"B ?x" for B \<Rightarrow> \<open>print_fact Y[where B=y], print_term B\<close>)
    46     apply (match X in Y:"B ?x" and Y':"B ?x" for B \<Rightarrow> \<open>print_fact Y, print_term B\<close>)
    47     apply (match X in Y:"B x" and Y':"B x" for B x \<Rightarrow> \<open>print_fact Y, print_term B, print_term x\<close>)
    48     apply (insert X)
    49     apply (match premises in Y:"\<And>B. A B" and Y':"B y" for B and y :: 'a \<Rightarrow> \<open>print_fact Y[where B=y], print_term B\<close>)
    50     apply (match premises in Y:"B ?x" and Y':"B ?x" for B \<Rightarrow> \<open>print_fact Y, print_term B\<close>)
    51     apply (match premises in Y:"B x" and Y':"B x" for B x \<Rightarrow> \<open>print_fact Y, print_term B\<close>)
    52     apply (match conclusion in "P x" and "P y" for P x \<Rightarrow> \<open>print_term P, print_term x\<close>)
    53     apply assumption
    54     done
    55 
    56   {
    57    fix B x y
    58    assume X: "\<And>x y. B x x y"
    59    have "B x x y"
    60      by (match X in Y:"\<And>y. B y y z" for z \<Rightarrow> \<open>rule Y[where y=x]\<close>)
    61 
    62    fix A B
    63    have "(\<And>x y. A (B x) y) \<Longrightarrow> A (B x) y"
    64      by (match premises in Y: "\<And>xx. ?H (B xx)" \<Rightarrow> \<open>rule Y\<close>)
    65   }
    66 
    67   (* match focusing retains prems *)
    68   fix B x
    69   have "(\<And>x. A x) \<Longrightarrow> (\<And>z. B z) \<Longrightarrow> A y \<Longrightarrow> B x"
    70     apply (match premises in Y: "\<And>z :: 'a. A z"  \<Rightarrow> \<open>match premises in Y': "\<And>z :: 'b. B z" \<Rightarrow> \<open>print_fact Y, print_fact Y', rule Y'[where z=x]\<close>\<close>)
    71     done
    72 
    73   (*Attributes *)
    74   fix C
    75   have "(\<And>x :: 'a. A x)  \<Longrightarrow> (\<And>z. B z) \<Longrightarrow> A y \<Longrightarrow> B x \<and> B x \<and> A y"
    76     apply (intro conjI)
    77     apply (match premises in Y: "\<And>z :: 'a. A z" and Y'[intro]:"\<And>z :: 'b. B z" \<Rightarrow> fastforce)
    78     apply (match premises in Y: "\<And>z :: 'a. A z"  \<Rightarrow> \<open>match premises in Y'[intro]:"\<And>z :: 'b. B z" \<Rightarrow> fastforce\<close>)
    79     apply (match premises in Y[thin]: "\<And>z :: 'a. A z"  \<Rightarrow> \<open>(match premises in Y':"\<And>z :: 'a. A z" \<Rightarrow> \<open>print_fact Y,fail\<close> \<bar> _ \<Rightarrow> \<open>print_fact Y\<close>)\<close>)
    80     (*apply (match premises in Y: "\<And>z :: 'b. B z"  \<Rightarrow> \<open>(match premises in Y'[thin]:"\<And>z :: 'b. B z" \<Rightarrow> \<open>(match premises in Y':"\<And>z :: 'a. A z" \<Rightarrow> fail \<bar> Y': _ \<Rightarrow> -)\<close>)\<close>)*)
    81     apply assumption
    82     done
    83 
    84   fix A B C D
    85   have "\<And>uu'' uu''' uu uu'. (\<And>x :: 'a. A uu' x)  \<Longrightarrow> D uu y \<Longrightarrow> (\<And>z. B uu z) \<Longrightarrow> C uu y \<Longrightarrow> (\<And>z y. C uu z)  \<Longrightarrow> B uu x \<and> B uu x \<and> C uu y"
    86     apply (match premises in Y[thin]: "\<And>z :: 'a. A ?zz' z" and
    87                           Y'[thin]: "\<And>rr :: 'b. B ?zz rr" \<Rightarrow>
    88           \<open>print_fact Y, print_fact Y', intro conjI, rule Y', insert Y', insert Y'[where rr=x]\<close>)
    89     apply (match premises in Y:"B ?u ?x" \<Rightarrow> \<open>rule Y\<close>)
    90     apply (insert TrueI)
    91     apply (match premises in Y'[thin]: "\<And>ff. B uu ff" for uu \<Rightarrow> \<open>insert Y', drule meta_spec[where x=x]\<close>)
    92     apply assumption
    93     done
    94 
    95 
    96   (* Multi-matches. As many facts as match are bound. *)
    97   fix A B C x
    98   have "(\<And>x :: 'a. A x) \<Longrightarrow> (\<And>y :: 'a. B y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
    99     apply (match premises in Y[thin]: "\<And>z :: 'a. ?A z" (multi) \<Rightarrow> \<open>intro conjI, (rule Y)+\<close>)
   100     apply (match premises in Y[thin]: "\<And>z :: 'a. ?A z" (multi) \<Rightarrow> fail \<bar> "C y" \<Rightarrow> -) (* multi-match must bind something *)
   101     apply (match premises in Y: "C y" \<Rightarrow> \<open>rule Y\<close>)
   102     done
   103 
   104   fix A B C x
   105   have "(\<And>x :: 'a. A x) \<Longrightarrow> (\<And>y :: 'a. B y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
   106     apply (match premises in Y[thin]: "\<And>z. ?A z" (multi) \<Rightarrow> \<open>intro conjI, (rule Y)+\<close>)
   107     apply (match premises in Y[thin]: "\<And>z. ?A z" (multi) \<Rightarrow> fail \<bar> "C y" \<Rightarrow> -) (* multi-match must bind something *)
   108     apply (match premises in Y: "C y" \<Rightarrow> \<open>rule Y\<close>)
   109     done
   110 
   111   fix A B C P Q and x :: 'a and y :: 'a
   112   have "(\<And>x y :: 'a. A x y \<and> Q) \<Longrightarrow> (\<And>a b. B (a :: 'a) (b :: 'a) \<and> Q) \<Longrightarrow> (\<And>x y. C (x :: 'a) (y :: 'a) \<and> P) \<Longrightarrow> A y x \<and> B y x"
   113     by (match premises in Y: "\<And>z a. ?A (z :: 'a) (a :: 'a) \<and> R" (multi) for R \<Rightarrow> \<open>rule conjI, rule Y[where z=x,THEN conjunct1], rule Y[THEN conjunct1]\<close>)
   114 
   115 
   116   (*We may use for-fixes in multi-matches too. All bound facts must agree on the fixed term *)
   117   fix A B C x
   118   have "(\<And>y :: 'a. B y \<and> C y) \<Longrightarrow> (\<And>x :: 'a. A x \<and> B x) \<Longrightarrow> (\<And>y :: 'a. A y \<and> C y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
   119     apply (match premises in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow>
   120                                   \<open>match (P) in B \<Rightarrow> fail
   121                                         \<bar> "\<lambda>a. B" \<Rightarrow> fail
   122                                         \<bar> _ \<Rightarrow> -,
   123                                   intro conjI, (rule Y[THEN conjunct1])\<close>)
   124     apply (rule dup)
   125     apply (match premises in Y':"\<And>x :: 'a. ?U x \<and> Q x" and Y: "\<And>x :: 'a. Q x \<and> ?U x" (multi)  for Q \<Rightarrow> \<open>insert Y[THEN conjunct1]\<close>)
   126     apply assumption (* Previous match requires that Q is consistent *)
   127     apply (match premises in Y: "\<And>z :: 'a. ?A z \<longrightarrow> False" (multi) \<Rightarrow> \<open>print_fact Y, fail\<close> \<bar> "C y" \<Rightarrow> \<open>print_term C\<close>) (* multi-match must bind something *)
   128     apply (match premises in Y: "\<And>x. B x \<and> C x" \<Rightarrow> \<open>intro conjI Y[THEN conjunct1]\<close>)
   129     apply (match premises in Y: "C ?x" \<Rightarrow> \<open>rule Y\<close>)
   130     done
   131 
   132   (* All bindings must be tried for a particular theorem.
   133      However all combinations are NOT explored. *)
   134   fix B A C
   135   assume asms:"\<And>a b. B (a :: 'a) (b :: 'a) \<and> Q" "\<And>x :: 'a. A x x \<and> Q" "\<And>a b. C (a :: 'a) (b :: 'a) \<and> Q"
   136   have "B y x \<and> C x y \<and> B x y \<and> C y x \<and> A x x"
   137     apply (intro conjI)
   138     apply (match asms in Y: "\<And>z a. ?A (z :: 'a) (a :: 'a) \<and> R" (multi) for R \<Rightarrow> \<open>rule Y[where z=x,THEN conjunct1]\<close>)
   139     apply (match asms in Y: "\<And>z a. ?A (z :: 'a) (a :: 'a) \<and> R" (multi) for R \<Rightarrow> \<open>rule Y[where a=x,THEN conjunct1]\<close>)
   140     apply (match asms in Y: "\<And>z a. ?A (z :: 'a) (a :: 'a) \<and> R" (multi) for R \<Rightarrow> \<open>rule Y[where a=x,THEN conjunct1]\<close>)
   141     apply (match asms in Y: "\<And>z a. ?A (z :: 'a) (a :: 'a) \<and> R" (multi) for R \<Rightarrow> \<open>rule Y[where z=x,THEN conjunct1]\<close>)
   142     apply (match asms in Y: "\<And>z a. A (z :: 'a) (a :: 'a) \<and> R"  for R \<Rightarrow> fail \<bar> _ \<Rightarrow> -)
   143     apply (rule asms[THEN conjunct1])
   144     done
   145 
   146   (* Attributes *)
   147   fix A B C x
   148   have "(\<And>x :: 'a. A x \<and> B x) \<Longrightarrow> (\<And>y :: 'a. A y \<and> C y) \<Longrightarrow> (\<And>y :: 'a. B y \<and> C y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
   149     apply (match premises in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>match Y[THEN conjunct1]  in Y':"?H"  (multi) \<Rightarrow> \<open>intro conjI,rule Y'\<close>\<close>)
   150     apply (match premises in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>match Y[THEN conjunct2]  in Y':"?H"  (multi) \<Rightarrow> \<open>rule Y'\<close>\<close>)
   151     apply assumption
   152     done
   153 
   154 (* Removed feature for now *)
   155 (*
   156   fix A B C x
   157   have "(\<And>x :: 'a. A x \<and> B x) \<Longrightarrow> (\<And>y :: 'a. A y \<and> C y) \<Longrightarrow> (\<And>y :: 'a. B y \<and> C y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
   158   apply (match prems in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>match \<open>K @{thms Y TrueI}\<close> in Y':"?H"  (multi) \<Rightarrow> \<open>rule conjI; (rule Y')?\<close>\<close>)
   159   apply (match prems in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>match \<open>K [@{thm Y}]\<close> in Y':"?H"  (multi) \<Rightarrow> \<open>rule Y'\<close>\<close>)
   160   done
   161 *)
   162   (* Testing THEN_ALL_NEW within match *)
   163   fix A B C x
   164   have "(\<And>x :: 'a. A x \<and> B x) \<Longrightarrow> (\<And>y :: 'a. A y \<and> C y) \<Longrightarrow> (\<And>y :: 'a. B y \<and> C y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
   165     apply (match premises in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>intro conjI ; ((rule Y[THEN conjunct1])?); rule Y[THEN conjunct2] \<close>)
   166     done
   167 
   168   (* Cut tests *)
   169   fix A B C
   170 
   171   have "D \<and> C  \<Longrightarrow> A \<and> B  \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> D \<longrightarrow> True \<Longrightarrow> C"
   172     by (((match premises in I: "P \<and> Q" (cut)
   173               and I': "P \<longrightarrow> ?U" for P Q \<Rightarrow> \<open>rule mp [OF I' I[THEN conjunct1]]\<close>)?), simp)
   174 
   175   have "D \<and> C  \<Longrightarrow> A \<and> B  \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> D \<longrightarrow> True \<Longrightarrow> C"
   176     by (match premises in I: "P \<and> Q" (cut 2)
   177               and I': "P \<longrightarrow> ?U" for P Q \<Rightarrow> \<open>rule mp [OF I' I[THEN conjunct1]]\<close>)
   178 
   179   have "A \<and> B \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> C"
   180     by (((match premises in I: "P \<and> Q" (cut)
   181               and I': "P \<longrightarrow> ?U" for P Q \<Rightarrow> \<open>rule mp [OF I' I[THEN conjunct1]]\<close>)?, simp) | simp)
   182 
   183   fix f x y
   184   have "f x y \<Longrightarrow> f x y"
   185     by (match conclusion in "f x y" for f x y  \<Rightarrow> \<open>print_term f\<close>)
   186 
   187   fix A B C
   188   assume X: "A \<and> B" "A \<and> C" C
   189   have "A \<and> B \<and> C"
   190     by (match X in H: "A \<and> ?H" (multi, cut) \<Rightarrow>
   191           \<open>match H in "A \<and> C" and "A \<and> B" \<Rightarrow> fail\<close>
   192         | simp add: X)
   193 
   194 
   195   (* Thinning an inner focus *)
   196   (* Thinning should persist within a match, even when on an external premise *)
   197 
   198   fix A
   199   have "(\<And>x. A x \<and> B) \<Longrightarrow> B \<and> C \<Longrightarrow> C"
   200     apply (match premises in H:"\<And>x. A x \<and> B" \<Rightarrow>
   201                      \<open>match premises in H'[thin]: "\<And>x. A x \<and> B" \<Rightarrow>
   202                       \<open>match premises in H'':"\<And>x. A x \<and> B" \<Rightarrow> fail
   203                                          \<bar> _ \<Rightarrow> -\<close>
   204                       ,match premises in H'':"\<And>x. A x \<and> B" \<Rightarrow> fail \<bar> _ \<Rightarrow> -\<close>)
   205     apply (match premises in H:"\<And>x. A x \<and> B" \<Rightarrow> fail
   206                               \<bar> H':_ \<Rightarrow> \<open>rule H'[THEN conjunct2]\<close>)
   207     done
   208 
   209 
   210   (* Local premises *)
   211   (* Only match premises which actually existed in the goal we just focused.*)
   212 
   213   fix A
   214   assume asms: "C \<and> D"
   215   have "B \<and> C \<Longrightarrow> C"
   216     by (match premises in _ \<Rightarrow> \<open>insert asms,
   217             match premises (local) in "B \<and> C" \<Rightarrow> fail
   218                                   \<bar> H:"C \<and> D" \<Rightarrow> \<open>rule H[THEN conjunct1]\<close>\<close>)
   219 end
   220 
   221 
   222 
   223 (* Testing inner focusing. This fails if we don't smash flex-flex pairs produced
   224    by retrofitting. This needs to be done more carefully to avoid smashing
   225    legitimate pairs.*)
   226 
   227 schematic_goal "?A x \<Longrightarrow> A x"
   228   apply (match conclusion in "H" for H \<Rightarrow> \<open>match conclusion in Y for Y \<Rightarrow> \<open>print_term Y\<close>\<close>)
   229   apply assumption
   230   done
   231 
   232 (* Ensure short-circuit after first match failure *)
   233 lemma
   234   assumes A: "P \<and> Q"
   235   shows "P"
   236   by ((match A in "P \<and> Q" \<Rightarrow> fail \<bar> "?H" \<Rightarrow> -) | simp add: A)
   237 
   238 lemma
   239   assumes A: "D \<and> C" "A \<and> B" "A \<longrightarrow> B"
   240   shows "A"
   241   apply ((match A in U: "P \<and> Q" (cut) and "P' \<longrightarrow> Q'" for P Q P' Q' \<Rightarrow>
   242       \<open>simp add: U\<close> \<bar> "?H" \<Rightarrow> -) | -)
   243   apply (simp add: A)
   244   done
   245 
   246 
   247 subsection \<open>Uses Tests\<close>
   248 
   249 ML \<open>
   250   fun test_internal_fact ctxt factnm =
   251     (case try (Proof_Context.get_thms ctxt) factnm of
   252       NONE => ()
   253     | SOME _ => error "Found internal fact");
   254 \<close>
   255 
   256 method uses_test\<^sub>1 uses uses_test\<^sub>1_uses = (rule uses_test\<^sub>1_uses)
   257 
   258 lemma assumes A shows A by (uses_test\<^sub>1 uses_test\<^sub>1_uses: assms)
   259 
   260 ML \<open>test_internal_fact @{context} "uses_test\<^sub>1_uses"\<close>
   261 
   262 ML \<open>test_internal_fact @{context} "Tests.uses_test\<^sub>1_uses"\<close>
   263 ML \<open>test_internal_fact @{context} "Tests.uses_test\<^sub>1.uses_test\<^sub>1_uses"\<close>
   264 
   265 subsection \<open>Basic fact passing\<close>
   266 
   267 method find_fact for x y :: bool uses facts1 facts2 =
   268   (match facts1 in U: "x" \<Rightarrow> \<open>insert U,
   269       match facts2 in U: "y" \<Rightarrow> \<open>insert U\<close>\<close>)
   270 
   271 lemma assumes A: A and B: B shows "A \<and> B"
   272   apply (find_fact "A" "B" facts1: A facts2: B)
   273   apply (rule conjI; assumption)
   274   done
   275 
   276 
   277 subsection \<open>Testing term and fact passing in recursion\<close>
   278 
   279 
   280 method recursion_example for x :: bool uses facts =
   281   (match (x) in
   282     "A \<and> B" for A B \<Rightarrow> \<open>(recursion_example A facts: facts, recursion_example B facts: facts)\<close>
   283   \<bar> "?H" \<Rightarrow> \<open>match facts in U: "x" \<Rightarrow> \<open>insert U\<close>\<close>)
   284 
   285 lemma
   286   assumes asms: "A" "B" "C" "D"
   287   shows "(A \<and> B) \<and> (C \<and> D)"
   288   apply (recursion_example "(A \<and> B) \<and> (C \<and> D)" facts: asms)
   289   apply simp
   290   done
   291 
   292 (* uses facts are not accumulated *)
   293 
   294 method recursion_example' for A :: bool and B :: bool uses facts =
   295   (match facts in
   296     H: "A" and H': "B" \<Rightarrow> \<open>recursion_example' "A" "B" facts: H TrueI\<close>
   297   \<bar> "A" and "True" \<Rightarrow> \<open>recursion_example' "A" "B" facts: TrueI\<close>
   298   \<bar> "True" \<Rightarrow> -
   299   \<bar> "PROP ?P" \<Rightarrow> fail)
   300 
   301 lemma
   302   assumes asms: "A" "B"
   303   shows "True"
   304   apply (recursion_example' "A" "B" facts: asms)
   305   apply simp
   306   done
   307 
   308 
   309 (*Method.sections in existing method*)
   310 method my_simp\<^sub>1 uses my_simp\<^sub>1_facts = (simp add: my_simp\<^sub>1_facts)
   311 lemma assumes A shows A by (my_simp\<^sub>1 my_simp\<^sub>1_facts: assms)
   312 
   313 (*Method.sections via Eisbach argument parser*)
   314 method uses_test\<^sub>2 uses uses_test\<^sub>2_uses = (uses_test\<^sub>1 uses_test\<^sub>1_uses: uses_test\<^sub>2_uses)
   315 lemma assumes A shows A by (uses_test\<^sub>2 uses_test\<^sub>2_uses: assms)
   316 
   317 
   318 subsection \<open>Declaration Tests\<close>
   319 
   320 named_theorems declare_facts\<^sub>1
   321 
   322 method declares_test\<^sub>1 declares declare_facts\<^sub>1 = (rule declare_facts\<^sub>1)
   323 
   324 lemma assumes A shows A by (declares_test\<^sub>1 declare_facts\<^sub>1: assms)
   325 
   326 lemma assumes A[declare_facts\<^sub>1]: A shows A by declares_test\<^sub>1
   327 
   328 
   329 subsection \<open>Rule Instantiation Tests\<close>
   330 
   331 method my_allE\<^sub>1 for x :: 'a and P :: "'a \<Rightarrow> bool" =
   332   (erule allE [where x = x and P = P])
   333 
   334 lemma "\<forall>x. Q x \<Longrightarrow> Q x" by (my_allE\<^sub>1 x Q)
   335 
   336 method my_allE\<^sub>2 for x :: 'a and P :: "'a \<Rightarrow> bool" =
   337   (erule allE [of P x])
   338 
   339 lemma "\<forall>x. Q x \<Longrightarrow> Q x" by (my_allE\<^sub>2 x Q)
   340 
   341 method my_allE\<^sub>3 for x :: 'a and P :: "'a \<Rightarrow> bool" =
   342   (match allE [where 'a = 'a] in X: "\<And>(x :: 'a) P R. \<forall>x. P x \<Longrightarrow> (P x \<Longrightarrow> R) \<Longrightarrow> R" \<Rightarrow>
   343     \<open>erule X [where x = x and P = P]\<close>)
   344 
   345 lemma "\<forall>x. Q x \<Longrightarrow> Q x" by (my_allE\<^sub>3 x Q)
   346 
   347 method my_allE\<^sub>4 for x :: 'a and P :: "'a \<Rightarrow> bool" =
   348   (match allE [where 'a = 'a] in X: "\<And>(x :: 'a) P R. \<forall>x. P x \<Longrightarrow> (P x \<Longrightarrow> R) \<Longrightarrow> R" \<Rightarrow>
   349     \<open>erule X [of x P]\<close>)
   350 
   351 lemma "\<forall>x. Q x \<Longrightarrow> Q x" by (my_allE\<^sub>4 x Q)
   352 
   353 
   354 
   355 subsection \<open>Polymorphism test\<close>
   356 
   357 axiomatization foo' :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> bool"
   358 axiomatization where foo'_ax1: "foo' x y z \<Longrightarrow> z \<and> y"
   359 axiomatization where foo'_ax2: "foo' x y y \<Longrightarrow> x \<and> z"
   360 axiomatization where foo'_ax3: "foo' (x :: int) y y \<Longrightarrow> y \<and> y"
   361 
   362 lemmas my_thms = foo'_ax1 foo'_ax2 foo'_ax3
   363 
   364 definition first_id where "first_id x = x"
   365 
   366 lemmas my_thms' = my_thms[of "first_id x" for x]
   367 
   368 method print_conclusion = (match conclusion in concl for concl \<Rightarrow> \<open>print_term concl\<close>)
   369 
   370 lemma
   371   assumes foo: "\<And>x (y :: bool). foo' (A x) B (A x)"
   372   shows "\<And>z. A z \<and> B"
   373   apply
   374     (match conclusion in "f x y" for f y and x :: "'d :: type" \<Rightarrow> \<open>
   375       match my_thms' in R:"\<And>(x :: 'f :: type). ?P (first_id x) \<Longrightarrow> ?R"
   376                      and R':"\<And>(x :: 'f :: type). ?P' (first_id x) \<Longrightarrow> ?R'" \<Rightarrow> \<open>
   377         match (x) in "q :: 'f" for q \<Rightarrow> \<open>
   378           rule R[of q,simplified first_id_def],
   379           print_conclusion,
   380           rule foo
   381       \<close>\<close>\<close>)
   382   done
   383 
   384 
   385 subsection \<open>Unchecked rule instantiation, with the possibility of runtime errors\<close>
   386 
   387 named_theorems my_thms_named
   388 
   389 declare foo'_ax3[my_thms_named]
   390 
   391 method foo_method3 declares my_thms_named =
   392   (match my_thms_named[of (unchecked) z for z] in R:"PROP ?H" \<Rightarrow> \<open>rule R\<close>)
   393 
   394 notepad
   395 begin
   396 
   397   (*FIXME: Shouldn't need unchecked keyword here. See Tests_Failing.thy *)
   398   fix A B x
   399   have "foo' x B A \<Longrightarrow> A \<and> B"
   400     by (match my_thms[of (unchecked) z for z] in R:"PROP ?H" \<Rightarrow> \<open>rule R\<close>)
   401 
   402   fix A B x
   403   note foo'_ax1[my_thms_named]
   404   have "foo' x B A \<Longrightarrow> A \<and> B"
   405     by (match my_thms_named[where x=z for z] in R:"PROP ?H" \<Rightarrow> \<open>rule R\<close>)
   406 
   407   fix A B x
   408   note foo'_ax1[my_thms_named] foo'_ax2[my_thms_named] foo'_ax3[my_thms_named]
   409   have "foo' x B A \<Longrightarrow> A \<and> B"
   410    by foo_method3
   411 
   412 end
   413 
   414 
   415 ML \<open>
   416 structure Data = Generic_Data
   417 (
   418   type T = thm list;
   419   val empty: T = [];
   420   val extend = I;
   421   fun merge data : T = Thm.merge_thms data;
   422 );
   423 \<close>
   424 
   425 local_setup \<open>Local_Theory.add_thms_dynamic (@{binding test_dyn}, Data.get)\<close>
   426 
   427 setup \<open>Context.theory_map (Data.put @{thms TrueI})\<close>
   428 
   429 method dynamic_thms_test = (rule test_dyn)
   430 
   431 locale foo =
   432   fixes A
   433   assumes A : "A"
   434 begin
   435 
   436 local_setup
   437   \<open>Local_Theory.declaration {pervasive = false, syntax = false}
   438     (fn phi => Data.put (Morphism.fact phi @{thms A}))\<close>
   439 
   440 lemma A by dynamic_thms_test
   441 
   442 end
   443 
   444 
   445 notepad
   446 begin
   447   fix A x
   448   assume X: "\<And>x. A x"
   449   have "A x"
   450     by (match X in H[of x]:"\<And>x. A x" \<Rightarrow> \<open>print_fact H,match H in "A x" \<Rightarrow> \<open>rule H\<close>\<close>)
   451 
   452   fix A x B
   453   assume X: "\<And>x :: bool. A x \<Longrightarrow> B" "\<And>x. A x"
   454   assume Y: "A B"
   455   have "B \<and> B \<and> B \<and> B \<and> B \<and> B"
   456     apply (intro conjI)
   457     apply (match X in H[OF X(2)]:"\<And>x. A x \<Longrightarrow> B" \<Rightarrow> \<open>print_fact H,rule H\<close>)
   458     apply (match X in H':"\<And>x. A x" and H[OF H']:"\<And>x. A x \<Longrightarrow> B" \<Rightarrow> \<open>print_fact H',print_fact H,rule H\<close>)
   459     apply (match X in H[of Q]:"\<And>x. A x \<Longrightarrow> ?R" and "?P \<Longrightarrow> Q" for Q \<Rightarrow> \<open>print_fact H,rule H, rule Y\<close>)
   460     apply (match X in H[of Q,OF Y]:"\<And>x. A x \<Longrightarrow> ?R" and "?P \<Longrightarrow> Q" for Q \<Rightarrow> \<open>print_fact H,rule H\<close>)
   461     apply (match X in H[OF Y,intro]:"\<And>x. A x \<Longrightarrow> ?R" \<Rightarrow> \<open>print_fact H,fastforce\<close>)
   462     apply (match X in H[intro]:"\<And>x. A x \<Longrightarrow> ?R" \<Rightarrow> \<open>rule H[where x=B], rule Y\<close>)
   463     done
   464 
   465   fix x :: "prop" and A
   466   assume X: "TERM x"
   467   assume Y: "\<And>x :: prop. A x"
   468   have "A TERM x"
   469     apply (match X in "PROP y" for y \<Rightarrow> \<open>rule Y[where x="PROP y"]\<close>)
   470     done
   471 end
   472 
   473 subsection \<open>Proper context for method parameters\<close>
   474 
   475 method add_simp methods m uses f = (match f in H[simp]:_ \<Rightarrow> m)
   476 
   477 method add_my_thms methods m uses f = (match f in H[my_thms_named]:_ \<Rightarrow> m)
   478 
   479 method rule_my_thms = (rule my_thms_named)
   480 method rule_my_thms' declares my_thms_named = (rule my_thms_named)
   481 
   482 lemma
   483   assumes A: A and B: B
   484   shows
   485   "(A \<or> B) \<and> A \<and> A \<and> A"
   486   apply (intro conjI)
   487   apply (add_simp \<open>add_simp simp f: B\<close> f: A)
   488   apply (add_my_thms rule_my_thms f:A)
   489   apply (add_my_thms rule_my_thms' f:A)
   490   apply (add_my_thms \<open>rule my_thms_named\<close> f:A)
   491   done
   492 
   493 
   494 subsection \<open>Shallow parser tests\<close>
   495 
   496 method all_args for A B methods m1 m2 uses f1 f2 declares my_thms_named = fail
   497 
   498 lemma True
   499   by (all_args True False - fail f1: TrueI f2: TrueI my_thms_named: TrueI | rule TrueI)
   500 
   501 
   502 subsection \<open>Method name internalization test\<close>
   503 
   504 
   505 method test2 = (simp)
   506 
   507 method simp = fail
   508 
   509 lemma "A \<Longrightarrow> A" by test2
   510 
   511 
   512 subsection \<open>Dynamic facts\<close>
   513 
   514 named_theorems my_thms_named'
   515 
   516 method foo_method1 for x =
   517   (match my_thms_named' [of (unchecked) x] in R: "PROP ?H" \<Rightarrow> \<open>rule R\<close>)
   518 
   519 lemma
   520   assumes A [my_thms_named']: "\<And>x. A x"
   521   shows "A y"
   522   by (foo_method1 y)
   523 
   524 
   525 subsection \<open>Eisbach method invocation from ML\<close>
   526 
   527 method test_method for x y uses r = (print_term x, print_term y, rule r)
   528 
   529 method_setup test_method' = \<open>
   530   Args.term -- Args.term --
   531   (Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thms) >>
   532     (fn ((x, y), r) => fn ctxt =>
   533       Method_Closure.apply_method ctxt @{method test_method} [x, y] [r] [] ctxt);
   534 \<close>
   535 
   536 lemma
   537   fixes a b :: nat
   538   assumes "a = b"
   539   shows "b = a"
   540   apply (test_method a b)?
   541   apply (test_method' a b rule: refl)?
   542   apply (test_method' a b rule: assms [symmetric])?
   543   done
   544 
   545 subsection \<open>Eisbach methods in locales\<close>
   546 
   547 locale my_locale1 = fixes A assumes A: A begin
   548 
   549 method apply_A =
   550   (match conclusion in "A" \<Rightarrow>
   551     \<open>match A in U:"A" \<Rightarrow>
   552       \<open>print_term A, print_fact A, rule U\<close>\<close>)
   553 
   554 end
   555 
   556 locale my_locale2 = fixes B assumes B: B begin
   557 
   558 interpretation my_locale1 B by (unfold_locales; rule B)
   559 
   560 lemma B by apply_A
   561 
   562 end
   563 
   564 context fixes C assumes C: C begin
   565 
   566 interpretation my_locale1 C by (unfold_locales; rule C)
   567 
   568 lemma C by apply_A
   569 
   570 end
   571 
   572 context begin
   573 
   574 interpretation my_locale1 "True \<longrightarrow> True" by (unfold_locales; blast)
   575 
   576 lemma "True \<longrightarrow> True" by apply_A
   577 
   578 end
   579 
   580 locale locale_poly = fixes P assumes P: "\<And>x :: 'a. P x" begin
   581 
   582 method solve_P for z :: 'a = (rule P[where x = z]) 
   583 
   584 end
   585 
   586 context begin
   587 
   588 interpretation locale_poly "\<lambda>x:: nat. 0 \<le> x" by (unfold_locales; blast)
   589 
   590 lemma "0 \<le> (n :: nat)" by (solve_P n)
   591 
   592 end
   593 
   594 subsection \<open>Mutual recursion via higher-order methods\<close>
   595 
   596 experiment begin
   597 
   598 method inner_method methods passed_method = (rule conjI; passed_method)
   599 
   600 method outer_method = (inner_method \<open>outer_method\<close> | assumption)
   601 
   602 lemma "Q \<Longrightarrow> R \<Longrightarrow> P \<Longrightarrow> (Q \<and> R) \<and> P"
   603   by outer_method
   604 
   605 end
   606 
   607 end