moved misc legacy stuff from OldGoals to Misc_Legacy;
OldGoals: removed unused strip_context, metahyps_thms, read_term, read_prop, gethyps;
--- a/src/HOL/HOL.thy Mon Jul 12 21:12:18 2010 +0200
+++ b/src/HOL/HOL.thy Mon Jul 12 21:38:37 2010 +0200
@@ -15,6 +15,7 @@
"~~/src/Tools/intuitionistic.ML"
"~~/src/Tools/project_rule.ML"
"~~/src/Tools/cong_tac.ML"
+ "~~/src/Tools/misc_legacy.ML"
"~~/src/Provers/hypsubst.ML"
"~~/src/Provers/splitter.ML"
"~~/src/Provers/classical.ML"
--- a/src/HOL/IsaMakefile Mon Jul 12 21:12:18 2010 +0200
+++ b/src/HOL/IsaMakefile Mon Jul 12 21:38:37 2010 +0200
@@ -129,6 +129,7 @@
$(SRC)/Tools/induct.ML \
$(SRC)/Tools/induct_tacs.ML \
$(SRC)/Tools/intuitionistic.ML \
+ $(SRC)/Tools/misc_legacy.ML \
$(SRC)/Tools/nbe.ML \
$(SRC)/Tools/project_rule.ML \
$(SRC)/Tools/quickcheck.ML \
--- a/src/HOL/Tools/meson.ML Mon Jul 12 21:12:18 2010 +0200
+++ b/src/HOL/Tools/meson.ML Mon Jul 12 21:38:37 2010 +0200
@@ -140,7 +140,7 @@
Display.string_of_thm ctxt st ::
"Premises:" :: map (Display.string_of_thm ctxt) prems))
in
- case Seq.pull (ALLGOALS (OldGoals.METAHYPS forward_tacf) st)
+ case Seq.pull (ALLGOALS (Misc_Legacy.METAHYPS forward_tacf) st)
of SOME(th,_) => th
| NONE => raise THM("forward_res", 0, [st])
end;
@@ -234,7 +234,7 @@
fun forward_res2 ctxt nf hyps st =
case Seq.pull
(REPEAT
- (OldGoals.METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
+ (Misc_Legacy.METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
st)
of SOME(th,_) => th
| NONE => raise THM("forward_res2", 0, [st]);
@@ -345,8 +345,8 @@
(*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
all combinations of converting P, Q to CNF.*)
let val tac =
- OldGoals.METAHYPS (resop cnf_nil) 1 THEN
- (fn st' => st' |> OldGoals.METAHYPS (resop cnf_nil) 1)
+ Misc_Legacy.METAHYPS (resop cnf_nil) 1 THEN
+ (fn st' => st' |> Misc_Legacy.METAHYPS (resop cnf_nil) 1)
in Seq.list_of (tac (th RS disj_forward)) @ ths end
| _ => nodups ctxt th :: ths (*no work to do*)
and cnf_nil th = cnf_aux (th,[])
@@ -706,7 +706,7 @@
let val ts = Logic.strip_assums_hyp goal
in
EVERY'
- [OldGoals.METAHYPS (fn hyps =>
+ [Misc_Legacy.METAHYPS (fn hyps =>
(cut_facts_tac (skolemize_nnf_list ctxt hyps) 1
THEN REPEAT (etac exE 1))),
REPEAT_DETERM_N (length ts) o (etac thin_rl)] i
--- a/src/HOL/Tools/record.ML Mon Jul 12 21:12:18 2010 +0200
+++ b/src/HOL/Tools/record.ML Mon Jul 12 21:38:37 2010 +0200
@@ -273,7 +273,7 @@
infix 0 :== ===;
infixr 0 ==>;
-val op :== = OldGoals.mk_defpair;
+val op :== = Misc_Legacy.mk_defpair;
val op === = Trueprop o HOLogic.mk_eq;
val op ==> = Logic.mk_implies;
--- a/src/HOLCF/IOA/meta_theory/automaton.ML Mon Jul 12 21:12:18 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/automaton.ML Mon Jul 12 21:38:37 2010 +0200
@@ -131,7 +131,7 @@
(* making a constructor set from a constructor term (of signature) *)
fun constr_set_string thy atyp ctstr =
let
-val trm = OldGoals.simple_read_term thy atyp ctstr;
+val trm = Misc_Legacy.simple_read_term thy atyp ctstr;
val l = free_vars_of trm
in
if (check_for_constr thy atyp trm) then
@@ -148,7 +148,7 @@
fun hd_of (Const(a,_)) = a |
hd_of (t $ _) = hd_of t |
hd_of _ = raise malformed;
-val trm = OldGoals.simple_read_term thy (Syntax.read_typ_global thy atypstr) s;
+val trm = Misc_Legacy.simple_read_term thy (Syntax.read_typ_global thy atypstr) s;
in
hd_of trm handle malformed =>
error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s)
@@ -177,8 +177,8 @@
(where bool indicates whether there is a precondition *)
fun extend thy atyp statetupel (actstr,r,[]) =
let
-val trm = OldGoals.simple_read_term thy atyp actstr;
-val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r;
+val trm = Misc_Legacy.simple_read_term thy atyp actstr;
+val rtrm = Misc_Legacy.simple_read_term thy (Type("bool",[])) r;
val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
in
if (check_for_constr thy atyp trm)
@@ -191,8 +191,8 @@
fun pseudo_poststring [] = "" |
pseudo_poststring ((a,b)::[]) = "(" ^ a ^ " = (" ^ b ^ "))" |
pseudo_poststring ((a,b)::r) = "(" ^ a ^ " = (" ^ b ^ ")) & " ^ (pseudo_poststring r);
-val trm = OldGoals.simple_read_term thy atyp actstr;
-val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r;
+val trm = Misc_Legacy.simple_read_term thy atyp actstr;
+val rtrm = Misc_Legacy.simple_read_term thy (Type("bool",[])) r;
val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
in
if (check_for_constr thy atyp trm) then
@@ -366,7 +366,7 @@
automaton_name ^ " == (" ^ automaton_name ^ "_asig, " ^ automaton_name ^
"_initial, " ^ automaton_name ^ "_trans,{},{})")
])
-val chk_prime_list = (check_free_primed (OldGoals.simple_read_term thy2 (Type("bool",[]))
+val chk_prime_list = (check_free_primed (Misc_Legacy.simple_read_term thy2 (Type("bool",[]))
( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string))))
in
(
--- a/src/Pure/old_goals.ML Mon Jul 12 21:12:18 2010 +0200
+++ b/src/Pure/old_goals.ML Mon Jul 12 21:38:37 2010 +0200
@@ -10,14 +10,6 @@
signature OLD_GOALS =
sig
- val mk_defpair: term * term -> string * term
- val strip_context: term -> (string * typ) list * term list * term
- val metahyps_thms: int -> thm -> thm list option
- val METAHYPS: (thm list -> tactic) -> int -> tactic
- val simple_read_term: theory -> typ -> string -> term
- val read_term: theory -> string -> term
- val read_prop: theory -> string -> term
- val get_def: theory -> xstring -> thm
type proof
val premises: unit -> thm list
val reset_goals: unit -> unit
@@ -31,7 +23,6 @@
val result: unit -> thm
val uresult: unit -> thm
val getgoal: int -> term
- val gethyps: int -> thm list
val print_exn: exn -> 'a
val filter_goal: (term*term->bool) -> thm list -> int -> thm list
val prlev: int -> unit
@@ -67,170 +58,6 @@
structure OldGoals: OLD_GOALS =
struct
-fun mk_defpair (lhs, rhs) =
- (case Term.head_of lhs of
- Const (name, _) =>
- (Long_Name.base_name name ^ "_def", Logic.mk_equals (lhs, rhs))
- | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
-
-
-(**** METAHYPS -- tactical for using hypotheses as meta-level assumptions
- METAHYPS (fn prems => tac prems) i
-
-converts subgoal i, of the form !!x1...xm. [| A1;...;An] ==> A into a new
-proof state A==>A, supplying A1,...,An as meta-level assumptions (in
-"prems"). The parameters x1,...,xm become free variables. If the
-resulting proof state is [| B1;...;Bk] ==> C (possibly assuming A1,...,An)
-then it is lifted back into the original context, yielding k subgoals.
-
-Replaces unknowns in the context by Frees having the prefix METAHYP_
-New unknowns in [| B1;...;Bk] ==> C are lifted over x1,...,xm.
-DOES NOT HANDLE TYPE UNKNOWNS.
-
-
-NOTE: This version does not observe the proof context, and thus cannot
-work reliably. See also Subgoal.SUBPROOF and Subgoal.FOCUS for
-properly localized variants of the same idea.
-****)
-
-(*Strips assumptions in goal yielding ( [x1,...,xm], [H1,...,Hn], B )
- H1,...,Hn are the hypotheses; x1...xm are variants of the parameters.
- Main difference from strip_assums concerns parameters:
- it replaces the bound variables by free variables. *)
-fun strip_context_aux (params, Hs, Const ("==>", _) $ H $ B) =
- strip_context_aux (params, H :: Hs, B)
- | strip_context_aux (params, Hs, Const ("all",_) $ Abs (a, T, t)) =
- let val (b, u) = Syntax.variant_abs (a, T, t)
- in strip_context_aux ((b, T) :: params, Hs, u) end
- | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);
-
-fun strip_context A = strip_context_aux ([], [], A);
-
-local
-
- (*Left-to-right replacements: ctpairs = [...,(vi,ti),...].
- Instantiates distinct free variables by terms of same type.*)
- fun free_instantiate ctpairs =
- forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs);
-
- fun free_of s ((a, i), T) =
- Free (s ^ (case i of 0 => a | _ => a ^ "_" ^ string_of_int i), T)
-
- fun mk_inst v = (Var v, free_of "METAHYP1_" v)
-in
-
-(*Common code for METAHYPS and metahyps_thms*)
-fun metahyps_split_prem prem =
- let (*find all vars in the hyps -- should find tvars also!*)
- val hyps_vars = fold Term.add_vars (Logic.strip_assums_hyp prem) []
- val insts = map mk_inst hyps_vars
- (*replace the hyps_vars by Frees*)
- val prem' = subst_atomic insts prem
- val (params,hyps,concl) = strip_context prem'
- in (insts,params,hyps,concl) end;
-
-fun metahyps_aux_tac tacf (prem,gno) state =
- let val (insts,params,hyps,concl) = metahyps_split_prem prem
- val maxidx = Thm.maxidx_of state
- val cterm = Thm.cterm_of (Thm.theory_of_thm state)
- val chyps = map cterm hyps
- val hypths = map Thm.assume chyps
- val subprems = map (Thm.forall_elim_vars 0) hypths
- val fparams = map Free params
- val cparams = map cterm fparams
- fun swap_ctpair (t,u) = (cterm u, cterm t)
- (*Subgoal variables: make Free; lift type over params*)
- fun mk_subgoal_inst concl_vars (v, T) =
- if member (op =) concl_vars (v, T)
- then ((v, T), true, free_of "METAHYP2_" (v, T))
- else ((v, T), false, free_of "METAHYP2_" (v, map #2 params ---> T))
- (*Instantiate subgoal vars by Free applied to params*)
- fun mk_ctpair (v, in_concl, u) =
- if in_concl then (cterm (Var v), cterm u)
- else (cterm (Var v), cterm (list_comb (u, fparams)))
- (*Restore Vars with higher type and index*)
- fun mk_subgoal_swap_ctpair (((a, i), T), in_concl, u as Free (_, U)) =
- if in_concl then (cterm u, cterm (Var ((a, i), T)))
- else (cterm u, cterm (Var ((a, i + maxidx), U)))
- (*Embed B in the original context of params and hyps*)
- fun embed B = list_all_free (params, Logic.list_implies (hyps, B))
- (*Strip the context using elimination rules*)
- fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths
- (*A form of lifting that discharges assumptions.*)
- fun relift st =
- let val prop = Thm.prop_of st
- val subgoal_vars = (*Vars introduced in the subgoals*)
- fold Term.add_vars (Logic.strip_imp_prems prop) []
- and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) []
- val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
- val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st
- val emBs = map (cterm o embed) (prems_of st')
- val Cth = implies_elim_list st' (map (elim o Thm.assume) emBs)
- in (*restore the unknowns to the hypotheses*)
- free_instantiate (map swap_ctpair insts @
- map mk_subgoal_swap_ctpair subgoal_insts)
- (*discharge assumptions from state in same order*)
- (implies_intr_list emBs
- (forall_intr_list cparams (implies_intr_list chyps Cth)))
- end
- (*function to replace the current subgoal*)
- fun next st = Thm.bicompose false (false, relift st, nprems_of st) gno state
- in Seq.maps next (tacf subprems (Thm.trivial (cterm concl))) end;
-
-end;
-
-(*Returns the theorem list that METAHYPS would supply to its tactic*)
-fun metahyps_thms i state =
- let val prem = Logic.nth_prem (i, Thm.prop_of state)
- and cterm = cterm_of (Thm.theory_of_thm state)
- val (_,_,hyps,_) = metahyps_split_prem prem
- in SOME (map (Thm.forall_elim_vars 0 o Thm.assume o cterm) hyps) end
- handle TERM ("nth_prem", [A]) => NONE;
-
-local
-
-fun print_vars_terms n thm =
- let
- val thy = theory_of_thm thm
- fun typed s ty =
- " " ^ s ^ " has type: " ^ Syntax.string_of_typ_global thy ty;
- fun find_vars (Const (c, ty)) =
- if null (Term.add_tvarsT ty []) then I
- else insert (op =) (typed c ty)
- | find_vars (Var (xi, ty)) =
- insert (op =) (typed (Term.string_of_vname xi) ty)
- | find_vars (Free _) = I
- | find_vars (Bound _) = I
- | find_vars (Abs (_, _, t)) = find_vars t
- | find_vars (t1 $ t2) = find_vars t1 #> find_vars t2;
- val prem = Logic.nth_prem (n, Thm.prop_of thm)
- val tms = find_vars prem []
- in warning (cat_lines ("Found schematic vars in assumptions:" :: tms)) end;
-
-in
-
-fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm
- handle THM("assume: variables",_,_) => (print_vars_terms n thm; Seq.empty)
-
-end;
-
-
-(* old ways of reading terms *)
-
-fun simple_read_term thy T s =
- let
- val ctxt = ProofContext.init_global thy
- |> ProofContext.allow_dummies
- |> ProofContext.set_mode ProofContext.mode_schematic;
- val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
- in parse ctxt s |> Type_Infer.constrain T |> Syntax.check_term ctxt end;
-
-fun read_term thy = simple_read_term thy dummyT;
-fun read_prop thy = simple_read_term thy propT;
-
-
-fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name;
-
(*** Goal package ***)
@@ -384,7 +211,7 @@
(*Version taking the goal as a string*)
fun prove_goalw thy rths agoal tacsf =
- let val chorn = cterm_of thy (read_prop thy agoal)
+ let val chorn = cterm_of thy (Syntax.read_prop_global thy agoal)
in prove_goalw_cterm_general true rths chorn tacsf end
handle ERROR msg => cat_error msg (*from read_prop?*)
("The error(s) above occurred for " ^ quote agoal);
@@ -446,15 +273,6 @@
(*Get subgoal i from goal stack*)
fun getgoal i = Logic.get_goal (prop_of (topthm())) i;
-(*Return subgoal i's hypotheses as meta-level assumptions.
- For debugging uses of METAHYPS*)
-local exception GETHYPS of thm list
-in
-fun gethyps i =
- (METAHYPS (fn hyps => raise (GETHYPS hyps)) i (topthm()); [])
- handle GETHYPS hyps => hyps
-end;
-
(*Prints exceptions nicely at top level;
raises the exception in order to have a polymorphic type!*)
fun print_exn e = (print_sign_exn_unit (Thm.theory_of_thm (topthm())) e; raise e);
@@ -499,7 +317,7 @@
(*Version taking the goal as a string*)
fun agoalw atomic thy rths agoal =
- agoalw_cterm atomic rths (cterm_of thy (read_prop thy agoal))
+ agoalw_cterm atomic rths (cterm_of thy (Syntax.read_prop_global thy agoal))
handle ERROR msg => cat_error msg (*from type_assign, etc via prepare_proof*)
("The error(s) above occurred for " ^ quote agoal);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/misc_legacy.ML Mon Jul 12 21:38:37 2010 +0200
@@ -0,0 +1,163 @@
+(* Title: Tools/misc_legacy.ML
+
+Misc legacy stuff -- to be phased out eventually.
+*)
+
+signature MISC_LEGACY =
+sig
+ val mk_defpair: term * term -> string * term
+ val get_def: theory -> xstring -> thm
+ val simple_read_term: theory -> typ -> string -> term
+ val METAHYPS: (thm list -> tactic) -> int -> tactic
+end;
+
+structure Misc_Legacy: MISC_LEGACY =
+struct
+
+fun mk_defpair (lhs, rhs) =
+ (case Term.head_of lhs of
+ Const (name, _) =>
+ (Long_Name.base_name name ^ "_def", Logic.mk_equals (lhs, rhs))
+ | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
+
+
+fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name;
+
+
+fun simple_read_term thy T s =
+ let
+ val ctxt = ProofContext.init_global thy
+ |> ProofContext.allow_dummies
+ |> ProofContext.set_mode ProofContext.mode_schematic;
+ val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
+ in parse ctxt s |> Type_Infer.constrain T |> Syntax.check_term ctxt end;
+
+
+(**** METAHYPS -- tactical for using hypotheses as meta-level assumptions
+ METAHYPS (fn prems => tac prems) i
+
+converts subgoal i, of the form !!x1...xm. [| A1;...;An] ==> A into a new
+proof state A==>A, supplying A1,...,An as meta-level assumptions (in
+"prems"). The parameters x1,...,xm become free variables. If the
+resulting proof state is [| B1;...;Bk] ==> C (possibly assuming A1,...,An)
+then it is lifted back into the original context, yielding k subgoals.
+
+Replaces unknowns in the context by Frees having the prefix METAHYP_
+New unknowns in [| B1;...;Bk] ==> C are lifted over x1,...,xm.
+DOES NOT HANDLE TYPE UNKNOWNS.
+
+
+NOTE: This version does not observe the proof context, and thus cannot
+work reliably. See also Subgoal.SUBPROOF and Subgoal.FOCUS for
+properly localized variants of the same idea.
+****)
+
+local
+
+(*Strips assumptions in goal yielding ( [x1,...,xm], [H1,...,Hn], B )
+ H1,...,Hn are the hypotheses; x1...xm are variants of the parameters.
+ Main difference from strip_assums concerns parameters:
+ it replaces the bound variables by free variables. *)
+fun strip_context_aux (params, Hs, Const ("==>", _) $ H $ B) =
+ strip_context_aux (params, H :: Hs, B)
+ | strip_context_aux (params, Hs, Const ("all",_) $ Abs (a, T, t)) =
+ let val (b, u) = Syntax.variant_abs (a, T, t)
+ in strip_context_aux ((b, T) :: params, Hs, u) end
+ | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);
+
+fun strip_context A = strip_context_aux ([], [], A);
+
+(*Left-to-right replacements: ctpairs = [...,(vi,ti),...].
+ Instantiates distinct free variables by terms of same type.*)
+fun free_instantiate ctpairs =
+ forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs);
+
+fun free_of s ((a, i), T) =
+ Free (s ^ (case i of 0 => a | _ => a ^ "_" ^ string_of_int i), T)
+
+fun mk_inst v = (Var v, free_of "METAHYP1_" v)
+
+fun metahyps_split_prem prem =
+ let (*find all vars in the hyps -- should find tvars also!*)
+ val hyps_vars = fold Term.add_vars (Logic.strip_assums_hyp prem) []
+ val insts = map mk_inst hyps_vars
+ (*replace the hyps_vars by Frees*)
+ val prem' = subst_atomic insts prem
+ val (params,hyps,concl) = strip_context prem'
+ in (insts,params,hyps,concl) end;
+
+fun metahyps_aux_tac tacf (prem,gno) state =
+ let val (insts,params,hyps,concl) = metahyps_split_prem prem
+ val maxidx = Thm.maxidx_of state
+ val cterm = Thm.cterm_of (Thm.theory_of_thm state)
+ val chyps = map cterm hyps
+ val hypths = map Thm.assume chyps
+ val subprems = map (Thm.forall_elim_vars 0) hypths
+ val fparams = map Free params
+ val cparams = map cterm fparams
+ fun swap_ctpair (t,u) = (cterm u, cterm t)
+ (*Subgoal variables: make Free; lift type over params*)
+ fun mk_subgoal_inst concl_vars (v, T) =
+ if member (op =) concl_vars (v, T)
+ then ((v, T), true, free_of "METAHYP2_" (v, T))
+ else ((v, T), false, free_of "METAHYP2_" (v, map #2 params ---> T))
+ (*Instantiate subgoal vars by Free applied to params*)
+ fun mk_ctpair (v, in_concl, u) =
+ if in_concl then (cterm (Var v), cterm u)
+ else (cterm (Var v), cterm (list_comb (u, fparams)))
+ (*Restore Vars with higher type and index*)
+ fun mk_subgoal_swap_ctpair (((a, i), T), in_concl, u as Free (_, U)) =
+ if in_concl then (cterm u, cterm (Var ((a, i), T)))
+ else (cterm u, cterm (Var ((a, i + maxidx), U)))
+ (*Embed B in the original context of params and hyps*)
+ fun embed B = list_all_free (params, Logic.list_implies (hyps, B))
+ (*Strip the context using elimination rules*)
+ fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths
+ (*A form of lifting that discharges assumptions.*)
+ fun relift st =
+ let val prop = Thm.prop_of st
+ val subgoal_vars = (*Vars introduced in the subgoals*)
+ fold Term.add_vars (Logic.strip_imp_prems prop) []
+ and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) []
+ val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
+ val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st
+ val emBs = map (cterm o embed) (prems_of st')
+ val Cth = implies_elim_list st' (map (elim o Thm.assume) emBs)
+ in (*restore the unknowns to the hypotheses*)
+ free_instantiate (map swap_ctpair insts @
+ map mk_subgoal_swap_ctpair subgoal_insts)
+ (*discharge assumptions from state in same order*)
+ (implies_intr_list emBs
+ (forall_intr_list cparams (implies_intr_list chyps Cth)))
+ end
+ (*function to replace the current subgoal*)
+ fun next st = Thm.bicompose false (false, relift st, nprems_of st) gno state
+ in Seq.maps next (tacf subprems (Thm.trivial (cterm concl))) end;
+
+fun print_vars_terms n thm =
+ let
+ val thy = theory_of_thm thm
+ fun typed s ty =
+ " " ^ s ^ " has type: " ^ Syntax.string_of_typ_global thy ty;
+ fun find_vars (Const (c, ty)) =
+ if null (Term.add_tvarsT ty []) then I
+ else insert (op =) (typed c ty)
+ | find_vars (Var (xi, ty)) =
+ insert (op =) (typed (Term.string_of_vname xi) ty)
+ | find_vars (Free _) = I
+ | find_vars (Bound _) = I
+ | find_vars (Abs (_, _, t)) = find_vars t
+ | find_vars (t1 $ t2) = find_vars t1 #> find_vars t2;
+ val prem = Logic.nth_prem (n, Thm.prop_of thm)
+ val tms = find_vars prem []
+ in warning (cat_lines ("Found schematic vars in assumptions:" :: tms)) end;
+
+in
+
+fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm
+ handle THM("assume: variables",_,_) => (print_vars_terms n thm; Seq.empty)
+
+end;
+
+end;
+
--- a/src/ZF/IsaMakefile Mon Jul 12 21:12:18 2010 +0200
+++ b/src/ZF/IsaMakefile Mon Jul 12 21:38:37 2010 +0200
@@ -26,18 +26,19 @@
FOL:
@cd $(SRC)/FOL; $(ISABELLE_TOOL) make FOL
-$(OUT)/ZF: $(OUT)/FOL AC.thy Arith.thy ArithSimp.thy Bin.thy Bool.thy \
- Cardinal.thy CardinalArith.thy Cardinal_AC.thy Datatype_ZF.thy \
- Epsilon.thy EquivClass.thy Finite.thy Fixedpt.thy Inductive_ZF.thy \
- InfDatatype.thy Int_ZF.thy IntArith.thy IntDiv_ZF.thy List_ZF.thy \
- Main.thy Main_ZF.thy Main_ZFC.thy Nat_ZF.thy OrdQuant.thy Order.thy \
- OrderArith.thy OrderType.thy Ordinal.thy Perm.thy QPair.thy \
- QUniv.thy ROOT.ML Sum.thy Tools/cartprod.ML \
- Tools/datatype_package.ML Tools/ind_cases.ML Tools/induct_tacs.ML \
- Tools/inductive_package.ML Tools/numeral_syntax.ML \
- Tools/primrec_package.ML Tools/typechk.ML Trancl.thy Univ.thy WF.thy \
- ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy ind_syntax.ML \
- int_arith.ML pair.thy simpdata.ML upair.thy
+$(OUT)/ZF: $(OUT)/FOL $(SRC)/Tools/misc_legacy.ML AC.thy Arith.thy \
+ ArithSimp.thy Bin.thy Bool.thy Cardinal.thy CardinalArith.thy \
+ Cardinal_AC.thy Datatype_ZF.thy Epsilon.thy EquivClass.thy \
+ Finite.thy Fixedpt.thy Inductive_ZF.thy InfDatatype.thy Int_ZF.thy \
+ IntArith.thy IntDiv_ZF.thy List_ZF.thy Main.thy Main_ZF.thy \
+ Main_ZFC.thy Nat_ZF.thy OrdQuant.thy Order.thy OrderArith.thy \
+ OrderType.thy Ordinal.thy Perm.thy QPair.thy QUniv.thy ROOT.ML \
+ Sum.thy Tools/cartprod.ML Tools/datatype_package.ML \
+ Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML \
+ Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML \
+ Trancl.thy Univ.thy WF.thy ZF.thy Zorn.thy arith_data.ML \
+ equalities.thy func.thy ind_syntax.ML int_arith.ML pair.thy \
+ simpdata.ML upair.thy
@$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/FOL ZF
--- a/src/ZF/Tools/datatype_package.ML Mon Jul 12 21:12:18 2010 +0200
+++ b/src/ZF/Tools/datatype_package.ML Mon Jul 12 21:38:37 2010 +0200
@@ -108,7 +108,7 @@
let val ncon = length con_ty_list (*number of constructors*)
fun mk_def (((id,T,syn), name, args, prems), kcon) =
(*kcon is index of constructor*)
- OldGoals.mk_defpair (list_comb (Const (full_name name, T), args),
+ Misc_Legacy.mk_defpair (list_comb (Const (full_name name, T), args),
mk_inject npart kpart
(mk_inject ncon kcon (mk_tuple args)))
in ListPair.map mk_def (con_ty_list, 1 upto ncon) end;
@@ -157,7 +157,7 @@
val case_const = Const (case_name, case_typ);
val case_tm = list_comb (case_const, case_args);
- val case_def = OldGoals.mk_defpair
+ val case_def = Misc_Legacy.mk_defpair
(case_tm, Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists));
@@ -232,7 +232,7 @@
val recursor_cases = map call_recursor (flat case_lists ~~ flat recursor_lists);
val recursor_def =
- OldGoals.mk_defpair
+ Misc_Legacy.mk_defpair
(recursor_tm,
@{const Univ.Vrecursor} $
absfree ("rec", @{typ i}, list_comb (case_const, recursor_cases)));
@@ -300,7 +300,7 @@
(*** Prove the recursor theorems ***)
- val recursor_eqns = case try (OldGoals.get_def thy1) recursor_base_name of
+ val recursor_eqns = case try (Misc_Legacy.get_def thy1) recursor_base_name of
NONE => (writeln " [ No recursion operator ]";
[])
| SOME recursor_def =>
--- a/src/ZF/Tools/inductive_package.ML Mon Jul 12 21:12:18 2010 +0200
+++ b/src/ZF/Tools/inductive_package.ML Mon Jul 12 21:38:37 2010 +0200
@@ -156,7 +156,7 @@
val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
(*The individual sets must already be declared*)
- val axpairs = map OldGoals.mk_defpair
+ val axpairs = map Misc_Legacy.mk_defpair
((big_rec_tm, fp_rhs) ::
(case parts of
[_] => [] (*no mutual recursion*)
@@ -179,7 +179,7 @@
(*fetch fp definitions from the theory*)
val big_rec_def::part_rec_defs =
- map (OldGoals.get_def thy1)
+ map (Misc_Legacy.get_def thy1)
(case rec_names of [_] => rec_names
| _ => big_rec_base_name::rec_names);
--- a/src/ZF/ZF.thy Mon Jul 12 21:12:18 2010 +0200
+++ b/src/ZF/ZF.thy Mon Jul 12 21:38:37 2010 +0200
@@ -5,7 +5,10 @@
header{*Zermelo-Fraenkel Set Theory*}
-theory ZF imports FOL begin
+theory ZF
+imports FOL
+uses "~~/src/Tools/misc_legacy.ML"
+begin
ML {* Unsynchronized.reset eta_contract *}