updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
authorwenzelm
Thu Apr 30 17:02:57 2015 +0200 (2015-04-30)
changeset 60209022ca2799c73
parent 60208 d72795f401c3
child 60210 3bcd15f14dcb
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
src/HOL/Eisbach/Eisbach.thy
src/HOL/Eisbach/Eisbach_Tools.thy
src/HOL/Eisbach/Examples.thy
src/HOL/Eisbach/Tests.thy
src/HOL/Eisbach/match_method.ML
src/HOL/Eisbach/method_closure.ML
     1.1 --- a/src/HOL/Eisbach/Eisbach.thy	Thu Apr 30 17:00:50 2015 +0200
     1.2 +++ b/src/HOL/Eisbach/Eisbach.thy	Thu Apr 30 17:02:57 2015 +0200
     1.3 @@ -8,14 +8,15 @@
     1.4  imports Pure
     1.5  keywords
     1.6    "method" :: thy_decl and
     1.7 -  "concl"
     1.8 -  "prems"  (* FIXME conflict with "prems" in Isar, which is presently dormant *)
     1.9 +  "conclusion"
    1.10 +  "premises"
    1.11    "declares"
    1.12    "methods"
    1.13    "\<bar>" "\<Rightarrow>"
    1.14    "uses"
    1.15  begin
    1.16  
    1.17 +
    1.18  ML_file "parse_tools.ML"
    1.19  ML_file "eisbach_rule_insts.ML"
    1.20  ML_file "method_closure.ML"
    1.21 @@ -38,6 +39,6 @@
    1.22      Method_Closure.free_aware_rule_attribute [] (fn _ => rotate_prems n)))\<close>
    1.23    "rotated theorem premises"
    1.24  
    1.25 -method solves methods m = \<open>m; fail\<close>
    1.26 +method solves methods m = (m; fail)
    1.27  
    1.28  end
     2.1 --- a/src/HOL/Eisbach/Eisbach_Tools.thy	Thu Apr 30 17:00:50 2015 +0200
     2.2 +++ b/src/HOL/Eisbach/Eisbach_Tools.thy	Thu Apr 30 17:02:57 2015 +0200
     2.3 @@ -35,7 +35,12 @@
     2.4        (Scan.lift (Scan.ahead Parse.not_eof) -- Args.term)
     2.5        (fn ctxt => fn (tok, t) =>
     2.6          (* FIXME proper formatting!? *)
     2.7 -        Token.unparse tok ^ ": " ^ Syntax.string_of_term ctxt t));
     2.8 +        Token.unparse tok ^ ": " ^ Syntax.string_of_term ctxt t) #>
     2.9 +    setup_trace_method @{binding print_type}
    2.10 +      (Scan.lift (Scan.ahead Parse.not_eof) -- Args.typ)
    2.11 +      (fn ctxt => fn (tok, t) =>
    2.12 +        (* FIXME proper formatting!? *)
    2.13 +        Token.unparse tok ^ ": " ^ Syntax.string_of_typ ctxt t));
    2.14  
    2.15  end
    2.16  \<close>
     3.1 --- a/src/HOL/Eisbach/Examples.thy	Thu Apr 30 17:00:50 2015 +0200
     3.2 +++ b/src/HOL/Eisbach/Examples.thy	Thu Apr 30 17:02:57 2015 +0200
     3.3 @@ -11,19 +11,19 @@
     3.4  
     3.5  subsection \<open>Basic methods\<close>
     3.6  
     3.7 -method my_intros = \<open>rule conjI | rule impI\<close>
     3.8 +method my_intros = (rule conjI | rule impI)
     3.9  
    3.10  lemma "P \<and> Q \<longrightarrow> Z \<and> X"
    3.11    apply my_intros+
    3.12    oops
    3.13  
    3.14 -method my_intros' uses intros = \<open>rule conjI | rule impI | rule intros\<close>
    3.15 +method my_intros' uses intros = (rule conjI | rule impI | rule intros)
    3.16  
    3.17  lemma "P \<and> Q \<longrightarrow> Z \<or> X"
    3.18    apply (my_intros' intros: disjI1)+
    3.19    oops
    3.20  
    3.21 -method my_spec for x :: 'a = \<open>drule spec[where x="x"]\<close>
    3.22 +method my_spec for x :: 'a = (drule spec[where x="x"])
    3.23  
    3.24  lemma "\<forall>x. P x \<Longrightarrow> P x"
    3.25    apply (my_spec x)
    3.26 @@ -34,11 +34,11 @@
    3.27  subsection \<open>Focusing and matching\<close>
    3.28  
    3.29  method match_test =
    3.30 -  \<open>match prems in U: "P x \<and> Q x" for P Q x \<Rightarrow>
    3.31 +  (match premises in U: "P x \<and> Q x" for P Q x \<Rightarrow>
    3.32      \<open>print_term P,
    3.33       print_term Q,
    3.34       print_term x,
    3.35 -     print_fact U\<close>\<close>
    3.36 +     print_fact U\<close>)
    3.37  
    3.38  lemma "\<And>x. P x \<and> Q x \<Longrightarrow> A x \<and> B x \<Longrightarrow> R x y \<Longrightarrow> True"
    3.39    apply match_test  -- \<open>Valid match, but not quite what we were expecting..\<close>
    3.40 @@ -51,8 +51,6 @@
    3.41    back
    3.42    back
    3.43    back
    3.44 -  back
    3.45 -  back
    3.46    oops
    3.47  
    3.48  text \<open>Use matching to avoid "improper" methods\<close>
    3.49 @@ -60,18 +58,18 @@
    3.50  lemma focus_test:
    3.51    shows "\<And>x. \<forall>x. P x \<Longrightarrow> P x"
    3.52    apply (my_spec "x :: 'a", assumption)?  -- \<open>Wrong x\<close>
    3.53 -  apply (match concl in "P x" for x \<Rightarrow> \<open>my_spec x, assumption\<close>)
    3.54 +  apply (match conclusion in "P x" for x \<Rightarrow> \<open>my_spec x, assumption\<close>)
    3.55    done
    3.56  
    3.57  
    3.58  text \<open>Matches are exclusive. Backtracking will not occur past a match\<close>
    3.59  
    3.60  method match_test' =
    3.61 -  \<open>match concl in
    3.62 +  (match conclusion in
    3.63      "P \<and> Q" for P Q \<Rightarrow>
    3.64        \<open>print_term P, print_term Q, rule conjI[where P="P" and Q="Q"]; assumption\<close>
    3.65      \<bar> "H" for H \<Rightarrow> \<open>print_term H\<close>
    3.66 -  \<close>
    3.67 +  )
    3.68  
    3.69  text \<open>Solves goal\<close>
    3.70  lemma "P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q"
    3.71 @@ -89,20 +87,20 @@
    3.72  
    3.73  
    3.74  method my_spec_guess =
    3.75 -  \<open>match concl in "P (x :: 'a)" for P x \<Rightarrow>
    3.76 +  (match conclusion in "P (x :: 'a)" for P x \<Rightarrow>
    3.77      \<open>drule spec[where x=x],
    3.78       print_term P,
    3.79 -     print_term x\<close>\<close>
    3.80 +     print_term x\<close>)
    3.81  
    3.82  lemma "\<forall>x. P (x :: nat) \<Longrightarrow> Q (x :: nat)"
    3.83    apply my_spec_guess
    3.84    oops
    3.85  
    3.86  method my_spec_guess2 =
    3.87 -  \<open>match prems in U[thin]:"\<forall>x. P x \<longrightarrow> Q x" and U':"P x" for P Q x \<Rightarrow>
    3.88 +  (match premises in U[thin]:"\<forall>x. P x \<longrightarrow> Q x" and U':"P x" for P Q x \<Rightarrow>
    3.89      \<open>insert spec[where x=x, OF U],
    3.90       print_term P,
    3.91 -     print_term Q\<close>\<close>
    3.92 +     print_term Q\<close>)
    3.93  
    3.94  lemma "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> Q x \<Longrightarrow> Q x"
    3.95    apply my_spec_guess2?  -- \<open>Fails. Note that both "P"s must match\<close>
    3.96 @@ -118,7 +116,7 @@
    3.97  subsection \<open>Higher-order methods\<close>
    3.98  
    3.99  method higher_order_example for x methods meth =
   3.100 -  \<open>cases x, meth, meth\<close>
   3.101 +  (cases x, meth, meth)
   3.102  
   3.103  lemma
   3.104    assumes A: "x = Some a"
   3.105 @@ -129,12 +127,12 @@
   3.106  subsection \<open>Recursion\<close>
   3.107  
   3.108  method recursion_example for x :: bool =
   3.109 -  \<open>print_term x,
   3.110 +  (print_term x,
   3.111       match (x) in "A \<and> B" for A B \<Rightarrow>
   3.112 -    \<open>(print_term A,
   3.113 +    \<open>print_term A,
   3.114       print_term B,
   3.115       recursion_example A,
   3.116 -     recursion_example B) | -\<close>\<close>
   3.117 +     recursion_example B | -\<close>)
   3.118  
   3.119  lemma "P"
   3.120    apply (recursion_example "(A \<and> D) \<and> (B \<and> C)")
   3.121 @@ -151,15 +149,15 @@
   3.122  
   3.123  subsection \<open>Demo\<close>
   3.124  
   3.125 -method solve methods m = \<open>m;fail\<close>
   3.126 +method solve methods m = (m; fail)
   3.127  
   3.128  named_theorems intros and elims and subst
   3.129  
   3.130  method prop_solver declares intros elims subst =
   3.131 -  \<open>(assumption |
   3.132 +  (assumption |
   3.133      rule intros | erule elims |
   3.134      subst subst | subst (asm) subst |
   3.135 -    (erule notE; solve \<open>prop_solver\<close>))+\<close>
   3.136 +    (erule notE; solve \<open>prop_solver\<close>))+
   3.137  
   3.138  lemmas [intros] =
   3.139    conjI
   3.140 @@ -177,11 +175,11 @@
   3.141    done
   3.142  
   3.143  method guess_all =
   3.144 -  \<open>match prems in U[thin]:"\<forall>x. P (x :: 'a)" for P \<Rightarrow>
   3.145 -    \<open>match prems in "?H (y :: 'a)" for y \<Rightarrow>
   3.146 +  (match premises in U[thin]:"\<forall>x. P (x :: 'a)" for P \<Rightarrow>
   3.147 +    \<open>match premises in "?H (y :: 'a)" for y \<Rightarrow>
   3.148         \<open>rule allE[where P = P and x = y, OF U]\<close>
   3.149 -   | match concl in "?H (y :: 'a)" for y \<Rightarrow>
   3.150 -       \<open>rule allE[where P = P and x = y, OF U]\<close>\<close>\<close>
   3.151 +   | match conclusion in "?H (y :: 'a)" for y \<Rightarrow>
   3.152 +       \<open>rule allE[where P = P and x = y, OF U]\<close>\<close>)
   3.153  
   3.154  lemma "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> P y \<Longrightarrow> Q y"
   3.155    apply guess_all
   3.156 @@ -193,10 +191,10 @@
   3.157    done
   3.158  
   3.159  method guess_ex =
   3.160 -  \<open>match concl in
   3.161 +  (match conclusion in
   3.162      "\<exists>x. P (x :: 'a)" for P \<Rightarrow>
   3.163 -      \<open>match prems in "?H (x :: 'a)" for x \<Rightarrow>
   3.164 -              \<open>rule exI[where x=x]\<close>\<close>\<close>
   3.165 +      \<open>match premises in "?H (x :: 'a)" for x \<Rightarrow>
   3.166 +              \<open>rule exI[where x=x]\<close>\<close>)
   3.167  
   3.168  lemma "P x \<Longrightarrow> \<exists>x. P x"
   3.169    apply guess_ex
   3.170 @@ -204,7 +202,7 @@
   3.171    done
   3.172  
   3.173  method fol_solver =
   3.174 -  \<open>(guess_ex | guess_all | prop_solver) ; solve \<open>fol_solver\<close>\<close>
   3.175 +  ((guess_ex | guess_all | prop_solver) ; solve \<open>fol_solver\<close>)
   3.176  
   3.177  declare
   3.178    allI [intros]
     4.1 --- a/src/HOL/Eisbach/Tests.thy	Thu Apr 30 17:00:50 2015 +0200
     4.2 +++ b/src/HOL/Eisbach/Tests.thy	Thu Apr 30 17:02:57 2015 +0200
     4.3 @@ -8,12 +8,12 @@
     4.4  imports Main Eisbach_Tools
     4.5  begin
     4.6  
     4.7 +
     4.8  section \<open>Named Theorems Tests\<close>
     4.9  
    4.10  named_theorems foo
    4.11  
    4.12 -method foo declares foo =
    4.13 -  \<open>rule foo\<close>
    4.14 +method foo declares foo = (rule foo)
    4.15  
    4.16  lemma
    4.17    assumes A [foo]: A
    4.18 @@ -30,12 +30,12 @@
    4.19  
    4.20    fix A y
    4.21    have "(\<And>x. A x) \<Longrightarrow> A y"
    4.22 -    apply (rule dup, match prems in Y: "\<And>B. P B" for P \<Rightarrow> \<open>match (P) in A \<Rightarrow> \<open>print_fact Y, rule Y\<close>\<close>)
    4.23 -    apply (rule dup, match prems in Y: "\<And>B :: 'a. P B" for P \<Rightarrow> \<open>match (P) in A \<Rightarrow> \<open>print_fact Y, rule Y\<close>\<close>)
    4.24 -    apply (rule dup, match prems in Y: "\<And>B :: 'a. P B" for P \<Rightarrow> \<open>match concl in "P y" for y \<Rightarrow> \<open>print_fact Y, print_term y, rule Y[where B=y]\<close>\<close>)
    4.25 -    apply (rule dup, match prems in Y: "\<And>B :: 'a. P B" for P \<Rightarrow> \<open>match concl in "P z" for z \<Rightarrow> \<open>print_fact Y, print_term y, rule Y[where B=z]\<close>\<close>)
    4.26 -    apply (rule dup, match concl in "P y" for P \<Rightarrow> \<open>match prems in Y: "\<And>z. P z" \<Rightarrow> \<open>print_fact Y, rule Y[where z=y]\<close>\<close>)
    4.27 -    apply (match prems in Y: "\<And>z :: 'a. P z" for P \<Rightarrow> \<open>match concl in "P y" \<Rightarrow> \<open>print_fact Y, rule Y[where z=y]\<close>\<close>)
    4.28 +    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>)
    4.29 +    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>)
    4.30 +    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>)
    4.31 +    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>)
    4.32 +    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>)
    4.33 +    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>)
    4.34      done
    4.35  
    4.36    assume X: "\<And>x. A x" "A y"
    4.37 @@ -44,37 +44,48 @@
    4.38      apply (match X in Y:"B ?x" and Y':"B ?x" for B \<Rightarrow> \<open>print_fact Y, print_term B\<close>)
    4.39      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>)
    4.40      apply (insert X)
    4.41 -    apply (match prems 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>)
    4.42 -    apply (match prems in Y:"B ?x" and Y':"B ?x" for B \<Rightarrow> \<open>print_fact Y, print_term B\<close>)
    4.43 -    apply (match prems in Y:"B x" and Y':"B x" for B x \<Rightarrow> \<open>print_fact Y, print_term B\<close>)
    4.44 -    apply (match concl in "P x" and "P y" for P x \<Rightarrow> \<open>print_term P, print_term x\<close>)
    4.45 +    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>)
    4.46 +    apply (match premises in Y:"B ?x" and Y':"B ?x" for B \<Rightarrow> \<open>print_fact Y, print_term B\<close>)
    4.47 +    apply (match premises in Y:"B x" and Y':"B x" for B x \<Rightarrow> \<open>print_fact Y, print_term B\<close>)
    4.48 +    apply (match conclusion in "P x" and "P y" for P x \<Rightarrow> \<open>print_term P, print_term x\<close>)
    4.49      apply assumption
    4.50      done
    4.51  
    4.52 +  {
    4.53 +   fix B x y
    4.54 +   assume X: "\<And>x y. B x x y"
    4.55 +   have "B x x y"
    4.56 +     by (match X in Y:"\<And>y. B y y z" for z \<Rightarrow> \<open>rule Y[where y=x]\<close>)
    4.57 +
    4.58 +   fix A B
    4.59 +   have "(\<And>x y. A (B x) y) \<Longrightarrow> A (B x) y"
    4.60 +     by (match premises in Y: "\<And>xx. ?H (B xx)" \<Rightarrow> \<open>rule Y\<close>)
    4.61 +  }
    4.62 +
    4.63    (* match focusing retains prems *)
    4.64    fix B x
    4.65    have "(\<And>x. A x) \<Longrightarrow> (\<And>z. B z) \<Longrightarrow> A y \<Longrightarrow> B x"
    4.66 -    apply (match prems in Y: "\<And>z :: 'a. A z"  \<Rightarrow> \<open>match prems in Y': "\<And>z :: 'b. B z" \<Rightarrow> \<open>print_fact Y, print_fact Y', rule Y'[where z=x]\<close>\<close>)
    4.67 +    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>)
    4.68      done
    4.69  
    4.70    (*Attributes *)
    4.71    fix C
    4.72    have "(\<And>x :: 'a. A x)  \<Longrightarrow> (\<And>z. B z) \<Longrightarrow> A y \<Longrightarrow> B x \<and> B x \<and> A y"
    4.73      apply (intro conjI)
    4.74 -    apply (match prems in Y: "\<And>z :: 'a. A z" and Y'[intro]:"\<And>z :: 'b. B z" \<Rightarrow> \<open>fastforce\<close>)
    4.75 -    apply (match prems in Y: "\<And>z :: 'a. A z"  \<Rightarrow> \<open>match prems in Y'[intro]:"\<And>z :: 'b. B z" \<Rightarrow> \<open>fastforce\<close>\<close>)
    4.76 -    apply (match prems in Y[thin]: "\<And>z :: 'a. A z"  \<Rightarrow> \<open>(match prems in Y':"\<And>z :: 'a. A z" \<Rightarrow> \<open>fail\<close> \<bar> Y': "?H" \<Rightarrow> \<open>-\<close>)\<close>)
    4.77 +    apply (match premises in Y: "\<And>z :: 'a. A z" and Y'[intro]:"\<And>z :: 'b. B z" \<Rightarrow> \<open>fastforce\<close>)
    4.78 +    apply (match premises in Y: "\<And>z :: 'a. A z"  \<Rightarrow> \<open>match premises in Y'[intro]:"\<And>z :: 'b. B z" \<Rightarrow> \<open>fastforce\<close>\<close>)
    4.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> Y': "?H" \<Rightarrow> \<open>-\<close>)\<close>)
    4.80      apply assumption
    4.81      done
    4.82  
    4.83    fix A B C D
    4.84    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"
    4.85 -    apply (match prems in Y[thin]: "\<And>z :: 'a. A ?zz' z" and
    4.86 +    apply (match premises in Y[thin]: "\<And>z :: 'a. A ?zz' z" and
    4.87                            Y'[thin]: "\<And>rr :: 'b. B ?zz rr" \<Rightarrow>
    4.88            \<open>print_fact Y, print_fact Y', intro conjI, rule Y', insert Y', insert Y'[where rr=x]\<close>)
    4.89 -    apply (match prems in Y:"B ?u ?x" \<Rightarrow> \<open>rule Y\<close>)
    4.90 +    apply (match premises in Y:"B ?u ?x" \<Rightarrow> \<open>rule Y\<close>)
    4.91      apply (insert TrueI)
    4.92 -    apply (match prems in Y'[thin]: "\<And>ff. B uu ff" for uu \<Rightarrow> \<open>insert Y', drule meta_spec[where x=x]\<close>)
    4.93 +    apply (match premises in Y'[thin]: "\<And>ff. B uu ff" for uu \<Rightarrow> \<open>insert Y', drule meta_spec[where x=x]\<close>)
    4.94      apply assumption
    4.95      done
    4.96  
    4.97 @@ -82,33 +93,33 @@
    4.98    (* Multi-matches. As many facts as match are bound. *)
    4.99    fix A B C x
   4.100    have "(\<And>x :: 'a. A x) \<Longrightarrow> (\<And>y :: 'a. B y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
   4.101 -    apply (match prems in Y[thin]: "\<And>z :: 'a. ?A z" (multi) \<Rightarrow> \<open>intro conjI, (rule Y)+\<close>)
   4.102 -    apply (match prems in Y[thin]: "\<And>z :: 'a. ?A z" (multi) \<Rightarrow> \<open>fail\<close> \<bar> "C y" \<Rightarrow> \<open>-\<close>) (* multi-match must bind something *)
   4.103 -    apply (match prems in Y: "C y" \<Rightarrow> \<open>rule Y\<close>)
   4.104 +    apply (match premises in Y[thin]: "\<And>z :: 'a. ?A z" (multi) \<Rightarrow> \<open>intro conjI, (rule Y)+\<close>)
   4.105 +    apply (match premises in Y[thin]: "\<And>z :: 'a. ?A z" (multi) \<Rightarrow> \<open>fail\<close> \<bar> "C y" \<Rightarrow> \<open>-\<close>) (* multi-match must bind something *)
   4.106 +    apply (match premises in Y: "C y" \<Rightarrow> \<open>rule Y\<close>)
   4.107      done
   4.108  
   4.109    fix A B C x
   4.110    have "(\<And>x :: 'a. A x) \<Longrightarrow> (\<And>y :: 'a. B y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
   4.111 -    apply (match prems in Y[thin]: "\<And>z. ?A z" (multi) \<Rightarrow> \<open>intro conjI, (rule Y)+\<close>)
   4.112 -    apply (match prems in Y[thin]: "\<And>z. ?A z" (multi) \<Rightarrow> \<open>fail\<close> \<bar> "C y" \<Rightarrow> \<open>-\<close>) (* multi-match must bind something *)
   4.113 -    apply (match prems in Y: "C y" \<Rightarrow> \<open>rule Y\<close>)
   4.114 +    apply (match premises in Y[thin]: "\<And>z. ?A z" (multi) \<Rightarrow> \<open>intro conjI, (rule Y)+\<close>)
   4.115 +    apply (match premises in Y[thin]: "\<And>z. ?A z" (multi) \<Rightarrow> \<open>fail\<close> \<bar> "C y" \<Rightarrow> \<open>-\<close>) (* multi-match must bind something *)
   4.116 +    apply (match premises in Y: "C y" \<Rightarrow> \<open>rule Y\<close>)
   4.117      done
   4.118  
   4.119  
   4.120    (*We may use for-fixes in multi-matches too. All bound facts must agree on the fixed term *)
   4.121    fix A B C x
   4.122    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)"
   4.123 -    apply (match prems in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>intro conjI Y[THEN conjunct1]\<close>)
   4.124 -    apply (match prems 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 *)
   4.125 -    apply (match prems in Y: "\<And>x. B x \<and> C x" \<Rightarrow> \<open>intro conjI Y[THEN conjunct1]\<close>)
   4.126 -    apply (match prems in Y: "C ?x" \<Rightarrow> \<open>rule Y\<close>)
   4.127 +    apply (match premises in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>intro conjI Y[THEN conjunct1]\<close>)
   4.128 +    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 *)
   4.129 +    apply (match premises in Y: "\<And>x. B x \<and> C x" \<Rightarrow> \<open>intro conjI Y[THEN conjunct1]\<close>)
   4.130 +    apply (match premises in Y: "C ?x" \<Rightarrow> \<open>rule Y\<close>)
   4.131      done
   4.132  
   4.133    (* Attributes *)
   4.134    fix A B C x
   4.135    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)"
   4.136 -    apply (match prems 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>)
   4.137 -    apply (match prems 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>)
   4.138 +    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>)
   4.139 +    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>)
   4.140      apply assumption
   4.141      done
   4.142  
   4.143 @@ -123,20 +134,31 @@
   4.144    (* Testing THEN_ALL_NEW within match *)
   4.145    fix A B C x
   4.146    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)"
   4.147 -    apply (match prems 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>)
   4.148 +    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>)
   4.149      done
   4.150  
   4.151    (* Cut tests *)
   4.152    fix A B C
   4.153  
   4.154    have "D \<and> C  \<Longrightarrow> A \<and> B  \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> D \<longrightarrow> True \<Longrightarrow> C"
   4.155 -    by (((match prems in I: "P \<and> Q" (cut)
   4.156 +    by (((match premises in I: "P \<and> Q" (cut)
   4.157                and I': "P \<longrightarrow> ?U" for P Q \<Rightarrow> \<open>rule mp [OF I' I[THEN conjunct1]]\<close>)?), simp)
   4.158  
   4.159    have "A \<and> B \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> C"
   4.160 -    by (((match prems in I: "P \<and> Q" (cut)
   4.161 +    by (((match premises in I: "P \<and> Q" (cut)
   4.162                and I': "P \<longrightarrow> ?U" for P Q \<Rightarrow> \<open>rule mp [OF I' I[THEN conjunct1]]\<close>)?, simp) | simp)
   4.163  
   4.164 +  fix f x y
   4.165 +  have "f x y \<Longrightarrow> f x y"
   4.166 +    by (match conclusion in "f x y" for f x y  \<Rightarrow> \<open>print_term f\<close>)
   4.167 +
   4.168 +  fix A B C
   4.169 +  assume X: "A \<and> B" "A \<and> C" C
   4.170 +  have "A \<and> B \<and> C"
   4.171 +    by (match X in H: "A \<and> ?H" (multi,cut) \<Rightarrow>
   4.172 +          \<open>match H in "A \<and> C" and "A \<and> B" \<Rightarrow> \<open>fail\<close>\<close>
   4.173 +        | simp add: X)
   4.174 +
   4.175  end
   4.176  
   4.177  (* Testing inner focusing. This fails if we don't smash flex-flex pairs produced
   4.178 @@ -144,7 +166,7 @@
   4.179     legitimate pairs.*)
   4.180  
   4.181  schematic_lemma "?A x \<Longrightarrow> A x"
   4.182 -  apply (match concl in "H" for H \<Rightarrow> \<open>match concl in Y for Y \<Rightarrow> \<open>print_term Y\<close>\<close>)
   4.183 +  apply (match conclusion in "H" for H \<Rightarrow> \<open>match conclusion in Y for Y \<Rightarrow> \<open>print_term Y\<close>\<close>)
   4.184    apply assumption
   4.185    done
   4.186  
   4.187 @@ -171,7 +193,7 @@
   4.188        NONE => ()
   4.189      | SOME _ => error "Found internal fact")\<close>
   4.190  
   4.191 -method uses_test\<^sub>1 uses uses_test\<^sub>1_uses = \<open>rule uses_test\<^sub>1_uses\<close>
   4.192 +method uses_test\<^sub>1 uses uses_test\<^sub>1_uses = (rule uses_test\<^sub>1_uses)
   4.193  
   4.194  lemma assumes A shows A by (uses_test\<^sub>1 uses_test\<^sub>1_uses: assms)
   4.195  
   4.196 @@ -184,9 +206,9 @@
   4.197  (* Testing term and fact passing in recursion *)
   4.198  
   4.199  method recursion_example for x :: bool uses facts =
   4.200 -  \<open>match (x) in
   4.201 +  (match (x) in
   4.202      "A \<and> B" for A B \<Rightarrow> \<open>(recursion_example A facts: facts, recursion_example B facts: facts)\<close>
   4.203 -  \<bar> "?H" \<Rightarrow> \<open>match facts in U: "x" \<Rightarrow> \<open>insert U\<close>\<close>\<close>
   4.204 +  \<bar> "?H" \<Rightarrow> \<open>match facts in U: "x" \<Rightarrow> \<open>insert U\<close>\<close>)
   4.205  
   4.206  lemma
   4.207    assumes asms: "A" "B" "C" "D"
   4.208 @@ -196,11 +218,11 @@
   4.209    done
   4.210  
   4.211  (*Method.sections in existing method*)
   4.212 -method my_simp\<^sub>1 uses my_simp\<^sub>1_facts = \<open>simp add: my_simp\<^sub>1_facts\<close>
   4.213 +method my_simp\<^sub>1 uses my_simp\<^sub>1_facts = (simp add: my_simp\<^sub>1_facts)
   4.214  lemma assumes A shows A by (my_simp\<^sub>1 my_simp\<^sub>1_facts: assms)
   4.215  
   4.216  (*Method.sections via Eisbach argument parser*)
   4.217 -method uses_test\<^sub>2 uses uses_test\<^sub>2_uses = \<open>uses_test\<^sub>1 uses_test\<^sub>1_uses: uses_test\<^sub>2_uses\<close>
   4.218 +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)
   4.219  lemma assumes A shows A by (uses_test\<^sub>2 uses_test\<^sub>2_uses: assms)
   4.220  
   4.221  
   4.222 @@ -208,7 +230,7 @@
   4.223  
   4.224  named_theorems declare_facts\<^sub>1
   4.225  
   4.226 -method declares_test\<^sub>1 declares declare_facts\<^sub>1 = \<open>rule declare_facts\<^sub>1\<close>
   4.227 +method declares_test\<^sub>1 declares declare_facts\<^sub>1 = (rule declare_facts\<^sub>1)
   4.228  
   4.229  lemma assumes A shows A by (declares_test\<^sub>1 declare_facts\<^sub>1: assms)
   4.230  
   4.231 @@ -218,28 +240,58 @@
   4.232  subsection \<open>Rule Instantiation Tests\<close>
   4.233  
   4.234  method my_allE\<^sub>1 for x :: 'a and P :: "'a \<Rightarrow> bool" =
   4.235 -  \<open>erule allE [where x = x and P = P]\<close>
   4.236 +  (erule allE [where x = x and P = P])
   4.237  
   4.238  lemma "\<forall>x. Q x \<Longrightarrow> Q x" by (my_allE\<^sub>1 x Q)
   4.239  
   4.240  method my_allE\<^sub>2 for x :: 'a and P :: "'a \<Rightarrow> bool" =
   4.241 -  \<open>erule allE [of P x]\<close>
   4.242 +  (erule allE [of P x])
   4.243  
   4.244  lemma "\<forall>x. Q x \<Longrightarrow> Q x" by (my_allE\<^sub>2 x Q)
   4.245  
   4.246  method my_allE\<^sub>3 for x :: 'a and P :: "'a \<Rightarrow> bool" =
   4.247 -  \<open>match allE [where 'a = 'a] in X: "\<And>(x :: 'a) P R. \<forall>x. P x \<Longrightarrow> (P x \<Longrightarrow> R) \<Longrightarrow> R" \<Rightarrow>
   4.248 -    \<open>erule X [where x = x and P = P]\<close>\<close>
   4.249 +  (match allE [where 'a = 'a] in X: "\<And>(x :: 'a) P R. \<forall>x. P x \<Longrightarrow> (P x \<Longrightarrow> R) \<Longrightarrow> R" \<Rightarrow>
   4.250 +    \<open>erule X [where x = x and P = P]\<close>)
   4.251  
   4.252  lemma "\<forall>x. Q x \<Longrightarrow> Q x" by (my_allE\<^sub>3 x Q)
   4.253  
   4.254  method my_allE\<^sub>4 for x :: 'a and P :: "'a \<Rightarrow> bool" =
   4.255 -  \<open>match allE [where 'a = 'a] in X: "\<And>(x :: 'a) P R. \<forall>x. P x \<Longrightarrow> (P x \<Longrightarrow> R) \<Longrightarrow> R" \<Rightarrow>
   4.256 -    \<open>erule X [of x P]\<close>\<close>
   4.257 +  (match allE [where 'a = 'a] in X: "\<And>(x :: 'a) P R. \<forall>x. P x \<Longrightarrow> (P x \<Longrightarrow> R) \<Longrightarrow> R" \<Rightarrow>
   4.258 +    \<open>erule X [of x P]\<close>)
   4.259  
   4.260  lemma "\<forall>x. Q x \<Longrightarrow> Q x" by (my_allE\<^sub>4 x Q)
   4.261  
   4.262  
   4.263 +
   4.264 +(* Polymorphism test *)
   4.265 +
   4.266 +axiomatization foo' :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> bool"
   4.267 +axiomatization where foo'_ax1: "foo' x y z \<Longrightarrow> z \<and> y"
   4.268 +axiomatization where foo'_ax2: "foo' x y y \<Longrightarrow> x \<and> z"
   4.269 +
   4.270 +lemmas my_thms = foo'_ax1 foo'_ax2
   4.271 +
   4.272 +definition first_id where "first_id x = x"
   4.273 +
   4.274 +lemmas my_thms' = my_thms[of "first_id x" for x]
   4.275 +
   4.276 +method print_conclusion = (match conclusion in concl for concl \<Rightarrow> \<open>print_term concl\<close>)
   4.277 +
   4.278 +lemma
   4.279 +  assumes foo: "\<And>x (y :: bool). foo' (A x) B (A x)"
   4.280 +  shows "\<And>z. A z \<and> B"
   4.281 +  apply
   4.282 +    (match conclusion in "f x y" for f y and x :: "'d :: type" \<Rightarrow> \<open>
   4.283 +      match my_thms' in R:"\<And>(x :: 'f :: type). ?P (first_id x) \<Longrightarrow> ?R"
   4.284 +                     and R':"\<And>(x :: 'f :: type). ?P' (first_id x) \<Longrightarrow> ?R'" \<Rightarrow> \<open>
   4.285 +        match (x) in "q :: 'f" for q \<Rightarrow> \<open>
   4.286 +          rule R[of q,simplified first_id_def],
   4.287 +          print_conclusion,
   4.288 +          rule foo
   4.289 +      \<close>\<close>\<close>)
   4.290 +  done
   4.291 +
   4.292 +
   4.293  ML {*
   4.294  structure Data = Generic_Data
   4.295  (
   4.296 @@ -254,7 +306,7 @@
   4.297  
   4.298  setup \<open>Context.theory_map (Data.put @{thms TrueI})\<close>
   4.299  
   4.300 -method dynamic_thms_test = \<open>rule test_dyn\<close>
   4.301 +method dynamic_thms_test = (rule test_dyn)
   4.302  
   4.303  locale foo =
   4.304    fixes A
   4.305 @@ -269,4 +321,12 @@
   4.306  
   4.307  end
   4.308  
   4.309 +(* Method name internalization test *)
   4.310 +
   4.311 +method test2 = (simp)
   4.312 +
   4.313 +method simp = fail
   4.314 +
   4.315 +lemma "A \<Longrightarrow> A" by test2
   4.316 +
   4.317  end
     5.1 --- a/src/HOL/Eisbach/match_method.ML	Thu Apr 30 17:00:50 2015 +0200
     5.2 +++ b/src/HOL/Eisbach/match_method.ML	Thu Apr 30 17:02:57 2015 +0200
     5.3 @@ -46,8 +46,8 @@
     5.4  val aconv_net = Item_Net.init (op aconv) single;
     5.5  
     5.6  val parse_match_kind =
     5.7 -  Scan.lift @{keyword "concl"} >> K Match_Concl ||
     5.8 -  Scan.lift @{keyword "prems"} >> K Match_Prems ||
     5.9 +  Scan.lift @{keyword "conclusion"} >> K Match_Concl ||
    5.10 +  Scan.lift @{keyword "premises"} >> K Match_Prems ||
    5.11    Scan.lift (@{keyword "("}) |-- Args.term --| Scan.lift (@{keyword ")"}) >>
    5.12      (fn t => Match_Term (Item_Net.update t aconv_net)) ||
    5.13    Attrib.thms >> (fn thms => Match_Fact (fold Item_Net.update thms Thm.full_rules));
    5.14 @@ -60,8 +60,8 @@
    5.15    Parse_Tools.parse_term_val Parse.binding;
    5.16  
    5.17  val fixes =
    5.18 -  Parse.and_list1 (Scan.repeat1 bound_term --
    5.19 -    Scan.option (@{keyword "::"} |-- Parse.!!! Parse.typ) >> (fn (xs, T) => map (rpair T) xs))
    5.20 +  Parse.and_list1 (Scan.repeat1  (Parse.position bound_term) --
    5.21 +    Scan.option (@{keyword "::"} |-- Parse.!!! Parse.typ) >> (fn (xs, T) => map (fn (nm,pos) => ((nm,T),pos)) xs))
    5.22    >> flat;
    5.23  
    5.24  val for_fixes = Scan.optional (@{keyword "for"} |-- fixes) [];
    5.25 @@ -77,18 +77,17 @@
    5.26  fun dynamic_fact ctxt =
    5.27    bound_term -- Args.opt_attribs (Attrib.check_name ctxt);
    5.28  
    5.29 -type match_args = {unify : bool, multi : bool, cut : bool};
    5.30 +type match_args = {multi : bool, cut : bool};
    5.31  
    5.32  val parse_match_args =
    5.33    Scan.optional (Args.parens (Parse.enum1 ","
    5.34 -    (Args.$$$ "unify" || Args.$$$ "multi" || Args.$$$ "cut"))) [] >>
    5.35 +    (Args.$$$ "multi" || Args.$$$ "cut"))) [] >>
    5.36      (fn ss =>
    5.37 -      fold (fn s => fn {unify, multi, cut} =>
    5.38 +      fold (fn s => fn {multi, cut} =>
    5.39          (case s of
    5.40 -          "unify" => {unify = true, multi = multi, cut = cut}
    5.41 -        | "multi" => {unify = unify, multi = true, cut = cut}
    5.42 -        | "cut" => {unify = unify, multi = multi, cut = true}))
    5.43 -      ss {unify = false, multi = false, cut = false});
    5.44 +         "multi" => {multi = true, cut = cut}
    5.45 +        | "cut" => {multi = multi, cut = true}))
    5.46 +      ss {multi = false, cut = false});
    5.47  
    5.48  (*TODO: Shape holes in thms *)
    5.49  fun parse_named_pats match_kind =
    5.50 @@ -114,12 +113,12 @@
    5.51                    (Parse_Tools.the_real_val b,
    5.52                      map (Attrib.attribute ctxt) att)) b, match_args), v)
    5.53                  | _ => raise Fail "Expected closed term") ts
    5.54 -          val fixes' = map (fn (p, _) => Parse_Tools.the_real_val p) fixes
    5.55 +          val fixes' = map (fn ((p, _),_) => Parse_Tools.the_real_val p) fixes
    5.56          in (ts', fixes', text) end
    5.57      | SOME _ => error "Unexpected token value in match cartouche"
    5.58      | NONE =>
    5.59          let
    5.60 -          val fixes' = map (fn (pb, otyp) => (Parse_Tools.the_parse_val pb, otyp, NoSyn)) fixes;
    5.61 +          val fixes' = map (fn ((pb, otyp),_) => (Parse_Tools.the_parse_val pb, otyp, NoSyn)) fixes;
    5.62            val (fixes'', ctxt1) = Proof_Context.read_vars fixes' ctxt;
    5.63            val (fix_nms, ctxt2) = Proof_Context.add_fixes fixes'' ctxt1;
    5.64  
    5.65 @@ -134,6 +133,14 @@
    5.66              map (fn (_, (term, _)) => parse_term (Parse_Tools.the_parse_val term)) ts
    5.67              |> Syntax.check_terms ctxt3;
    5.68  
    5.69 +          val pat_fixes = fold (Term.add_frees) pats [] |> map fst;
    5.70 +
    5.71 +          val _ = map2 (fn nm => fn (_,pos) => member (op =) pat_fixes nm orelse
    5.72 +            error ("For-fixed variable must be bound in some pattern." ^ Position.here pos))
    5.73 +            fix_nms fixes;
    5.74 +
    5.75 +          val _ = map (Term.map_types Type.no_tvars) pats
    5.76 +
    5.77            val ctxt4 = fold Variable.declare_term pats ctxt3;
    5.78  
    5.79            val (Ts, ctxt5) = ctxt4 |> fold_map Proof_Context.inferred_param fix_nms;
    5.80 @@ -146,12 +153,6 @@
    5.81              | reject_extra_free _ () = ();
    5.82            val _ = (fold o fold_aterms) reject_extra_free pats ();
    5.83  
    5.84 -          (*fun test_multi_bind {multi = multi, ...} pat = multi andalso
    5.85 -           not (null (inter (op =) (map Free (Term.add_frees pat [])) real_fixes)) andalso
    5.86 -           error "Cannot fix terms in multi-match. Use a schematic instead."
    5.87 -
    5.88 -          val _ = map2 (fn pat => fn (_, (_, match_args)) => test_multi_bind match_args pat) pats ts*)
    5.89 -
    5.90            val binds =
    5.91              map (fn (b, _) => Option.map (fn (b, att) => (Parse_Tools.the_parse_val b, att)) b) ts;
    5.92  
    5.93 @@ -184,7 +185,7 @@
    5.94              |> (fn ctxt => fold2 upd_ctxt binds pats ([], ctxt) |> apfst rev)
    5.95              ||> Proof_Context.restore_mode ctxt;
    5.96  
    5.97 -          val (src, text) = Method_Closure.read_text_closure ctxt6 (Token.input_of cartouche);
    5.98 +          val (src, text) = Method_Closure.read_inner_text_closure ctxt6 (Token.input_of cartouche);
    5.99  
   5.100            val morphism =
   5.101              Variable.export_morphism ctxt6
   5.102 @@ -206,7 +207,7 @@
   5.103  
   5.104            val real_fixes' = map (Morphism.term morphism) real_fixes;
   5.105            val _ =
   5.106 -            ListPair.app (fn ((Parse_Tools.Parse_Val (_, f), _), t) => f t) (fixes, real_fixes');
   5.107 +            ListPair.app (fn (( (Parse_Tools.Parse_Val (_, f),_) , _), t) => f t) (fixes, real_fixes');
   5.108  
   5.109            val match_args = map (fn (_, (_, match_args)) => match_args) ts;
   5.110            val binds'' = (binds' ~~ match_args) ~~ pats';
   5.111 @@ -234,19 +235,9 @@
   5.112    let
   5.113      val ts' = map (Envir.norm_term env) ts;
   5.114      val insts = map (Thm.cterm_of ctxt) ts' ~~ map (Thm.cterm_of ctxt) params;
   5.115 -    val tags = Thm.get_tags thm;
   5.116  
   5.117 -   (*
   5.118 -    val Tinsts = Type.raw_matches ((map (fastype_of) params), (map (fastype_of) ts')) Vartab.empty
   5.119 -    |> Vartab.dest
   5.120 -    |> map (fn (xi, (S, typ)) => (certT (TVar (xi, S)), certT typ))
   5.121 -   *)
   5.122 -
   5.123 -    val thm' = Drule.cterm_instantiate insts thm
   5.124 -    (*|> Thm.instantiate (Tinsts, [])*)
   5.125 -      |> Thm.map_tags (K tags);
   5.126    in
   5.127 -    thm'
   5.128 +    Drule.cterm_instantiate insts thm
   5.129    end;
   5.130  
   5.131  fun do_inst fact_insts' env text ctxt =
   5.132 @@ -282,6 +273,7 @@
   5.133  
   5.134      val morphism =
   5.135        Morphism.term_morphism "do_inst.term" (Envir.norm_term env) $>
   5.136 +      Morphism.typ_morphism "do_inst.type" (Envir.norm_type (Envir.type_env env)) $>
   5.137        Morphism.fact_morphism "do_inst.fact" (maps expand_fact);
   5.138  
   5.139      val text' = Method.map_source (Token.transform_src morphism) text;
   5.140 @@ -303,32 +295,61 @@
   5.141      val pat'' :: params'' = map (Morphism.term morphism) (pat' :: params');
   5.142  
   5.143      fun prep_head (t, att) = (dest_internal_fact t, att);
   5.144 +
   5.145    in
   5.146      ((((Option.map prep_head x, args), params''), pat''), ctxt')
   5.147    end;
   5.148  
   5.149 -fun match_filter_env ctxt fixes (ts, params) thm env =
   5.150 +fun recalculate_maxidx env =
   5.151    let
   5.152 +    val tenv = Envir.term_env env;
   5.153 +    val tyenv = Envir.type_env env;
   5.154 +    val max_tidx = Vartab.fold (fn (_,(_,t)) => curry Int.max (maxidx_of_term t)) tenv ~1;
   5.155 +    val max_Tidx = Vartab.fold (fn (_,(_,T)) => curry Int.max (maxidx_of_typ T)) tyenv ~1;
   5.156 +  in
   5.157 +    Envir.Envir
   5.158 +      {maxidx = Int.max (Int.max (max_tidx,max_Tidx),Envir.maxidx_of env),
   5.159 +        tenv = tenv, tyenv = tyenv}
   5.160 +  end
   5.161 +
   5.162 +fun match_filter_env inner_ctxt morphism pat_vars fixes (ts, params) thm inner_env =
   5.163 +  let
   5.164 +    val tenv = Envir.term_env inner_env
   5.165 +      |> Vartab.map (K (fn (T,t) => (Morphism.typ morphism T,Morphism.term morphism t)));
   5.166 +
   5.167 +    val tyenv = Envir.type_env inner_env
   5.168 +      |> Vartab.map (K (fn (S,T) => (S,Morphism.typ morphism T)));
   5.169 +
   5.170 +    val outer_env = Envir.Envir {maxidx = Envir.maxidx_of inner_env, tenv = tenv, tyenv = tyenv};
   5.171 +
   5.172      val param_vars = map Term.dest_Var params;
   5.173 -    val params' = map (Envir.lookup env) param_vars;
   5.174 +
   5.175 +    val params' = map (fn (xi,_) => Vartab.lookup (Envir.term_env outer_env) xi) param_vars;
   5.176  
   5.177      val fixes_vars = map Term.dest_Var fixes;
   5.178  
   5.179 -    val tenv = Envir.term_env env;
   5.180      val all_vars = Vartab.keys tenv;
   5.181  
   5.182      val extra_vars = subtract (fn ((xi, _), xi') => xi = xi') fixes_vars all_vars;
   5.183  
   5.184 -    val tenv' = Envir.term_env env
   5.185 +    val tenv' = tenv
   5.186        |> fold (Vartab.delete_safe) extra_vars;
   5.187  
   5.188      val env' =
   5.189 -      Envir.Envir {maxidx = Envir.maxidx_of env, tenv = tenv', tyenv = Envir.type_env env};
   5.190 +      Envir.Envir {maxidx = Envir.maxidx_of outer_env, tenv = tenv', tyenv = tyenv}
   5.191 +      |> recalculate_maxidx;
   5.192 +
   5.193 +    val all_params_bound = forall (fn SOME (_,(Var _)) => true | _ => false) params';
   5.194 +
   5.195 +    val pat_fixes = inter (eq_fst (op =)) fixes_vars pat_vars;
   5.196  
   5.197 -    val all_params_bound = forall (fn SOME (Var _) => true | _ => false) params';
   5.198 +    val all_pat_fixes_bound = forall (fn (xi,_) => is_some (Vartab.lookup tenv' xi)) pat_fixes;
   5.199 +
   5.200 +    val thm' = Morphism.thm morphism thm;
   5.201 +
   5.202    in
   5.203 -    if all_params_bound
   5.204 -    then SOME (case ts of SOME ts => inst_thm ctxt env params ts thm | _ => thm, env')
   5.205 +    if all_params_bound andalso all_pat_fixes_bound then
   5.206 +      SOME (case ts of SOME ts => inst_thm inner_ctxt outer_env params ts thm' | _ => thm', env')
   5.207      else NONE
   5.208    end;
   5.209  
   5.210 @@ -436,28 +457,78 @@
   5.211  
   5.212  val raise_match : (thm * Envir.env) Seq.seq = Seq.make (fn () => raise MATCH_CUT);
   5.213  
   5.214 +fun map_handle seq =
   5.215 +  Seq.make (fn () =>
   5.216 +    (case (Seq.pull seq handle MATCH_CUT => NONE) of
   5.217 +      SOME (x, seq') => SOME (x, map_handle seq')
   5.218 +    | NONE => NONE));
   5.219 +
   5.220 +fun deduplicate eq prev seq =
   5.221 +  Seq.make (fn () =>
   5.222 +    (case (Seq.pull seq) of
   5.223 +      SOME (x, seq') =>
   5.224 +        if member eq prev x
   5.225 +        then Seq.pull (deduplicate eq prev seq')
   5.226 +        else SOME (x,deduplicate eq (x :: prev) seq')
   5.227 +    | NONE => NONE));
   5.228 +
   5.229 +fun consistent_env env =
   5.230 +  let
   5.231 +    val tenv = Envir.term_env env;
   5.232 +    val tyenv = Envir.type_env env;
   5.233 +  in
   5.234 +    forall (fn (_, (T, t)) => Envir.norm_type tyenv T = fastype_of t) (Vartab.dest tenv)
   5.235 +  end;
   5.236 +
   5.237 +fun eq_env (env1,env2) =
   5.238 +  let
   5.239 +    val tyenv1 = Envir.type_env env1;
   5.240 +    val tyenv2 = Envir.type_env env2;
   5.241 +  in
   5.242 +    Envir.maxidx_of env1 = Envir.maxidx_of env1 andalso
   5.243 +    ListPair.allEq (fn ((var, (_, t)), (var', (_, t'))) =>
   5.244 +        (var = var' andalso
   5.245 +          Envir.eta_contract (Envir.norm_term env1 t) aconv
   5.246 +          Envir.eta_contract (Envir.norm_term env2 t')))
   5.247 +      (apply2 Vartab.dest (Envir.term_env env1, Envir.term_env env2))
   5.248 +    andalso
   5.249 +    ListPair.allEq (fn ((var, (_, T)), (var', (_,T'))) =>
   5.250 +        var = var' andalso Envir.norm_type tyenv1 T = Envir.norm_type tyenv2 T')
   5.251 +      (apply2 Vartab.dest (Envir.type_env env1, Envir.type_env env2))
   5.252 +  end;
   5.253 +
   5.254 +
   5.255  fun match_facts ctxt fixes prop_pats get =
   5.256    let
   5.257      fun is_multi (((_, x : match_args), _), _) = #multi x;
   5.258 -    fun is_unify (_, x : match_args) = #unify x;
   5.259      fun is_cut (_, x : match_args) = #cut x;
   5.260  
   5.261      fun match_thm (((x, params), pat), thm) env  =
   5.262        let
   5.263          fun try_dest_term term = the_default term (try Logic.dest_term term);
   5.264  
   5.265 +        val pat_vars = Term.add_vars pat [];
   5.266 +
   5.267          val pat' = pat |> Envir.norm_term env |> try_dest_term;
   5.268  
   5.269 -        val item' = Thm.prop_of thm |> try_dest_term;
   5.270 +        val (((Tinsts', insts),[thm']), inner_ctxt) = Variable.import false [thm] ctxt
   5.271 +
   5.272 +        val item' = Thm.prop_of thm' |> try_dest_term;
   5.273 +
   5.274          val ts = Option.map (fst o fst) (fst x);
   5.275 -        (*FIXME: Do we need to move one of these patterns above the other?*)
   5.276 +
   5.277 +        val outer_ctxt = ctxt |> Variable.declare_maxidx (Envir.maxidx_of env);
   5.278 +
   5.279 +        val morphism = Variable.export_morphism inner_ctxt outer_ctxt;
   5.280  
   5.281          val matches =
   5.282 -          (if is_unify x
   5.283 -           then Unify.smash_unifiers (Context.Proof ctxt) [(pat', item') ] env
   5.284 -           else Unify.matchers (Context.Proof ctxt) [(pat', item')])
   5.285 +          (Unify.matchers (Context.Proof ctxt) [(pat', item')])
   5.286 +          |> Seq.filter consistent_env
   5.287            |> Seq.map_filter (fn env' =>
   5.288 -              match_filter_env ctxt fixes (ts, params) thm (Envir.merge (env, env')))
   5.289 +              match_filter_env inner_ctxt morphism pat_vars fixes
   5.290 +                (ts, params) thm' (Envir.merge (env, env')))
   5.291 +          |> Seq.map (apfst (Thm.map_tags (K (Thm.get_tags thm))))
   5.292 +          |> deduplicate (eq_snd eq_env) []
   5.293            |> is_cut x ? (fn t => Seq.make (fn () =>
   5.294              Option.map (fn (x, _) => (x, raise_match)) (Seq.pull t)));
   5.295        in
   5.296 @@ -487,12 +558,6 @@
   5.297  
   5.298      val all_matches =
   5.299        Seq.EVERY (map proc_multi_match all_matches) ([], Envir.empty ~1)
   5.300 -      |> Seq.filter (fn (_, e) => forall (is_some o Envir.lookup e o Term.dest_Var) fixes);
   5.301 -
   5.302 -    fun map_handle seq = Seq.make (fn () =>
   5.303 -      (case (Seq.pull seq handle MATCH_CUT => NONE) of
   5.304 -        SOME (x, seq') => SOME (x, map_handle seq')
   5.305 -      | NONE => NONE));
   5.306    in
   5.307      map_handle all_matches
   5.308    end;
     6.1 --- a/src/HOL/Eisbach/method_closure.ML	Thu Apr 30 17:00:50 2015 +0200
     6.2 +++ b/src/HOL/Eisbach/method_closure.ML	Thu Apr 30 17:02:57 2015 +0200
     6.3 @@ -14,7 +14,8 @@
     6.4    val tag_free_thm: thm -> thm
     6.5    val free_aware_rule_attribute: thm list -> (Context.generic -> thm -> thm) -> Thm.attribute
     6.6    val read_inner_method: Proof.context -> Token.src -> Method.text
     6.7 -  val read_text_closure: Proof.context -> Input.source -> Token.src * Method.text
     6.8 +  val read_text_closure: Proof.context -> Token.src -> Token.src * Method.text
     6.9 +  val read_inner_text_closure: Proof.context -> Input.source -> Token.src * Method.text
    6.10    val method_evaluate: Method.text -> Proof.context -> Method.method
    6.11    val get_inner_method: Proof.context -> string * Position.T ->
    6.12      (term list * (string list * string list)) * Method.text
    6.13 @@ -22,9 +23,9 @@
    6.14      term list -> (string * thm list) list -> Method.method list ->
    6.15      Proof.context -> Method.method
    6.16    val method_definition: binding -> (binding * typ option * mixfix) list ->
    6.17 -    binding list -> binding list -> binding list -> Input.source -> local_theory -> local_theory
    6.18 +    binding list -> binding list -> binding list -> Token.src -> local_theory -> local_theory
    6.19    val method_definition_cmd: binding -> (binding * string option * mixfix) list ->
    6.20 -    binding list -> binding list -> binding list -> Input.source -> local_theory -> local_theory
    6.21 +    binding list -> binding list -> binding list -> Token.src -> local_theory -> local_theory
    6.22  end;
    6.23  
    6.24  structure Method_Closure: METHOD_CLOSURE =
    6.25 @@ -97,38 +98,36 @@
    6.26      val parser = Parse.!!! (Method.parser' ctxt 0 --| Scan.ahead Parse.eof);
    6.27    in
    6.28      (case Scan.read Token.stopper parser toks of
    6.29 -      SOME (method_text, _) => method_text
    6.30 +      SOME (method_text, pos) => (Method.report (method_text, pos); method_text)
    6.31      | NONE => error ("Failed to parse method" ^ Position.here (#2 (Token.name_of_src src))))
    6.32    end;
    6.33  
    6.34 -fun read_text_closure ctxt input =
    6.35 +fun read_text_closure ctxt source =
    6.36    let
    6.37 -    (*tokens*)
    6.38 +    val src = Token.init_assignable_src source;
    6.39 +    val method_text = read_inner_method ctxt src;
    6.40 +    val method_text' = Method.map_source (Method.method_closure ctxt) method_text;
    6.41 +    (*FIXME: Does not markup method parameters. Needs to be done by Method.parser' directly. *)
    6.42 +    val _ = Method.map_source (fn src => (try (Method.check_name ctxt) (Token.name_of_src src);src)) method_text;
    6.43 +    val src' = Token.closure_src src;
    6.44 +  in (src', method_text') end;
    6.45 +
    6.46 +fun read_inner_text_closure ctxt input =
    6.47 +  let
    6.48      val keywords = Thy_Header.get_keywords' ctxt;
    6.49      val toks =
    6.50        Input.source_explode input
    6.51        |> Token.read_no_commands keywords (Scan.one Token.not_eof);
    6.52 -    val _ =
    6.53 -      toks |> List.app (fn tok =>
    6.54 -        if Token.keyword_with Symbol.is_ascii_identifier tok then
    6.55 -          Context_Position.report ctxt (Token.pos_of tok) Markup.keyword1
    6.56 -        else ());
    6.57 +  in read_text_closure ctxt (Token.src ("", Input.pos_of input) toks) end;
    6.58  
    6.59 -    (*source closure*)
    6.60 -    val src =
    6.61 -      Token.src ("", Input.pos_of input) toks
    6.62 -      |> Token.init_assignable_src;
    6.63 -    val method_text = read_inner_method ctxt src;
    6.64 -    val method_text' = Method.map_source (Method.method_closure ctxt) method_text;
    6.65 -    val src' = Token.closure_src src;
    6.66 -  in (src', method_text') end;
    6.67  
    6.68  val parse_method =
    6.69    Args.context -- Scan.lift (Parse.token Parse.cartouche) >> (fn (ctxt, tok) =>
    6.70      (case Token.get_value tok of
    6.71        NONE =>
    6.72          let
    6.73 -           val (src, text) = read_text_closure ctxt (Token.input_of tok);
    6.74 +           val input = Token.input_of tok;
    6.75 +           val (src,text) = read_inner_text_closure ctxt input;
    6.76             val _ = Token.assign (SOME (Token.Source src)) tok;
    6.77          in text end
    6.78      | SOME (Token.Source src) => read_inner_method ctxt src
    6.79 @@ -274,7 +273,7 @@
    6.80      fn ctxt => evaluate_method_def (match fixes) text (setup_ctxt ctxt)
    6.81    end;
    6.82  
    6.83 -fun gen_method_definition prep_vars name vars uses attribs methods body lthy =
    6.84 +fun gen_method_definition prep_vars name vars uses attribs methods source lthy =
    6.85    let
    6.86      val (uses_nms, lthy1) = lthy
    6.87        |> Proof_Context.concealed
    6.88 @@ -304,7 +303,7 @@
    6.89          (parser term_args
    6.90            (fn (fixes, decl) => fn ctxt => get_recursive_method ctxt fixes (decl ctxt))) "(internal)";
    6.91  
    6.92 -    val (src, text) = read_text_closure lthy3 body;
    6.93 +    val (src, text) = read_text_closure lthy3 source;
    6.94  
    6.95      val morphism =
    6.96        Variable.export_morphism lthy3
    6.97 @@ -338,7 +337,8 @@
    6.98        ((Scan.optional (@{keyword "uses"} |-- Parse.!!! (Scan.repeat1 Parse.binding)) []) --
    6.99          (Scan.optional (@{keyword "declares"} |-- Parse.!!! (Scan.repeat1 Parse.binding)) [])) --
   6.100        (Scan.optional (@{keyword "methods"} |-- Parse.!!! (Scan.repeat1 Parse.binding)) []) --
   6.101 -      Parse.!!! (@{keyword "="} |-- Parse.token Parse.cartouche)
   6.102 -      >> (fn ((((name, vars), (uses, attribs)), methods), cartouche) =>
   6.103 -        method_definition_cmd name vars uses attribs methods (Token.input_of cartouche)));
   6.104 +      Parse.!!! (@{keyword "="}
   6.105 +        |-- (Parse.position (Parse.args1 (K true)) >> (fn (args, pos) => Token.src ("", pos) args)))
   6.106 +      >> (fn ((((name, vars), (uses, attribs)), methods), source) =>
   6.107 +        method_definition_cmd name vars uses attribs methods source));
   6.108  end;