reorganized structure Goal vs. Tactic;
authorwenzelm
Thu Dec 07 00:42:04 2006 +0100 (2006-12-07)
changeset 21687f689f729afab
parent 21686 4f5f6c685ab4
child 21688 e5287f12f1e1
reorganized structure Goal vs. Tactic;
src/HOL/Tools/record_package.ML
src/Provers/classical.ML
src/Provers/induct_method.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/method.ML
src/Pure/Isar/object_logic.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/ROOT.ML
src/Pure/axclass.ML
src/Pure/goal.ML
src/Pure/simplifier.ML
src/Pure/tactic.ML
src/ZF/UNITY/Constrains.thy
     1.1 --- a/src/HOL/Tools/record_package.ML	Wed Dec 06 21:19:03 2006 +0100
     1.2 +++ b/src/HOL/Tools/record_package.ML	Thu Dec 07 00:42:04 2006 +0100
     1.3 @@ -905,8 +905,8 @@
     1.4      val prove_standard = quick_and_dirty_prove true thy;
     1.5      val thm = prove_standard [] prop (fn prems =>
     1.6  	 EVERY [rtac equal_intr_rule 1, 
     1.7 -                norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1,
     1.8 -                norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1]);
     1.9 +                Goal.norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1,
    1.10 +                Goal.norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1]);
    1.11    in thm end
    1.12    | mk_fun_apply_eq t thy = raise TERM ("mk_fun_apply_eq",[t]);
    1.13  
    1.14 @@ -1649,7 +1649,7 @@
    1.15  
    1.16      fun split_meta_prf () =
    1.17          prove_standard [] split_meta_prop (fn prems =>
    1.18 -         EVERY [rtac equal_intr_rule 1, norm_hhf_tac 1,
    1.19 +         EVERY [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1,
    1.20                  etac meta_allE 1, atac 1,
    1.21                  rtac (prop_subst OF [surjective]) 1,
    1.22                  REPEAT (etac meta_allE 1), atac 1]);
    1.23 @@ -2058,7 +2058,7 @@
    1.24  
    1.25      fun split_meta_prf () =
    1.26          prove false [] split_meta_prop (fn prems =>
    1.27 -         EVERY [rtac equal_intr_rule 1, norm_hhf_tac 1,
    1.28 +         EVERY [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1,
    1.29                  etac meta_allE 1, atac 1,
    1.30                  rtac (prop_subst OF [surjective]) 1,
    1.31                  REPEAT (etac meta_allE 1), atac 1]);
     2.1 --- a/src/Provers/classical.ML	Wed Dec 06 21:19:03 2006 +0100
     2.2 +++ b/src/Provers/classical.ML	Thu Dec 07 00:42:04 2006 +0100
     2.3 @@ -1005,7 +1005,7 @@
     2.4      Method.trace ctxt rules;
     2.5      fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq)
     2.6    end)
     2.7 -  THEN_ALL_NEW Tactic.norm_hhf_tac;
     2.8 +  THEN_ALL_NEW Goal.norm_hhf_tac;
     2.9  
    2.10  fun rule_tac [] ctxt cs facts = some_rule_tac ctxt cs facts
    2.11    | rule_tac rules _ _ facts = Method.rule_tac rules facts;
     3.1 --- a/src/Provers/induct_method.ML	Wed Dec 06 21:19:03 2006 +0100
     3.2 +++ b/src/Provers/induct_method.ML	Thu Dec 07 00:42:04 2006 +0100
     3.3 @@ -162,10 +162,10 @@
     3.4  
     3.5  val atomize_cterm = Tactic.rewrite true Data.atomize;
     3.6  
     3.7 -val atomize_tac = Tactic.rewrite_goal_tac Data.atomize;
     3.8 +val atomize_tac = Goal.rewrite_goal_tac Data.atomize;
     3.9  
    3.10  val inner_atomize_tac =
    3.11 -  Tactic.rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac;
    3.12 +  Goal.rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac;
    3.13  
    3.14  
    3.15  (* rulify *)
    3.16 @@ -182,10 +182,10 @@
    3.17    in (thy, Logic.list_implies (map rulify As, rulify B)) end;
    3.18  
    3.19  val rulify_tac =
    3.20 -  Tactic.rewrite_goal_tac (Data.rulify @ conjunction_congs) THEN'
    3.21 -  Tactic.rewrite_goal_tac Data.rulify_fallback THEN'
    3.22 -  Tactic.conjunction_tac THEN_ALL_NEW
    3.23 -  (Tactic.rewrite_goal_tac [conjunction_imp] THEN' Tactic.norm_hhf_tac);
    3.24 +  Goal.rewrite_goal_tac (Data.rulify @ conjunction_congs) THEN'
    3.25 +  Goal.rewrite_goal_tac Data.rulify_fallback THEN'
    3.26 +  Goal.conjunction_tac THEN_ALL_NEW
    3.27 +  (Goal.rewrite_goal_tac [conjunction_imp] THEN' Goal.norm_hhf_tac);
    3.28  
    3.29  
    3.30  (* prepare rule *)
     4.1 --- a/src/Pure/Isar/local_defs.ML	Wed Dec 06 21:19:03 2006 +0100
     4.2 +++ b/src/Pure/Isar/local_defs.ML	Thu Dec 07 00:42:04 2006 +0100
     4.3 @@ -183,7 +183,7 @@
     4.4        in
     4.5          Goal.prove ctxt' frees [] prop (K (ALLGOALS
     4.6            (meta_rewrite_tac ctxt' THEN'
     4.7 -            Tactic.rewrite_goal_tac [def] THEN'
     4.8 +            Goal.rewrite_goal_tac [def] THEN'
     4.9              Tactic.resolve_tac [Drule.reflexive_thm])))
    4.10          handle ERROR msg => cat_error msg "Failed to prove definitional specification."
    4.11        end;
     5.1 --- a/src/Pure/Isar/method.ML	Wed Dec 06 21:19:03 2006 +0100
     5.2 +++ b/src/Pure/Isar/method.ML	Thu Dec 07 00:42:04 2006 +0100
     5.3 @@ -140,9 +140,9 @@
     5.4  fun RAW_METHOD tac = RAW_METHOD_CASES (NO_CASES o tac);
     5.5  
     5.6  fun METHOD_CASES tac = RAW_METHOD_CASES (fn facts =>
     5.7 -  Seq.THEN (ALLGOALS Tactic.conjunction_tac, tac facts));
     5.8 +  Seq.THEN (ALLGOALS Goal.conjunction_tac, tac facts));
     5.9  
    5.10 -fun METHOD tac = RAW_METHOD (fn facts => ALLGOALS Tactic.conjunction_tac THEN tac facts);
    5.11 +fun METHOD tac = RAW_METHOD (fn facts => ALLGOALS Goal.conjunction_tac THEN tac facts);
    5.12  
    5.13  val fail = METHOD (K no_tac);
    5.14  val succeed = METHOD (K all_tac);
    5.15 @@ -256,7 +256,7 @@
    5.16    (fn i => fn st =>
    5.17      if null facts then tac rules i st
    5.18      else Seq.maps (fn rule => (tac o single) rule i st) (Drule.multi_resolves facts rules))
    5.19 -  THEN_ALL_NEW Tactic.norm_hhf_tac;
    5.20 +  THEN_ALL_NEW Goal.norm_hhf_tac;
    5.21  
    5.22  fun gen_arule_tac tac j rules facts =
    5.23    EVERY' (gen_rule_tac tac rules facts :: replicate j Tactic.assume_tac);
     6.1 --- a/src/Pure/Isar/object_logic.ML	Wed Dec 06 21:19:03 2006 +0100
     6.2 +++ b/src/Pure/Isar/object_logic.ML	Thu Dec 07 00:42:04 2006 +0100
     6.3 @@ -162,7 +162,7 @@
     6.4    else all_tac st;
     6.5  
     6.6  fun full_atomize_tac i st =
     6.7 -  rewrite_goal_tac (get_atomize (Thm.theory_of_thm st)) i st;
     6.8 +  Goal.rewrite_goal_tac (get_atomize (Thm.theory_of_thm st)) i st;
     6.9  
    6.10  fun atomize_goal i st =
    6.11    (case Seq.pull (atomize_tac i st) of NONE => st | SOME (st', _) => st');
    6.12 @@ -171,7 +171,7 @@
    6.13  (* rulify *)
    6.14  
    6.15  fun rulify_term thy = MetaSimplifier.rewrite_term thy (get_rulify thy) [];
    6.16 -fun rulify_tac i st = rewrite_goal_tac (get_rulify (Thm.theory_of_thm st)) i st;
    6.17 +fun rulify_tac i st = Goal.rewrite_goal_tac (get_rulify (Thm.theory_of_thm st)) i st;
    6.18  
    6.19  fun gen_rulify full thm =
    6.20    Tactic.simplify full (get_rulify (Thm.theory_of_thm thm)) thm
     7.1 --- a/src/Pure/Isar/proof.ML	Wed Dec 06 21:19:03 2006 +0100
     7.2 +++ b/src/Pure/Isar/proof.ML	Thu Dec 07 00:42:04 2006 +0100
     7.3 @@ -391,10 +391,10 @@
     7.4  fun select_goals n meth state =
     7.5    state
     7.6    |> (#2 o #2 o get_goal)
     7.7 -  |> ALLGOALS Tactic.conjunction_tac
     7.8 +  |> ALLGOALS Goal.conjunction_tac
     7.9    |> Seq.maps (fn goal =>
    7.10      state
    7.11 -    |> Seq.lift set_goal (Goal.extract 1 n goal |> Seq.maps (Tactic.conjunction_tac 1))
    7.12 +    |> Seq.lift set_goal (Goal.extract 1 n goal |> Seq.maps (Goal.conjunction_tac 1))
    7.13      |> Seq.maps meth
    7.14      |> Seq.maps (fn state' => state'
    7.15        |> Seq.lift set_goal (Goal.retrofit 1 n (#2 (#2 (get_goal state'))) goal))
    7.16 @@ -428,8 +428,8 @@
    7.17  (* refine via sub-proof *)
    7.18  
    7.19  fun goal_tac rule =
    7.20 -  Tactic.norm_hhf_tac THEN' Tactic.rtac rule THEN_ALL_NEW
    7.21 -    (Tactic.norm_hhf_tac THEN' (SUBGOAL (fn (goal, i) =>
    7.22 +  Goal.norm_hhf_tac THEN' Tactic.rtac rule THEN_ALL_NEW
    7.23 +    (Goal.norm_hhf_tac THEN' (SUBGOAL (fn (goal, i) =>
    7.24        if can Logic.unprotect (Logic.strip_assums_concl goal) then
    7.25          Tactic.etac Drule.protectI i
    7.26        else all_tac)));
     8.1 --- a/src/Pure/Isar/proof_context.ML	Wed Dec 06 21:19:03 2006 +0100
     8.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Dec 07 00:42:04 2006 +0100
     8.3 @@ -702,7 +702,7 @@
     8.4    | comp_incr_tac (th :: ths) i st =
     8.5        (Goal.compose_hhf_tac (Drule.incr_indexes st th) i APPEND comp_incr_tac ths i) st;
     8.6  
     8.7 -fun fact_tac facts = Tactic.norm_hhf_tac THEN' comp_incr_tac facts;
     8.8 +fun fact_tac facts = Goal.norm_hhf_tac THEN' comp_incr_tac facts;
     8.9  
    8.10  fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) =>
    8.11    let
     9.1 --- a/src/Pure/ROOT.ML	Wed Dec 06 21:19:03 2006 +0100
     9.2 +++ b/src/Pure/ROOT.ML	Thu Dec 07 00:42:04 2006 +0100
     9.3 @@ -56,10 +56,10 @@
     9.4  use "tctical.ML";
     9.5  use "search.ML";
     9.6  use "meta_simplifier.ML";
     9.7 +use "tactic.ML";
     9.8  use "conjunction.ML";
     9.9  use "assumption.ML";
    9.10  use "goal.ML";
    9.11 -use "tactic.ML";
    9.12  
    9.13  (*proof term operations*)
    9.14  use "Proof/reconstruct.ML";
    10.1 --- a/src/Pure/axclass.ML	Wed Dec 06 21:19:03 2006 +0100
    10.2 +++ b/src/Pure/axclass.ML	Thu Dec 07 00:42:04 2006 +0100
    10.3 @@ -257,7 +257,7 @@
    10.4      val names = map (prefix arity_prefix) (Logic.name_arities arity);
    10.5      val props = Logic.mk_arities arity;
    10.6      val ths = Goal.prove_multi (ProofContext.init thy) [] [] props
    10.7 -      (fn _ => Tactic.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg =>
    10.8 +      (fn _ => Goal.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg =>
    10.9          cat_error msg ("The error(s) above occurred while trying to prove type arity " ^
   10.10            quote (Sign.string_of_arity thy arity));
   10.11    in
    11.1 --- a/src/Pure/goal.ML	Wed Dec 06 21:19:03 2006 +0100
    11.2 +++ b/src/Pure/goal.ML	Thu Dec 07 00:42:04 2006 +0100
    11.3 @@ -8,6 +8,8 @@
    11.4  signature BASIC_GOAL =
    11.5  sig
    11.6    val SELECT_GOAL: tactic -> int -> tactic
    11.7 +  val CONJUNCTS: tactic -> int -> tactic
    11.8 +  val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
    11.9  end;
   11.10  
   11.11  signature GOAL =
   11.12 @@ -19,9 +21,6 @@
   11.13    val finish: thm -> thm
   11.14    val norm_result: thm -> thm
   11.15    val close_result: thm -> thm
   11.16 -  val compose_hhf: thm -> int -> thm -> thm Seq.seq
   11.17 -  val compose_hhf_tac: thm -> int -> tactic
   11.18 -  val comp_hhf: thm -> thm -> thm
   11.19    val prove_raw: cterm list -> cterm -> (thm list -> tactic) -> thm
   11.20    val prove_multi: Proof.context -> string list -> term list -> term list ->
   11.21      ({prems: thm list, context: Proof.context} -> tactic) -> thm list
   11.22 @@ -30,6 +29,14 @@
   11.23    val prove_global: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
   11.24    val extract: int -> int -> thm -> thm Seq.seq
   11.25    val retrofit: int -> int -> thm -> thm -> thm Seq.seq
   11.26 +  val conjunction_tac: int -> tactic
   11.27 +  val precise_conjunction_tac: int -> int -> tactic
   11.28 +  val asm_rewrite_goal_tac: bool * bool * bool -> (simpset -> tactic) -> simpset -> int -> tactic
   11.29 +  val rewrite_goal_tac: thm list -> int -> tactic
   11.30 +  val norm_hhf_tac: int -> tactic
   11.31 +  val compose_hhf: thm -> int -> thm -> thm Seq.seq
   11.32 +  val compose_hhf_tac: thm -> int -> tactic
   11.33 +  val comp_hhf: thm -> thm -> thm
   11.34  end;
   11.35  
   11.36  structure Goal: GOAL =
   11.37 @@ -92,20 +99,6 @@
   11.38    #> Drule.close_derivation;
   11.39  
   11.40  
   11.41 -(* composition of normal results *)
   11.42 -
   11.43 -fun compose_hhf tha i thb =
   11.44 -  Thm.bicompose false (false, Drule.lift_all (Thm.cprem_of thb i) tha, 0) i thb;
   11.45 -
   11.46 -fun compose_hhf_tac th i = PRIMSEQ (compose_hhf th i);
   11.47 -
   11.48 -fun comp_hhf tha thb =
   11.49 -  (case Seq.chop 2 (compose_hhf tha 1 thb) of
   11.50 -    ([th], _) => th
   11.51 -  | ([], _) => raise THM ("comp_hhf: no unifiers", 1, [tha, thb])
   11.52 -  | _  => raise THM ("comp_hhf: multiple unifiers", 1, [tha, thb]));
   11.53 -
   11.54 -
   11.55  
   11.56  (** tactical theorem proving **)
   11.57  
   11.58 @@ -164,7 +157,9 @@
   11.59  
   11.60  
   11.61  
   11.62 -(** local goal states **)
   11.63 +(** goal structure **)
   11.64 +
   11.65 +(* nested goals *)
   11.66  
   11.67  fun extract i n st =
   11.68    (if i < 1 orelse n < 1 orelse i + n - 1 > Thm.nprems_of st then Seq.empty
   11.69 @@ -181,6 +176,66 @@
   11.70    if Thm.nprems_of st = 1 andalso i = 1 then tac st
   11.71    else Seq.lifts (retrofit i 1) (Seq.maps tac (extract i 1 st)) st;
   11.72  
   11.73 +
   11.74 +(* multiple goals *)
   11.75 +
   11.76 +val conj_tac = SUBGOAL (fn (goal, i) =>
   11.77 +  if can Logic.dest_conjunction goal then rtac Conjunction.conjunctionI i
   11.78 +  else no_tac);
   11.79 +
   11.80 +val conjunction_tac = TRY o REPEAT_ALL_NEW conj_tac;
   11.81 +
   11.82 +val precise_conjunction_tac =
   11.83 +  let
   11.84 +    fun tac 0 i = eq_assume_tac i
   11.85 +      | tac 1 i = SUBGOAL (K all_tac) i
   11.86 +      | tac n i = conj_tac i THEN TRY (fn st => tac (n - 1) (i + 1) st);
   11.87 +  in TRY oo tac end;
   11.88 +
   11.89 +fun CONJUNCTS tac =
   11.90 +  SELECT_GOAL (conjunction_tac 1
   11.91 +    THEN tac
   11.92 +    THEN PRIMITIVE (Conjunction.uncurry ~1));
   11.93 +
   11.94 +fun PRECISE_CONJUNCTS n tac =
   11.95 +  SELECT_GOAL (precise_conjunction_tac n 1
   11.96 +    THEN tac
   11.97 +    THEN PRIMITIVE (Conjunction.uncurry ~1));
   11.98 +
   11.99 +
  11.100 +(* rewriting *)
  11.101 +
  11.102 +(*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)
  11.103 +fun asm_rewrite_goal_tac mode prover_tac ss =
  11.104 +  SELECT_GOAL
  11.105 +    (PRIMITIVE (MetaSimplifier.rewrite_goal_rule mode (SINGLE o prover_tac) ss 1));
  11.106 +
  11.107 +fun rewrite_goal_tac rews =
  11.108 +  let val ss = MetaSimplifier.empty_ss addsimps rews in
  11.109 +    fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac)
  11.110 +      (MetaSimplifier.theory_context (Thm.theory_of_thm st) ss) i st
  11.111 +  end;
  11.112 +
  11.113 +
  11.114 +(* hhf normal form *)
  11.115 +
  11.116 +val norm_hhf_tac =
  11.117 +  rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
  11.118 +  THEN' SUBGOAL (fn (t, i) =>
  11.119 +    if Drule.is_norm_hhf t then all_tac
  11.120 +    else rewrite_goal_tac [Drule.norm_hhf_eq] i);
  11.121 +
  11.122 +fun compose_hhf tha i thb =
  11.123 +  Thm.bicompose false (false, Drule.lift_all (Thm.cprem_of thb i) tha, 0) i thb;
  11.124 +
  11.125 +fun compose_hhf_tac th i = PRIMSEQ (compose_hhf th i);
  11.126 +
  11.127 +fun comp_hhf tha thb =
  11.128 +  (case Seq.chop 2 (compose_hhf tha 1 thb) of
  11.129 +    ([th], _) => th
  11.130 +  | ([], _) => raise THM ("comp_hhf: no unifiers", 1, [tha, thb])
  11.131 +  | _  => raise THM ("comp_hhf: multiple unifiers", 1, [tha, thb]));
  11.132 +
  11.133  end;
  11.134  
  11.135  structure BasicGoal: BASIC_GOAL = Goal;
    12.1 --- a/src/Pure/simplifier.ML	Wed Dec 06 21:19:03 2006 +0100
    12.2 +++ b/src/Pure/simplifier.ML	Thu Dec 07 00:42:04 2006 +0100
    12.3 @@ -166,7 +166,7 @@
    12.4        (if safe then solvers else unsafe_solvers));
    12.5  
    12.6      fun simp_loop_tac i =
    12.7 -      asm_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN
    12.8 +      Goal.asm_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN
    12.9        (solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i));
   12.10    in simp_loop_tac end;
   12.11  
    13.1 --- a/src/Pure/tactic.ML	Wed Dec 06 21:19:03 2006 +0100
    13.2 +++ b/src/Pure/tactic.ML	Thu Dec 07 00:42:04 2006 +0100
    13.3 @@ -69,7 +69,6 @@
    13.4    val net_biresolve_tac : (bool*thm) list -> int -> tactic
    13.5    val net_match_tac     : thm list -> int -> tactic
    13.6    val net_resolve_tac   : thm list -> int -> tactic
    13.7 -  val norm_hhf_tac      : int -> tactic
    13.8    val prune_params_tac  : tactic
    13.9    val rename_params_tac : string list -> int -> tactic
   13.10    val rename_tac        : string -> int -> tactic
   13.11 @@ -77,12 +76,10 @@
   13.12    val resolve_from_net_tac      : (int*thm) Net.net -> int -> tactic
   13.13    val resolve_tac       : thm list -> int -> tactic
   13.14    val res_inst_tac      : (string*string)list -> thm -> int -> tactic
   13.15 -  val rewrite_goal_tac  : thm list -> int -> tactic
   13.16    val rewrite_goals_rule: thm list -> thm -> thm
   13.17    val rewrite_rule      : thm list -> thm -> thm
   13.18    val rewrite_goals_tac : thm list -> tactic
   13.19    val rewrite_tac       : thm list -> tactic
   13.20 -  val asm_rewrite_goal_tac: bool * bool * bool -> (simpset -> tactic) -> simpset -> int -> tactic
   13.21    val rewtac            : thm -> tactic
   13.22    val rotate_tac        : int -> int -> tactic
   13.23    val rtac              : thm -> int -> tactic
   13.24 @@ -97,8 +94,6 @@
   13.25    val instantiate_tac   : (string * string) list -> tactic
   13.26    val thin_tac          : string -> int -> tactic
   13.27    val trace_goalno_tac  : (int -> tactic) -> int -> tactic
   13.28 -  val CONJUNCTS: tactic -> int -> tactic
   13.29 -  val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
   13.30  end;
   13.31  
   13.32  signature TACTIC =
   13.33 @@ -110,8 +105,6 @@
   13.34    val orderlist: (int * 'a) list -> 'a list
   13.35    val rewrite: bool -> thm list -> cterm -> thm
   13.36    val simplify: bool -> thm list -> thm -> thm
   13.37 -  val conjunction_tac: int -> tactic
   13.38 -  val precise_conjunction_tac: int -> int -> tactic
   13.39    val compose_inst_tac' : (indexname * string) list -> (bool * thm * int) ->
   13.40                            int -> tactic
   13.41    val lift_inst_rule'   : thm * int * (indexname * string) list * thm -> thm
   13.42 @@ -529,17 +522,6 @@
   13.43  val rewrite_rule = simplify true;
   13.44  val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover;
   13.45  
   13.46 -(*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)
   13.47 -fun asm_rewrite_goal_tac mode prover_tac ss =
   13.48 -  SELECT_GOAL
   13.49 -    (PRIMITIVE (MetaSimplifier.rewrite_goal_rule mode (SINGLE o prover_tac) ss 1));
   13.50 -
   13.51 -fun rewrite_goal_tac rews =
   13.52 -  let val ss = MetaSimplifier.empty_ss addsimps rews in
   13.53 -    fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac)
   13.54 -      (MetaSimplifier.theory_context (Thm.theory_of_thm st) ss) i st
   13.55 -  end;
   13.56 -
   13.57  (*Rewrite throughout proof state. *)
   13.58  fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
   13.59  
   13.60 @@ -547,12 +529,6 @@
   13.61  fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
   13.62  fun rewtac def = rewrite_goals_tac [def];
   13.63  
   13.64 -val norm_hhf_tac =
   13.65 -  rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
   13.66 -  THEN' SUBGOAL (fn (t, i) =>
   13.67 -    if Drule.is_norm_hhf t then all_tac
   13.68 -    else rewrite_goal_tac [Drule.norm_hhf_eq] i);
   13.69 -
   13.70  
   13.71  (*** for folding definitions, handling critical pairs ***)
   13.72  
   13.73 @@ -633,32 +609,6 @@
   13.74         end)
   13.75    end;
   13.76  
   13.77 -
   13.78 -(* meta-level conjunction *)
   13.79 -
   13.80 -val conj_tac = SUBGOAL (fn (goal, i) =>
   13.81 -  if can Logic.dest_conjunction goal then rtac Conjunction.conjunctionI i
   13.82 -  else no_tac);
   13.83 -
   13.84 -val conjunction_tac = TRY o REPEAT_ALL_NEW conj_tac;
   13.85 -
   13.86 -val precise_conjunction_tac =
   13.87 -  let
   13.88 -    fun tac 0 i = eq_assume_tac i
   13.89 -      | tac 1 i = SUBGOAL (K all_tac) i
   13.90 -      | tac n i = conj_tac i THEN TRY (fn st => tac (n - 1) (i + 1) st);
   13.91 -  in TRY oo tac end;
   13.92 -
   13.93 -fun CONJUNCTS tac =
   13.94 -  SELECT_GOAL (conjunction_tac 1
   13.95 -    THEN tac
   13.96 -    THEN PRIMITIVE (Conjunction.uncurry ~1));
   13.97 -
   13.98 -fun PRECISE_CONJUNCTS n tac =
   13.99 -  SELECT_GOAL (precise_conjunction_tac n 1
  13.100 -    THEN tac
  13.101 -    THEN PRIMITIVE (Conjunction.uncurry ~1));
  13.102 -
  13.103  end;
  13.104  
  13.105  structure BasicTactic: BASIC_TACTIC = Tactic;
    14.1 --- a/src/ZF/UNITY/Constrains.thy	Wed Dec 06 21:19:03 2006 +0100
    14.2 +++ b/src/ZF/UNITY/Constrains.thy	Thu Dec 07 00:42:04 2006 +0100
    14.3 @@ -546,7 +546,7 @@
    14.4                                     constrains_imp_Constrains] 1),
    14.5                rtac constrainsI 1,
    14.6                (* Three subgoals *)
    14.7 -              rewrite_goal_tac [st_set_def] 3,
    14.8 +              Goal.rewrite_goal_tac [st_set_def] 3,
    14.9                REPEAT (Force_tac 2),
   14.10                full_simp_tac (ss addsimps !program_defs_ref) 1,
   14.11                ALLGOALS (clarify_tac cs),