moved METAHYPS to old_goals.ML (cf. SUBPROOF and FOCUS in subgoal.ML for properly localized versions of the same idea);
--- a/src/HOL/Tools/cnf_funcs.ML Mon Jul 27 17:36:30 2009 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML Mon Jul 27 20:45:40 2009 +0200
@@ -520,7 +520,7 @@
fun cnf_rewrite_tac i =
(* cut the CNF formulas as new premises *)
- METAHYPS (fn prems =>
+ OldGoals.METAHYPS (fn prems =>
let
val cnf_thms = map (fn pr => make_cnf_thm (theory_of_thm pr) ((HOLogic.dest_Trueprop o prop_of) pr)) prems
val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems)
@@ -544,7 +544,7 @@
fun cnfx_rewrite_tac i =
(* cut the CNF formulas as new premises *)
- METAHYPS (fn prems =>
+ OldGoals.METAHYPS (fn prems =>
let
val cnfx_thms = map (fn pr => make_cnfx_thm (theory_of_thm pr) ((HOLogic.dest_Trueprop o prop_of) pr)) prems
val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems)
--- a/src/HOL/Tools/meson.ML Mon Jul 27 17:36:30 2009 +0200
+++ b/src/HOL/Tools/meson.ML Mon Jul 27 20:45:40 2009 +0200
@@ -132,7 +132,7 @@
Display.string_of_thm_without_context st ::
"Premises:" :: map Display.string_of_thm_without_context prems))
in
- case Seq.pull (ALLGOALS (METAHYPS forward_tacf) st)
+ case Seq.pull (ALLGOALS (OldGoals.METAHYPS forward_tacf) st)
of SOME(th,_) => th
| NONE => raise THM("forward_res", 0, [st])
end;
@@ -226,7 +226,7 @@
fun forward_res2 nf hyps st =
case Seq.pull
(REPEAT
- (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
+ (OldGoals.METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
st)
of SOME(th,_) => th
| NONE => raise THM("forward_res2", 0, [st]);
@@ -335,8 +335,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 =
- (METAHYPS (resop cnf_nil) 1) THEN
- (fn st' => st' |> METAHYPS (resop cnf_nil) 1)
+ (OldGoals.METAHYPS (resop cnf_nil) 1) THEN
+ (fn st' => st' |> OldGoals.METAHYPS (resop cnf_nil) 1)
in Seq.list_of (tac (th RS disj_forward)) @ ths end
| _ => nodups th :: ths (*no work to do*)
and cnf_nil th = cnf_aux (th,[])
@@ -584,9 +584,9 @@
SELECT_GOAL
(EVERY [ObjectLogic.atomize_prems_tac 1,
rtac ccontr 1,
- METAHYPS (fn negs =>
+ OldGoals.METAHYPS (fn negs =>
EVERY1 [skolemize_prems_tac negs,
- METAHYPS (cltac o mkcl)]) 1]) i st
+ OldGoals.METAHYPS (cltac o mkcl)]) 1]) i st
handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*)
(** Best-first search versions **)
@@ -698,7 +698,7 @@
fun skolemize_tac i st =
let val ts = Logic.strip_assums_hyp (List.nth (prems_of st, i-1))
in
- EVERY' [METAHYPS
+ EVERY' [OldGoals.METAHYPS
(fn hyps => (cut_facts_tac (skolemize_nnf_list hyps) 1
THEN REPEAT (etac exE 1))),
REPEAT_DETERM_N (length ts) o (etac thin_rl)] i st
--- a/src/HOL/Tools/res_axioms.ML Mon Jul 27 17:36:30 2009 +0200
+++ b/src/HOL/Tools/res_axioms.ML Mon Jul 27 20:45:40 2009 +0200
@@ -503,8 +503,8 @@
fun neg_conjecture_clauses st0 n =
let val st = Seq.hd (neg_skolemize_tac n st0)
- val (params,_,_) = strip_context (Logic.nth_prem (n, Thm.prop_of st))
- in (neg_clausify (the (metahyps_thms n st)), params) end
+ val (params,_,_) = OldGoals.strip_context (Logic.nth_prem (n, Thm.prop_of st))
+ in (neg_clausify (the (OldGoals.metahyps_thms n st)), params) end
handle Option => error "unable to Skolemize subgoal";
(*Conversion of a subgoal to conjecture clauses. Each clause has
@@ -515,7 +515,7 @@
(fn (prop,_) =>
let val ts = Logic.strip_assums_hyp prop
in EVERY1
- [METAHYPS
+ [OldGoals.METAHYPS
(fn hyps =>
(Method.insert_tac
(map forall_intr_vars (neg_clausify hyps)) 1)),
--- a/src/HOL/Tools/sat_funcs.ML Mon Jul 27 17:36:30 2009 +0200
+++ b/src/HOL/Tools/sat_funcs.ML Mon Jul 27 20:45:40 2009 +0200
@@ -410,7 +410,7 @@
(* or "True" *)
(* ------------------------------------------------------------------------- *)
-fun rawsat_tac i = METAHYPS (fn prems => rtac (rawsat_thm (map cprop_of prems)) 1) i;
+fun rawsat_tac i = OldGoals.METAHYPS (fn prems => rtac (rawsat_thm (map cprop_of prems)) 1) i;
(* ------------------------------------------------------------------------- *)
(* pre_cnf_tac: converts the i-th subgoal *)
--- a/src/Pure/old_goals.ML Mon Jul 27 17:36:30 2009 +0200
+++ b/src/Pure/old_goals.ML Mon Jul 27 20:45:40 2009 +0200
@@ -10,6 +10,9 @@
signature OLD_GOALS =
sig
+ 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
@@ -62,6 +65,147 @@
structure OldGoals: OLD_GOALS =
struct
+(**** 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 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 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 (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 thy (n,thm) =
+ let
+ fun typed ty = " has type: " ^ Syntax.string_of_typ_global thy ty;
+ fun find_vars thy (Const (c, ty)) =
+ if null (Term.add_tvarsT ty []) then I
+ else insert (op =) (c ^ typed ty)
+ | find_vars thy (Var (xi, ty)) = insert (op =) (Term.string_of_vname xi ^ typed ty)
+ | find_vars _ (Free _) = I
+ | find_vars _ (Bound _) = I
+ | find_vars thy (Abs (_, _, t)) = find_vars thy t
+ | find_vars thy (t1 $ t2) =
+ find_vars thy t1 #> find_vars thy t1;
+ val prem = Logic.nth_prem (n, Thm.prop_of thm)
+ val tms = find_vars thy prem []
+ in
+ (warning "Found schematic vars in assumptions:"; warning (cat_lines tms))
+ end;
+
+in
+
+fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm
+ handle THM("assume: variables",_,_) => (print_vars_terms (theory_of_thm thm) (n,thm); Seq.empty)
+
+end;
+
+
(* old ways of reading terms *)
fun simple_read_term thy T s =
--- a/src/Pure/tactical.ML Mon Jul 27 17:36:30 2009 +0200
+++ b/src/Pure/tactical.ML Mon Jul 27 20:45:40 2009 +0200
@@ -60,9 +60,6 @@
val CHANGED_GOAL: (int -> tactic) -> int -> tactic
val THEN_ALL_NEW: (int -> tactic) * (int -> tactic) -> int -> tactic
val REPEAT_ALL_NEW: (int -> tactic) -> int -> tactic
- 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 PRIMSEQ: (thm -> thm Seq.seq) -> tactic
val PRIMITIVE: (thm -> thm) -> tactic
val SINGLE: tactic -> thm -> thm option
@@ -366,143 +363,6 @@
fun REPEAT_ALL_NEW tac =
tac THEN_ALL_NEW (TRY o (fn i => REPEAT_ALL_NEW tac i));
-
-(*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);
-
-
-(**** 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.
-****)
-
-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 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 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 (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 thy (n,thm) =
- let
- fun typed ty = " has type: " ^ Syntax.string_of_typ_global thy ty;
- fun find_vars thy (Const (c, ty)) =
- if null (Term.add_tvarsT ty []) then I
- else insert (op =) (c ^ typed ty)
- | find_vars thy (Var (xi, ty)) = insert (op =) (Term.string_of_vname xi ^ typed ty)
- | find_vars _ (Free _) = I
- | find_vars _ (Bound _) = I
- | find_vars thy (Abs (_, _, t)) = find_vars thy t
- | find_vars thy (t1 $ t2) =
- find_vars thy t1 #> find_vars thy t1;
- val prem = Logic.nth_prem (n, Thm.prop_of thm)
- val tms = find_vars thy prem []
- in
- (warning "Found schematic vars in assumptions:"; warning (cat_lines tms))
- end;
-
-in
-
-fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm
- handle THM("assume: variables",_,_) => (print_vars_terms (theory_of_thm thm) (n,thm); Seq.empty)
-
-end;
-
(*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)
fun PRIMSEQ thmfun st = thmfun st handle THM _ => Seq.empty;
--- a/src/ZF/Tools/induct_tacs.ML Mon Jul 27 17:36:30 2009 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Mon Jul 27 20:45:40 2009 +0200
@@ -75,7 +75,7 @@
(v, #1 (dest_Const (head_of A)))
| mk_pair _ = raise Match
val pairs = List.mapPartial (try (mk_pair o FOLogic.dest_Trueprop))
- (#2 (strip_context Bi))
+ (#2 (OldGoals.strip_context Bi))
in case AList.lookup (op =) pairs var of
NONE => raise Find_tname ("Cannot determine datatype of " ^ quote var)
| SOME t => t