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