# HG changeset patch # User wenzelm # Date 1278963517 -7200 # Node ID 2fbbf0a48cef5600244a607f7fe636efbe5d565f # Parent 7e91b3f98c468e7f2a11f0d42ff3aa0a09bef8a8 moved misc legacy stuff from OldGoals to Misc_Legacy; OldGoals: removed unused strip_context, metahyps_thms, read_term, read_prop, gethyps; diff -r 7e91b3f98c46 -r 2fbbf0a48cef src/HOL/HOL.thy --- 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" diff -r 7e91b3f98c46 -r 2fbbf0a48cef src/HOL/IsaMakefile --- 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 \ diff -r 7e91b3f98c46 -r 2fbbf0a48cef src/HOL/Tools/meson.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 diff -r 7e91b3f98c46 -r 2fbbf0a48cef src/HOL/Tools/record.ML --- 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; diff -r 7e91b3f98c46 -r 2fbbf0a48cef src/HOLCF/IOA/meta_theory/automaton.ML --- 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 ( diff -r 7e91b3f98c46 -r 2fbbf0a48cef src/Pure/old_goals.ML --- 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); diff -r 7e91b3f98c46 -r 2fbbf0a48cef src/Tools/misc_legacy.ML --- /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; + diff -r 7e91b3f98c46 -r 2fbbf0a48cef src/ZF/IsaMakefile --- 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 diff -r 7e91b3f98c46 -r 2fbbf0a48cef src/ZF/Tools/datatype_package.ML --- 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 => diff -r 7e91b3f98c46 -r 2fbbf0a48cef src/ZF/Tools/inductive_package.ML --- 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); diff -r 7e91b3f98c46 -r 2fbbf0a48cef src/ZF/ZF.thy --- 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 *}