author matichuk Mon, 11 Jan 2016 15:58:18 +1100 changeset 62133 43518f70b438 parent 62132 09c2a77f91d3 child 62134 2405ab06d5b1
match method now makes proper use of context_tactic
```--- a/src/HOL/Eisbach/match_method.ML	Mon Jan 11 22:14:42 2016 +0000
+++ b/src/HOL/Eisbach/match_method.ML	Mon Jan 11 15:58:18 2016 +1100
@@ -16,26 +16,28 @@
structure Match_Method : MATCH_METHOD =
struct

-(*Variant of filter_prems_tac with auxiliary configuration;
-  recovers premise order afterwards.*)
-fun filter_prems_tac' ctxt prep pred a =
+(* Filter premises by predicate, with premise order; recovers premise order afterwards.*)
+fun filter_prems_tac' ctxt prem =
let
fun Then NONE tac = SOME tac
| Then (SOME tac) tac' = SOME (tac THEN' tac');
-    fun thins H (tac, n, a, i) =
-      (case pred a H of
-        NONE => (tac, n + 1, a, i)
-      | SOME a' => (Then tac (rotate_tac n THEN' eresolve_tac ctxt [thin_rl]), 0, a', i + n));
+    fun thins idxH (tac, n, i) =
+       if prem idxH then (tac, n + 1 , i)
+       else (Then tac (rotate_tac n THEN' eresolve_tac ctxt [thin_rl]), 0, i + n);
in
SUBGOAL (fn (goal, i) =>
-      let val Hs = Logic.strip_assums_hyp (prep goal) in
-        (case fold thins Hs (NONE, 0, a, 0) of
-          (NONE, _, _, _) => no_tac
-        | (SOME tac, _, _, n) => tac i THEN rotate_tac (~ n) i)
+      let val idxHs = tag_list 0 (Logic.strip_assums_hyp goal) in
+        (case fold thins idxHs (NONE, 0, 0) of
+          (NONE, _, _) => no_tac
+        | (SOME tac, _, n) => tac i THEN rotate_tac (~ n) i)
end)
end;

+fun Item_Net_filter f net =
+  fold (fn item => not (f item) ? Item_Net.remove item) (Item_Net.content net) net
+
+
datatype match_kind =
Match_Term of term Item_Net.T
| Match_Fact of thm Item_Net.T
@@ -378,23 +380,9 @@

val focus_prems = #1 o Focus_Data.get;

-fun hyp_from_premid ctxt (ident, prem) =
-  let
-    val ident = Thm.cterm_of ctxt (HOLogic.mk_number @{typ nat} ident |> Logic.mk_term);
-    val hyp =
-      (case Thm.chyps_of prem of
-        [hyp] => hyp
-      | _ => error "Prem should have exactly one hyp");  (* FIXME error vs. raise Fail !? *)
-    val ct = Drule.mk_term (hyp) |> Thm.cprop_of;
-  in Drule.protect (Conjunction.mk_conjunction (ident, ct)) end;
+fun transfer_focus_prems from_ctxt =
+  Focus_Data.map (@{apply 3(1)} (K (focus_prems from_ctxt)))

-fun hyp_from_ctermid ctxt (ident, cterm) =
-  let
-    val ident = Thm.cterm_of ctxt (HOLogic.mk_number @{typ nat} ident |> Logic.mk_term);
-  in Drule.protect (Conjunction.mk_conjunction (ident, cterm)) end;
-
-  Thm.declare_hyps (hyp_from_premid ctxt premid) ctxt;

`(Focus_Data.get #> #1 #> #1) ##>
@@ -433,27 +421,6 @@
(Focus_Data.map o @{apply 3(3)})
(append (map (fn (_, ct) => Thm.term_of ct) params));

-fun solve_term ct = Thm.trivial ct OF [Drule.termI];
-
-fun get_thinned_prems goal =
-  let
-    val chyps = Thm.chyps_of goal;
-
-    fun prem_from_hyp hyp goal =
-    let
-      val asm = Thm.assume hyp;
-      val (identt, ct) = asm |> Goal.conclude |> Thm.cprop_of |> Conjunction.dest_conjunction;
-      val ident = HOLogic.dest_number (Thm.term_of identt |> Logic.dest_term) |> snd;
-      val thm = Conjunction.intr (solve_term identt) (solve_term ct) |> Goal.protect 0
-      val goal' = Thm.implies_elim (Thm.implies_intr hyp goal) thm;
-    in
-      (SOME (ident, ct), goal')
-    end handle TERM _ => (NONE, goal) | THM _ => (NONE, goal);
-  in
-    fold_map prem_from_hyp chyps goal
-    |>> map_filter I
-  end;
-

(* Add focus elements as proof data *)
fun augment_focus (focus: Subgoal.focus) : (int list * Subgoal.focus) =
@@ -467,10 +434,9 @@

val local_prems = map2 pair prem_ids (rev prems);

-    val ctxt'' = fold add_premid_hyp local_prems ctxt';
in
(prem_ids,
-      {context = ctxt'',
+      {context = ctxt',
params = params,
prems = prems,
concl = concl,
@@ -615,7 +581,7 @@
let
val (result, envthms') =
Seq_retrieve envthms (fn (env, _) => eq_env (env, env'));
-                    in
+                    in
(case result of
SOME (_, thms) => SOME ((env', thm :: thms), maximal_set tail seq' envthms')
| NONE => Seq.pull (maximal_set (tail @ [(env', [thm])]) seq' envthms'))
@@ -647,8 +613,13 @@
|> Seq.map (apsnd (morphism_env morphism))
end;

-fun real_match using goal_ctxt fixes m text pats st =
-  let
+fun real_match using outer_ctxt fixes m text pats st =
+  let
+    val goal_ctxt =
+      fold Variable.declare_term fixes outer_ctxt
+      (*FIXME Is this a good idea? We really only care about the maxidx*)
+      |> fold (fn (_, t) => Variable.declare_term t) pats;
+
fun make_fact_matches ctxt get =
let
val (pats', ctxt') = fold_map prep_fact_pat pats ctxt;
@@ -675,12 +646,12 @@
make_fact_matches goal_ctxt (Item_Net.retrieve net)
|> Seq.map (fn (text, ctxt') =>
Method_Closure.method_evaluate text ctxt' using (ctxt', st)
-          |> Seq.filter_results |> Seq.map snd)
+          |> Seq.filter_results |> Seq.map (fn (_, thm) => (outer_ctxt, thm)))
| Match_Term net =>
make_term_matches goal_ctxt (Item_Net.retrieve net)
|> Seq.map (fn (text, ctxt') =>
Method_Closure.method_evaluate text ctxt' using (ctxt', st)
-          |> Seq.filter_results |> Seq.map snd)
+          |> Seq.filter_results |> Seq.map (fn (_, thm) => (outer_ctxt, thm)))
| match_kind =>
if Thm.no_prems st then Seq.empty
else
@@ -691,18 +662,15 @@
| Match_Concl => g
| _ => raise Fail "Match kind fell through");

-            val (goal_thins, st') = get_thinned_prems st;
-
-            val ((local_premids, {context = focus_ctxt, params, asms, concl, ...}), focused_goal) =
-              focus_cases (K Subgoal.focus_prems) focus_concl goal_ctxt 1 NONE st'
+            val ((local_premids, {context = focus_ctxt, params, asms, concl, prems, ...}), focused_goal) =
+              focus_cases (K Subgoal.focus_prems) focus_concl goal_ctxt 1 NONE st
|>> augment_focus;
-
+
val texts =
focus_cases
(fn is_local => fn _ =>
make_fact_matches focus_ctxt
(Item_Net.retrieve (focus_prems focus_ctxt |> snd)
-                     #> filter_out (member (eq_fst (op =)) goal_thins)
#> is_local ? filter (fn (p, _) => exists (fn id' => id' = p) local_premids)
#> order_list))
(fn _ =>
@@ -712,56 +680,51 @@

(*TODO: How to handle cases? *)

-            fun do_retrofit inner_ctxt st1 =
+            fun do_retrofit (inner_ctxt, st1) =
let
-                val (goal_thins', st2) = get_thinned_prems st1;
+                val (_, before_prems) = focus_prems focus_ctxt;
+                val (_, after_prems) = focus_prems inner_ctxt;

-                val thinned_prems =
-                  ((subtract (eq_fst (op =))
-                    (focus_prems inner_ctxt |> snd |> Item_Net.content)
-                    (focus_prems focus_ctxt |> snd |> Item_Net.content))
-                    |> map (fn (id, thm) =>
-                        Thm.chyps_of thm
-                        |> (fn [chyp] => (id, (SOME chyp, NONE))
-                             | _ => error "Prem should have only one hyp")));
+                val removed_prems =
+                  Item_Net_filter (null o Item_Net.lookup after_prems) before_prems

-                val all_thinned_prems =
-                  thinned_prems @
-                    map (fn (id, prem) => (id, (NONE, SOME prem))) (goal_thins' @ goal_thins);
-
-                val (thinned_local_prems, thinned_extra_prems) =
-                  List.partition (fn (id, _) => member (op =) local_premids id) all_thinned_prems;
+                val removed_local_prems = Item_Net.content removed_prems
+                  |> filter (fn (id, _) => member (op =) local_premids id)
+                  |> map (fn (_, prem) => Thm.prop_of prem)

-                val local_thins =
-                  thinned_local_prems |> map
-                    (fn (_, (SOME t, _)) => Thm.term_of t
-                      | (_, (_, SOME pt)) => Thm.term_of pt |> Logic.dest_term);
+                fun filter_removed_prems prems =
+                  Item_Net_filter (null o Item_Net.lookup removed_prems) prems;
+
+                val outer_ctxt' = outer_ctxt
+                  |> Focus_Data.map (@{apply 3(1)} (apsnd filter_removed_prems));
+
+                val n_subgoals = Thm.nprems_of st1;

-                val extra_thins =
-                  thinned_extra_prems |> map
-                    (fn (id, (SOME ct, _)) => (id, Drule.mk_term ct |> Thm.cprop_of)
-                      | (id, (_, SOME pt)) => (id, pt))
-                  |> map (hyp_from_ctermid inner_ctxt);
+                val removed_prem_idxs =
+                  prems
+                  |> tag_list 0
+                  |> filter (member (op aconv) removed_local_prems o Thm.prop_of o snd)
+                  |> map fst

-                val n_subgoals = Thm.nprems_of st2;
-                fun prep_filter t =
-                  Term.subst_bounds (map (Thm.term_of o snd) params |> rev, Term.strip_all_body t);
-                fun filter_test prems t =
-                  if member (op aconv) prems t then SOME (remove1 (op aconv) t prems) else NONE;
+                fun filter_prem (i, _) = not (member (op =) removed_prem_idxs i);
+
in
-                Subgoal.retrofit inner_ctxt goal_ctxt params asms 1 st2 st
-                |> (n_subgoals > 0 andalso not (null local_thins)) ?
+                Subgoal.retrofit inner_ctxt goal_ctxt params asms 1 st1 st
+                |> focus_cases
+                   (fn _ => (n_subgoals > 0 andalso length removed_local_prems > 0) ?
(Seq.map (Goal.restrict 1 n_subgoals)
#> Seq.maps (ALLGOALS (fn i =>
-                          DETERM (filter_prems_tac' goal_ctxt prep_filter filter_test local_thins i)))
-                      #> Seq.map (Goal.unrestrict 1))
-                |> Seq.map (fold Thm.weaken extra_thins)
+                          DETERM (filter_prems_tac' goal_ctxt filter_prem i)))
+                      #> Seq.map (Goal.unrestrict 1)))
+                   I
+                |> Seq.map (pair outer_ctxt')
end;

fun apply_text (text, ctxt') =
-              Method.NO_CONTEXT_TACTIC ctxt'
-                (Method_Closure.method_evaluate text ctxt' using) focused_goal
-              |> Seq.maps (DETERM (do_retrofit ctxt'));
+                Method_Closure.method_evaluate text ctxt' using (ctxt', focused_goal)
+              |> Seq.filter_results
+              |> Seq.maps (Seq.DETERM do_retrofit)
+
in Seq.map apply_text texts end)
end;

@@ -773,16 +736,13 @@
(fn (matches, bodies) => fn ctxt =>
CONTEXT_METHOD (fn using => Method.RUNTIME (fn (goal_ctxt, st) =>
let
+              val ctxt' = transfer_focus_prems goal_ctxt ctxt;
fun exec (pats, fixes, text) st' =
-                let
-                  val ctxt' =
-                    fold Variable.declare_term fixes ctxt
-                    (*FIXME Is this a good idea? We really only care about the maxidx*)
-                    |> fold (fn (_, t) => Variable.declare_term t) pats;
-                in real_match using ctxt' fixes matches text pats st' end;
+                real_match using ctxt' fixes matches text pats st';
in
Seq.flat (Seq.FIRST (map exec bodies) st)
-              |> Method.CONTEXT goal_ctxt
+              |> Seq.map (apfst (fn ctxt' => transfer_focus_prems ctxt' goal_ctxt))
+              |> Seq.make_results
end))))
"structural analysis/matching on goals");
```