moved misc legacy stuff from OldGoals to Misc_Legacy;
authorwenzelm
Mon Jul 12 21:38:37 2010 +0200 (2010-07-12)
changeset 377812fbbf0a48cef
parent 37780 7e91b3f98c46
child 37782 71dd62132eda
moved misc legacy stuff from OldGoals to Misc_Legacy;
OldGoals: removed unused strip_context, metahyps_thms, read_term, read_prop, gethyps;
src/HOL/HOL.thy
src/HOL/IsaMakefile
src/HOL/Tools/meson.ML
src/HOL/Tools/record.ML
src/HOLCF/IOA/meta_theory/automaton.ML
src/Pure/old_goals.ML
src/Tools/misc_legacy.ML
src/ZF/IsaMakefile
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/inductive_package.ML
src/ZF/ZF.thy
     1.1 --- a/src/HOL/HOL.thy	Mon Jul 12 21:12:18 2010 +0200
     1.2 +++ b/src/HOL/HOL.thy	Mon Jul 12 21:38:37 2010 +0200
     1.3 @@ -15,6 +15,7 @@
     1.4    "~~/src/Tools/intuitionistic.ML"
     1.5    "~~/src/Tools/project_rule.ML"
     1.6    "~~/src/Tools/cong_tac.ML"
     1.7 +  "~~/src/Tools/misc_legacy.ML"
     1.8    "~~/src/Provers/hypsubst.ML"
     1.9    "~~/src/Provers/splitter.ML"
    1.10    "~~/src/Provers/classical.ML"
     2.1 --- a/src/HOL/IsaMakefile	Mon Jul 12 21:12:18 2010 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Mon Jul 12 21:38:37 2010 +0200
     2.3 @@ -129,6 +129,7 @@
     2.4    $(SRC)/Tools/induct.ML \
     2.5    $(SRC)/Tools/induct_tacs.ML \
     2.6    $(SRC)/Tools/intuitionistic.ML \
     2.7 +  $(SRC)/Tools/misc_legacy.ML \
     2.8    $(SRC)/Tools/nbe.ML \
     2.9    $(SRC)/Tools/project_rule.ML \
    2.10    $(SRC)/Tools/quickcheck.ML \
     3.1 --- a/src/HOL/Tools/meson.ML	Mon Jul 12 21:12:18 2010 +0200
     3.2 +++ b/src/HOL/Tools/meson.ML	Mon Jul 12 21:38:37 2010 +0200
     3.3 @@ -140,7 +140,7 @@
     3.4                  Display.string_of_thm ctxt st ::
     3.5                  "Premises:" :: map (Display.string_of_thm ctxt) prems))
     3.6    in
     3.7 -    case Seq.pull (ALLGOALS (OldGoals.METAHYPS forward_tacf) st)
     3.8 +    case Seq.pull (ALLGOALS (Misc_Legacy.METAHYPS forward_tacf) st)
     3.9      of SOME(th,_) => th
    3.10       | NONE => raise THM("forward_res", 0, [st])
    3.11    end;
    3.12 @@ -234,7 +234,7 @@
    3.13  fun forward_res2 ctxt nf hyps st =
    3.14    case Seq.pull
    3.15          (REPEAT
    3.16 -         (OldGoals.METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
    3.17 +         (Misc_Legacy.METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
    3.18           st)
    3.19    of SOME(th,_) => th
    3.20     | NONE => raise THM("forward_res2", 0, [st]);
    3.21 @@ -345,8 +345,8 @@
    3.22                (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
    3.23                  all combinations of converting P, Q to CNF.*)
    3.24                let val tac =
    3.25 -                  OldGoals.METAHYPS (resop cnf_nil) 1 THEN
    3.26 -                   (fn st' => st' |> OldGoals.METAHYPS (resop cnf_nil) 1)
    3.27 +                  Misc_Legacy.METAHYPS (resop cnf_nil) 1 THEN
    3.28 +                   (fn st' => st' |> Misc_Legacy.METAHYPS (resop cnf_nil) 1)
    3.29                in  Seq.list_of (tac (th RS disj_forward)) @ ths  end
    3.30            | _ => nodups ctxt th :: ths  (*no work to do*)
    3.31        and cnf_nil th = cnf_aux (th,[])
    3.32 @@ -706,7 +706,7 @@
    3.33    let val ts = Logic.strip_assums_hyp goal
    3.34    in
    3.35      EVERY'
    3.36 -     [OldGoals.METAHYPS (fn hyps =>
    3.37 +     [Misc_Legacy.METAHYPS (fn hyps =>
    3.38          (cut_facts_tac (skolemize_nnf_list ctxt hyps) 1
    3.39            THEN REPEAT (etac exE 1))),
    3.40        REPEAT_DETERM_N (length ts) o (etac thin_rl)] i
     4.1 --- a/src/HOL/Tools/record.ML	Mon Jul 12 21:12:18 2010 +0200
     4.2 +++ b/src/HOL/Tools/record.ML	Mon Jul 12 21:38:37 2010 +0200
     4.3 @@ -273,7 +273,7 @@
     4.4  infix 0 :== ===;
     4.5  infixr 0 ==>;
     4.6  
     4.7 -val op :== = OldGoals.mk_defpair;
     4.8 +val op :== = Misc_Legacy.mk_defpair;
     4.9  val op === = Trueprop o HOLogic.mk_eq;
    4.10  val op ==> = Logic.mk_implies;
    4.11  
     5.1 --- a/src/HOLCF/IOA/meta_theory/automaton.ML	Mon Jul 12 21:12:18 2010 +0200
     5.2 +++ b/src/HOLCF/IOA/meta_theory/automaton.ML	Mon Jul 12 21:38:37 2010 +0200
     5.3 @@ -131,7 +131,7 @@
     5.4  (* making a constructor set from a constructor term (of signature) *)
     5.5  fun constr_set_string thy atyp ctstr =
     5.6  let
     5.7 -val trm = OldGoals.simple_read_term thy atyp ctstr;
     5.8 +val trm = Misc_Legacy.simple_read_term thy atyp ctstr;
     5.9  val l = free_vars_of trm
    5.10  in
    5.11  if (check_for_constr thy atyp trm) then
    5.12 @@ -148,7 +148,7 @@
    5.13  fun hd_of (Const(a,_)) = a |
    5.14  hd_of (t $ _) = hd_of t |
    5.15  hd_of _ = raise malformed;
    5.16 -val trm = OldGoals.simple_read_term thy (Syntax.read_typ_global thy atypstr) s;
    5.17 +val trm = Misc_Legacy.simple_read_term thy (Syntax.read_typ_global thy atypstr) s;
    5.18  in
    5.19  hd_of trm handle malformed =>
    5.20  error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s)
    5.21 @@ -177,8 +177,8 @@
    5.22  (where bool indicates whether there is a precondition *)
    5.23  fun extend thy atyp statetupel (actstr,r,[]) =
    5.24  let
    5.25 -val trm = OldGoals.simple_read_term thy atyp actstr;
    5.26 -val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r;
    5.27 +val trm = Misc_Legacy.simple_read_term thy atyp actstr;
    5.28 +val rtrm = Misc_Legacy.simple_read_term thy (Type("bool",[])) r;
    5.29  val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
    5.30  in
    5.31  if (check_for_constr thy atyp trm)
    5.32 @@ -191,8 +191,8 @@
    5.33  fun pseudo_poststring [] = "" |
    5.34  pseudo_poststring ((a,b)::[]) = "(" ^ a ^ " = (" ^ b ^ "))" |
    5.35  pseudo_poststring ((a,b)::r) = "(" ^ a ^ " = (" ^ b ^ ")) & " ^ (pseudo_poststring r); 
    5.36 -val trm = OldGoals.simple_read_term thy atyp actstr;
    5.37 -val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r;
    5.38 +val trm = Misc_Legacy.simple_read_term thy atyp actstr;
    5.39 +val rtrm = Misc_Legacy.simple_read_term thy (Type("bool",[])) r;
    5.40  val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
    5.41  in
    5.42  if (check_for_constr thy atyp trm) then
    5.43 @@ -366,7 +366,7 @@
    5.44  automaton_name ^ " == (" ^ automaton_name ^ "_asig, " ^ automaton_name ^
    5.45  "_initial, " ^ automaton_name ^ "_trans,{},{})")
    5.46  ])
    5.47 -val chk_prime_list = (check_free_primed (OldGoals.simple_read_term thy2 (Type("bool",[]))
    5.48 +val chk_prime_list = (check_free_primed (Misc_Legacy.simple_read_term thy2 (Type("bool",[]))
    5.49  ( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string))))
    5.50  in
    5.51  (
     6.1 --- a/src/Pure/old_goals.ML	Mon Jul 12 21:12:18 2010 +0200
     6.2 +++ b/src/Pure/old_goals.ML	Mon Jul 12 21:38:37 2010 +0200
     6.3 @@ -10,14 +10,6 @@
     6.4  
     6.5  signature OLD_GOALS =
     6.6  sig
     6.7 -  val mk_defpair: term * term -> string * term
     6.8 -  val strip_context: term -> (string * typ) list * term list * term
     6.9 -  val metahyps_thms: int -> thm -> thm list option
    6.10 -  val METAHYPS: (thm list -> tactic) -> int -> tactic
    6.11 -  val simple_read_term: theory -> typ -> string -> term
    6.12 -  val read_term: theory -> string -> term
    6.13 -  val read_prop: theory -> string -> term
    6.14 -  val get_def: theory -> xstring -> thm
    6.15    type proof
    6.16    val premises: unit -> thm list
    6.17    val reset_goals: unit -> unit
    6.18 @@ -31,7 +23,6 @@
    6.19    val result: unit -> thm
    6.20    val uresult: unit -> thm
    6.21    val getgoal: int -> term
    6.22 -  val gethyps: int -> thm list
    6.23    val print_exn: exn -> 'a
    6.24    val filter_goal: (term*term->bool) -> thm list -> int -> thm list
    6.25    val prlev: int -> unit
    6.26 @@ -67,170 +58,6 @@
    6.27  structure OldGoals: OLD_GOALS =
    6.28  struct
    6.29  
    6.30 -fun mk_defpair (lhs, rhs) =
    6.31 -  (case Term.head_of lhs of
    6.32 -    Const (name, _) =>
    6.33 -      (Long_Name.base_name name ^ "_def", Logic.mk_equals (lhs, rhs))
    6.34 -  | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
    6.35 -
    6.36 -
    6.37 -(**** METAHYPS -- tactical for using hypotheses as meta-level assumptions
    6.38 -       METAHYPS (fn prems => tac prems) i
    6.39 -
    6.40 -converts subgoal i, of the form !!x1...xm. [| A1;...;An] ==> A into a new
    6.41 -proof state A==>A, supplying A1,...,An as meta-level assumptions (in
    6.42 -"prems").  The parameters x1,...,xm become free variables.  If the
    6.43 -resulting proof state is [| B1;...;Bk] ==> C (possibly assuming A1,...,An)
    6.44 -then it is lifted back into the original context, yielding k subgoals.
    6.45 -
    6.46 -Replaces unknowns in the context by Frees having the prefix METAHYP_
    6.47 -New unknowns in [| B1;...;Bk] ==> C are lifted over x1,...,xm.
    6.48 -DOES NOT HANDLE TYPE UNKNOWNS.
    6.49 -
    6.50 -
    6.51 -NOTE: This version does not observe the proof context, and thus cannot
    6.52 -work reliably.  See also Subgoal.SUBPROOF and Subgoal.FOCUS for
    6.53 -properly localized variants of the same idea.
    6.54 -****)
    6.55 -
    6.56 -(*Strips assumptions in goal yielding  ( [x1,...,xm], [H1,...,Hn], B )
    6.57 -    H1,...,Hn are the hypotheses;  x1...xm are variants of the parameters.
    6.58 -  Main difference from strip_assums concerns parameters:
    6.59 -    it replaces the bound variables by free variables.  *)
    6.60 -fun strip_context_aux (params, Hs, Const ("==>", _) $ H $ B) =
    6.61 -      strip_context_aux (params, H :: Hs, B)
    6.62 -  | strip_context_aux (params, Hs, Const ("all",_) $ Abs (a, T, t)) =
    6.63 -      let val (b, u) = Syntax.variant_abs (a, T, t)
    6.64 -      in strip_context_aux ((b, T) :: params, Hs, u) end
    6.65 -  | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);
    6.66 -
    6.67 -fun strip_context A = strip_context_aux ([], [], A);
    6.68 -
    6.69 -local
    6.70 -
    6.71 -  (*Left-to-right replacements: ctpairs = [...,(vi,ti),...].
    6.72 -    Instantiates distinct free variables by terms of same type.*)
    6.73 -  fun free_instantiate ctpairs =
    6.74 -    forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs);
    6.75 -
    6.76 -  fun free_of s ((a, i), T) =
    6.77 -    Free (s ^ (case i of 0 => a | _ => a ^ "_" ^ string_of_int i), T)
    6.78 -
    6.79 -  fun mk_inst v = (Var v, free_of "METAHYP1_" v)
    6.80 -in
    6.81 -
    6.82 -(*Common code for METAHYPS and metahyps_thms*)
    6.83 -fun metahyps_split_prem prem =
    6.84 -  let (*find all vars in the hyps -- should find tvars also!*)
    6.85 -      val hyps_vars = fold Term.add_vars (Logic.strip_assums_hyp prem) []
    6.86 -      val insts = map mk_inst hyps_vars
    6.87 -      (*replace the hyps_vars by Frees*)
    6.88 -      val prem' = subst_atomic insts prem
    6.89 -      val (params,hyps,concl) = strip_context prem'
    6.90 -  in (insts,params,hyps,concl)  end;
    6.91 -
    6.92 -fun metahyps_aux_tac tacf (prem,gno) state =
    6.93 -  let val (insts,params,hyps,concl) = metahyps_split_prem prem
    6.94 -      val maxidx = Thm.maxidx_of state
    6.95 -      val cterm = Thm.cterm_of (Thm.theory_of_thm state)
    6.96 -      val chyps = map cterm hyps
    6.97 -      val hypths = map Thm.assume chyps
    6.98 -      val subprems = map (Thm.forall_elim_vars 0) hypths
    6.99 -      val fparams = map Free params
   6.100 -      val cparams = map cterm fparams
   6.101 -      fun swap_ctpair (t,u) = (cterm u, cterm t)
   6.102 -      (*Subgoal variables: make Free; lift type over params*)
   6.103 -      fun mk_subgoal_inst concl_vars (v, T) =
   6.104 -          if member (op =) concl_vars (v, T)
   6.105 -          then ((v, T), true, free_of "METAHYP2_" (v, T))
   6.106 -          else ((v, T), false, free_of "METAHYP2_" (v, map #2 params ---> T))
   6.107 -      (*Instantiate subgoal vars by Free applied to params*)
   6.108 -      fun mk_ctpair (v, in_concl, u) =
   6.109 -          if in_concl then (cterm (Var v), cterm u)
   6.110 -          else (cterm (Var v), cterm (list_comb (u, fparams)))
   6.111 -      (*Restore Vars with higher type and index*)
   6.112 -      fun mk_subgoal_swap_ctpair (((a, i), T), in_concl, u as Free (_, U)) =
   6.113 -          if in_concl then (cterm u, cterm (Var ((a, i), T)))
   6.114 -          else (cterm u, cterm (Var ((a, i + maxidx), U)))
   6.115 -      (*Embed B in the original context of params and hyps*)
   6.116 -      fun embed B = list_all_free (params, Logic.list_implies (hyps, B))
   6.117 -      (*Strip the context using elimination rules*)
   6.118 -      fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths
   6.119 -      (*A form of lifting that discharges assumptions.*)
   6.120 -      fun relift st =
   6.121 -        let val prop = Thm.prop_of st
   6.122 -            val subgoal_vars = (*Vars introduced in the subgoals*)
   6.123 -              fold Term.add_vars (Logic.strip_imp_prems prop) []
   6.124 -            and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) []
   6.125 -            val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
   6.126 -            val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st
   6.127 -            val emBs = map (cterm o embed) (prems_of st')
   6.128 -            val Cth  = implies_elim_list st' (map (elim o Thm.assume) emBs)
   6.129 -        in  (*restore the unknowns to the hypotheses*)
   6.130 -            free_instantiate (map swap_ctpair insts @
   6.131 -                              map mk_subgoal_swap_ctpair subgoal_insts)
   6.132 -                (*discharge assumptions from state in same order*)
   6.133 -                (implies_intr_list emBs
   6.134 -                  (forall_intr_list cparams (implies_intr_list chyps Cth)))
   6.135 -        end
   6.136 -      (*function to replace the current subgoal*)
   6.137 -      fun next st = Thm.bicompose false (false, relift st, nprems_of st) gno state
   6.138 -  in Seq.maps next (tacf subprems (Thm.trivial (cterm concl))) end;
   6.139 -
   6.140 -end;
   6.141 -
   6.142 -(*Returns the theorem list that METAHYPS would supply to its tactic*)
   6.143 -fun metahyps_thms i state =
   6.144 -  let val prem = Logic.nth_prem (i, Thm.prop_of state)
   6.145 -      and cterm = cterm_of (Thm.theory_of_thm state)
   6.146 -      val (_,_,hyps,_) = metahyps_split_prem prem
   6.147 -  in SOME (map (Thm.forall_elim_vars 0 o Thm.assume o cterm) hyps) end
   6.148 -  handle TERM ("nth_prem", [A]) => NONE;
   6.149 -
   6.150 -local
   6.151 -
   6.152 -fun print_vars_terms n thm =
   6.153 -  let
   6.154 -    val thy = theory_of_thm thm
   6.155 -    fun typed s ty =
   6.156 -      "  " ^ s ^ " has type: " ^ Syntax.string_of_typ_global thy ty;
   6.157 -    fun find_vars (Const (c, ty)) =
   6.158 -          if null (Term.add_tvarsT ty []) then I
   6.159 -          else insert (op =) (typed c ty)
   6.160 -      | find_vars (Var (xi, ty)) =
   6.161 -          insert (op =) (typed (Term.string_of_vname xi) ty)
   6.162 -      | find_vars (Free _) = I
   6.163 -      | find_vars (Bound _) = I
   6.164 -      | find_vars (Abs (_, _, t)) = find_vars t
   6.165 -      | find_vars (t1 $ t2) = find_vars t1 #> find_vars t2;
   6.166 -    val prem = Logic.nth_prem (n, Thm.prop_of thm)
   6.167 -    val tms = find_vars prem []
   6.168 -  in warning (cat_lines ("Found schematic vars in assumptions:" :: tms)) end;
   6.169 -
   6.170 -in
   6.171 -
   6.172 -fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm
   6.173 -  handle THM("assume: variables",_,_) => (print_vars_terms n thm; Seq.empty)
   6.174 -
   6.175 -end;
   6.176 -
   6.177 -
   6.178 -(* old ways of reading terms *)
   6.179 -
   6.180 -fun simple_read_term thy T s =
   6.181 -  let
   6.182 -    val ctxt = ProofContext.init_global thy
   6.183 -      |> ProofContext.allow_dummies
   6.184 -      |> ProofContext.set_mode ProofContext.mode_schematic;
   6.185 -    val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
   6.186 -  in parse ctxt s |> Type_Infer.constrain T |> Syntax.check_term ctxt end;
   6.187 -
   6.188 -fun read_term thy = simple_read_term thy dummyT;
   6.189 -fun read_prop thy = simple_read_term thy propT;
   6.190 -
   6.191 -
   6.192 -fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name;
   6.193 -
   6.194  
   6.195  (*** Goal package ***)
   6.196  
   6.197 @@ -384,7 +211,7 @@
   6.198  
   6.199  (*Version taking the goal as a string*)
   6.200  fun prove_goalw thy rths agoal tacsf =
   6.201 -  let val chorn = cterm_of thy (read_prop thy agoal)
   6.202 +  let val chorn = cterm_of thy (Syntax.read_prop_global thy agoal)
   6.203    in prove_goalw_cterm_general true rths chorn tacsf end
   6.204    handle ERROR msg => cat_error msg (*from read_prop?*)
   6.205                  ("The error(s) above occurred for " ^ quote agoal);
   6.206 @@ -446,15 +273,6 @@
   6.207  (*Get subgoal i from goal stack*)
   6.208  fun getgoal i = Logic.get_goal (prop_of (topthm())) i;
   6.209  
   6.210 -(*Return subgoal i's hypotheses as meta-level assumptions.
   6.211 -  For debugging uses of METAHYPS*)
   6.212 -local exception GETHYPS of thm list
   6.213 -in
   6.214 -fun gethyps i =
   6.215 -    (METAHYPS (fn hyps => raise (GETHYPS hyps)) i (topthm());  [])
   6.216 -    handle GETHYPS hyps => hyps
   6.217 -end;
   6.218 -
   6.219  (*Prints exceptions nicely at top level;
   6.220    raises the exception in order to have a polymorphic type!*)
   6.221  fun print_exn e = (print_sign_exn_unit (Thm.theory_of_thm (topthm())) e;  raise e);
   6.222 @@ -499,7 +317,7 @@
   6.223  
   6.224  (*Version taking the goal as a string*)
   6.225  fun agoalw atomic thy rths agoal =
   6.226 -    agoalw_cterm atomic rths (cterm_of thy (read_prop thy agoal))
   6.227 +    agoalw_cterm atomic rths (cterm_of thy (Syntax.read_prop_global thy agoal))
   6.228      handle ERROR msg => cat_error msg (*from type_assign, etc via prepare_proof*)
   6.229          ("The error(s) above occurred for " ^ quote agoal);
   6.230  
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Tools/misc_legacy.ML	Mon Jul 12 21:38:37 2010 +0200
     7.3 @@ -0,0 +1,163 @@
     7.4 +(*  Title:      Tools/misc_legacy.ML
     7.5 +
     7.6 +Misc legacy stuff -- to be phased out eventually.
     7.7 +*)
     7.8 +
     7.9 +signature MISC_LEGACY =
    7.10 +sig
    7.11 +  val mk_defpair: term * term -> string * term
    7.12 +  val get_def: theory -> xstring -> thm
    7.13 +  val simple_read_term: theory -> typ -> string -> term
    7.14 +  val METAHYPS: (thm list -> tactic) -> int -> tactic
    7.15 +end;
    7.16 +
    7.17 +structure Misc_Legacy: MISC_LEGACY =
    7.18 +struct
    7.19 +
    7.20 +fun mk_defpair (lhs, rhs) =
    7.21 +  (case Term.head_of lhs of
    7.22 +    Const (name, _) =>
    7.23 +      (Long_Name.base_name name ^ "_def", Logic.mk_equals (lhs, rhs))
    7.24 +  | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
    7.25 +
    7.26 +
    7.27 +fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name;
    7.28 +
    7.29 +
    7.30 +fun simple_read_term thy T s =
    7.31 +  let
    7.32 +    val ctxt = ProofContext.init_global thy
    7.33 +      |> ProofContext.allow_dummies
    7.34 +      |> ProofContext.set_mode ProofContext.mode_schematic;
    7.35 +    val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
    7.36 +  in parse ctxt s |> Type_Infer.constrain T |> Syntax.check_term ctxt end;
    7.37 +
    7.38 +
    7.39 +(**** METAHYPS -- tactical for using hypotheses as meta-level assumptions
    7.40 +       METAHYPS (fn prems => tac prems) i
    7.41 +
    7.42 +converts subgoal i, of the form !!x1...xm. [| A1;...;An] ==> A into a new
    7.43 +proof state A==>A, supplying A1,...,An as meta-level assumptions (in
    7.44 +"prems").  The parameters x1,...,xm become free variables.  If the
    7.45 +resulting proof state is [| B1;...;Bk] ==> C (possibly assuming A1,...,An)
    7.46 +then it is lifted back into the original context, yielding k subgoals.
    7.47 +
    7.48 +Replaces unknowns in the context by Frees having the prefix METAHYP_
    7.49 +New unknowns in [| B1;...;Bk] ==> C are lifted over x1,...,xm.
    7.50 +DOES NOT HANDLE TYPE UNKNOWNS.
    7.51 +
    7.52 +
    7.53 +NOTE: This version does not observe the proof context, and thus cannot
    7.54 +work reliably.  See also Subgoal.SUBPROOF and Subgoal.FOCUS for
    7.55 +properly localized variants of the same idea.
    7.56 +****)
    7.57 +
    7.58 +local
    7.59 +
    7.60 +(*Strips assumptions in goal yielding  ( [x1,...,xm], [H1,...,Hn], B )
    7.61 +    H1,...,Hn are the hypotheses;  x1...xm are variants of the parameters.
    7.62 +  Main difference from strip_assums concerns parameters:
    7.63 +    it replaces the bound variables by free variables.  *)
    7.64 +fun strip_context_aux (params, Hs, Const ("==>", _) $ H $ B) =
    7.65 +      strip_context_aux (params, H :: Hs, B)
    7.66 +  | strip_context_aux (params, Hs, Const ("all",_) $ Abs (a, T, t)) =
    7.67 +      let val (b, u) = Syntax.variant_abs (a, T, t)
    7.68 +      in strip_context_aux ((b, T) :: params, Hs, u) end
    7.69 +  | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);
    7.70 +
    7.71 +fun strip_context A = strip_context_aux ([], [], A);
    7.72 +
    7.73 +(*Left-to-right replacements: ctpairs = [...,(vi,ti),...].
    7.74 +  Instantiates distinct free variables by terms of same type.*)
    7.75 +fun free_instantiate ctpairs =
    7.76 +  forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs);
    7.77 +
    7.78 +fun free_of s ((a, i), T) =
    7.79 +  Free (s ^ (case i of 0 => a | _ => a ^ "_" ^ string_of_int i), T)
    7.80 +
    7.81 +fun mk_inst v = (Var v, free_of "METAHYP1_" v)
    7.82 +
    7.83 +fun metahyps_split_prem prem =
    7.84 +  let (*find all vars in the hyps -- should find tvars also!*)
    7.85 +      val hyps_vars = fold Term.add_vars (Logic.strip_assums_hyp prem) []
    7.86 +      val insts = map mk_inst hyps_vars
    7.87 +      (*replace the hyps_vars by Frees*)
    7.88 +      val prem' = subst_atomic insts prem
    7.89 +      val (params,hyps,concl) = strip_context prem'
    7.90 +  in (insts,params,hyps,concl)  end;
    7.91 +
    7.92 +fun metahyps_aux_tac tacf (prem,gno) state =
    7.93 +  let val (insts,params,hyps,concl) = metahyps_split_prem prem
    7.94 +      val maxidx = Thm.maxidx_of state
    7.95 +      val cterm = Thm.cterm_of (Thm.theory_of_thm state)
    7.96 +      val chyps = map cterm hyps
    7.97 +      val hypths = map Thm.assume chyps
    7.98 +      val subprems = map (Thm.forall_elim_vars 0) hypths
    7.99 +      val fparams = map Free params
   7.100 +      val cparams = map cterm fparams
   7.101 +      fun swap_ctpair (t,u) = (cterm u, cterm t)
   7.102 +      (*Subgoal variables: make Free; lift type over params*)
   7.103 +      fun mk_subgoal_inst concl_vars (v, T) =
   7.104 +          if member (op =) concl_vars (v, T)
   7.105 +          then ((v, T), true, free_of "METAHYP2_" (v, T))
   7.106 +          else ((v, T), false, free_of "METAHYP2_" (v, map #2 params ---> T))
   7.107 +      (*Instantiate subgoal vars by Free applied to params*)
   7.108 +      fun mk_ctpair (v, in_concl, u) =
   7.109 +          if in_concl then (cterm (Var v), cterm u)
   7.110 +          else (cterm (Var v), cterm (list_comb (u, fparams)))
   7.111 +      (*Restore Vars with higher type and index*)
   7.112 +      fun mk_subgoal_swap_ctpair (((a, i), T), in_concl, u as Free (_, U)) =
   7.113 +          if in_concl then (cterm u, cterm (Var ((a, i), T)))
   7.114 +          else (cterm u, cterm (Var ((a, i + maxidx), U)))
   7.115 +      (*Embed B in the original context of params and hyps*)
   7.116 +      fun embed B = list_all_free (params, Logic.list_implies (hyps, B))
   7.117 +      (*Strip the context using elimination rules*)
   7.118 +      fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths
   7.119 +      (*A form of lifting that discharges assumptions.*)
   7.120 +      fun relift st =
   7.121 +        let val prop = Thm.prop_of st
   7.122 +            val subgoal_vars = (*Vars introduced in the subgoals*)
   7.123 +              fold Term.add_vars (Logic.strip_imp_prems prop) []
   7.124 +            and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) []
   7.125 +            val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
   7.126 +            val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st
   7.127 +            val emBs = map (cterm o embed) (prems_of st')
   7.128 +            val Cth  = implies_elim_list st' (map (elim o Thm.assume) emBs)
   7.129 +        in  (*restore the unknowns to the hypotheses*)
   7.130 +            free_instantiate (map swap_ctpair insts @
   7.131 +                              map mk_subgoal_swap_ctpair subgoal_insts)
   7.132 +                (*discharge assumptions from state in same order*)
   7.133 +                (implies_intr_list emBs
   7.134 +                  (forall_intr_list cparams (implies_intr_list chyps Cth)))
   7.135 +        end
   7.136 +      (*function to replace the current subgoal*)
   7.137 +      fun next st = Thm.bicompose false (false, relift st, nprems_of st) gno state
   7.138 +  in Seq.maps next (tacf subprems (Thm.trivial (cterm concl))) end;
   7.139 +
   7.140 +fun print_vars_terms n thm =
   7.141 +  let
   7.142 +    val thy = theory_of_thm thm
   7.143 +    fun typed s ty =
   7.144 +      "  " ^ s ^ " has type: " ^ Syntax.string_of_typ_global thy ty;
   7.145 +    fun find_vars (Const (c, ty)) =
   7.146 +          if null (Term.add_tvarsT ty []) then I
   7.147 +          else insert (op =) (typed c ty)
   7.148 +      | find_vars (Var (xi, ty)) =
   7.149 +          insert (op =) (typed (Term.string_of_vname xi) ty)
   7.150 +      | find_vars (Free _) = I
   7.151 +      | find_vars (Bound _) = I
   7.152 +      | find_vars (Abs (_, _, t)) = find_vars t
   7.153 +      | find_vars (t1 $ t2) = find_vars t1 #> find_vars t2;
   7.154 +    val prem = Logic.nth_prem (n, Thm.prop_of thm)
   7.155 +    val tms = find_vars prem []
   7.156 +  in warning (cat_lines ("Found schematic vars in assumptions:" :: tms)) end;
   7.157 +
   7.158 +in
   7.159 +
   7.160 +fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm
   7.161 +  handle THM("assume: variables",_,_) => (print_vars_terms n thm; Seq.empty)
   7.162 +
   7.163 +end;
   7.164 +
   7.165 +end;
   7.166 +
     8.1 --- a/src/ZF/IsaMakefile	Mon Jul 12 21:12:18 2010 +0200
     8.2 +++ b/src/ZF/IsaMakefile	Mon Jul 12 21:38:37 2010 +0200
     8.3 @@ -26,18 +26,19 @@
     8.4  FOL:
     8.5  	@cd $(SRC)/FOL; $(ISABELLE_TOOL) make FOL
     8.6  
     8.7 -$(OUT)/ZF: $(OUT)/FOL AC.thy Arith.thy ArithSimp.thy Bin.thy Bool.thy	\
     8.8 -  Cardinal.thy CardinalArith.thy Cardinal_AC.thy Datatype_ZF.thy	\
     8.9 -  Epsilon.thy EquivClass.thy Finite.thy Fixedpt.thy Inductive_ZF.thy	\
    8.10 -  InfDatatype.thy Int_ZF.thy IntArith.thy IntDiv_ZF.thy List_ZF.thy	\
    8.11 -  Main.thy Main_ZF.thy Main_ZFC.thy Nat_ZF.thy OrdQuant.thy Order.thy	\
    8.12 -  OrderArith.thy OrderType.thy Ordinal.thy Perm.thy QPair.thy		\
    8.13 -  QUniv.thy ROOT.ML Sum.thy Tools/cartprod.ML				\
    8.14 -  Tools/datatype_package.ML Tools/ind_cases.ML Tools/induct_tacs.ML	\
    8.15 -  Tools/inductive_package.ML Tools/numeral_syntax.ML			\
    8.16 -  Tools/primrec_package.ML Tools/typechk.ML Trancl.thy Univ.thy WF.thy	\
    8.17 -  ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy ind_syntax.ML	\
    8.18 -  int_arith.ML pair.thy simpdata.ML upair.thy
    8.19 +$(OUT)/ZF: $(OUT)/FOL $(SRC)/Tools/misc_legacy.ML AC.thy Arith.thy	\
    8.20 +  ArithSimp.thy Bin.thy Bool.thy Cardinal.thy CardinalArith.thy		\
    8.21 +  Cardinal_AC.thy Datatype_ZF.thy Epsilon.thy EquivClass.thy		\
    8.22 +  Finite.thy Fixedpt.thy Inductive_ZF.thy InfDatatype.thy Int_ZF.thy	\
    8.23 +  IntArith.thy IntDiv_ZF.thy List_ZF.thy Main.thy Main_ZF.thy		\
    8.24 +  Main_ZFC.thy Nat_ZF.thy OrdQuant.thy Order.thy OrderArith.thy		\
    8.25 +  OrderType.thy Ordinal.thy Perm.thy QPair.thy QUniv.thy ROOT.ML	\
    8.26 +  Sum.thy Tools/cartprod.ML Tools/datatype_package.ML			\
    8.27 +  Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML	\
    8.28 +  Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML	\
    8.29 +  Trancl.thy Univ.thy WF.thy ZF.thy Zorn.thy arith_data.ML		\
    8.30 +  equalities.thy func.thy ind_syntax.ML int_arith.ML pair.thy		\
    8.31 +  simpdata.ML upair.thy
    8.32  	@$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/FOL ZF
    8.33  
    8.34  
     9.1 --- a/src/ZF/Tools/datatype_package.ML	Mon Jul 12 21:12:18 2010 +0200
     9.2 +++ b/src/ZF/Tools/datatype_package.ML	Mon Jul 12 21:38:37 2010 +0200
     9.3 @@ -108,7 +108,7 @@
     9.4      let val ncon = length con_ty_list    (*number of constructors*)
     9.5          fun mk_def (((id,T,syn), name, args, prems), kcon) =
     9.6                (*kcon is index of constructor*)
     9.7 -            OldGoals.mk_defpair (list_comb (Const (full_name name, T), args),
     9.8 +            Misc_Legacy.mk_defpair (list_comb (Const (full_name name, T), args),
     9.9                          mk_inject npart kpart
    9.10                          (mk_inject ncon kcon (mk_tuple args)))
    9.11      in  ListPair.map mk_def (con_ty_list, 1 upto ncon)  end;
    9.12 @@ -157,7 +157,7 @@
    9.13    val case_const = Const (case_name, case_typ);
    9.14    val case_tm = list_comb (case_const, case_args);
    9.15  
    9.16 -  val case_def = OldGoals.mk_defpair
    9.17 +  val case_def = Misc_Legacy.mk_defpair
    9.18      (case_tm, Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists));
    9.19  
    9.20  
    9.21 @@ -232,7 +232,7 @@
    9.22    val recursor_cases = map call_recursor (flat case_lists ~~ flat recursor_lists);
    9.23  
    9.24    val recursor_def =
    9.25 -      OldGoals.mk_defpair
    9.26 +      Misc_Legacy.mk_defpair
    9.27          (recursor_tm,
    9.28           @{const Univ.Vrecursor} $
    9.29             absfree ("rec", @{typ i}, list_comb (case_const, recursor_cases)));
    9.30 @@ -300,7 +300,7 @@
    9.31  
    9.32    (*** Prove the recursor theorems ***)
    9.33  
    9.34 -  val recursor_eqns = case try (OldGoals.get_def thy1) recursor_base_name of
    9.35 +  val recursor_eqns = case try (Misc_Legacy.get_def thy1) recursor_base_name of
    9.36       NONE => (writeln "  [ No recursion operator ]";
    9.37                [])
    9.38     | SOME recursor_def =>
    10.1 --- a/src/ZF/Tools/inductive_package.ML	Mon Jul 12 21:12:18 2010 +0200
    10.2 +++ b/src/ZF/Tools/inductive_package.ML	Mon Jul 12 21:38:37 2010 +0200
    10.3 @@ -156,7 +156,7 @@
    10.4    val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
    10.5  
    10.6    (*The individual sets must already be declared*)
    10.7 -  val axpairs = map OldGoals.mk_defpair
    10.8 +  val axpairs = map Misc_Legacy.mk_defpair
    10.9          ((big_rec_tm, fp_rhs) ::
   10.10           (case parts of
   10.11               [_] => []                        (*no mutual recursion*)
   10.12 @@ -179,7 +179,7 @@
   10.13  
   10.14    (*fetch fp definitions from the theory*)
   10.15    val big_rec_def::part_rec_defs =
   10.16 -    map (OldGoals.get_def thy1)
   10.17 +    map (Misc_Legacy.get_def thy1)
   10.18          (case rec_names of [_] => rec_names
   10.19                           | _   => big_rec_base_name::rec_names);
   10.20  
    11.1 --- a/src/ZF/ZF.thy	Mon Jul 12 21:12:18 2010 +0200
    11.2 +++ b/src/ZF/ZF.thy	Mon Jul 12 21:38:37 2010 +0200
    11.3 @@ -5,7 +5,10 @@
    11.4  
    11.5  header{*Zermelo-Fraenkel Set Theory*}
    11.6  
    11.7 -theory ZF imports FOL begin
    11.8 +theory ZF
    11.9 +imports FOL
   11.10 +uses "~~/src/Tools/misc_legacy.ML"
   11.11 +begin
   11.12  
   11.13  ML {* Unsynchronized.reset eta_contract *}
   11.14