updated Eisbach, using version fb741500f533 of its Bitbucket repository;
authorwenzelm
Sun May 03 18:51:26 2015 +0200 (2015-05-03)
changeset 60248f7e4294216d2
parent 60247 6a5015b096a2
child 60249 09377954133b
updated Eisbach, using version fb741500f533 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/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
     1.1 --- a/src/HOL/Eisbach/Eisbach.thy	Sun May 03 18:45:58 2015 +0200
     1.2 +++ b/src/HOL/Eisbach/Eisbach.thy	Sun May 03 18:51:26 2015 +0200
     1.3 @@ -1,11 +1,11 @@
     1.4 -(*  Title:      Eisbach.thy
     1.5 +(*  Title:      HOL/Eisbach/Eisbach.thy
     1.6      Author:     Daniel Matichuk, NICTA/UNSW
     1.7  
     1.8  Main entry point for Eisbach proof method language.
     1.9  *)
    1.10  
    1.11  theory Eisbach
    1.12 -imports Pure
    1.13 +imports Main
    1.14  keywords
    1.15    "method" :: thy_decl and
    1.16    "conclusion"
    1.17 @@ -16,7 +16,6 @@
    1.18    "uses"
    1.19  begin
    1.20  
    1.21 -
    1.22  ML_file "parse_tools.ML"
    1.23  ML_file "eisbach_rule_insts.ML"
    1.24  ML_file "method_closure.ML"
    1.25 @@ -24,20 +23,12 @@
    1.26  ML_file "eisbach_antiquotations.ML"
    1.27  
    1.28  (* FIXME reform Isabelle/Pure attributes to make this work by default *)
    1.29 -attribute_setup THEN =
    1.30 -  \<open>Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm >> (fn (i, B) =>
    1.31 -    Method_Closure.free_aware_rule_attribute [B] (fn _ => fn A => A RSN (i, B)))\<close>
    1.32 -  "resolution with rule"
    1.33 -
    1.34 -attribute_setup OF =
    1.35 -  \<open>Attrib.thms >> (fn Bs =>
    1.36 -    Method_Closure.free_aware_rule_attribute Bs (fn _ => fn A => A OF Bs))\<close>
    1.37 -  "rule resolved with facts"
    1.38 -
    1.39 -attribute_setup rotated =
    1.40 -  \<open>Scan.lift (Scan.optional Parse.int 1 >> (fn n =>
    1.41 -    Method_Closure.free_aware_rule_attribute [] (fn _ => rotate_prems n)))\<close>
    1.42 -  "rotated theorem premises"
    1.43 +setup \<open>
    1.44 +  fold (Method_Closure.wrap_attribute true)
    1.45 +    [@{binding intro}, @{binding elim}, @{binding dest}, @{binding simp}] #>
    1.46 +  fold (Method_Closure.wrap_attribute false)
    1.47 +    [@{binding THEN}, @{binding OF}, @{binding rotated}, @{binding simplified}]
    1.48 +\<close>
    1.49  
    1.50  method solves methods m = (m; fail)
    1.51  
     2.1 --- a/src/HOL/Eisbach/Eisbach_Tools.thy	Sun May 03 18:45:58 2015 +0200
     2.2 +++ b/src/HOL/Eisbach/Eisbach_Tools.thy	Sun May 03 18:51:26 2015 +0200
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:      Eisbach_Tools.thy
     2.5 +(*  Title:      HOL/Eisbach/Eisbach_Tools.thy
     2.6      Author:     Daniel Matichuk, NICTA/UNSW
     2.7  
     2.8  Usability tools for Eisbach.
     3.1 --- a/src/HOL/Eisbach/Examples.thy	Sun May 03 18:45:58 2015 +0200
     3.2 +++ b/src/HOL/Eisbach/Examples.thy	Sun May 03 18:51:26 2015 +0200
     3.3 @@ -1,4 +1,4 @@
     3.4 -(*  Title:      Examples.thy
     3.5 +(*  Title:      HOL/Eisbach/Examples.thy
     3.6      Author:     Daniel Matichuk, NICTA/UNSW
     3.7  *)
     3.8  
     4.1 --- a/src/HOL/Eisbach/Tests.thy	Sun May 03 18:45:58 2015 +0200
     4.2 +++ b/src/HOL/Eisbach/Tests.thy	Sun May 03 18:51:26 2015 +0200
     4.3 @@ -1,4 +1,4 @@
     4.4 -(*  Title:      Tests.thy
     4.5 +(*  Title:      HOL/Eisbach/Tests.thy
     4.6      Author:     Daniel Matichuk, NICTA/UNSW
     4.7  *)
     4.8  
     4.9 @@ -9,6 +9,7 @@
    4.10  begin
    4.11  
    4.12  
    4.13 +
    4.14  section \<open>Named Theorems Tests\<close>
    4.15  
    4.16  named_theorems foo
    4.17 @@ -161,6 +162,7 @@
    4.18  
    4.19  end
    4.20  
    4.21 +
    4.22  (* Testing inner focusing. This fails if we don't smash flex-flex pairs produced
    4.23     by retrofitting. This needs to be done more carefully to avoid smashing
    4.24     legitimate pairs.*)
    4.25 @@ -292,7 +294,7 @@
    4.26    done
    4.27  
    4.28  
    4.29 -ML {*
    4.30 +ML \<open>
    4.31  structure Data = Generic_Data
    4.32  (
    4.33    type T = thm list;
    4.34 @@ -300,7 +302,7 @@
    4.35    val extend = I;
    4.36    fun merge data : T = Thm.merge_thms data;
    4.37  );
    4.38 -*}
    4.39 +\<close>
    4.40  
    4.41  local_setup \<open>Local_Theory.add_thms_dynamic (@{binding test_dyn}, Data.get)\<close>
    4.42  
    4.43 @@ -321,6 +323,34 @@
    4.44  
    4.45  end
    4.46  
    4.47 +
    4.48 +notepad begin
    4.49 +  fix A x
    4.50 +  assume X: "\<And>x. A x"
    4.51 +  have "A x"
    4.52 +  by (match X in H[of x]:"\<And>x. A x" \<Rightarrow> \<open>print_fact H,match H in "A x" \<Rightarrow> \<open>rule H\<close>\<close>)
    4.53 +
    4.54 +  fix A x B
    4.55 +  assume X: "\<And>x :: bool. A x \<Longrightarrow> B" "\<And>x. A x"
    4.56 +  assume Y: "A B"
    4.57 +  have "B \<and> B \<and> B \<and> B \<and> B \<and> B"
    4.58 +  apply (intro conjI)
    4.59 +  apply (match X in H[OF X(2)]:"\<And>x. A x \<Longrightarrow> B" \<Rightarrow> \<open>print_fact H,rule H\<close>)
    4.60 +  apply (match X in H':"\<And>x. A x" and H[OF H']:"\<And>x. A x \<Longrightarrow> B" \<Rightarrow> \<open>print_fact H',print_fact H,rule H\<close>)
    4.61 +  apply (match X in H[of Q]:"\<And>x. A x \<Longrightarrow> ?R" and "?P \<Longrightarrow> Q" for Q \<Rightarrow> \<open>print_fact H,rule H, rule Y\<close>)
    4.62 +  apply (match X in H[of Q,OF Y]:"\<And>x. A x \<Longrightarrow> ?R" and "?P \<Longrightarrow> Q" for Q \<Rightarrow> \<open>print_fact H,rule H\<close>)
    4.63 +  apply (match X in H[OF Y,intro]:"\<And>x. A x \<Longrightarrow> ?R" \<Rightarrow> \<open>print_fact H,fastforce\<close>)
    4.64 +  apply (match X in H[intro]:"\<And>x. A x \<Longrightarrow> ?R" \<Rightarrow> \<open>rule H[where x=B], rule Y\<close>)  
    4.65 +  done
    4.66 +  
    4.67 +  fix x :: "prop" and A
    4.68 +  assume X: "TERM x"
    4.69 +  assume Y: "\<And>x :: prop. A x"
    4.70 +  have "A TERM x"
    4.71 +  apply (match X in "PROP y" for y \<Rightarrow> \<open>rule Y[where x="PROP y"]\<close>)
    4.72 +  done
    4.73 +end
    4.74 +
    4.75  (* Method name internalization test *)
    4.76  
    4.77  method test2 = (simp)
     5.1 --- a/src/HOL/Eisbach/eisbach_antiquotations.ML	Sun May 03 18:45:58 2015 +0200
     5.2 +++ b/src/HOL/Eisbach/eisbach_antiquotations.ML	Sun May 03 18:51:26 2015 +0200
     5.3 @@ -1,4 +1,4 @@
     5.4 -(*  Title:      eisbach_antiquotations.ML
     5.5 +(*  Title:      HOL/Eisbach/eisbach_antiquotations.ML
     5.6      Author:     Daniel Matichuk, NICTA/UNSW
     5.7  
     5.8  ML antiquotations for Eisbach.
     6.1 --- a/src/HOL/Eisbach/eisbach_rule_insts.ML	Sun May 03 18:45:58 2015 +0200
     6.2 +++ b/src/HOL/Eisbach/eisbach_rule_insts.ML	Sun May 03 18:51:26 2015 +0200
     6.3 @@ -1,4 +1,4 @@
     6.4 -(*  Title:      eisbach_rule_insts.ML
     6.5 +(*  Title:      HOL/Eisbach/eisbach_rule_insts.ML
     6.6      Author:     Daniel Matichuk, NICTA/UNSW
     6.7  
     6.8  Eisbach-aware variants of the "where" and "of" attributes.
     6.9 @@ -77,10 +77,11 @@
    6.10    Named_Insts of ((indexname * string) * (term -> unit)) list
    6.11  | Term_Insts of (indexname * term) list;
    6.12  
    6.13 -fun embed_indexname ((xi,s),f) =
    6.14 +fun embed_indexname ((xi, s), f) =
    6.15    let
    6.16 -    fun wrap_xi xi t = Logic.mk_conjunction (Logic.mk_term (Var (xi,fastype_of t)),Logic.mk_term t);
    6.17 -  in ((xi,s),f o wrap_xi xi) end;
    6.18 +    fun wrap_xi xi t =
    6.19 +      Logic.mk_conjunction (Logic.mk_term (Var (xi, fastype_of t)), Logic.mk_term t);
    6.20 +  in ((xi, s), f o wrap_xi xi) end;
    6.21  
    6.22  fun unembed_indexname t =
    6.23    let
    6.24 @@ -98,9 +99,9 @@
    6.25  
    6.26      val insts' =
    6.27        if forall (fn (_, v) => Parse_Tools.is_real_val v) insts
    6.28 -      then Term_Insts (map (fn (_,t) => unembed_indexname (Parse_Tools.the_real_val t)) insts)
    6.29 +      then Term_Insts (map (fn (_, t) => unembed_indexname (Parse_Tools.the_real_val t)) insts)
    6.30        else Named_Insts (map (fn (xi, p) => embed_indexname
    6.31 -            ((xi,Parse_Tools.the_parse_val p),Parse_Tools.the_parse_fun p)) insts);
    6.32 +            ((xi, Parse_Tools.the_parse_val p), Parse_Tools.the_parse_fun p)) insts);
    6.33    in
    6.34      (insts', fixes)
    6.35    end;
    6.36 @@ -132,13 +133,14 @@
    6.37        if forall (fn SOME t => Parse_Tools.is_real_val t | NONE => true) (insts @ concl_insts)
    6.38        then
    6.39          Term_Insts
    6.40 -          (map_filter (Option.map (Parse_Tools.the_real_val #> unembed_indexname)) (insts @ concl_insts))
    6.41 -
    6.42 +          (map_filter
    6.43 +            (Option.map (Parse_Tools.the_real_val #> unembed_indexname)) (insts @ concl_insts))
    6.44        else
    6.45          Named_Insts
    6.46 -          (apply2 (map (Option.map (fn p => (Parse_Tools.the_parse_val p,Parse_Tools.the_parse_fun p))))
    6.47 +          (apply2
    6.48 +            (map (Option.map (fn p => (Parse_Tools.the_parse_val p, Parse_Tools.the_parse_fun p))))
    6.49              (insts, concl_insts)
    6.50 -            |> of_rule thm |> map ((fn (xi, (nm, tok)) => embed_indexname ((xi, nm), tok))));
    6.51 +          |> of_rule thm |> map ((fn (xi, (nm, tok)) => embed_indexname ((xi, nm), tok))));
    6.52    in
    6.53      (insts', fixes)
    6.54    end;
     7.1 --- a/src/HOL/Eisbach/match_method.ML	Sun May 03 18:45:58 2015 +0200
     7.2 +++ b/src/HOL/Eisbach/match_method.ML	Sun May 03 18:51:26 2015 +0200
     7.3 @@ -1,4 +1,4 @@
     7.4 -(*  Title:      match_method.ML
     7.5 +(*  Title:      HOL/Eisbach/match_method.ML
     7.6      Author:     Daniel Matichuk, NICTA/UNSW
     7.7  
     7.8  Setup for "match" proof method. It provides basic fact/term matching in
     7.9 @@ -61,8 +61,8 @@
    7.10  
    7.11  val fixes =
    7.12    Parse.and_list1 (Scan.repeat1  (Parse.position bound_term) --
    7.13 -    Scan.option (@{keyword "::"} |-- Parse.!!! Parse.typ) >> (fn (xs, T) => map (fn (nm,pos) => ((nm,T),pos)) xs))
    7.14 -  >> flat;
    7.15 +    Scan.option (@{keyword "::"} |-- Parse.!!! Parse.typ)
    7.16 +    >> (fn (xs, T) => map (fn (nm, pos) => ((nm, T), pos)) xs)) >> flat;
    7.17  
    7.18  val for_fixes = Scan.optional (@{keyword "for"} |-- fixes) [];
    7.19  
    7.20 @@ -89,7 +89,6 @@
    7.21          | "cut" => {multi = multi, cut = true}))
    7.22        ss {multi = false, cut = false});
    7.23  
    7.24 -(*TODO: Shape holes in thms *)
    7.25  fun parse_named_pats match_kind =
    7.26    Args.context :|-- (fn ctxt =>
    7.27      Scan.lift (Parse.and_list1 (Scan.option (dynamic_fact ctxt --| Args.colon) :--
    7.28 @@ -105,20 +104,18 @@
    7.29        SOME (Token.Source src) =>
    7.30          let
    7.31            val text = Method_Closure.read_inner_method ctxt src
    7.32 -          (*TODO: Correct parse context for attributes?*)
    7.33            val ts' =
    7.34              map
    7.35                (fn (b, (Parse_Tools.Real_Val v, match_args)) =>
    7.36                  ((Option.map (fn (b, att) =>
    7.37 -                  (Parse_Tools.the_real_val b,
    7.38 -                    map (Attrib.attribute ctxt) att)) b, match_args), v)
    7.39 +                  (Parse_Tools.the_real_val b, att)) b, match_args), v)
    7.40                  | _ => raise Fail "Expected closed term") ts
    7.41 -          val fixes' = map (fn ((p, _),_) => Parse_Tools.the_real_val p) fixes
    7.42 +          val fixes' = map (fn ((p, _), _) => Parse_Tools.the_real_val p) fixes
    7.43          in (ts', fixes', text) end
    7.44      | SOME _ => error "Unexpected token value in match cartouche"
    7.45      | NONE =>
    7.46          let
    7.47 -          val fixes' = map (fn ((pb, otyp),_) => (Parse_Tools.the_parse_val pb, otyp, NoSyn)) fixes;
    7.48 +          val fixes' = map (fn ((pb, otyp), _) => (Parse_Tools.the_parse_val pb, otyp, NoSyn)) fixes;
    7.49            val (fixes'', ctxt1) = Proof_Context.read_vars fixes' ctxt;
    7.50            val (fix_nms, ctxt2) = Proof_Context.add_fixes fixes'' ctxt1;
    7.51  
    7.52 @@ -135,9 +132,11 @@
    7.53  
    7.54            val pat_fixes = fold (Term.add_frees) pats [] |> map fst;
    7.55  
    7.56 -          val _ = map2 (fn nm => fn (_,pos) => member (op =) pat_fixes nm orelse
    7.57 -            error ("For-fixed variable must be bound in some pattern." ^ Position.here pos))
    7.58 -            fix_nms fixes;
    7.59 +          val _ =
    7.60 +            map2 (fn nm => fn (_, pos) =>
    7.61 +                member (op =) pat_fixes nm orelse
    7.62 +                error ("For-fixed variable must be bound in some pattern" ^ Position.here pos))
    7.63 +              fix_nms fixes;
    7.64  
    7.65            val _ = map (Term.map_types Type.no_tvars) pats
    7.66  
    7.67 @@ -164,20 +163,27 @@
    7.68  
    7.69                    val param_thm = map (Drule.mk_term o Thm.cterm_of ctxt' o Free) abs_nms
    7.70                      |> Conjunction.intr_balanced
    7.71 -                    |> Drule.generalize ([], map fst abs_nms);
    7.72 +                    |> Drule.generalize ([], map fst abs_nms)
    7.73 +                    |> Method_Closure.tag_free_thm;
    7.74  
    7.75 -                  val thm =
    7.76 +                  val atts = map (Attrib.attribute ctxt') att;
    7.77 +                  val (param_thm', ctxt'') = Thm.proof_attributes atts param_thm ctxt';
    7.78 +
    7.79 +                  fun label_thm thm =
    7.80                      Thm.cterm_of ctxt' (Free (nm, propT))
    7.81                      |> Drule.mk_term
    7.82 -                    |> not (null abs_nms) ? Conjunction.intr param_thm
    7.83 -                    |> Drule.zero_var_indexes
    7.84 -                    |> Method_Closure.tag_free_thm;
    7.85 +                    |> not (null abs_nms) ? Conjunction.intr thm
    7.86 +
    7.87 +                  val [head_thm, body_thm] =
    7.88 +                    Drule.zero_var_indexes_list (map label_thm [param_thm, param_thm'])
    7.89 +                    |> map Method_Closure.tag_free_thm;
    7.90  
    7.91 -                  (*TODO: Preprocess attributes here?*)
    7.92 -
    7.93 -                  val (_, ctxt'') = Proof_Context.note_thmss "" [((b, []), [([thm], [])])] ctxt';
    7.94 +                  val ctxt''' =
    7.95 +                    Attrib.local_notes "" [((b, []), [([body_thm], [])])] ctxt''
    7.96 +                    |> snd
    7.97 +                    |> Variable.declare_maxidx (Thm.maxidx_of head_thm);
    7.98                  in
    7.99 -                  (SOME (Thm.prop_of thm, map (Attrib.attribute ctxt) att) :: tms, ctxt'')
   7.100 +                  (SOME (Thm.prop_of head_thm, att) :: tms, ctxt''')
   7.101                  end
   7.102              | upd_ctxt NONE _ (tms, ctxt) = (NONE :: tms, ctxt);
   7.103  
   7.104 @@ -196,7 +202,20 @@
   7.105            val pats' = map (Term.map_types Type_Infer.paramify_vars #> Morphism.term morphism) pats;
   7.106            val _ = ListPair.app (fn ((_, (Parse_Tools.Parse_Val (_, f), _)), t) => f t) (ts, pats');
   7.107  
   7.108 -          val binds' = map (Option.map (fn (t, atts) => (Morphism.term morphism t, atts))) binds;
   7.109 +          fun close_src src =
   7.110 +            let
   7.111 +              val src' = Token.closure_src src |> Token.transform_src morphism;
   7.112 +              val _ =
   7.113 +                map2 (fn tok1 => fn tok2 =>
   7.114 +                  (case (Token.get_value tok2) of
   7.115 +                    SOME value => Token.assign (SOME value) tok1
   7.116 +                  | NONE => ()))
   7.117 +                  (Token.args_of_src src)
   7.118 +                  (Token.args_of_src src');
   7.119 +            in src' end;
   7.120 +
   7.121 +          val binds' =
   7.122 +            map (Option.map (fn (t, atts) => (Morphism.term morphism t, map close_src atts))) binds;
   7.123  
   7.124            val _ =
   7.125              ListPair.app
   7.126 @@ -207,7 +226,8 @@
   7.127  
   7.128            val real_fixes' = map (Morphism.term morphism) real_fixes;
   7.129            val _ =
   7.130 -            ListPair.app (fn (( (Parse_Tools.Parse_Val (_, f),_) , _), t) => f t) (fixes, real_fixes');
   7.131 +            ListPair.app (fn (( (Parse_Tools.Parse_Val (_, f), _) , _), t) => f t)
   7.132 +              (fixes, real_fixes');
   7.133  
   7.134            val match_args = map (fn (_, (_, match_args)) => match_args) ts;
   7.135            val binds'' = (binds' ~~ match_args) ~~ pats';
   7.136 @@ -247,36 +267,30 @@
   7.137          (fn ((((SOME ((_, head), att), _), _), _), thms) => SOME (head, (thms, att))
   7.138            | _ => NONE) fact_insts';
   7.139  
   7.140 -    fun apply_attribute thm att ctxt =
   7.141 -      let
   7.142 -        val (opt_context', thm') = att (Context.Proof ctxt, thm)
   7.143 -      in
   7.144 -        (case thm' of
   7.145 -          SOME _ => error "Rule attributes cannot be applied here"
   7.146 -        | _ => the_default ctxt (Option.map Context.proof_of opt_context'))
   7.147 -      end;
   7.148 -
   7.149 -    fun apply_attributes atts thm = fold (apply_attribute thm) atts;
   7.150 -
   7.151 -     (*TODO: What to do about attributes that raise errors?*)
   7.152 -    val (fact_insts, ctxt') =
   7.153 -      fold_map (fn (head, (thms, atts : attribute list)) => fn ctxt =>
   7.154 -        ((head, thms), fold (apply_attributes atts) thms ctxt)) fact_insts ctxt;
   7.155 -
   7.156      fun try_dest_term thm = try (Thm.prop_of #> dest_internal_fact #> snd) thm;
   7.157  
   7.158 -    fun expand_fact thm =
   7.159 +    fun expand_fact fact_insts thm =
   7.160        the_default [thm]
   7.161          (case try_dest_term thm of
   7.162            SOME t_ident => AList.lookup (op aconv) fact_insts t_ident
   7.163          | NONE => NONE);
   7.164  
   7.165 -    val morphism =
   7.166 +    fun fact_morphism fact_insts =
   7.167        Morphism.term_morphism "do_inst.term" (Envir.norm_term env) $>
   7.168        Morphism.typ_morphism "do_inst.type" (Envir.norm_type (Envir.type_env env)) $>
   7.169 -      Morphism.fact_morphism "do_inst.fact" (maps expand_fact);
   7.170 +      Morphism.fact_morphism "do_inst.fact" (maps (expand_fact fact_insts));
   7.171  
   7.172 -    val text' = Method.map_source (Token.transform_src morphism) text;
   7.173 +    fun apply_attribute (head, (fact, atts)) (fact_insts, ctxt) =
   7.174 +      let
   7.175 +        val morphism = fact_morphism fact_insts;
   7.176 +        val atts' = map (Attrib.attribute ctxt o Token.transform_src morphism) atts;
   7.177 +        val (fact'', ctxt') = fold_map (Thm.proof_attributes atts') fact ctxt;
   7.178 +      in ((head, fact'') :: fact_insts, ctxt') end;
   7.179 +
   7.180 +     (*TODO: What to do about attributes that raise errors?*)
   7.181 +    val (fact_insts', ctxt') = fold_rev (apply_attribute) fact_insts ([], ctxt);
   7.182 +
   7.183 +    val text' = Method.map_source (Token.transform_src (fact_morphism fact_insts')) text;
   7.184    in
   7.185      (text', ctxt')
   7.186    end;
   7.187 @@ -304,27 +318,27 @@
   7.188    let
   7.189      val tenv = Envir.term_env env;
   7.190      val tyenv = Envir.type_env env;
   7.191 -    val max_tidx = Vartab.fold (fn (_,(_,t)) => curry Int.max (maxidx_of_term t)) tenv ~1;
   7.192 -    val max_Tidx = Vartab.fold (fn (_,(_,T)) => curry Int.max (maxidx_of_typ T)) tyenv ~1;
   7.193 +    val max_tidx = Vartab.fold (fn (_, (_, t)) => curry Int.max (maxidx_of_term t)) tenv ~1;
   7.194 +    val max_Tidx = Vartab.fold (fn (_, (_, T)) => curry Int.max (maxidx_of_typ T)) tyenv ~1;
   7.195    in
   7.196      Envir.Envir
   7.197 -      {maxidx = Int.max (Int.max (max_tidx,max_Tidx),Envir.maxidx_of env),
   7.198 +      {maxidx = Int.max (Int.max (max_tidx, max_Tidx), Envir.maxidx_of env),
   7.199          tenv = tenv, tyenv = tyenv}
   7.200    end
   7.201  
   7.202  fun match_filter_env inner_ctxt morphism pat_vars fixes (ts, params) thm inner_env =
   7.203    let
   7.204      val tenv = Envir.term_env inner_env
   7.205 -      |> Vartab.map (K (fn (T,t) => (Morphism.typ morphism T,Morphism.term morphism t)));
   7.206 +      |> Vartab.map (K (fn (T, t) => (Morphism.typ morphism T, Morphism.term morphism t)));
   7.207  
   7.208      val tyenv = Envir.type_env inner_env
   7.209 -      |> Vartab.map (K (fn (S,T) => (S,Morphism.typ morphism T)));
   7.210 +      |> Vartab.map (K (fn (S, T) => (S, Morphism.typ morphism T)));
   7.211  
   7.212      val outer_env = Envir.Envir {maxidx = Envir.maxidx_of inner_env, tenv = tenv, tyenv = tyenv};
   7.213  
   7.214      val param_vars = map Term.dest_Var params;
   7.215  
   7.216 -    val params' = map (fn (xi,_) => Vartab.lookup (Envir.term_env outer_env) xi) param_vars;
   7.217 +    val params' = map (fn (xi, _) => Vartab.lookup (Envir.term_env outer_env) xi) param_vars;
   7.218  
   7.219      val fixes_vars = map Term.dest_Var fixes;
   7.220  
   7.221 @@ -339,11 +353,11 @@
   7.222        Envir.Envir {maxidx = Envir.maxidx_of outer_env, tenv = tenv', tyenv = tyenv}
   7.223        |> recalculate_maxidx;
   7.224  
   7.225 -    val all_params_bound = forall (fn SOME (_,(Var _)) => true | _ => false) params';
   7.226 +    val all_params_bound = forall (fn SOME (_, Var _) => true | _ => false) params';
   7.227  
   7.228      val pat_fixes = inter (eq_fst (op =)) fixes_vars pat_vars;
   7.229  
   7.230 -    val all_pat_fixes_bound = forall (fn (xi,_) => is_some (Vartab.lookup tenv' xi)) pat_fixes;
   7.231 +    val all_pat_fixes_bound = forall (fn (xi, _) => is_some (Vartab.lookup tenv' xi)) pat_fixes;
   7.232  
   7.233      val thm' = Morphism.thm morphism thm;
   7.234  
   7.235 @@ -469,7 +483,7 @@
   7.236        SOME (x, seq') =>
   7.237          if member eq prev x
   7.238          then Seq.pull (deduplicate eq prev seq')
   7.239 -        else SOME (x,deduplicate eq (x :: prev) seq')
   7.240 +        else SOME (x, deduplicate eq (x :: prev) seq')
   7.241      | NONE => NONE));
   7.242  
   7.243  fun consistent_env env =
   7.244 @@ -480,7 +494,7 @@
   7.245      forall (fn (_, (T, t)) => Envir.norm_type tyenv T = fastype_of t) (Vartab.dest tenv)
   7.246    end;
   7.247  
   7.248 -fun eq_env (env1,env2) =
   7.249 +fun eq_env (env1, env2) =
   7.250    let
   7.251      val tyenv1 = Envir.type_env env1;
   7.252      val tyenv2 = Envir.type_env env2;
   7.253 @@ -492,7 +506,7 @@
   7.254            Envir.eta_contract (Envir.norm_term env2 t')))
   7.255        (apply2 Vartab.dest (Envir.term_env env1, Envir.term_env env2))
   7.256      andalso
   7.257 -    ListPair.allEq (fn ((var, (_, T)), (var', (_,T'))) =>
   7.258 +    ListPair.allEq (fn ((var, (_, T)), (var', (_, T'))) =>
   7.259          var = var' andalso Envir.norm_type tyenv1 T = Envir.norm_type tyenv2 T')
   7.260        (apply2 Vartab.dest (Envir.type_env env1, Envir.type_env env2))
   7.261    end;
   7.262 @@ -505,15 +519,13 @@
   7.263  
   7.264      fun match_thm (((x, params), pat), thm) env  =
   7.265        let
   7.266 -        fun try_dest_term term = the_default term (try Logic.dest_term term);
   7.267 -
   7.268          val pat_vars = Term.add_vars pat [];
   7.269  
   7.270 -        val pat' = pat |> Envir.norm_term env |> try_dest_term;
   7.271 +        val pat' = pat |> Envir.norm_term env;
   7.272  
   7.273 -        val (((Tinsts', insts),[thm']), inner_ctxt) = Variable.import false [thm] ctxt
   7.274 +        val (((Tinsts', insts), [thm']), inner_ctxt) = Variable.import false [thm] ctxt;
   7.275  
   7.276 -        val item' = Thm.prop_of thm' |> try_dest_term;
   7.277 +        val item' = Thm.prop_of thm';
   7.278  
   7.279          val ts = Option.map (fst o fst) (fst x);
   7.280  
   7.281 @@ -572,7 +584,6 @@
   7.282          |> Seq.map (fn (fact_insts, env) => do_inst fact_insts env text ctxt')
   7.283        end;
   7.284  
   7.285 -    (*TODO: Slightly hacky re-use of fact match implementation in plain term matching *)
   7.286      fun make_term_matches ctxt get =
   7.287        let
   7.288          val pats' =
     8.1 --- a/src/HOL/Eisbach/method_closure.ML	Sun May 03 18:45:58 2015 +0200
     8.2 +++ b/src/HOL/Eisbach/method_closure.ML	Sun May 03 18:51:26 2015 +0200
     8.3 @@ -1,4 +1,4 @@
     8.4 -(*  Title:      method_closure.ML
     8.5 +(*  Title:      HOL/Eisbach/method_closure.ML
     8.6      Author:     Daniel Matichuk, NICTA/UNSW
     8.7  
     8.8  Facilities for treating method syntax as a closure, with abstraction
     8.9 @@ -13,6 +13,7 @@
    8.10    val is_dummy: thm -> bool
    8.11    val tag_free_thm: thm -> thm
    8.12    val free_aware_rule_attribute: thm list -> (Context.generic -> thm -> thm) -> Thm.attribute
    8.13 +  val wrap_attribute: bool -> Binding.binding -> theory -> theory
    8.14    val read_inner_method: Proof.context -> Token.src -> Method.text
    8.15    val read_text_closure: Proof.context -> Token.src -> Token.src * Method.text
    8.16    val read_inner_text_closure: Proof.context -> Input.source -> Token.src * Method.text
    8.17 @@ -35,12 +36,10 @@
    8.18  
    8.19  structure Data = Generic_Data
    8.20  (
    8.21 -  type T =
    8.22 -    ((term list * (string list * string list)) * Method.text) Symtab.table;
    8.23 +  type T = ((term list * (string list * string list)) * Method.text) Symtab.table;
    8.24    val empty: T = Symtab.empty;
    8.25    val extend = I;
    8.26 -  fun merge (methods1,methods2) : T =
    8.27 -    (Symtab.merge (K true) (methods1, methods2));
    8.28 +  fun merge data : T = Symtab.merge (K true) data;
    8.29  );
    8.30  
    8.31  val get_methods = Data.get o Context.Proof;
    8.32 @@ -88,6 +87,32 @@
    8.33      if exists is_free_thm (thm :: args) then dummy_free_thm
    8.34      else f context thm);
    8.35  
    8.36 +fun free_aware_attribute thy declaration src (context, thm) =
    8.37 +  let
    8.38 +    val src' = Token.init_assignable_src src;
    8.39 +    fun apply_att thm = (Attrib.attribute_global thy src') (context, thm);
    8.40 +    val _ = try apply_att Drule.dummy_thm;
    8.41 +    val src'' = Token.closure_src src';
    8.42 +    val thms =
    8.43 +      map_filter Token.get_value (Token.args_of_src src'')
    8.44 +      |> map_filter (fn (Token.Fact (_, f)) => SOME f | _ => NONE)
    8.45 +      |> flat;
    8.46 +  in
    8.47 +    if exists is_free_thm (thm :: thms) then
    8.48 +      if declaration then (NONE, NONE)
    8.49 +      else (NONE, SOME dummy_free_thm)
    8.50 +    else apply_att thm
    8.51 +  end;
    8.52 +
    8.53 +fun wrap_attribute declaration binding thy =
    8.54 +  let
    8.55 +    val name = Binding.name_of binding;
    8.56 +    val name' = Attrib.check_name_generic (Context.Theory thy) (name, Position.none);
    8.57 +    fun get_src src = Token.src (name', Token.range_of_src src) (Token.args_of_src src);
    8.58 +  in
    8.59 +    Attrib.define_global binding (free_aware_attribute thy declaration o get_src) "" thy
    8.60 +    |> snd
    8.61 +  end;
    8.62  
    8.63  (* thm semantics for combined methods with internal parser. Simulates outer syntax parsing. *)
    8.64  (* Creates closures for each combined method while parsing, based on the parse context *)
    8.65 @@ -108,7 +133,8 @@
    8.66      val method_text = read_inner_method ctxt src;
    8.67      val method_text' = Method.map_source (Method.method_closure ctxt) method_text;
    8.68      (*FIXME: Does not markup method parameters. Needs to be done by Method.parser' directly. *)
    8.69 -    val _ = Method.map_source (fn src => (try (Method.check_name ctxt) (Token.name_of_src src);src)) method_text;
    8.70 +    val _ = Method.map_source (fn src =>
    8.71 +                  (try (Method.check_name ctxt) (Token.name_of_src src);src)) method_text;
    8.72      val src' = Token.closure_src src;
    8.73    in (src', method_text') end;
    8.74  
    8.75 @@ -127,7 +153,7 @@
    8.76        NONE =>
    8.77          let
    8.78             val input = Token.input_of tok;
    8.79 -           val (src,text) = read_inner_text_closure ctxt input;
    8.80 +           val (src, text) = read_inner_text_closure ctxt input;
    8.81             val _ = Token.assign (SOME (Token.Source src)) tok;
    8.82          in text end
    8.83      | SOME (Token.Source src) => read_inner_method ctxt src
     9.1 --- a/src/HOL/Eisbach/parse_tools.ML	Sun May 03 18:45:58 2015 +0200
     9.2 +++ b/src/HOL/Eisbach/parse_tools.ML	Sun May 03 18:51:26 2015 +0200
     9.3 @@ -1,4 +1,4 @@
     9.4 -(*  Title:      parse_tools.ML
     9.5 +(*  Title:      HOL/Eisbach/parse_tools.ML
     9.6      Author:     Daniel Matichuk, NICTA/UNSW
     9.7  
     9.8  Simple tools for deferred stateful token values.