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
```