# HG changeset patch
# User wenzelm
# Date 1165448524 -3600
# Node ID f689f729afab042565fe288ac951fdc1e69b4eee
# Parent  4f5f6c685ab41adb7549fef42b4ea7eefcb4b85a
reorganized structure Goal vs. Tactic;

diff -r 4f5f6c685ab4 -r f689f729afab src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Wed Dec 06 21:19:03 2006 +0100
+++ b/src/HOL/Tools/record_package.ML	Thu Dec 07 00:42:04 2006 +0100
@@ -905,8 +905,8 @@
     val prove_standard = quick_and_dirty_prove true thy;
     val thm = prove_standard [] prop (fn prems =>
 	 EVERY [rtac equal_intr_rule 1, 
-                norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1,
-                norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1]);
+                Goal.norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1,
+                Goal.norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1]);
   in thm end
   | mk_fun_apply_eq t thy = raise TERM ("mk_fun_apply_eq",[t]);
 
@@ -1649,7 +1649,7 @@
 
     fun split_meta_prf () =
         prove_standard [] split_meta_prop (fn prems =>
-         EVERY [rtac equal_intr_rule 1, norm_hhf_tac 1,
+         EVERY [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1,
                 etac meta_allE 1, atac 1,
                 rtac (prop_subst OF [surjective]) 1,
                 REPEAT (etac meta_allE 1), atac 1]);
@@ -2058,7 +2058,7 @@
 
     fun split_meta_prf () =
         prove false [] split_meta_prop (fn prems =>
-         EVERY [rtac equal_intr_rule 1, norm_hhf_tac 1,
+         EVERY [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1,
                 etac meta_allE 1, atac 1,
                 rtac (prop_subst OF [surjective]) 1,
                 REPEAT (etac meta_allE 1), atac 1]);
diff -r 4f5f6c685ab4 -r f689f729afab src/Provers/classical.ML
--- a/src/Provers/classical.ML	Wed Dec 06 21:19:03 2006 +0100
+++ b/src/Provers/classical.ML	Thu Dec 07 00:42:04 2006 +0100
@@ -1005,7 +1005,7 @@
     Method.trace ctxt rules;
     fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq)
   end)
-  THEN_ALL_NEW Tactic.norm_hhf_tac;
+  THEN_ALL_NEW Goal.norm_hhf_tac;
 
 fun rule_tac [] ctxt cs facts = some_rule_tac ctxt cs facts
   | rule_tac rules _ _ facts = Method.rule_tac rules facts;
diff -r 4f5f6c685ab4 -r f689f729afab src/Provers/induct_method.ML
--- a/src/Provers/induct_method.ML	Wed Dec 06 21:19:03 2006 +0100
+++ b/src/Provers/induct_method.ML	Thu Dec 07 00:42:04 2006 +0100
@@ -162,10 +162,10 @@
 
 val atomize_cterm = Tactic.rewrite true Data.atomize;
 
-val atomize_tac = Tactic.rewrite_goal_tac Data.atomize;
+val atomize_tac = Goal.rewrite_goal_tac Data.atomize;
 
 val inner_atomize_tac =
-  Tactic.rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac;
+  Goal.rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac;
 
 
 (* rulify *)
@@ -182,10 +182,10 @@
   in (thy, Logic.list_implies (map rulify As, rulify B)) end;
 
 val rulify_tac =
-  Tactic.rewrite_goal_tac (Data.rulify @ conjunction_congs) THEN'
-  Tactic.rewrite_goal_tac Data.rulify_fallback THEN'
-  Tactic.conjunction_tac THEN_ALL_NEW
-  (Tactic.rewrite_goal_tac [conjunction_imp] THEN' Tactic.norm_hhf_tac);
+  Goal.rewrite_goal_tac (Data.rulify @ conjunction_congs) THEN'
+  Goal.rewrite_goal_tac Data.rulify_fallback THEN'
+  Goal.conjunction_tac THEN_ALL_NEW
+  (Goal.rewrite_goal_tac [conjunction_imp] THEN' Goal.norm_hhf_tac);
 
 
 (* prepare rule *)
diff -r 4f5f6c685ab4 -r f689f729afab src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Wed Dec 06 21:19:03 2006 +0100
+++ b/src/Pure/Isar/local_defs.ML	Thu Dec 07 00:42:04 2006 +0100
@@ -183,7 +183,7 @@
       in
         Goal.prove ctxt' frees [] prop (K (ALLGOALS
           (meta_rewrite_tac ctxt' THEN'
-            Tactic.rewrite_goal_tac [def] THEN'
+            Goal.rewrite_goal_tac [def] THEN'
             Tactic.resolve_tac [Drule.reflexive_thm])))
         handle ERROR msg => cat_error msg "Failed to prove definitional specification."
       end;
diff -r 4f5f6c685ab4 -r f689f729afab src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Wed Dec 06 21:19:03 2006 +0100
+++ b/src/Pure/Isar/method.ML	Thu Dec 07 00:42:04 2006 +0100
@@ -140,9 +140,9 @@
 fun RAW_METHOD tac = RAW_METHOD_CASES (NO_CASES o tac);
 
 fun METHOD_CASES tac = RAW_METHOD_CASES (fn facts =>
-  Seq.THEN (ALLGOALS Tactic.conjunction_tac, tac facts));
+  Seq.THEN (ALLGOALS Goal.conjunction_tac, tac facts));
 
-fun METHOD tac = RAW_METHOD (fn facts => ALLGOALS Tactic.conjunction_tac THEN tac facts);
+fun METHOD tac = RAW_METHOD (fn facts => ALLGOALS Goal.conjunction_tac THEN tac facts);
 
 val fail = METHOD (K no_tac);
 val succeed = METHOD (K all_tac);
@@ -256,7 +256,7 @@
   (fn i => fn st =>
     if null facts then tac rules i st
     else Seq.maps (fn rule => (tac o single) rule i st) (Drule.multi_resolves facts rules))
-  THEN_ALL_NEW Tactic.norm_hhf_tac;
+  THEN_ALL_NEW Goal.norm_hhf_tac;
 
 fun gen_arule_tac tac j rules facts =
   EVERY' (gen_rule_tac tac rules facts :: replicate j Tactic.assume_tac);
diff -r 4f5f6c685ab4 -r f689f729afab src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Wed Dec 06 21:19:03 2006 +0100
+++ b/src/Pure/Isar/object_logic.ML	Thu Dec 07 00:42:04 2006 +0100
@@ -162,7 +162,7 @@
   else all_tac st;
 
 fun full_atomize_tac i st =
-  rewrite_goal_tac (get_atomize (Thm.theory_of_thm st)) i st;
+  Goal.rewrite_goal_tac (get_atomize (Thm.theory_of_thm st)) i st;
 
 fun atomize_goal i st =
   (case Seq.pull (atomize_tac i st) of NONE => st | SOME (st', _) => st');
@@ -171,7 +171,7 @@
 (* rulify *)
 
 fun rulify_term thy = MetaSimplifier.rewrite_term thy (get_rulify thy) [];
-fun rulify_tac i st = rewrite_goal_tac (get_rulify (Thm.theory_of_thm st)) i st;
+fun rulify_tac i st = Goal.rewrite_goal_tac (get_rulify (Thm.theory_of_thm st)) i st;
 
 fun gen_rulify full thm =
   Tactic.simplify full (get_rulify (Thm.theory_of_thm thm)) thm
diff -r 4f5f6c685ab4 -r f689f729afab src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Dec 06 21:19:03 2006 +0100
+++ b/src/Pure/Isar/proof.ML	Thu Dec 07 00:42:04 2006 +0100
@@ -391,10 +391,10 @@
 fun select_goals n meth state =
   state
   |> (#2 o #2 o get_goal)
-  |> ALLGOALS Tactic.conjunction_tac
+  |> ALLGOALS Goal.conjunction_tac
   |> Seq.maps (fn goal =>
     state
-    |> Seq.lift set_goal (Goal.extract 1 n goal |> Seq.maps (Tactic.conjunction_tac 1))
+    |> Seq.lift set_goal (Goal.extract 1 n goal |> Seq.maps (Goal.conjunction_tac 1))
     |> Seq.maps meth
     |> Seq.maps (fn state' => state'
       |> Seq.lift set_goal (Goal.retrofit 1 n (#2 (#2 (get_goal state'))) goal))
@@ -428,8 +428,8 @@
 (* refine via sub-proof *)
 
 fun goal_tac rule =
-  Tactic.norm_hhf_tac THEN' Tactic.rtac rule THEN_ALL_NEW
-    (Tactic.norm_hhf_tac THEN' (SUBGOAL (fn (goal, i) =>
+  Goal.norm_hhf_tac THEN' Tactic.rtac rule THEN_ALL_NEW
+    (Goal.norm_hhf_tac THEN' (SUBGOAL (fn (goal, i) =>
       if can Logic.unprotect (Logic.strip_assums_concl goal) then
         Tactic.etac Drule.protectI i
       else all_tac)));
diff -r 4f5f6c685ab4 -r f689f729afab src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Dec 06 21:19:03 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Dec 07 00:42:04 2006 +0100
@@ -702,7 +702,7 @@
   | comp_incr_tac (th :: ths) i st =
       (Goal.compose_hhf_tac (Drule.incr_indexes st th) i APPEND comp_incr_tac ths i) st;
 
-fun fact_tac facts = Tactic.norm_hhf_tac THEN' comp_incr_tac facts;
+fun fact_tac facts = Goal.norm_hhf_tac THEN' comp_incr_tac facts;
 
 fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) =>
   let
diff -r 4f5f6c685ab4 -r f689f729afab src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Dec 06 21:19:03 2006 +0100
+++ b/src/Pure/ROOT.ML	Thu Dec 07 00:42:04 2006 +0100
@@ -56,10 +56,10 @@
 use "tctical.ML";
 use "search.ML";
 use "meta_simplifier.ML";
+use "tactic.ML";
 use "conjunction.ML";
 use "assumption.ML";
 use "goal.ML";
-use "tactic.ML";
 
 (*proof term operations*)
 use "Proof/reconstruct.ML";
diff -r 4f5f6c685ab4 -r f689f729afab src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Wed Dec 06 21:19:03 2006 +0100
+++ b/src/Pure/axclass.ML	Thu Dec 07 00:42:04 2006 +0100
@@ -257,7 +257,7 @@
     val names = map (prefix arity_prefix) (Logic.name_arities arity);
     val props = Logic.mk_arities arity;
     val ths = Goal.prove_multi (ProofContext.init thy) [] [] props
-      (fn _ => Tactic.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg =>
+      (fn _ => Goal.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg =>
         cat_error msg ("The error(s) above occurred while trying to prove type arity " ^
           quote (Sign.string_of_arity thy arity));
   in
diff -r 4f5f6c685ab4 -r f689f729afab src/Pure/goal.ML
--- a/src/Pure/goal.ML	Wed Dec 06 21:19:03 2006 +0100
+++ b/src/Pure/goal.ML	Thu Dec 07 00:42:04 2006 +0100
@@ -8,6 +8,8 @@
 signature BASIC_GOAL =
 sig
   val SELECT_GOAL: tactic -> int -> tactic
+  val CONJUNCTS: tactic -> int -> tactic
+  val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
 end;
 
 signature GOAL =
@@ -19,9 +21,6 @@
   val finish: thm -> thm
   val norm_result: thm -> thm
   val close_result: thm -> thm
-  val compose_hhf: thm -> int -> thm -> thm Seq.seq
-  val compose_hhf_tac: thm -> int -> tactic
-  val comp_hhf: thm -> thm -> thm
   val prove_raw: cterm list -> cterm -> (thm list -> tactic) -> thm
   val prove_multi: Proof.context -> string list -> term list -> term list ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm list
@@ -30,6 +29,14 @@
   val prove_global: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
   val extract: int -> int -> thm -> thm Seq.seq
   val retrofit: int -> int -> thm -> thm -> thm Seq.seq
+  val conjunction_tac: int -> tactic
+  val precise_conjunction_tac: int -> int -> tactic
+  val asm_rewrite_goal_tac: bool * bool * bool -> (simpset -> tactic) -> simpset -> int -> tactic
+  val rewrite_goal_tac: thm list -> int -> tactic
+  val norm_hhf_tac: int -> tactic
+  val compose_hhf: thm -> int -> thm -> thm Seq.seq
+  val compose_hhf_tac: thm -> int -> tactic
+  val comp_hhf: thm -> thm -> thm
 end;
 
 structure Goal: GOAL =
@@ -92,20 +99,6 @@
   #> Drule.close_derivation;
 
 
-(* composition of normal results *)
-
-fun compose_hhf tha i thb =
-  Thm.bicompose false (false, Drule.lift_all (Thm.cprem_of thb i) tha, 0) i thb;
-
-fun compose_hhf_tac th i = PRIMSEQ (compose_hhf th i);
-
-fun comp_hhf tha thb =
-  (case Seq.chop 2 (compose_hhf tha 1 thb) of
-    ([th], _) => th
-  | ([], _) => raise THM ("comp_hhf: no unifiers", 1, [tha, thb])
-  | _  => raise THM ("comp_hhf: multiple unifiers", 1, [tha, thb]));
-
-
 
 (** tactical theorem proving **)
 
@@ -164,7 +157,9 @@
 
 
 
-(** local goal states **)
+(** goal structure **)
+
+(* nested goals *)
 
 fun extract i n st =
   (if i < 1 orelse n < 1 orelse i + n - 1 > Thm.nprems_of st then Seq.empty
@@ -181,6 +176,66 @@
   if Thm.nprems_of st = 1 andalso i = 1 then tac st
   else Seq.lifts (retrofit i 1) (Seq.maps tac (extract i 1 st)) st;
 
+
+(* multiple goals *)
+
+val conj_tac = SUBGOAL (fn (goal, i) =>
+  if can Logic.dest_conjunction goal then rtac Conjunction.conjunctionI i
+  else no_tac);
+
+val conjunction_tac = TRY o REPEAT_ALL_NEW conj_tac;
+
+val precise_conjunction_tac =
+  let
+    fun tac 0 i = eq_assume_tac i
+      | tac 1 i = SUBGOAL (K all_tac) i
+      | tac n i = conj_tac i THEN TRY (fn st => tac (n - 1) (i + 1) st);
+  in TRY oo tac end;
+
+fun CONJUNCTS tac =
+  SELECT_GOAL (conjunction_tac 1
+    THEN tac
+    THEN PRIMITIVE (Conjunction.uncurry ~1));
+
+fun PRECISE_CONJUNCTS n tac =
+  SELECT_GOAL (precise_conjunction_tac n 1
+    THEN tac
+    THEN PRIMITIVE (Conjunction.uncurry ~1));
+
+
+(* rewriting *)
+
+(*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)
+fun asm_rewrite_goal_tac mode prover_tac ss =
+  SELECT_GOAL
+    (PRIMITIVE (MetaSimplifier.rewrite_goal_rule mode (SINGLE o prover_tac) ss 1));
+
+fun rewrite_goal_tac rews =
+  let val ss = MetaSimplifier.empty_ss addsimps rews in
+    fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac)
+      (MetaSimplifier.theory_context (Thm.theory_of_thm st) ss) i st
+  end;
+
+
+(* hhf normal form *)
+
+val norm_hhf_tac =
+  rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
+  THEN' SUBGOAL (fn (t, i) =>
+    if Drule.is_norm_hhf t then all_tac
+    else rewrite_goal_tac [Drule.norm_hhf_eq] i);
+
+fun compose_hhf tha i thb =
+  Thm.bicompose false (false, Drule.lift_all (Thm.cprem_of thb i) tha, 0) i thb;
+
+fun compose_hhf_tac th i = PRIMSEQ (compose_hhf th i);
+
+fun comp_hhf tha thb =
+  (case Seq.chop 2 (compose_hhf tha 1 thb) of
+    ([th], _) => th
+  | ([], _) => raise THM ("comp_hhf: no unifiers", 1, [tha, thb])
+  | _  => raise THM ("comp_hhf: multiple unifiers", 1, [tha, thb]));
+
 end;
 
 structure BasicGoal: BASIC_GOAL = Goal;
diff -r 4f5f6c685ab4 -r f689f729afab src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Wed Dec 06 21:19:03 2006 +0100
+++ b/src/Pure/simplifier.ML	Thu Dec 07 00:42:04 2006 +0100
@@ -166,7 +166,7 @@
       (if safe then solvers else unsafe_solvers));
 
     fun simp_loop_tac i =
-      asm_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN
+      Goal.asm_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN
       (solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i));
   in simp_loop_tac end;
 
diff -r 4f5f6c685ab4 -r f689f729afab src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Wed Dec 06 21:19:03 2006 +0100
+++ b/src/Pure/tactic.ML	Thu Dec 07 00:42:04 2006 +0100
@@ -69,7 +69,6 @@
   val net_biresolve_tac : (bool*thm) list -> int -> tactic
   val net_match_tac     : thm list -> int -> tactic
   val net_resolve_tac   : thm list -> int -> tactic
-  val norm_hhf_tac      : int -> tactic
   val prune_params_tac  : tactic
   val rename_params_tac : string list -> int -> tactic
   val rename_tac        : string -> int -> tactic
@@ -77,12 +76,10 @@
   val resolve_from_net_tac      : (int*thm) Net.net -> int -> tactic
   val resolve_tac       : thm list -> int -> tactic
   val res_inst_tac      : (string*string)list -> thm -> int -> tactic
-  val rewrite_goal_tac  : thm list -> int -> tactic
   val rewrite_goals_rule: thm list -> thm -> thm
   val rewrite_rule      : thm list -> thm -> thm
   val rewrite_goals_tac : thm list -> tactic
   val rewrite_tac       : thm list -> tactic
-  val asm_rewrite_goal_tac: bool * bool * bool -> (simpset -> tactic) -> simpset -> int -> tactic
   val rewtac            : thm -> tactic
   val rotate_tac        : int -> int -> tactic
   val rtac              : thm -> int -> tactic
@@ -97,8 +94,6 @@
   val instantiate_tac   : (string * string) list -> tactic
   val thin_tac          : string -> int -> tactic
   val trace_goalno_tac  : (int -> tactic) -> int -> tactic
-  val CONJUNCTS: tactic -> int -> tactic
-  val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
 end;
 
 signature TACTIC =
@@ -110,8 +105,6 @@
   val orderlist: (int * 'a) list -> 'a list
   val rewrite: bool -> thm list -> cterm -> thm
   val simplify: bool -> thm list -> thm -> thm
-  val conjunction_tac: int -> tactic
-  val precise_conjunction_tac: int -> int -> tactic
   val compose_inst_tac' : (indexname * string) list -> (bool * thm * int) ->
                           int -> tactic
   val lift_inst_rule'   : thm * int * (indexname * string) list * thm -> thm
@@ -529,17 +522,6 @@
 val rewrite_rule = simplify true;
 val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover;
 
-(*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)
-fun asm_rewrite_goal_tac mode prover_tac ss =
-  SELECT_GOAL
-    (PRIMITIVE (MetaSimplifier.rewrite_goal_rule mode (SINGLE o prover_tac) ss 1));
-
-fun rewrite_goal_tac rews =
-  let val ss = MetaSimplifier.empty_ss addsimps rews in
-    fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac)
-      (MetaSimplifier.theory_context (Thm.theory_of_thm st) ss) i st
-  end;
-
 (*Rewrite throughout proof state. *)
 fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
 
@@ -547,12 +529,6 @@
 fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
 fun rewtac def = rewrite_goals_tac [def];
 
-val norm_hhf_tac =
-  rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
-  THEN' SUBGOAL (fn (t, i) =>
-    if Drule.is_norm_hhf t then all_tac
-    else rewrite_goal_tac [Drule.norm_hhf_eq] i);
-
 
 (*** for folding definitions, handling critical pairs ***)
 
@@ -633,32 +609,6 @@
        end)
   end;
 
-
-(* meta-level conjunction *)
-
-val conj_tac = SUBGOAL (fn (goal, i) =>
-  if can Logic.dest_conjunction goal then rtac Conjunction.conjunctionI i
-  else no_tac);
-
-val conjunction_tac = TRY o REPEAT_ALL_NEW conj_tac;
-
-val precise_conjunction_tac =
-  let
-    fun tac 0 i = eq_assume_tac i
-      | tac 1 i = SUBGOAL (K all_tac) i
-      | tac n i = conj_tac i THEN TRY (fn st => tac (n - 1) (i + 1) st);
-  in TRY oo tac end;
-
-fun CONJUNCTS tac =
-  SELECT_GOAL (conjunction_tac 1
-    THEN tac
-    THEN PRIMITIVE (Conjunction.uncurry ~1));
-
-fun PRECISE_CONJUNCTS n tac =
-  SELECT_GOAL (precise_conjunction_tac n 1
-    THEN tac
-    THEN PRIMITIVE (Conjunction.uncurry ~1));
-
 end;
 
 structure BasicTactic: BASIC_TACTIC = Tactic;
diff -r 4f5f6c685ab4 -r f689f729afab src/ZF/UNITY/Constrains.thy
--- a/src/ZF/UNITY/Constrains.thy	Wed Dec 06 21:19:03 2006 +0100
+++ b/src/ZF/UNITY/Constrains.thy	Thu Dec 07 00:42:04 2006 +0100
@@ -546,7 +546,7 @@
                                    constrains_imp_Constrains] 1),
               rtac constrainsI 1,
               (* Three subgoals *)
-              rewrite_goal_tac [st_set_def] 3,
+              Goal.rewrite_goal_tac [st_set_def] 3,
               REPEAT (Force_tac 2),
               full_simp_tac (ss addsimps !program_defs_ref) 1,
               ALLGOALS (clarify_tac cs),