added Eisbach, using version 3752768caa17 of its Bitbucket repository;
authorwenzelm
Fri Apr 17 17:49:19 2015 +0200 (2015-04-17)
changeset 6011954bea620e54f
parent 60116 5d90d301ad66
child 60120 a32504fefa94
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
ANNOUNCE
CONTRIBUTORS
NEWS
src/HOL/Eisbach/Eisbach.thy
src/HOL/Eisbach/Eisbach_Tools.thy
src/HOL/Eisbach/Examples.thy
src/HOL/Eisbach/Tests.thy
src/HOL/Eisbach/eisbach_antiquotations.ML
src/HOL/Eisbach/eisbach_rule_insts.ML
src/HOL/Eisbach/match_method.ML
src/HOL/Eisbach/method_closure.ML
src/HOL/Eisbach/parse_tools.ML
src/HOL/ROOT
     1.1 --- a/ANNOUNCE	Fri Apr 17 16:54:25 2015 +0200
     1.2 +++ b/ANNOUNCE	Fri Apr 17 17:49:19 2015 +0200
     1.3 @@ -24,6 +24,8 @@
     1.4  * New proof method "rewrite" for single-step rewriting with subterm
     1.5  selection based on patterns.
     1.6  
     1.7 +* New Eisbach proof method language and "match" method.
     1.8 +
     1.9  * Updated manuals: datatypes, implementation, isar-ref, jedit, sledgehammer,
    1.10  system.
    1.11  
     2.1 --- a/CONTRIBUTORS	Fri Apr 17 16:54:25 2015 +0200
     2.2 +++ b/CONTRIBUTORS	Fri Apr 17 17:49:19 2015 +0200
     2.3 @@ -6,6 +6,9 @@
     2.4  Contributions to Isabelle2015
     2.5  -----------------------------
     2.6  
     2.7 +* 2014/2015: Daniel Matichuk, Toby Murray, NICTA and Makarius Wenzel
     2.8 +  The Eisbach proof method language and "match" method.
     2.9 +
    2.10  * March 2015: Jasmin Blanchette, Inria & LORIA & MPII, Mathias Fleury, MPII,
    2.11    and Dmitriy Traytel, TUM
    2.12    More multiset theorems, syntax, and operations.
     3.1 --- a/NEWS	Fri Apr 17 16:54:25 2015 +0200
     3.2 +++ b/NEWS	Fri Apr 17 17:49:19 2015 +0200
     3.3 @@ -59,6 +59,13 @@
     3.4  * Structural composition of proof methods (meth1; meth2) in Isar
     3.5  corresponds to (tac1 THEN_ALL_NEW tac2) in ML.
     3.6  
     3.7 +* The Eisbach proof method language allows to define new proof methods
     3.8 +by combining existing ones with their usual syntax. The "match" proof
     3.9 +method provides basic fact/term matching in addition to
    3.10 +premise/conclusion matching through Subgoal.focus, and binds fact names
    3.11 +from matches as well as term patterns within matches. See also
    3.12 +~~/src/HOL/Eisbach/Eisbach.thy and the included examples.
    3.13 +
    3.14  
    3.15  *** Prover IDE -- Isabelle/Scala/jEdit ***
    3.16  
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Eisbach/Eisbach.thy	Fri Apr 17 17:49:19 2015 +0200
     4.3 @@ -0,0 +1,43 @@
     4.4 +(*  Title:      Eisbach.thy
     4.5 +    Author:     Daniel Matichuk, NICTA/UNSW
     4.6 +
     4.7 +Main entry point for Eisbach proof method language.
     4.8 +*)
     4.9 +
    4.10 +theory Eisbach
    4.11 +imports Pure
    4.12 +keywords
    4.13 +  "method" :: thy_decl and
    4.14 +  "concl"
    4.15 +  "prems"  (* FIXME conflict with "prems" in Isar, which is presently dormant *)
    4.16 +  "declares"
    4.17 +  "methods"
    4.18 +  "\<bar>" "\<Rightarrow>"
    4.19 +  "uses"
    4.20 +begin
    4.21 +
    4.22 +ML_file "parse_tools.ML"
    4.23 +ML_file "eisbach_rule_insts.ML"
    4.24 +ML_file "method_closure.ML"
    4.25 +ML_file "match_method.ML"
    4.26 +ML_file "eisbach_antiquotations.ML"
    4.27 +
    4.28 +(* FIXME reform Isabelle/Pure attributes to make this work by default *)
    4.29 +attribute_setup THEN =
    4.30 +  \<open>Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm >> (fn (i, B) =>
    4.31 +    Method_Closure.free_aware_rule_attribute [B] (fn _ => fn A => A RSN (i, B)))\<close>
    4.32 +  "resolution with rule"
    4.33 +
    4.34 +attribute_setup OF =
    4.35 +  \<open>Attrib.thms >> (fn Bs =>
    4.36 +    Method_Closure.free_aware_rule_attribute Bs (fn _ => fn A => A OF Bs))\<close>
    4.37 +  "rule resolved with facts"
    4.38 +
    4.39 +attribute_setup rotated =
    4.40 +  \<open>Scan.lift (Scan.optional Parse.int 1 >> (fn n =>
    4.41 +    Method_Closure.free_aware_rule_attribute [] (fn _ => rotate_prems n)))\<close>
    4.42 +  "rotated theorem premises"
    4.43 +
    4.44 +method solves methods m = \<open>m; fail\<close>
    4.45 +
    4.46 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Eisbach/Eisbach_Tools.thy	Fri Apr 17 17:49:19 2015 +0200
     5.3 @@ -0,0 +1,43 @@
     5.4 +(*  Title:      Eisbach_Tools.thy
     5.5 +    Author:     Daniel Matichuk, NICTA/UNSW
     5.6 +
     5.7 +Usability tools for Eisbach.
     5.8 +*)
     5.9 +
    5.10 +theory Eisbach_Tools
    5.11 +imports Eisbach
    5.12 +begin
    5.13 +
    5.14 +ML \<open>
    5.15 +local
    5.16 +
    5.17 +fun trace_method parser print =
    5.18 +  Scan.lift (Args.mode "dummy") -- parser >>
    5.19 +    (fn (dummy, x) => fn ctxt => SIMPLE_METHOD (fn st =>
    5.20 +      (if dummy orelse not (Method_Closure.is_dummy st) then tracing (print ctxt x) else ();
    5.21 +       all_tac st)));
    5.22 +
    5.23 +fun setup_trace_method binding parser print =
    5.24 +  Method.setup binding
    5.25 +    (trace_method parser (fn ctxt => fn x => Binding.name_of binding ^ ": " ^ print ctxt x))
    5.26 +    "";
    5.27 +
    5.28 +in
    5.29 +
    5.30 +val _ =
    5.31 +  Theory.setup
    5.32 +   (setup_trace_method @{binding print_fact}
    5.33 +      (Scan.lift (Scan.ahead Parse.not_eof) -- Attrib.thms)
    5.34 +      (fn ctxt => fn (tok, thms) =>
    5.35 +        (* FIXME proper formatting!? *)
    5.36 +        Token.unparse tok ^ ": " ^ commas (map (Display.string_of_thm ctxt) thms)) #>
    5.37 +    setup_trace_method @{binding print_term}
    5.38 +      (Scan.lift (Scan.ahead Parse.not_eof) -- Args.term)
    5.39 +      (fn ctxt => fn (tok, t) =>
    5.40 +        (* FIXME proper formatting!? *)
    5.41 +        Token.unparse tok ^ ": " ^ Syntax.string_of_term ctxt t));
    5.42 +
    5.43 +end
    5.44 +\<close>
    5.45 +
    5.46 +end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Eisbach/Examples.thy	Fri Apr 17 17:49:19 2015 +0200
     6.3 @@ -0,0 +1,220 @@
     6.4 +(*  Title:      Examples.thy
     6.5 +    Author:     Daniel Matichuk, NICTA/UNSW
     6.6 +*)
     6.7 +
     6.8 +section \<open>Basic Eisbach examples\<close>
     6.9 +
    6.10 +theory Examples
    6.11 +imports Main Eisbach_Tools
    6.12 +begin
    6.13 +
    6.14 +
    6.15 +subsection \<open>Basic methods\<close>
    6.16 +
    6.17 +method my_intros = \<open>rule conjI | rule impI\<close>
    6.18 +
    6.19 +lemma "P \<and> Q \<longrightarrow> Z \<and> X"
    6.20 +  apply my_intros+
    6.21 +  oops
    6.22 +
    6.23 +method my_intros' uses intros = \<open>rule conjI | rule impI | rule intros\<close>
    6.24 +
    6.25 +lemma "P \<and> Q \<longrightarrow> Z \<or> X"
    6.26 +  apply (my_intros' intros: disjI1)+
    6.27 +  oops
    6.28 +
    6.29 +method my_spec for x :: 'a = \<open>drule spec[where x="x"]\<close>
    6.30 +
    6.31 +lemma "\<forall>x. P x \<Longrightarrow> P x"
    6.32 +  apply (my_spec x)
    6.33 +  apply assumption
    6.34 +  done
    6.35 +
    6.36 +
    6.37 +subsection \<open>Focusing and matching\<close>
    6.38 +
    6.39 +method match_test =
    6.40 +  \<open>match prems in U: "P x \<and> Q x" for P Q x \<Rightarrow>
    6.41 +    \<open>print_term P,
    6.42 +     print_term Q,
    6.43 +     print_term x,
    6.44 +     print_fact U\<close>\<close>
    6.45 +
    6.46 +lemma "\<And>x. P x \<and> Q x \<Longrightarrow> A x \<and> B x \<Longrightarrow> R x y \<Longrightarrow> True"
    6.47 +  apply match_test  -- \<open>Valid match, but not quite what we were expecting..\<close>
    6.48 +  back  -- \<open>Can backtrack over matches, exploring all bindings\<close>
    6.49 +  back
    6.50 +  back
    6.51 +  back
    6.52 +  back
    6.53 +  back  -- \<open>Found the other conjunction\<close>
    6.54 +  back
    6.55 +  back
    6.56 +  back
    6.57 +  back
    6.58 +  back
    6.59 +  oops
    6.60 +
    6.61 +text \<open>Use matching to avoid "improper" methods\<close>
    6.62 +
    6.63 +lemma focus_test:
    6.64 +  shows "\<And>x. \<forall>x. P x \<Longrightarrow> P x"
    6.65 +  apply (my_spec "x :: 'a", assumption)?  -- \<open>Wrong x\<close>
    6.66 +  apply (match concl in "P x" for x \<Rightarrow> \<open>my_spec x, assumption\<close>)
    6.67 +  done
    6.68 +
    6.69 +
    6.70 +text \<open>Matches are exclusive. Backtracking will not occur past a match\<close>
    6.71 +
    6.72 +method match_test' =
    6.73 +  \<open>match concl in
    6.74 +    "P \<and> Q" for P Q \<Rightarrow>
    6.75 +      \<open>print_term P, print_term Q, rule conjI[where P="P" and Q="Q"]; assumption\<close>
    6.76 +    \<bar> "H" for H \<Rightarrow> \<open>print_term H\<close>
    6.77 +  \<close>
    6.78 +
    6.79 +text \<open>Solves goal\<close>
    6.80 +lemma "P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q"
    6.81 +  apply match_test'
    6.82 +  done
    6.83 +
    6.84 +text \<open>Fall-through case never taken\<close>
    6.85 +lemma "P \<and> Q"
    6.86 +  apply match_test'?
    6.87 +  oops
    6.88 +
    6.89 +lemma "P"
    6.90 +  apply match_test'
    6.91 +  oops
    6.92 +
    6.93 +
    6.94 +method my_spec_guess =
    6.95 +  \<open>match concl in "P (x :: 'a)" for P x \<Rightarrow>
    6.96 +    \<open>drule spec[where x=x],
    6.97 +     print_term P,
    6.98 +     print_term x\<close>\<close>
    6.99 +
   6.100 +lemma "\<forall>x. P (x :: nat) \<Longrightarrow> Q (x :: nat)"
   6.101 +  apply my_spec_guess
   6.102 +  oops
   6.103 +
   6.104 +method my_spec_guess2 =
   6.105 +  \<open>match prems in U[thin]:"\<forall>x. P x \<longrightarrow> Q x" and U':"P x" for P Q x \<Rightarrow>
   6.106 +    \<open>insert spec[where x=x, OF U],
   6.107 +     print_term P,
   6.108 +     print_term Q\<close>\<close>
   6.109 +
   6.110 +lemma "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> Q x \<Longrightarrow> Q x"
   6.111 +  apply my_spec_guess2?  -- \<open>Fails. Note that both "P"s must match\<close>
   6.112 +  oops
   6.113 +
   6.114 +lemma "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> P x \<Longrightarrow> Q x"
   6.115 +  apply my_spec_guess2
   6.116 +  apply (erule mp)
   6.117 +  apply assumption
   6.118 +  done
   6.119 +
   6.120 +
   6.121 +subsection \<open>Higher-order methods\<close>
   6.122 +
   6.123 +method higher_order_example for x methods meth =
   6.124 +  \<open>cases x, meth, meth\<close>
   6.125 +
   6.126 +lemma
   6.127 +  assumes A: "x = Some a"
   6.128 +  shows "the x = a"
   6.129 +  by (higher_order_example x \<open>simp add: A\<close>)
   6.130 +
   6.131 +
   6.132 +subsection \<open>Recursion\<close>
   6.133 +
   6.134 +method recursion_example for x :: bool =
   6.135 +  \<open>print_term x,
   6.136 +     match (x) in "A \<and> B" for A B \<Rightarrow>
   6.137 +    \<open>(print_term A,
   6.138 +     print_term B,
   6.139 +     recursion_example A,
   6.140 +     recursion_example B) | -\<close>\<close>
   6.141 +
   6.142 +lemma "P"
   6.143 +  apply (recursion_example "(A \<and> D) \<and> (B \<and> C)")
   6.144 +  oops
   6.145 +
   6.146 +
   6.147 +subsection \<open>Solves combinator\<close>
   6.148 +
   6.149 +lemma "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
   6.150 +  apply (solves \<open>rule conjI\<close>)?  -- \<open>Doesn't solve the goal!\<close>
   6.151 +  apply (solves \<open>rule conjI, assumption, assumption\<close>)
   6.152 +  done
   6.153 +
   6.154 +
   6.155 +subsection \<open>Demo\<close>
   6.156 +
   6.157 +method solve methods m = \<open>m;fail\<close>
   6.158 +
   6.159 +named_theorems intros and elims and subst
   6.160 +
   6.161 +method prop_solver declares intros elims subst =
   6.162 +  \<open>(assumption |
   6.163 +    rule intros | erule elims |
   6.164 +    subst subst | subst (asm) subst |
   6.165 +    (erule notE; solve \<open>prop_solver\<close>))+\<close>
   6.166 +
   6.167 +lemmas [intros] =
   6.168 +  conjI
   6.169 +  impI
   6.170 +  disjCI
   6.171 +  iffI
   6.172 +  notI
   6.173 +lemmas [elims] =
   6.174 +  impCE
   6.175 +  conjE
   6.176 +  disjE
   6.177 +
   6.178 +lemma "((A \<or> B) \<and> (A \<longrightarrow> C) \<and> (B \<longrightarrow> C)) \<longrightarrow> C"
   6.179 +  apply prop_solver
   6.180 +  done
   6.181 +
   6.182 +method guess_all =
   6.183 +  \<open>match prems in U[thin]:"\<forall>x. P (x :: 'a)" for P \<Rightarrow>
   6.184 +    \<open>match prems in "?H (y :: 'a)" for y \<Rightarrow>
   6.185 +       \<open>rule allE[where P = P and x = y, OF U]\<close>
   6.186 +   | match concl in "?H (y :: 'a)" for y \<Rightarrow>
   6.187 +       \<open>rule allE[where P = P and x = y, OF U]\<close>\<close>\<close>
   6.188 +
   6.189 +lemma "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> P y \<Longrightarrow> Q y"
   6.190 +  apply guess_all
   6.191 +  apply prop_solver
   6.192 +  done
   6.193 +
   6.194 +lemma "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow>  P z \<Longrightarrow> P y \<Longrightarrow> Q y"
   6.195 +  apply (solve \<open>guess_all, prop_solver\<close>)  -- \<open>Try it without solve\<close>
   6.196 +  done
   6.197 +
   6.198 +method guess_ex =
   6.199 +  \<open>match concl in
   6.200 +    "\<exists>x. P (x :: 'a)" for P \<Rightarrow>
   6.201 +      \<open>match prems in "?H (x :: 'a)" for x \<Rightarrow>
   6.202 +              \<open>rule exI[where x=x]\<close>\<close>\<close>
   6.203 +
   6.204 +lemma "P x \<Longrightarrow> \<exists>x. P x"
   6.205 +  apply guess_ex
   6.206 +  apply prop_solver
   6.207 +  done
   6.208 +
   6.209 +method fol_solver =
   6.210 +  \<open>(guess_ex | guess_all | prop_solver) ; solve \<open>fol_solver\<close>\<close>
   6.211 +
   6.212 +declare
   6.213 +  allI [intros]
   6.214 +  exE [elims]
   6.215 +  ex_simps [subst]
   6.216 +  all_simps [subst]
   6.217 +
   6.218 +lemma "(\<forall>x. P x) \<and> (\<forall>x. Q x) \<Longrightarrow> (\<forall>x. P x \<and> Q x)"
   6.219 +  and  "\<exists>x. P x \<longrightarrow> (\<forall>x. P x)"
   6.220 +  and "(\<exists>x. \<forall>y. R x y) \<longrightarrow> (\<forall>y. \<exists>x. R x y)"
   6.221 +  by fol_solver+
   6.222 +
   6.223 +end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Eisbach/Tests.thy	Fri Apr 17 17:49:19 2015 +0200
     7.3 @@ -0,0 +1,272 @@
     7.4 +(*  Title:      Tests.thy
     7.5 +    Author:     Daniel Matichuk, NICTA/UNSW
     7.6 +*)
     7.7 +
     7.8 +section \<open>Miscellaneous Eisbach tests\<close>
     7.9 +
    7.10 +theory Tests
    7.11 +imports Main Eisbach_Tools
    7.12 +begin
    7.13 +
    7.14 +section \<open>Named Theorems Tests\<close>
    7.15 +
    7.16 +named_theorems foo
    7.17 +
    7.18 +method foo declares foo =
    7.19 +  \<open>rule foo\<close>
    7.20 +
    7.21 +lemma
    7.22 +  assumes A [foo]: A
    7.23 +  shows A
    7.24 +  apply foo
    7.25 +  done
    7.26 +
    7.27 +
    7.28 +section \<open>Match Tests\<close>
    7.29 +
    7.30 +notepad
    7.31 +begin
    7.32 +  have dup: "\<And>A. A \<Longrightarrow> A \<Longrightarrow> A" by simp
    7.33 +
    7.34 +  fix A y
    7.35 +  have "(\<And>x. A x) \<Longrightarrow> A y"
    7.36 +    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>)
    7.37 +    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>)
    7.38 +    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>)
    7.39 +    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>)
    7.40 +    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>)
    7.41 +    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>)
    7.42 +    done
    7.43 +
    7.44 +  assume X: "\<And>x. A x" "A y"
    7.45 +  have "A y"
    7.46 +    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>)
    7.47 +    apply (match X in Y:"B ?x" and Y':"B ?x" for B \<Rightarrow> \<open>print_fact Y, print_term B\<close>)
    7.48 +    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>)
    7.49 +    apply (insert X)
    7.50 +    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>)
    7.51 +    apply (match prems in Y:"B ?x" and Y':"B ?x" for B \<Rightarrow> \<open>print_fact Y, print_term B\<close>)
    7.52 +    apply (match prems in Y:"B x" and Y':"B x" for B x \<Rightarrow> \<open>print_fact Y, print_term B\<close>)
    7.53 +    apply (match concl in "P x" and "P y" for P x \<Rightarrow> \<open>print_term P, print_term x\<close>)
    7.54 +    apply assumption
    7.55 +    done
    7.56 +
    7.57 +  (* match focusing retains prems *)
    7.58 +  fix B x
    7.59 +  have "(\<And>x. A x) \<Longrightarrow> (\<And>z. B z) \<Longrightarrow> A y \<Longrightarrow> B x"
    7.60 +    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>)
    7.61 +    done
    7.62 +
    7.63 +  (*Attributes *)
    7.64 +  fix C
    7.65 +  have "(\<And>x :: 'a. A x)  \<Longrightarrow> (\<And>z. B z) \<Longrightarrow> A y \<Longrightarrow> B x \<and> B x \<and> A y"
    7.66 +    apply (intro conjI)
    7.67 +    apply (match prems in Y: "\<And>z :: 'a. A z" and Y'[intro]:"\<And>z :: 'b. B z" \<Rightarrow> \<open>fastforce\<close>)
    7.68 +    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>)
    7.69 +    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>)
    7.70 +    apply assumption
    7.71 +    done
    7.72 +
    7.73 +  fix A B C D
    7.74 +  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"
    7.75 +    apply (match prems in Y[thin]: "\<And>z :: 'a. A ?zz' z" and
    7.76 +                          Y'[thin]: "\<And>rr :: 'b. B ?zz rr" \<Rightarrow>
    7.77 +          \<open>print_fact Y, print_fact Y', intro conjI, rule Y', insert Y', insert Y'[where rr=x]\<close>)
    7.78 +    apply (match prems in Y:"B ?u ?x" \<Rightarrow> \<open>rule Y\<close>)
    7.79 +    apply (insert TrueI)
    7.80 +    apply (match prems in Y'[thin]: "\<And>ff. B uu ff" for uu \<Rightarrow> \<open>insert Y', drule meta_spec[where x=x]\<close>)
    7.81 +    apply assumption
    7.82 +    done
    7.83 +
    7.84 +
    7.85 +  (* Multi-matches. As many facts as match are bound. *)
    7.86 +  fix A B C x
    7.87 +  have "(\<And>x :: 'a. A x) \<Longrightarrow> (\<And>y :: 'a. B y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
    7.88 +    apply (match prems in Y[thin]: "\<And>z :: 'a. ?A z" (multi) \<Rightarrow> \<open>intro conjI, (rule Y)+\<close>)
    7.89 +    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 *)
    7.90 +    apply (match prems in Y: "C y" \<Rightarrow> \<open>rule Y\<close>)
    7.91 +    done
    7.92 +
    7.93 +  fix A B C x
    7.94 +  have "(\<And>x :: 'a. A x) \<Longrightarrow> (\<And>y :: 'a. B y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
    7.95 +    apply (match prems in Y[thin]: "\<And>z. ?A z" (multi) \<Rightarrow> \<open>intro conjI, (rule Y)+\<close>)
    7.96 +    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 *)
    7.97 +    apply (match prems in Y: "C y" \<Rightarrow> \<open>rule Y\<close>)
    7.98 +    done
    7.99 +
   7.100 +
   7.101 +  (*We may use for-fixes in multi-matches too. All bound facts must agree on the fixed term *)
   7.102 +  fix A B C x
   7.103 +  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)"
   7.104 +    apply (match prems in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>intro conjI Y[THEN conjunct1]\<close>)
   7.105 +    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 *)
   7.106 +    apply (match prems in Y: "\<And>x. B x \<and> C x" \<Rightarrow> \<open>intro conjI Y[THEN conjunct1]\<close>)
   7.107 +    apply (match prems in Y: "C ?x" \<Rightarrow> \<open>rule Y\<close>)
   7.108 +    done
   7.109 +
   7.110 +  (* Attributes *)
   7.111 +  fix A B C x
   7.112 +  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)"
   7.113 +    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>)
   7.114 +    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>)
   7.115 +    apply assumption
   7.116 +    done
   7.117 +
   7.118 +(* Removed feature for now *)
   7.119 +(*
   7.120 +  fix A B C x
   7.121 +  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)"
   7.122 +  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>)
   7.123 +  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>)
   7.124 +  done
   7.125 +*)
   7.126 +  (* Testing THEN_ALL_NEW within match *)
   7.127 +  fix A B C x
   7.128 +  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)"
   7.129 +    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>)
   7.130 +    done
   7.131 +
   7.132 +  (* Cut tests *)
   7.133 +  fix A B C
   7.134 +
   7.135 +  have "D \<and> C  \<Longrightarrow> A \<and> B  \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> D \<longrightarrow> True \<Longrightarrow> C"
   7.136 +    by (((match prems in I: "P \<and> Q" (cut)
   7.137 +              and I': "P \<longrightarrow> ?U" for P Q \<Rightarrow> \<open>rule mp [OF I' I[THEN conjunct1]]\<close>)?), simp)
   7.138 +
   7.139 +  have "A \<and> B \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> C"
   7.140 +    by (((match prems in I: "P \<and> Q" (cut)
   7.141 +              and I': "P \<longrightarrow> ?U" for P Q \<Rightarrow> \<open>rule mp [OF I' I[THEN conjunct1]]\<close>)?, simp) | simp)
   7.142 +
   7.143 +end
   7.144 +
   7.145 +(* Testing inner focusing. This fails if we don't smash flex-flex pairs produced
   7.146 +   by retrofitting. This needs to be done more carefully to avoid smashing
   7.147 +   legitimate pairs.*)
   7.148 +
   7.149 +schematic_lemma "?A x \<Longrightarrow> A x"
   7.150 +  apply (match concl in "H" for H \<Rightarrow> \<open>match concl in Y for Y \<Rightarrow> \<open>print_term Y\<close>\<close>)
   7.151 +  apply assumption
   7.152 +  done
   7.153 +
   7.154 +(* Ensure short-circuit after first match failure *)
   7.155 +lemma
   7.156 +  assumes A: "P \<and> Q"
   7.157 +  shows "P"
   7.158 +  by ((match A in "P \<and> Q" \<Rightarrow> \<open>fail\<close> \<bar> "?H" \<Rightarrow> \<open>-\<close>) | simp add: A)
   7.159 +
   7.160 +lemma
   7.161 +  assumes A: "D \<and> C" "A \<and> B" "A \<longrightarrow> B"
   7.162 +  shows "A"
   7.163 +  apply ((match A in U: "P \<and> Q" (cut) and "P' \<longrightarrow> Q'" for P Q P' Q' \<Rightarrow>
   7.164 +      \<open>simp add: U\<close> \<bar> "?H" \<Rightarrow> \<open>-\<close>) | -)
   7.165 +  apply (simp add: A)
   7.166 +  done
   7.167 +
   7.168 +
   7.169 +subsection \<open>Uses Tests\<close>
   7.170 +
   7.171 +ML \<open>
   7.172 +  fun test_internal_fact ctxt factnm =
   7.173 +    (case try (Proof_Context.get_thms ctxt) factnm of
   7.174 +      NONE => ()
   7.175 +    | SOME _ => error "Found internal fact")\<close>
   7.176 +
   7.177 +method uses_test\<^sub>1 uses uses_test\<^sub>1_uses = \<open>rule uses_test\<^sub>1_uses\<close>
   7.178 +
   7.179 +lemma assumes A shows A by (uses_test\<^sub>1 uses_test\<^sub>1_uses: assms)
   7.180 +
   7.181 +ML \<open>test_internal_fact @{context} "uses_test\<^sub>1_uses"\<close>
   7.182 +
   7.183 +ML \<open>test_internal_fact @{context} "Tests.uses_test\<^sub>1_uses"\<close>
   7.184 +ML \<open>test_internal_fact @{context} "Tests.uses_test\<^sub>1.uses_test\<^sub>1_uses"\<close>
   7.185 +
   7.186 +
   7.187 +(* Testing term and fact passing in recursion *)
   7.188 +
   7.189 +method recursion_example for x :: bool uses facts =
   7.190 +  \<open>match (x) in
   7.191 +    "A \<and> B" for A B \<Rightarrow> \<open>(recursion_example A facts: facts, recursion_example B facts: facts)\<close>
   7.192 +  \<bar> "?H" \<Rightarrow> \<open>match facts in U: "x" \<Rightarrow> \<open>insert U\<close>\<close>\<close>
   7.193 +
   7.194 +lemma
   7.195 +  assumes asms: "A" "B" "C" "D"
   7.196 +  shows "(A \<and> B) \<and> (C \<and> D)"
   7.197 +  apply (recursion_example "(A \<and> B) \<and> (C \<and> D)" facts: asms)
   7.198 +  apply simp
   7.199 +  done
   7.200 +
   7.201 +(*Method.sections in existing method*)
   7.202 +method my_simp\<^sub>1 uses my_simp\<^sub>1_facts = \<open>simp add: my_simp\<^sub>1_facts\<close>
   7.203 +lemma assumes A shows A by (my_simp\<^sub>1 my_simp\<^sub>1_facts: assms)
   7.204 +
   7.205 +(*Method.sections via Eisbach argument parser*)
   7.206 +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>
   7.207 +lemma assumes A shows A by (uses_test\<^sub>2 uses_test\<^sub>2_uses: assms)
   7.208 +
   7.209 +
   7.210 +subsection \<open>Declaration Tests\<close>
   7.211 +
   7.212 +named_theorems declare_facts\<^sub>1
   7.213 +
   7.214 +method declares_test\<^sub>1 declares declare_facts\<^sub>1 = \<open>rule declare_facts\<^sub>1\<close>
   7.215 +
   7.216 +lemma assumes A shows A by (declares_test\<^sub>1 declare_facts\<^sub>1: assms)
   7.217 +
   7.218 +lemma assumes A[declare_facts\<^sub>1]: A shows A by declares_test\<^sub>1
   7.219 +
   7.220 +
   7.221 +subsection \<open>Rule Instantiation Tests\<close>
   7.222 +
   7.223 +method my_allE\<^sub>1 for x :: 'a and P :: "'a \<Rightarrow> bool" =
   7.224 +  \<open>erule allE [where x = x and P = P]\<close>
   7.225 +
   7.226 +lemma "\<forall>x. Q x \<Longrightarrow> Q x" by (my_allE\<^sub>1 x Q)
   7.227 +
   7.228 +method my_allE\<^sub>2 for x :: 'a and P :: "'a \<Rightarrow> bool" =
   7.229 +  \<open>erule allE [of P x]\<close>
   7.230 +
   7.231 +lemma "\<forall>x. Q x \<Longrightarrow> Q x" by (my_allE\<^sub>2 x Q)
   7.232 +
   7.233 +method my_allE\<^sub>3 for x :: 'a and P :: "'a \<Rightarrow> bool" =
   7.234 +  \<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>
   7.235 +    \<open>erule X [where x = x and P = P]\<close>\<close>
   7.236 +
   7.237 +lemma "\<forall>x. Q x \<Longrightarrow> Q x" by (my_allE\<^sub>3 x Q)
   7.238 +
   7.239 +method my_allE\<^sub>4 for x :: 'a and P :: "'a \<Rightarrow> bool" =
   7.240 +  \<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>
   7.241 +    \<open>erule X [of x P]\<close>\<close>
   7.242 +
   7.243 +lemma "\<forall>x. Q x \<Longrightarrow> Q x" by (my_allE\<^sub>4 x Q)
   7.244 +
   7.245 +
   7.246 +ML {*
   7.247 +structure Data = Generic_Data
   7.248 +(
   7.249 +  type T = thm list;
   7.250 +  val empty: T = [];
   7.251 +  val extend = I;
   7.252 +  fun merge data : T = Thm.merge_thms data;
   7.253 +);
   7.254 +*}
   7.255 +
   7.256 +local_setup \<open>Local_Theory.add_thms_dynamic (@{binding test_dyn}, Data.get)\<close>
   7.257 +
   7.258 +setup \<open>Context.theory_map (Data.put @{thms TrueI})\<close>
   7.259 +
   7.260 +method dynamic_thms_test = \<open>rule test_dyn\<close>
   7.261 +
   7.262 +locale foo =
   7.263 +  fixes A
   7.264 +  assumes A : "A"
   7.265 +begin
   7.266 +
   7.267 +local_setup
   7.268 +  \<open>Local_Theory.declaration {pervasive = false, syntax = false}
   7.269 +    (fn phi => Data.put (Morphism.fact phi @{thms A}))\<close>
   7.270 +
   7.271 +lemma A by dynamic_thms_test
   7.272 +
   7.273 +end
   7.274 +
   7.275 +end
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Eisbach/eisbach_antiquotations.ML	Fri Apr 17 17:49:19 2015 +0200
     8.3 @@ -0,0 +1,54 @@
     8.4 +(*  Title:      eisbach_antiquotations.ML
     8.5 +    Author:     Daniel Matichuk, NICTA/UNSW
     8.6 +
     8.7 +ML antiquotations for Eisbach.
     8.8 +*)
     8.9 +
    8.10 +structure Eisbach_Antiquotations: sig end =
    8.11 +struct
    8.12 +
    8.13 +(** evaluate Eisbach method from ML **)
    8.14 +
    8.15 +val _ =
    8.16 +  Theory.setup
    8.17 +    (ML_Antiquotation.inline @{binding method}  (* FIXME ML_Antiquotation.value (!?) *)
    8.18 +      (Args.context -- Scan.lift (Args.mode "drop_cases") -- Scan.lift (Parse.position Parse.name)
    8.19 +        >> (fn ((ctxt, drop_cases), nameref) =>
    8.20 +          let
    8.21 +            val ((targs, (factargs, margs)), _) = Method_Closure.get_inner_method ctxt nameref;
    8.22 +
    8.23 +            val has_factargs = not (null factargs);
    8.24 +
    8.25 +            val (targnms, ctxt') =
    8.26 +              fold_map (fn (Var ((x, _), _)) => ML_Context.variant x) targs ctxt;
    8.27 +            val (margnms, ctxt'') = fold_map ML_Context.variant margs ctxt';
    8.28 +            val (factsnm, _) = ML_Context.variant "facts" ctxt'';
    8.29 +
    8.30 +            val fn_header =
    8.31 +              margnms
    8.32 +              |> has_factargs ? append [factsnm]
    8.33 +              |> append targnms
    8.34 +              |> map (fn nm => "fn " ^ nm ^ " => ")
    8.35 +              |> implode;
    8.36 +
    8.37 +            val ML_context = ML_Context.struct_name ctxt ^ ".ML_context";
    8.38 +            val ml_inner =
    8.39 +              ML_Syntax.atomic
    8.40 +                ("Method_Closure.get_inner_method " ^  ML_context ^
    8.41 +                  ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position nameref ^
    8.42 +                  "|> (fn ((targs, (_, margs)), text) => Method_Closure.eval_inner_method " ^
    8.43 +                  ML_context ^ " ((targs, margs), text))");
    8.44 +
    8.45 +            val drop_cases_suffix =
    8.46 +              if drop_cases then "#> (fn f => (fn ctxt => fn thms => f ctxt thms |> Seq.map snd))"
    8.47 +              else "";
    8.48 +
    8.49 +            val factsnm = if has_factargs then factsnm else "[]";
    8.50 +          in
    8.51 +            ML_Syntax.atomic
    8.52 +              (fn_header ^ ml_inner ^ " " ^ ML_Syntax.print_list I targnms ^ " " ^
    8.53 +                factsnm ^ " " ^
    8.54 +                ML_Syntax.print_list I margnms ^ drop_cases_suffix)
    8.55 +          end)));
    8.56 +
    8.57 +end;
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Eisbach/eisbach_rule_insts.ML	Fri Apr 17 17:49:19 2015 +0200
     9.3 @@ -0,0 +1,189 @@
     9.4 +(*  Title:      eisbach_rule_insts.ML
     9.5 +    Author:     Daniel Matichuk, NICTA/UNSW
     9.6 +
     9.7 +Eisbach-aware variants of the "where" and "of" attributes.
     9.8 +
     9.9 +Alternate syntax for rule_insts.ML participates in token closures by
    9.10 +examining the behaviour of Rule_Insts.where_rule and instantiating token
    9.11 +values accordingly. Instantiations in re-interpretation are done with
    9.12 +Drule.cterm_instantiate.
    9.13 +*)
    9.14 +
    9.15 +structure Eisbach_Rule_Insts : sig end =
    9.16 +struct
    9.17 +
    9.18 +fun restore_tags thm = Thm.map_tags (K (Thm.get_tags thm));
    9.19 +
    9.20 +fun add_thm_insts thm =
    9.21 +  let
    9.22 +    val thy = Thm.theory_of_thm thm;
    9.23 +    val tyvars = Thm.fold_terms Term.add_tvars thm [];
    9.24 +    val tyvars' = tyvars |> map (Logic.mk_term o Logic.mk_type o TVar);
    9.25 +
    9.26 +    val tvars = Thm.fold_terms Term.add_vars thm [];
    9.27 +    val tvars' = tvars  |> map (Logic.mk_term o Var);
    9.28 +
    9.29 +    val conj =
    9.30 +      Logic.mk_conjunction_list (tyvars' @ tvars') |> Thm.global_cterm_of thy |> Drule.mk_term;
    9.31 +  in
    9.32 +    ((tyvars, tvars), Conjunction.intr thm conj)
    9.33 +  end;
    9.34 +
    9.35 +fun get_thm_insts thm =
    9.36 +  let
    9.37 +    val (thm', insts) = Conjunction.elim thm;
    9.38 +
    9.39 +    val insts' = insts
    9.40 +      |> Drule.dest_term
    9.41 +      |> Thm.term_of
    9.42 +      |> Logic.dest_conjunction_list
    9.43 +      |> map Logic.dest_term
    9.44 +      |> (fn f => fold (fn t => fn (tys, ts) =>
    9.45 +          (case try Logic.dest_type t of
    9.46 +            SOME T => (T :: tys, ts)
    9.47 +          | NONE => (tys, t :: ts))) f ([], []))
    9.48 +      ||> rev
    9.49 +      |>> rev;
    9.50 +  in
    9.51 +    (thm', insts')
    9.52 +  end;
    9.53 +
    9.54 +fun instantiate_xis insts thm =
    9.55 +  let
    9.56 +    val tyvars = Thm.fold_terms Term.add_tvars thm [];
    9.57 +    val tvars = Thm.fold_terms Term.add_vars thm [];
    9.58 +    val cert = Thm.global_cterm_of (Thm.theory_of_thm thm);
    9.59 +    val certT = Thm.global_ctyp_of (Thm.theory_of_thm thm);
    9.60 +
    9.61 +    fun add_inst (xi, t) (Ts, ts) =
    9.62 +      (case AList.lookup (op =) tyvars xi of
    9.63 +        SOME S => ((certT (TVar (xi, S)), certT (Logic.dest_type t)) :: Ts, ts)
    9.64 +      | NONE =>
    9.65 +          (case AList.lookup (op =) tvars xi of
    9.66 +            SOME T => (Ts, (cert (Var (xi, T)), cert t) :: ts)
    9.67 +          | NONE => error "indexname not found in thm"));
    9.68 +
    9.69 +    val (cTinsts, cinsts) = fold add_inst insts ([], []);
    9.70 +  in
    9.71 +    (Thm.instantiate (cTinsts, []) thm
    9.72 +    |> Drule.cterm_instantiate cinsts
    9.73 +    COMP_INCR asm_rl)
    9.74 +    |> Thm.adjust_maxidx_thm ~1
    9.75 +    |> restore_tags thm
    9.76 +  end;
    9.77 +
    9.78 +
    9.79 +datatype rule_inst =
    9.80 +  Named_Insts of ((indexname * string) * (term -> unit)) list
    9.81 +| Term_Insts of (indexname * term) list;
    9.82 +
    9.83 +fun embed_indexname ((xi,s),f) =
    9.84 +  let
    9.85 +    fun wrap_xi xi t = Logic.mk_conjunction (Logic.mk_term (Var (xi,fastype_of t)),Logic.mk_term t);
    9.86 +  in ((xi,s),f o wrap_xi xi) end;
    9.87 +
    9.88 +fun unembed_indexname t =
    9.89 +  let
    9.90 +    val (t, t') = apply2 Logic.dest_term (Logic.dest_conjunction t);
    9.91 +    val (xi, _) = Term.dest_Var t;
    9.92 +  in (xi, t') end;
    9.93 +
    9.94 +fun read_where_insts toks =
    9.95 +  let
    9.96 +    val parser =
    9.97 +      Parse.!!!
    9.98 +        (Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse_Tools.name_term)) -- Parse.for_fixes)
    9.99 +          --| Scan.ahead Parse.eof;
   9.100 +    val (insts, fixes) = the (Scan.read Token.stopper parser toks);
   9.101 +
   9.102 +    val insts' =
   9.103 +      if forall (fn (_, v) => Parse_Tools.is_real_val v) insts
   9.104 +      then Term_Insts (map (fn (_,t) => unembed_indexname (Parse_Tools.the_real_val t)) insts)
   9.105 +      else Named_Insts (map (fn (xi, p) => embed_indexname
   9.106 +            ((xi,Parse_Tools.the_parse_val p),Parse_Tools.the_parse_fun p)) insts);
   9.107 +  in
   9.108 +    (insts', fixes)
   9.109 +  end;
   9.110 +
   9.111 +fun of_rule thm  (args, concl_args) =
   9.112 +  let
   9.113 +    fun zip_vars _ [] = []
   9.114 +      | zip_vars (_ :: xs) (NONE :: rest) = zip_vars xs rest
   9.115 +      | zip_vars ((x, _) :: xs) (SOME t :: rest) = (x, t) :: zip_vars xs rest
   9.116 +      | zip_vars [] _ = error "More instantiations than variables in theorem";
   9.117 +    val insts =
   9.118 +      zip_vars (rev (Term.add_vars (Thm.full_prop_of thm) [])) args @
   9.119 +      zip_vars (rev (Term.add_vars (Thm.concl_of thm) [])) concl_args;
   9.120 +  in insts end;
   9.121 +
   9.122 +val inst =  Args.maybe Parse_Tools.name_term;
   9.123 +val concl = Args.$$$ "concl" -- Args.colon;
   9.124 +
   9.125 +fun read_of_insts toks thm =
   9.126 +  let
   9.127 +    val parser =
   9.128 +      Parse.!!!
   9.129 +        ((Scan.repeat (Scan.unless concl inst) -- Scan.optional (concl |-- Scan.repeat inst) [])
   9.130 +          -- Parse.for_fixes) --| Scan.ahead Parse.eof;
   9.131 +    val ((insts, concl_insts), fixes) =
   9.132 +      the (Scan.read Token.stopper parser toks);
   9.133 +
   9.134 +    val insts' =
   9.135 +      if forall (fn SOME t => Parse_Tools.is_real_val t | NONE => true) (insts @ concl_insts)
   9.136 +      then
   9.137 +        Term_Insts
   9.138 +          (map_filter (Option.map (Parse_Tools.the_real_val #> unembed_indexname)) (insts @ concl_insts))
   9.139 +
   9.140 +      else
   9.141 +        Named_Insts
   9.142 +          (apply2 (map (Option.map (fn p => (Parse_Tools.the_parse_val p,Parse_Tools.the_parse_fun p))))
   9.143 +            (insts, concl_insts)
   9.144 +            |> of_rule thm |> map ((fn (xi, (nm, tok)) => embed_indexname ((xi, nm), tok))));
   9.145 +  in
   9.146 +    (insts', fixes)
   9.147 +  end;
   9.148 +
   9.149 +fun read_instantiate_closed ctxt ((Named_Insts insts), fixes) thm  =
   9.150 +      let
   9.151 +        val insts' = map (fn ((v, t), _) => ((v, Position.none), t)) insts;
   9.152 +
   9.153 +        val (thm_insts, thm') = add_thm_insts thm
   9.154 +        val (thm'', thm_insts') =
   9.155 +          Rule_Insts.where_rule ctxt insts' fixes thm'
   9.156 +          |> get_thm_insts;
   9.157 +
   9.158 +        val tyinst =
   9.159 +          ListPair.zip (fst thm_insts, fst thm_insts') |> map (fn ((xi, _), typ) => (xi, typ));
   9.160 +        val tinst =
   9.161 +          ListPair.zip (snd thm_insts, snd thm_insts') |> map (fn ((xi, _), t) => (xi, t));
   9.162 +
   9.163 +        val _ =
   9.164 +          map (fn ((xi, _), f) =>
   9.165 +            (case AList.lookup (op =) tyinst xi of
   9.166 +              SOME typ => f (Logic.mk_type typ)
   9.167 +            | NONE =>
   9.168 +                (case AList.lookup (op =) tinst xi of
   9.169 +                  SOME t => f t
   9.170 +                | NONE => error "Lost indexname in instantiated theorem"))) insts;
   9.171 +      in
   9.172 +        (thm'' |> restore_tags thm)
   9.173 +      end
   9.174 +  | read_instantiate_closed _ ((Term_Insts insts), _) thm = instantiate_xis insts thm;
   9.175 +
   9.176 +val parse_all : Token.T list context_parser = Scan.lift (Scan.many Token.not_eof);
   9.177 +
   9.178 +val _ =
   9.179 +  Theory.setup
   9.180 +    (Attrib.setup @{binding "where"} (parse_all >>
   9.181 +      (fn toks => Thm.rule_attribute (fn context =>
   9.182 +        read_instantiate_closed (Context.proof_of context) (read_where_insts toks))))
   9.183 +      "named instantiation of theorem");
   9.184 +
   9.185 +val _ =
   9.186 +  Theory.setup
   9.187 +    (Attrib.setup @{binding "of"} (parse_all >>
   9.188 +      (fn toks => Thm.rule_attribute (fn context => fn thm =>
   9.189 +        read_instantiate_closed (Context.proof_of context) (read_of_insts toks thm) thm)))
   9.190 +      "positional instantiation of theorem");
   9.191 +
   9.192 +end;
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Eisbach/match_method.ML	Fri Apr 17 17:49:19 2015 +0200
    10.3 @@ -0,0 +1,619 @@
    10.4 +(*  Title:      match_method.ML
    10.5 +    Author:     Daniel Matichuk, NICTA/UNSW
    10.6 +
    10.7 +Setup for "match" proof method. It provides basic fact/term matching in
    10.8 +addition to premise/conclusion matching through Subgoal.focus, and binds
    10.9 +fact names from matches as well as term patterns within matches.
   10.10 +*)
   10.11 +
   10.12 +signature MATCH_METHOD =
   10.13 +sig
   10.14 +  val focus_schematics: Proof.context -> Envir.tenv
   10.15 +  val focus_params: Proof.context -> term list
   10.16 +  (* FIXME proper ML interface for the main thing *)
   10.17 +end
   10.18 +
   10.19 +structure Match_Method : MATCH_METHOD =
   10.20 +struct
   10.21 +
   10.22 +(*Variant of filter_prems_tac with auxiliary configuration;
   10.23 +  recovers premise order afterwards.*)
   10.24 +fun filter_prems_tac' ctxt prep pred a =
   10.25 +  let
   10.26 +    fun Then NONE tac = SOME tac
   10.27 +      | Then (SOME tac) tac' = SOME (tac THEN' tac');
   10.28 +    fun thins H (tac, n, a, i) =
   10.29 +      (case pred a H of
   10.30 +        NONE => (tac, n + 1, a, i)
   10.31 +      | SOME a' => (Then tac (rotate_tac n THEN' eresolve_tac ctxt [thin_rl]), 0, a', i + n));
   10.32 +  in
   10.33 +    SUBGOAL (fn (goal, i) =>
   10.34 +      let val Hs = Logic.strip_assums_hyp (prep goal) in
   10.35 +        (case fold thins Hs (NONE, 0, a, 0) of
   10.36 +          (NONE, _, _, _) => no_tac
   10.37 +        | (SOME tac, _, _, n) => tac i THEN rotate_tac (~ n) i)
   10.38 +      end)
   10.39 +  end;
   10.40 +
   10.41 +
   10.42 +datatype match_kind =
   10.43 +    Match_Term of term Item_Net.T
   10.44 +  | Match_Fact of thm Item_Net.T
   10.45 +  | Match_Concl
   10.46 +  | Match_Prems;
   10.47 +
   10.48 +
   10.49 +val aconv_net = Item_Net.init (op aconv) single;
   10.50 +
   10.51 +val parse_match_kind =
   10.52 +  Scan.lift @{keyword "concl"} >> K Match_Concl ||
   10.53 +  Scan.lift @{keyword "prems"} >> K Match_Prems ||
   10.54 +  Scan.lift (@{keyword "("}) |-- Args.term --| Scan.lift (@{keyword ")"}) >>
   10.55 +    (fn t => Match_Term (Item_Net.update t aconv_net)) ||
   10.56 +  Attrib.thms >> (fn thms => Match_Fact (fold Item_Net.update thms Thm.full_rules));
   10.57 +
   10.58 +
   10.59 +fun nameable_match m = (case m of Match_Fact _ => true | Match_Prems => true | _ => false);
   10.60 +fun prop_match m = (case m of Match_Term _ => false | _ => true);
   10.61 +
   10.62 +val bound_term : (term, binding) Parse_Tools.parse_val parser =
   10.63 +  Parse_Tools.parse_term_val Parse.binding;
   10.64 +
   10.65 +val fixes =
   10.66 +  Parse.and_list1 (Scan.repeat1 bound_term --
   10.67 +    Scan.option (@{keyword "::"} |-- Parse.!!! Parse.typ) >> (fn (xs, T) => map (rpair T) xs))
   10.68 +  >> flat;
   10.69 +
   10.70 +val for_fixes = Scan.optional (@{keyword "for"} |-- fixes) [];
   10.71 +
   10.72 +fun pos_of dyn =
   10.73 +  (case dyn of
   10.74 +    Parse_Tools.Parse_Val (b, _) => Binding.pos_of b
   10.75 +  | _ => raise Fail "Not a parse value");
   10.76 +
   10.77 +
   10.78 +(*FIXME: Dynamic facts modify the background theory, so we have to resort
   10.79 +  to token replacement for matched facts. *)
   10.80 +fun dynamic_fact ctxt =
   10.81 +  bound_term -- Args.opt_attribs (Attrib.check_name ctxt);
   10.82 +
   10.83 +type match_args = {unify : bool, multi : bool, cut : bool};
   10.84 +
   10.85 +val parse_match_args =
   10.86 +  Scan.optional (Args.parens (Parse.enum1 ","
   10.87 +    (Args.$$$ "unify" || Args.$$$ "multi" || Args.$$$ "cut"))) [] >>
   10.88 +    (fn ss =>
   10.89 +      fold (fn s => fn {unify, multi, cut} =>
   10.90 +        (case s of
   10.91 +          "unify" => {unify = true, multi = multi, cut = cut}
   10.92 +        | "multi" => {unify = unify, multi = true, cut = cut}
   10.93 +        | "cut" => {unify = unify, multi = multi, cut = true}))
   10.94 +      ss {unify = false, multi = false, cut = false});
   10.95 +
   10.96 +(*TODO: Shape holes in thms *)
   10.97 +fun parse_named_pats match_kind =
   10.98 +  Args.context :|-- (fn ctxt =>
   10.99 +    Scan.lift (Parse.and_list1 (Scan.option (dynamic_fact ctxt --| Args.colon) :--
  10.100 +      (fn opt_dyn =>
  10.101 +        if is_none opt_dyn orelse nameable_match match_kind
  10.102 +        then Parse_Tools.name_term -- parse_match_args
  10.103 +        else
  10.104 +          let val b = #1 (the opt_dyn)
  10.105 +          in error ("Cannot bind fact name in term match" ^ Position.here (pos_of b)) end))
  10.106 +    -- for_fixes -- (@{keyword "\<Rightarrow>"} |-- Parse.token Parse.cartouche))
  10.107 +  >> (fn ((ts, fixes), cartouche) =>
  10.108 +    (case Token.get_value cartouche of
  10.109 +      SOME (Token.Source src) =>
  10.110 +        let
  10.111 +          val text = Method_Closure.read_inner_method ctxt src
  10.112 +          (*TODO: Correct parse context for attributes?*)
  10.113 +          val ts' =
  10.114 +            map
  10.115 +              (fn (b, (Parse_Tools.Real_Val v, match_args)) =>
  10.116 +                ((Option.map (fn (b, att) =>
  10.117 +                  (Parse_Tools.the_real_val b,
  10.118 +                    map (Attrib.attribute ctxt) att)) b, match_args), v)
  10.119 +                | _ => raise Fail "Expected closed term") ts
  10.120 +          val fixes' = map (fn (p, _) => Parse_Tools.the_real_val p) fixes
  10.121 +        in (ts', fixes', text) end
  10.122 +    | SOME _ => error "Unexpected token value in match cartouche"
  10.123 +    | NONE =>
  10.124 +        let
  10.125 +          val fixes' = map (fn (pb, otyp) => (Parse_Tools.the_parse_val pb, otyp, NoSyn)) fixes;
  10.126 +          val (fixes'', ctxt1) = Proof_Context.read_vars fixes' ctxt;
  10.127 +          val (fix_nms, ctxt2) = Proof_Context.add_fixes fixes'' ctxt1;
  10.128 +
  10.129 +          val ctxt3 = Proof_Context.set_mode Proof_Context.mode_schematic ctxt2;
  10.130 +
  10.131 +          fun parse_term term =
  10.132 +            if prop_match match_kind
  10.133 +            then Syntax.parse_prop ctxt3 term
  10.134 +            else Syntax.parse_term ctxt3 term;
  10.135 +
  10.136 +          val pats =
  10.137 +            map (fn (_, (term, _)) => parse_term (Parse_Tools.the_parse_val term)) ts
  10.138 +            |> Syntax.check_terms ctxt3;
  10.139 +
  10.140 +          val ctxt4 = fold Variable.declare_term pats ctxt3;
  10.141 +
  10.142 +          val (Ts, ctxt5) = ctxt4 |> fold_map Proof_Context.inferred_param fix_nms;
  10.143 +
  10.144 +          val real_fixes = map Free (fix_nms ~~ Ts);
  10.145 +
  10.146 +          fun reject_extra_free (Free (x, _)) () =
  10.147 +                if Variable.is_fixed ctxt5 x then ()
  10.148 +                else error ("Illegal use of free (unfixed) variable " ^ quote x)
  10.149 +            | reject_extra_free _ () = ();
  10.150 +          val _ = (fold o fold_aterms) reject_extra_free pats ();
  10.151 +
  10.152 +          (*fun test_multi_bind {multi = multi, ...} pat = multi andalso
  10.153 +           not (null (inter (op =) (map Free (Term.add_frees pat [])) real_fixes)) andalso
  10.154 +           error "Cannot fix terms in multi-match. Use a schematic instead."
  10.155 +
  10.156 +          val _ = map2 (fn pat => fn (_, (_, match_args)) => test_multi_bind match_args pat) pats ts*)
  10.157 +
  10.158 +          val binds =
  10.159 +            map (fn (b, _) => Option.map (fn (b, att) => (Parse_Tools.the_parse_val b, att)) b) ts;
  10.160 +
  10.161 +          fun upd_ctxt (SOME (b, att)) pat (tms, ctxt) =
  10.162 +                let
  10.163 +                  val ([nm], ctxt') =
  10.164 +                    Variable.variant_fixes [Name.internal (Binding.name_of b)] ctxt;
  10.165 +                  val abs_nms = Term.strip_all_vars pat;
  10.166 +
  10.167 +                  val param_thm = map (Drule.mk_term o Thm.cterm_of ctxt' o Free) abs_nms
  10.168 +                    |> Conjunction.intr_balanced
  10.169 +                    |> Drule.generalize ([], map fst abs_nms);
  10.170 +
  10.171 +                  val thm =
  10.172 +                    Thm.cterm_of ctxt' (Free (nm, propT))
  10.173 +                    |> Drule.mk_term
  10.174 +                    |> not (null abs_nms) ? Conjunction.intr param_thm
  10.175 +                    |> Drule.zero_var_indexes
  10.176 +                    |> Method_Closure.tag_free_thm;
  10.177 +
  10.178 +                  (*TODO: Preprocess attributes here?*)
  10.179 +
  10.180 +                  val (_, ctxt'') = Proof_Context.note_thmss "" [((b, []), [([thm], [])])] ctxt';
  10.181 +                in
  10.182 +                  (SOME (Thm.prop_of thm, map (Attrib.attribute ctxt) att) :: tms, ctxt'')
  10.183 +                end
  10.184 +            | upd_ctxt NONE _ (tms, ctxt) = (NONE :: tms, ctxt);
  10.185 +
  10.186 +          val (binds, ctxt6) = ctxt5
  10.187 +            |> (fn ctxt => fold2 upd_ctxt binds pats ([], ctxt) |> apfst rev)
  10.188 +            ||> Proof_Context.restore_mode ctxt;
  10.189 +
  10.190 +          val (src, text) = Method_Closure.read_text_closure ctxt6 (Token.input_of cartouche);
  10.191 +
  10.192 +          val morphism =
  10.193 +            Variable.export_morphism ctxt6
  10.194 +              (ctxt
  10.195 +                |> Token.declare_maxidx_src src
  10.196 +                |> Variable.declare_maxidx (Variable.maxidx_of ctxt6));
  10.197 +
  10.198 +          val pats' = map (Term.map_types Type_Infer.paramify_vars #> Morphism.term morphism) pats;
  10.199 +          val _ = ListPair.app (fn ((_, (Parse_Tools.Parse_Val (_, f), _)), t) => f t) (ts, pats');
  10.200 +
  10.201 +          val binds' = map (Option.map (fn (t, atts) => (Morphism.term morphism t, atts))) binds;
  10.202 +
  10.203 +          val _ =
  10.204 +            ListPair.app
  10.205 +              (fn ((SOME ((Parse_Tools.Parse_Val (_, f), _)), _), SOME (t, _)) => f t
  10.206 +                | ((NONE, _), NONE) => ()
  10.207 +                | _ => error "Mismatch between real and parsed bound variables")
  10.208 +              (ts, binds');
  10.209 +
  10.210 +          val real_fixes' = map (Morphism.term morphism) real_fixes;
  10.211 +          val _ =
  10.212 +            ListPair.app (fn ((Parse_Tools.Parse_Val (_, f), _), t) => f t) (fixes, real_fixes');
  10.213 +
  10.214 +          val match_args = map (fn (_, (_, match_args)) => match_args) ts;
  10.215 +          val binds'' = (binds' ~~ match_args) ~~ pats';
  10.216 +
  10.217 +          val src' = Token.transform_src morphism src;
  10.218 +          val _ = Token.assign (SOME (Token.Source src')) cartouche;
  10.219 +        in
  10.220 +          (binds'', real_fixes', text)
  10.221 +        end)));
  10.222 +
  10.223 +
  10.224 +fun parse_match_bodies match_kind =
  10.225 +  Parse.enum1' "\<bar>" (parse_named_pats match_kind);
  10.226 +
  10.227 +
  10.228 +fun dest_internal_fact t =
  10.229 +  (case try Logic.dest_conjunction t of
  10.230 +    SOME (params, head) =>
  10.231 +     (params |> Logic.dest_conjunctions |> map Logic.dest_term,
  10.232 +      head |> Logic.dest_term)
  10.233 +  | NONE => ([], t |> Logic.dest_term));
  10.234 +
  10.235 +
  10.236 +fun inst_thm ctxt env ts params thm =
  10.237 +  let
  10.238 +    val ts' = map (Envir.norm_term env) ts;
  10.239 +    val insts = map (Thm.cterm_of ctxt) ts' ~~ map (Thm.cterm_of ctxt) params;
  10.240 +    val tags = Thm.get_tags thm;
  10.241 +
  10.242 +   (*
  10.243 +    val Tinsts = Type.raw_matches ((map (fastype_of) params), (map (fastype_of) ts')) Vartab.empty
  10.244 +    |> Vartab.dest
  10.245 +    |> map (fn (xi, (S, typ)) => (certT (TVar (xi, S)), certT typ))
  10.246 +   *)
  10.247 +
  10.248 +    val thm' = Drule.cterm_instantiate insts thm
  10.249 +    (*|> Thm.instantiate (Tinsts, [])*)
  10.250 +      |> Thm.map_tags (K tags);
  10.251 +  in
  10.252 +    thm'
  10.253 +  end;
  10.254 +
  10.255 +fun do_inst fact_insts' env text ctxt =
  10.256 +  let
  10.257 +    val fact_insts =
  10.258 +      map_filter
  10.259 +        (fn ((((SOME ((_, head), att), _), _), _), thms) => SOME (head, (thms, att))
  10.260 +          | _ => NONE) fact_insts';
  10.261 +
  10.262 +    fun apply_attribute thm att ctxt =
  10.263 +      let
  10.264 +        val (opt_context', thm') = att (Context.Proof ctxt, thm)
  10.265 +      in
  10.266 +        (case thm' of
  10.267 +          SOME _ => error "Rule attributes cannot be applied here"
  10.268 +        | _ => the_default ctxt (Option.map Context.proof_of opt_context'))
  10.269 +      end;
  10.270 +
  10.271 +    fun apply_attributes atts thm = fold (apply_attribute thm) atts;
  10.272 +
  10.273 +     (*TODO: What to do about attributes that raise errors?*)
  10.274 +    val (fact_insts, ctxt') =
  10.275 +      fold_map (fn (head, (thms, atts : attribute list)) => fn ctxt =>
  10.276 +        ((head, thms), fold (apply_attributes atts) thms ctxt)) fact_insts ctxt;
  10.277 +
  10.278 +    fun try_dest_term thm = try (Thm.prop_of #> dest_internal_fact #> snd) thm;
  10.279 +
  10.280 +    fun expand_fact thm =
  10.281 +      the_default [thm]
  10.282 +        (case try_dest_term thm of
  10.283 +          SOME t_ident => AList.lookup (op aconv) fact_insts t_ident
  10.284 +        | NONE => NONE);
  10.285 +
  10.286 +    val morphism =
  10.287 +      Morphism.term_morphism "do_inst.term" (Envir.norm_term env) $>
  10.288 +      Morphism.fact_morphism "do_inst.fact" (maps expand_fact);
  10.289 +
  10.290 +    val text' = Method.map_source (Token.transform_src morphism) text;
  10.291 +  in
  10.292 +    (text', ctxt')
  10.293 +  end;
  10.294 +
  10.295 +fun DROP_CASES (tac: cases_tactic) : tactic =
  10.296 +  tac #> Seq.map (fn (_, st) => st);
  10.297 +
  10.298 +fun prep_fact_pat ((x, args), pat) ctxt =
  10.299 +  let
  10.300 +    val ((params, pat'), ctxt') = Variable.focus pat ctxt;
  10.301 +    val params' = map (Free o snd) params;
  10.302 +
  10.303 +    val morphism =
  10.304 +      Variable.export_morphism ctxt'
  10.305 +        (ctxt |> Variable.declare_maxidx (Variable.maxidx_of ctxt'));
  10.306 +    val pat'' :: params'' = map (Morphism.term morphism) (pat' :: params');
  10.307 +
  10.308 +    fun prep_head (t, att) = (dest_internal_fact t, att);
  10.309 +  in
  10.310 +    ((((Option.map prep_head x, args), params''), pat''), ctxt')
  10.311 +  end;
  10.312 +
  10.313 +fun match_filter_env ctxt fixes (ts, params) thm env =
  10.314 +  let
  10.315 +    val param_vars = map Term.dest_Var params;
  10.316 +    val params' = map (Envir.lookup env) param_vars;
  10.317 +
  10.318 +    val fixes_vars = map Term.dest_Var fixes;
  10.319 +
  10.320 +    val tenv = Envir.term_env env;
  10.321 +    val all_vars = Vartab.keys tenv;
  10.322 +
  10.323 +    val extra_vars = subtract (fn ((xi, _), xi') => xi = xi') fixes_vars all_vars;
  10.324 +
  10.325 +    val tenv' = Envir.term_env env
  10.326 +      |> fold (Vartab.delete_safe) extra_vars;
  10.327 +
  10.328 +    val env' =
  10.329 +      Envir.Envir {maxidx = Envir.maxidx_of env, tenv = tenv', tyenv = Envir.type_env env};
  10.330 +
  10.331 +    val all_params_bound = forall (fn SOME (Var _) => true | _ => false) params';
  10.332 +  in
  10.333 +    if all_params_bound
  10.334 +    then SOME (case ts of SOME ts => inst_thm ctxt env params ts thm | _ => thm, env')
  10.335 +    else NONE
  10.336 +  end;
  10.337 +
  10.338 +
  10.339 +(* Slightly hacky way of uniquely identifying focus premises *)
  10.340 +val prem_idN = "premise_id";
  10.341 +
  10.342 +fun prem_id_eq ((id, _ : thm), (id', _ : thm)) = id = id';
  10.343 +
  10.344 +val prem_rules : (int * thm) Item_Net.T =
  10.345 +   Item_Net.init prem_id_eq (single o Thm.full_prop_of o snd);
  10.346 +
  10.347 +fun raw_thm_to_id thm =
  10.348 +  (case Properties.get (Thm.get_tags thm) prem_idN of NONE => NONE | SOME id => Int.fromString id)
  10.349 +  |> the_default ~1;
  10.350 +
  10.351 +structure Focus_Data = Proof_Data
  10.352 +(
  10.353 +  type T =
  10.354 +    (int * (int * thm) Item_Net.T) *  (*prems*)
  10.355 +    Envir.tenv *  (*schematics*)
  10.356 +    term list  (*params*)
  10.357 +  fun init _ : T = ((0, prem_rules), Vartab.empty, [])
  10.358 +);
  10.359 +
  10.360 +
  10.361 +(* focus prems *)
  10.362 +
  10.363 +val focus_prems = #1 o Focus_Data.get;
  10.364 +
  10.365 +fun add_focus_prem prem =
  10.366 +  (Focus_Data.map o @{apply 3(1)}) (fn (next, net) =>
  10.367 +    (next + 1, Item_Net.update (next, Thm.tag_rule (prem_idN, string_of_int next) prem) net));
  10.368 +
  10.369 +fun remove_focus_prem thm =
  10.370 +  (Focus_Data.map o @{apply 3(1)} o apsnd)
  10.371 +    (Item_Net.remove (raw_thm_to_id thm, thm));
  10.372 +
  10.373 +(*TODO: Preliminary analysis to see if we're trying to clear in a non-focus match?*)
  10.374 +val _ =
  10.375 +  Theory.setup
  10.376 +    (Attrib.setup @{binding "thin"}
  10.377 +      (Scan.succeed
  10.378 +        (Thm.declaration_attribute (fn th => Context.mapping I (remove_focus_prem th))))
  10.379 +        "clear premise inside match method");
  10.380 +
  10.381 +
  10.382 +(* focus schematics *)
  10.383 +
  10.384 +val focus_schematics = #2 o Focus_Data.get;
  10.385 +
  10.386 +fun add_focus_schematics cterms =
  10.387 +  (Focus_Data.map o @{apply 3(2)})
  10.388 +    (fold (fn (Var (xi, T), t) => Vartab.update_new (xi, (T, t)))
  10.389 +      (map (apply2 Thm.term_of) cterms));
  10.390 +
  10.391 +
  10.392 +(* focus params *)
  10.393 +
  10.394 +val focus_params = #3 o Focus_Data.get;
  10.395 +
  10.396 +fun add_focus_params params =
  10.397 +  (Focus_Data.map o @{apply 3(3)})
  10.398 +    (append (map (fn (_, ct) => Thm.term_of ct) params));
  10.399 +
  10.400 +
  10.401 +(* Add focus elements as proof data *)
  10.402 +fun augment_focus
  10.403 +    ({context, params, prems, asms, concl, schematics} : Subgoal.focus) : Subgoal.focus =
  10.404 +  let
  10.405 +    val context' = context
  10.406 +      |> add_focus_params params
  10.407 +      |> add_focus_schematics (snd schematics)
  10.408 +      |> fold add_focus_prem (rev prems);
  10.409 +  in
  10.410 +    {context = context',
  10.411 +     params = params,
  10.412 +     prems = prems,
  10.413 +     concl = concl,
  10.414 +     schematics = schematics,
  10.415 +     asms = asms}
  10.416 +  end;
  10.417 +
  10.418 +
  10.419 +(* Fix schematics in the goal *)
  10.420 +fun focus_concl ctxt i goal =
  10.421 +  let
  10.422 +    val ({context, concl, params, prems, asms, schematics}, goal') =
  10.423 +      Subgoal.focus_params ctxt i goal;
  10.424 +
  10.425 +    val ((_, schematic_terms), context') =
  10.426 +      Variable.import_inst true [Thm.term_of concl] context
  10.427 +      |>> Thm.certify_inst (Thm.theory_of_thm goal');
  10.428 +
  10.429 +    val goal'' = Thm.instantiate ([], schematic_terms) goal';
  10.430 +    val concl' = Thm.instantiate_cterm ([], schematic_terms) concl;
  10.431 +    val (schematic_types, schematic_terms') = schematics;
  10.432 +    val schematics' = (schematic_types, schematic_terms @ schematic_terms');
  10.433 +  in
  10.434 +    ({context = context', concl = concl', params = params, prems = prems,
  10.435 +      schematics = schematics', asms = asms} : Subgoal.focus, goal'')
  10.436 +  end;
  10.437 +
  10.438 +exception MATCH_CUT;
  10.439 +
  10.440 +val raise_match : (thm * Envir.env) Seq.seq = Seq.make (fn () => raise MATCH_CUT);
  10.441 +
  10.442 +fun match_facts ctxt fixes prop_pats get =
  10.443 +  let
  10.444 +    fun is_multi (((_, x : match_args), _), _) = #multi x;
  10.445 +    fun is_unify (_, x : match_args) = #unify x;
  10.446 +    fun is_cut (_, x : match_args) = #cut x;
  10.447 +
  10.448 +    fun match_thm (((x, params), pat), thm) env  =
  10.449 +      let
  10.450 +        fun try_dest_term term = the_default term (try Logic.dest_term term);
  10.451 +
  10.452 +        val pat' = pat |> Envir.norm_term env |> try_dest_term;
  10.453 +
  10.454 +        val item' = Thm.prop_of thm |> try_dest_term;
  10.455 +        val ts = Option.map (fst o fst) (fst x);
  10.456 +        (*FIXME: Do we need to move one of these patterns above the other?*)
  10.457 +
  10.458 +        val matches =
  10.459 +          (if is_unify x
  10.460 +           then Unify.smash_unifiers (Context.Proof ctxt) [(pat', item') ] env
  10.461 +           else Unify.matchers (Context.Proof ctxt) [(pat', item')])
  10.462 +          |> Seq.map_filter (fn env' =>
  10.463 +              match_filter_env ctxt fixes (ts, params) thm (Envir.merge (env, env')))
  10.464 +          |> is_cut x ? (fn t => Seq.make (fn () =>
  10.465 +            Option.map (fn (x, _) => (x, raise_match)) (Seq.pull t)));
  10.466 +      in
  10.467 +        matches
  10.468 +      end;
  10.469 +
  10.470 +    val all_matches =
  10.471 +      map (fn pat => (pat, get (snd pat))) prop_pats
  10.472 +      |> map (fn (pat, matches) => (pat, map (fn thm => match_thm (pat, thm)) matches));
  10.473 +
  10.474 +    fun proc_multi_match (pat, thmenvs) (pats, env) =
  10.475 +      if is_multi pat then
  10.476 +        let
  10.477 +          val empty = ([], Envir.empty ~1);
  10.478 +
  10.479 +          val thmenvs' =
  10.480 +            Seq.EVERY (map (fn e => fn (thms, env) =>
  10.481 +              Seq.append (Seq.map (fn (thm, env') => (thm :: thms, env')) (e env))
  10.482 +                (Seq.single (thms, env))) thmenvs) empty;
  10.483 +        in
  10.484 +          Seq.map_filter (fn (fact, env') =>
  10.485 +            if not (null fact) then SOME ((pat, fact) :: pats, env') else NONE) thmenvs'
  10.486 +        end
  10.487 +      else
  10.488 +        fold (fn e => Seq.append (Seq.map (fn (thm, env') =>
  10.489 +          ((pat, [thm]) :: pats, env')) (e env))) thmenvs Seq.empty;
  10.490 +
  10.491 +    val all_matches =
  10.492 +      Seq.EVERY (map proc_multi_match all_matches) ([], Envir.empty ~1)
  10.493 +      |> Seq.filter (fn (_, e) => forall (is_some o Envir.lookup e o Term.dest_Var) fixes);
  10.494 +
  10.495 +    fun map_handle seq = Seq.make (fn () =>
  10.496 +      (case (Seq.pull seq handle MATCH_CUT => NONE) of
  10.497 +        SOME (x, seq') => SOME (x, map_handle seq')
  10.498 +      | NONE => NONE));
  10.499 +  in
  10.500 +    map_handle all_matches
  10.501 +  end;
  10.502 +
  10.503 +fun real_match using ctxt fixes m text pats goal =
  10.504 +  let
  10.505 +    fun make_fact_matches ctxt get =
  10.506 +      let
  10.507 +        val (pats', ctxt') = fold_map prep_fact_pat pats ctxt;
  10.508 +      in
  10.509 +        match_facts ctxt' fixes pats' get
  10.510 +        |> Seq.map (fn (fact_insts, env) => do_inst fact_insts env text ctxt')
  10.511 +      end;
  10.512 +
  10.513 +    (*TODO: Slightly hacky re-use of fact match implementation in plain term matching *)
  10.514 +    fun make_term_matches ctxt get =
  10.515 +      let
  10.516 +        val pats' =
  10.517 +          map
  10.518 +            (fn ((SOME _, _), _) => error "Cannot name term match"
  10.519 +              | ((_, x), t) => (((NONE, x), []), Logic.mk_term t)) pats;
  10.520 +
  10.521 +        val thm_of = Drule.mk_term o Thm.cterm_of ctxt;
  10.522 +        fun get' t = get (Logic.dest_term t) |> map thm_of;
  10.523 +      in
  10.524 +        match_facts ctxt fixes pats' get'
  10.525 +        |> Seq.map (fn (fact_insts, env) => do_inst fact_insts env text ctxt)
  10.526 +      end;
  10.527 +  in
  10.528 +    (case m of
  10.529 +      Match_Fact net =>
  10.530 +        Seq.map (fn (text, ctxt') => Method_Closure.method_evaluate text ctxt' using goal)
  10.531 +          (make_fact_matches ctxt (Item_Net.retrieve net))
  10.532 +    | Match_Term net =>
  10.533 +        Seq.map (fn (text, ctxt') => Method_Closure.method_evaluate text ctxt' using goal)
  10.534 +          (make_term_matches ctxt (Item_Net.retrieve net))
  10.535 +    | match_kind =>
  10.536 +        if Thm.no_prems goal then Seq.empty
  10.537 +        else
  10.538 +          let
  10.539 +            fun focus_cases f g =
  10.540 +              (case match_kind of
  10.541 +                Match_Prems => f
  10.542 +              | Match_Concl => g
  10.543 +              | _ => raise Fail "Match kind fell through");
  10.544 +
  10.545 +            val ({context = focus_ctxt, params, asms, concl, ...}, focused_goal) =
  10.546 +              focus_cases (Subgoal.focus_prems) (focus_concl) ctxt 1 goal
  10.547 +              |>> augment_focus;
  10.548 +
  10.549 +            val texts =
  10.550 +              focus_cases
  10.551 +                (fn _ =>
  10.552 +                  make_fact_matches focus_ctxt
  10.553 +                    (Item_Net.retrieve (focus_prems focus_ctxt |> snd) #>
  10.554 +                  order_list))
  10.555 +                (fn _ =>
  10.556 +                  make_term_matches focus_ctxt (fn _ => [Logic.strip_imp_concl (Thm.term_of concl)]))
  10.557 +                ();
  10.558 +
  10.559 +            (*TODO: How to handle cases? *)
  10.560 +
  10.561 +            fun do_retrofit inner_ctxt goal' =
  10.562 +              let
  10.563 +                val cleared_prems =
  10.564 +                  subtract (eq_fst (op =))
  10.565 +                    (focus_prems inner_ctxt |> snd |> Item_Net.content)
  10.566 +                    (focus_prems focus_ctxt |> snd |> Item_Net.content)
  10.567 +                  |> map (fn (_, thm) =>
  10.568 +                    Thm.hyps_of thm
  10.569 +                    |> (fn [hyp] => hyp | _ => error "Prem should have only one hyp"));
  10.570 +
  10.571 +                val n_subgoals = Thm.nprems_of goal';
  10.572 +                fun prep_filter t =
  10.573 +                  Term.subst_bounds (map (Thm.term_of o snd) params |> rev, Term.strip_all_body t);
  10.574 +                fun filter_test prems t =
  10.575 +                  if member (op =) prems t then SOME (remove1 (op aconv) t prems) else NONE;
  10.576 +              in
  10.577 +                Subgoal.retrofit inner_ctxt ctxt params asms 1 goal' goal |>
  10.578 +                (if n_subgoals = 0 orelse null cleared_prems then I
  10.579 +                 else
  10.580 +                  Seq.map (Goal.restrict 1 n_subgoals)
  10.581 +                  #> Seq.maps (ALLGOALS (fn i =>
  10.582 +                      DETERM (filter_prems_tac' ctxt prep_filter filter_test cleared_prems i)))
  10.583 +                  #> Seq.map (Goal.unrestrict 1))
  10.584 +              end;
  10.585 +
  10.586 +            fun apply_text (text, ctxt') =
  10.587 +              let
  10.588 +                val goal' =
  10.589 +                  DROP_CASES (Method_Closure.method_evaluate text ctxt' using) focused_goal
  10.590 +                  |> Seq.maps (DETERM (do_retrofit ctxt'))
  10.591 +                  |> Seq.map (fn goal => ([]: cases, goal))
  10.592 +              in goal' end;
  10.593 +          in
  10.594 +            Seq.map apply_text texts
  10.595 +          end)
  10.596 +  end;
  10.597 +
  10.598 +val match_parser =
  10.599 +  parse_match_kind :-- (fn kind => Scan.lift @{keyword "in"} |-- parse_match_bodies kind) >>
  10.600 +    (fn (matches, bodies) => fn ctxt => fn using => fn goal =>
  10.601 +      if Method_Closure.is_dummy goal then Seq.empty
  10.602 +      else
  10.603 +        let
  10.604 +          fun exec (pats, fixes, text) goal =
  10.605 +            let
  10.606 +              val ctxt' = fold Variable.declare_term fixes ctxt
  10.607 +              |> fold (fn (_, t) => Variable.declare_term t) pats; (*Is this a good idea? We really only care about the maxidx*)
  10.608 +            in
  10.609 +              real_match using ctxt' fixes matches text pats goal
  10.610 +            end;
  10.611 +        in
  10.612 +          Seq.FIRST (map exec bodies) goal
  10.613 +          |> Seq.flat
  10.614 +        end);
  10.615 +
  10.616 +val _ =
  10.617 +  Theory.setup
  10.618 +    (Method.setup @{binding match}
  10.619 +      (match_parser >> (fn m => fn ctxt => METHOD_CASES (m ctxt)))
  10.620 +      "structural analysis/matching on goals");
  10.621 +
  10.622 +end;
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Eisbach/method_closure.ML	Fri Apr 17 17:49:19 2015 +0200
    11.3 @@ -0,0 +1,344 @@
    11.4 +(*  Title:      method_closure.ML
    11.5 +    Author:     Daniel Matichuk, NICTA/UNSW
    11.6 +
    11.7 +Facilities for treating method syntax as a closure, with abstraction
    11.8 +over terms, facts and other methods.
    11.9 +
   11.10 +The 'method' command allows to define new proof methods by combining
   11.11 +existing ones with their usual syntax.
   11.12 +*)
   11.13 +
   11.14 +signature METHOD_CLOSURE =
   11.15 +sig
   11.16 +  val is_dummy: thm -> bool
   11.17 +  val tag_free_thm: thm -> thm
   11.18 +  val free_aware_rule_attribute: thm list -> (Context.generic -> thm -> thm) -> Thm.attribute
   11.19 +  val read_inner_method: Proof.context -> Token.src -> Method.text
   11.20 +  val read_text_closure: Proof.context -> Input.source -> Token.src * Method.text
   11.21 +  val method_evaluate: Method.text -> Proof.context -> Method.method
   11.22 +  val get_inner_method: Proof.context -> string * Position.T ->
   11.23 +    (term list * (string list * string list)) * Method.text
   11.24 +  val eval_inner_method: Proof.context -> (term list * string list) * Method.text ->
   11.25 +    term list -> (string * thm list) list -> Method.method list ->
   11.26 +    Proof.context -> Method.method
   11.27 +  val method_definition: binding -> (binding * typ option * mixfix) list ->
   11.28 +    binding list -> binding list -> binding list -> Input.source -> local_theory -> local_theory
   11.29 +  val method_definition_cmd: binding -> (binding * string option * mixfix) list ->
   11.30 +    binding list -> binding list -> binding list -> Input.source -> local_theory -> local_theory
   11.31 +end;
   11.32 +
   11.33 +structure Method_Closure: METHOD_CLOSURE =
   11.34 +struct
   11.35 +
   11.36 +(* context data *)
   11.37 +
   11.38 +structure Data = Generic_Data
   11.39 +(
   11.40 +  type T =
   11.41 +    ((term list * (string list * string list)) * Method.text) Symtab.table;
   11.42 +  val empty: T = Symtab.empty;
   11.43 +  val extend = I;
   11.44 +  fun merge (methods1,methods2) : T =
   11.45 +    (Symtab.merge (K true) (methods1, methods2));
   11.46 +);
   11.47 +
   11.48 +val get_methods = Data.get o Context.Proof;
   11.49 +val map_methods = Data.map;
   11.50 +
   11.51 +
   11.52 +structure Local_Data = Proof_Data
   11.53 +(
   11.54 +  type T =
   11.55 +    Method.method Symtab.table *  (*dynamic methods*)
   11.56 +    (term list -> Proof.context -> Method.method)  (*recursive method*);
   11.57 +  fun init _ : T = (Symtab.empty, fn _ => fn _ => Method.fail);
   11.58 +);
   11.59 +
   11.60 +fun lookup_dynamic_method full_name ctxt =
   11.61 +  (case Symtab.lookup (#1 (Local_Data.get ctxt)) full_name of
   11.62 +    SOME m => m
   11.63 +  | NONE => error ("Illegal use of internal Eisbach method: " ^ quote full_name));
   11.64 +
   11.65 +val update_dynamic_method = Local_Data.map o apfst o Symtab.update;
   11.66 +
   11.67 +val get_recursive_method = #2 o Local_Data.get;
   11.68 +val put_recursive_method = Local_Data.map o apsnd o K;
   11.69 +
   11.70 +
   11.71 +(* free thm *)
   11.72 +
   11.73 +fun is_dummy thm =
   11.74 +  (case try Logic.dest_term (Thm.concl_of (perhaps (try Goal.conclude) thm)) of
   11.75 +    NONE => false
   11.76 +  | SOME t => Term.is_dummy_pattern t);
   11.77 +
   11.78 +val free_thmN = "Method_Closure.free_thm";
   11.79 +fun tag_free_thm thm = Thm.tag_rule (free_thmN, "") thm;
   11.80 +
   11.81 +val dummy_free_thm = tag_free_thm Drule.dummy_thm;
   11.82 +
   11.83 +fun is_free_thm thm = Properties.defined (Thm.get_tags thm) free_thmN;
   11.84 +
   11.85 +fun is_free_fact [thm] = is_free_thm thm
   11.86 +  | is_free_fact _ = false;
   11.87 +
   11.88 +fun free_aware_rule_attribute args f =
   11.89 +  Thm.rule_attribute (fn context => fn thm =>
   11.90 +    if exists is_free_thm (thm :: args) then dummy_free_thm
   11.91 +    else f context thm);
   11.92 +
   11.93 +
   11.94 +(* thm semantics for combined methods with internal parser. Simulates outer syntax parsing. *)
   11.95 +(* Creates closures for each combined method while parsing, based on the parse context *)
   11.96 +
   11.97 +fun read_inner_method ctxt src =
   11.98 +  let
   11.99 +    val toks = Token.args_of_src src;
  11.100 +    val parser = Parse.!!! (Method.parser' ctxt 0 --| Scan.ahead Parse.eof);
  11.101 +  in
  11.102 +    (case Scan.read Token.stopper parser toks of
  11.103 +      SOME (method_text, _) => method_text
  11.104 +    | NONE => error ("Failed to parse method" ^ Position.here (#2 (Token.name_of_src src))))
  11.105 +  end;
  11.106 +
  11.107 +fun read_text_closure ctxt input =
  11.108 +  let
  11.109 +    (*tokens*)
  11.110 +    val keywords = Thy_Header.get_keywords' ctxt;
  11.111 +    val toks =
  11.112 +      Input.source_explode input
  11.113 +      |> Token.read_no_commands keywords (Scan.one Token.not_eof);
  11.114 +    val _ =
  11.115 +      toks |> List.app (fn tok =>
  11.116 +        if Token.keyword_with Symbol.is_ascii_identifier tok then
  11.117 +          Context_Position.report ctxt (Token.pos_of tok) Markup.keyword1
  11.118 +        else ());
  11.119 +
  11.120 +    (*source closure*)
  11.121 +    val src =
  11.122 +      Token.src ("", Input.pos_of input) toks
  11.123 +      |> Token.init_assignable_src;
  11.124 +    val method_text = read_inner_method ctxt src;
  11.125 +    val method_text' = Method.map_source (Method.method_closure ctxt) method_text;
  11.126 +    val src' = Token.closure_src src;
  11.127 +  in (src', method_text') end;
  11.128 +
  11.129 +val parse_method =
  11.130 +  Args.context -- Scan.lift (Parse.token Parse.cartouche) >> (fn (ctxt, tok) =>
  11.131 +    (case Token.get_value tok of
  11.132 +      NONE =>
  11.133 +        let
  11.134 +           val (src, text) = read_text_closure ctxt (Token.input_of tok);
  11.135 +           val _ = Token.assign (SOME (Token.Source src)) tok;
  11.136 +        in text end
  11.137 +    | SOME (Token.Source src) => read_inner_method ctxt src
  11.138 +    | SOME _ =>
  11.139 +        error ("Unexpected inner token value for method cartouche" ^
  11.140 +          Position.here (Token.pos_of tok))));
  11.141 +
  11.142 +fun method_evaluate text ctxt : Method.method = fn facts => fn st =>
  11.143 +  if is_dummy st then Seq.empty
  11.144 +  else Method.evaluate text (Config.put Method.closure false ctxt) facts st;
  11.145 +
  11.146 +
  11.147 +fun parse_term_args args =
  11.148 +  Args.context :|-- (fn ctxt =>
  11.149 +    let
  11.150 +      fun parse T =
  11.151 +        (if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt)
  11.152 +        #> Type.constraint (Type_Infer.paramify_vars T);
  11.153 +
  11.154 +      fun do_parse' T =
  11.155 +        Parse_Tools.name_term >>
  11.156 +          (fn Parse_Tools.Parse_Val (s, f) => (parse T s, f)
  11.157 +            | Parse_Tools.Real_Val t' => (t', K ()));
  11.158 +
  11.159 +      fun do_parse (Var (_, T)) = do_parse' T
  11.160 +        | do_parse (Free (_, T)) = do_parse' T
  11.161 +        | do_parse t = error ("Unexpected method parameter: " ^ Syntax.string_of_term ctxt t);
  11.162 +
  11.163 +       fun rep [] x = Scan.succeed [] x
  11.164 +         | rep (t :: ts) x  = (do_parse t -- rep ts >> op ::) x;
  11.165 +
  11.166 +      fun check ts =
  11.167 +        let
  11.168 +          val (ts, fs) = split_list ts;
  11.169 +          val ts' = Syntax.check_terms ctxt ts |> Variable.polymorphic ctxt;
  11.170 +          val _ = ListPair.app (fn (f, t) => f t) (fs, ts');
  11.171 +        in ts' end;
  11.172 +    in Scan.lift (rep args) >> check end);
  11.173 +
  11.174 +fun match_term_args ctxt args ts =
  11.175 +  let
  11.176 +    val match_types = Sign.typ_match (Proof_Context.theory_of ctxt) o apply2 Term.fastype_of;
  11.177 +    val tyenv = fold match_types (args ~~ ts) Vartab.empty;
  11.178 +    val tenv =
  11.179 +      fold (fn ((xi, T), t) => Vartab.update_new (xi, (T, t)))
  11.180 +        (map Term.dest_Var args ~~ ts) Vartab.empty;
  11.181 +  in Envir.Envir {maxidx = ~1, tenv = tenv, tyenv = tyenv} end;
  11.182 +
  11.183 +fun check_attrib ctxt attrib =
  11.184 +  let
  11.185 +    val name = Binding.name_of attrib;
  11.186 +    val pos = Binding.pos_of attrib;
  11.187 +    val named_thm = Named_Theorems.check ctxt (name, pos);
  11.188 +    val parser: Method.modifier parser =
  11.189 +      Args.$$$ name -- Args.colon >>
  11.190 +        K {init = I, attribute = Named_Theorems.add named_thm, pos = pos};
  11.191 +  in (named_thm, parser) end;
  11.192 +
  11.193 +
  11.194 +fun instantiate_text env text =
  11.195 +  let val morphism = Morphism.term_morphism "instantiate_text" (Envir.norm_term env);
  11.196 +  in Method.map_source (Token.transform_src morphism) text end;
  11.197 +
  11.198 +fun evaluate_dynamic_thm ctxt name =
  11.199 +  (case (try (Named_Theorems.get ctxt) name) of
  11.200 +    SOME thms => thms
  11.201 +  | NONE => Proof_Context.get_thms ctxt name);
  11.202 +
  11.203 +
  11.204 +fun evaluate_named_theorems ctxt =
  11.205 +  (Method.map_source o Token.map_values)
  11.206 +    (fn Token.Fact (SOME name, _) =>
  11.207 +          Token.Fact (SOME name, evaluate_dynamic_thm ctxt name)
  11.208 +      | x => x);
  11.209 +
  11.210 +fun evaluate_method_def fix_env raw_text ctxt =
  11.211 +  let
  11.212 +    val text = raw_text
  11.213 +      |> instantiate_text fix_env
  11.214 +      |> evaluate_named_theorems ctxt;
  11.215 +  in method_evaluate text ctxt end;
  11.216 +
  11.217 +fun setup_local_method binding lthy =
  11.218 +  let
  11.219 +    val full_name = Local_Theory.full_name lthy binding;
  11.220 +  in
  11.221 +    lthy
  11.222 +    |> update_dynamic_method (full_name, Method.fail)
  11.223 +    |> Method.local_setup binding (Scan.succeed (lookup_dynamic_method full_name)) "(internal)"
  11.224 +  end;
  11.225 +
  11.226 +fun setup_local_fact binding = Named_Theorems.declare binding "";
  11.227 +
  11.228 +fun parse_method_args method_names =
  11.229 +  let
  11.230 +    fun bind_method (name, text) ctxt =
  11.231 +      update_dynamic_method (name, method_evaluate text ctxt) ctxt;
  11.232 +
  11.233 +    fun do_parse t = parse_method >> pair t;
  11.234 +    fun rep [] x = Scan.succeed [] x
  11.235 +      | rep (t :: ts) x  = (do_parse t -- rep ts >> op ::) x;
  11.236 +  in rep method_names >> fold bind_method end;
  11.237 +
  11.238 +
  11.239 +(* FIXME redundant!? -- base name of binding is not changed by usual morphisms*)
  11.240 +fun Morphism_name phi name =
  11.241 +  Morphism.binding phi (Binding.make (name, Position.none)) |> Binding.name_of;
  11.242 +
  11.243 +fun add_method binding ((fixes, declares, methods), text) lthy =
  11.244 +  lthy |>
  11.245 +  Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
  11.246 +    map_methods
  11.247 +      (Symtab.update (Local_Theory.full_name lthy binding,
  11.248 +        (((map (Morphism.term phi) fixes),
  11.249 +          (map (Morphism_name phi) declares, map (Morphism_name phi) methods)),
  11.250 +          Method.map_source (Token.transform_src phi) text))));
  11.251 +
  11.252 +fun get_inner_method ctxt (xname, pos) =
  11.253 +  let
  11.254 +    val name = Method.check_name ctxt (xname, pos);
  11.255 +  in
  11.256 +    (case Symtab.lookup (get_methods ctxt) name of
  11.257 +      SOME entry => entry
  11.258 +    | NONE => error ("Unknown Eisbach method: " ^ quote name ^ Position.here pos))
  11.259 +  end;
  11.260 +
  11.261 +fun eval_inner_method ctxt0 header fixes attribs methods =
  11.262 +  let
  11.263 +    val ((term_args, hmethods), text) = header;
  11.264 +
  11.265 +    fun match fixes = (* FIXME proper context!? *)
  11.266 +      (case Seq.pull (Unify.matchers (Context.Proof ctxt0) (term_args ~~ fixes)) of
  11.267 +        SOME (env, _) => env
  11.268 +      | NONE => error "Couldn't match term arguments");
  11.269 +
  11.270 +    fun add_thms (name, thms) =
  11.271 +      fold (Context.proof_map o Named_Theorems.add_thm name) thms;
  11.272 +
  11.273 +    val setup_ctxt = fold add_thms attribs
  11.274 +      #> fold update_dynamic_method (hmethods ~~ methods)
  11.275 +      #> put_recursive_method (fn fixes => evaluate_method_def (match fixes) text);
  11.276 +  in
  11.277 +    fn ctxt => evaluate_method_def (match fixes) text (setup_ctxt ctxt)
  11.278 +  end;
  11.279 +
  11.280 +fun gen_method_definition prep_vars name vars uses attribs methods body lthy =
  11.281 +  let
  11.282 +    val (uses_nms, lthy1) = lthy
  11.283 +      |> Proof_Context.concealed
  11.284 +      |> Local_Theory.open_target |-> Proof_Context.private_scope
  11.285 +      |> Local_Theory.map_background_naming (Name_Space.add_path (Binding.name_of name))
  11.286 +      |> Config.put Method.old_section_parser true
  11.287 +      |> fold setup_local_method methods
  11.288 +      |> fold_map setup_local_fact uses;
  11.289 +
  11.290 +    val ((xs, Ts), lthy2) = lthy1
  11.291 +      |> prep_vars vars |-> Proof_Context.add_fixes
  11.292 +      |-> (fn xs => fold_map Proof_Context.inferred_param xs #>> pair xs);
  11.293 +
  11.294 +    val term_args = map Free (xs ~~ Ts);
  11.295 +    val (named_thms, modifiers) = map (check_attrib lthy2) (attribs @ uses) |> split_list;
  11.296 +    val self_name :: method_names = map (Local_Theory.full_name lthy2) (name :: methods);
  11.297 +
  11.298 +    fun parser args eval =
  11.299 +      apfst (Config.put_generic Method.old_section_parser true) #>
  11.300 +      (parse_term_args args --|
  11.301 +        Method.sections modifiers --
  11.302 +        (*Scan.depend (fn context => Scan.succeed () >> (K (fold XNamed_Theorems.empty uses_nms context, ()))) --*)  (* FIXME *)
  11.303 +        parse_method_args method_names >> eval);
  11.304 +
  11.305 +    val lthy3 = lthy2
  11.306 +      |> Method.local_setup (Binding.make (Binding.name_of name, Position.none))
  11.307 +        (parser term_args
  11.308 +          (fn (fixes, decl) => fn ctxt => get_recursive_method ctxt fixes (decl ctxt))) "(internal)";
  11.309 +
  11.310 +    val (src, text) = read_text_closure lthy3 body;
  11.311 +
  11.312 +    val morphism =
  11.313 +      Variable.export_morphism lthy3
  11.314 +        (lthy
  11.315 +          |> Proof_Context.transfer (Proof_Context.theory_of lthy3)
  11.316 +          |> Token.declare_maxidx_src src
  11.317 +          |> Variable.declare_maxidx (Variable.maxidx_of lthy3));
  11.318 +
  11.319 +    val text' = Method.map_source (Token.transform_src morphism) text;
  11.320 +    val term_args' = map (Morphism.term morphism) term_args;
  11.321 +
  11.322 +    fun real_exec ts ctxt =
  11.323 +      evaluate_method_def (match_term_args ctxt term_args' ts) text' ctxt;
  11.324 +    val real_parser =
  11.325 +      parser term_args' (fn (fixes, decl) => fn ctxt =>
  11.326 +        real_exec fixes (put_recursive_method real_exec (decl ctxt)));
  11.327 +  in
  11.328 +    lthy3
  11.329 +    |> Local_Theory.close_target
  11.330 +    |> Proof_Context.restore_naming lthy
  11.331 +    |> Method.local_setup name real_parser "(defined in Eisbach)"
  11.332 +    |> add_method name ((term_args', named_thms, method_names), text')
  11.333 +  end;
  11.334 +
  11.335 +val method_definition = gen_method_definition Proof_Context.cert_vars;
  11.336 +val method_definition_cmd = gen_method_definition Proof_Context.read_vars;
  11.337 +
  11.338 +val _ =
  11.339 +  Outer_Syntax.local_theory @{command_keyword method} "Eisbach method definition"
  11.340 +    (Parse.binding -- Parse.for_fixes --
  11.341 +      ((Scan.optional (@{keyword "uses"} |-- Parse.!!! (Scan.repeat1 Parse.binding)) []) --
  11.342 +        (Scan.optional (@{keyword "declares"} |-- Parse.!!! (Scan.repeat1 Parse.binding)) [])) --
  11.343 +      (Scan.optional (@{keyword "methods"} |-- Parse.!!! (Scan.repeat1 Parse.binding)) []) --
  11.344 +      Parse.!!! (@{keyword "="} |-- Parse.token Parse.cartouche)
  11.345 +      >> (fn ((((name, vars), (uses, attribs)), methods), cartouche) =>
  11.346 +        method_definition_cmd name vars uses attribs methods (Token.input_of cartouche)));
  11.347 +end;
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOL/Eisbach/parse_tools.ML	Fri Apr 17 17:49:19 2015 +0200
    12.3 @@ -0,0 +1,49 @@
    12.4 +(*  Title:      parse_tools.ML
    12.5 +    Author:     Daniel Matichuk, NICTA/UNSW
    12.6 +
    12.7 +Simple tools for deferred stateful token values.
    12.8 +*)
    12.9 +
   12.10 +signature PARSE_TOOLS =
   12.11 +sig
   12.12 +  datatype ('a, 'b) parse_val =
   12.13 +    Real_Val of 'a
   12.14 +  | Parse_Val of 'b * ('a -> unit)
   12.15 +
   12.16 +  val parse_term_val : 'b parser -> (term, 'b) parse_val parser
   12.17 +
   12.18 +  val name_term : (term, string) parse_val parser
   12.19 +  val is_real_val : ('a, 'b) parse_val -> bool
   12.20 +
   12.21 +  val the_real_val : ('a, 'b) parse_val -> 'a
   12.22 +  val the_parse_val : ('a, 'b) parse_val -> 'b
   12.23 +  val the_parse_fun : ('a, 'b) parse_val -> ('a -> unit)
   12.24 +end;
   12.25 +
   12.26 +structure Parse_Tools: PARSE_TOOLS =
   12.27 +struct
   12.28 +
   12.29 +datatype ('a, 'b) parse_val =
   12.30 +  Real_Val of 'a
   12.31 +| Parse_Val of 'b * ('a -> unit);
   12.32 +
   12.33 +fun parse_term_val scan =
   12.34 +  Scan.ahead Parse.not_eof -- Scan.ahead (Scan.option Args.internal_term) -- scan >>
   12.35 +    (fn ((_, SOME t), _) => Real_Val t
   12.36 +      | ((tok, NONE), v) => Parse_Val (v, fn t => Token.assign (SOME (Token.Term t)) tok));
   12.37 +
   12.38 +val name_term = parse_term_val Args.name_inner_syntax;
   12.39 +
   12.40 +fun is_real_val (Real_Val _) = true
   12.41 +  | is_real_val _ = false;
   12.42 +
   12.43 +fun the_real_val (Real_Val t) = t
   12.44 +  | the_real_val _ = raise Fail "Expected close parsed value";
   12.45 +
   12.46 +fun the_parse_val (Parse_Val (b, _)) = b
   12.47 +  | the_parse_val _ = raise Fail "Expected open parsed value";
   12.48 +
   12.49 +fun the_parse_fun (Parse_Val (_, f)) = f
   12.50 +  | the_parse_fun _ = raise Fail "Expected open parsed value";
   12.51 +
   12.52 +end;
    13.1 --- a/src/HOL/ROOT	Fri Apr 17 16:54:25 2015 +0200
    13.2 +++ b/src/HOL/ROOT	Fri Apr 17 17:49:19 2015 +0200
    13.3 @@ -631,6 +631,15 @@
    13.4      "root.tex"
    13.5      "style.tex"
    13.6  
    13.7 +session "HOL-Eisbach" in Eisbach = HOL +
    13.8 +  description {*
    13.9 +    The Eisbach proof method language and "match" method.
   13.10 +  *}
   13.11 +  theories
   13.12 +    Eisbach
   13.13 +    Tests
   13.14 +    Examples
   13.15 +
   13.16  session "HOL-SET_Protocol" in SET_Protocol = HOL +
   13.17    description {*
   13.18      Verification of the SET Protocol.