# HG changeset patch # User wenzelm # Date 1248720340 -7200 # Node ID 95b8afcbb0ed37ac15d7df7158a11eaecd1a5269 # Parent 9f6461b1c9ccbbaedbd62a07d4d2d8d24beff78e moved METAHYPS to old_goals.ML (cf. SUBPROOF and FOCUS in subgoal.ML for properly localized versions of the same idea); diff -r 9f6461b1c9cc -r 95b8afcbb0ed src/HOL/Tools/cnf_funcs.ML --- 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) diff -r 9f6461b1c9cc -r 95b8afcbb0ed src/HOL/Tools/meson.ML --- 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 diff -r 9f6461b1c9cc -r 95b8afcbb0ed src/HOL/Tools/res_axioms.ML --- 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)), diff -r 9f6461b1c9cc -r 95b8afcbb0ed src/HOL/Tools/sat_funcs.ML --- 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 *) diff -r 9f6461b1c9cc -r 95b8afcbb0ed src/Pure/old_goals.ML --- 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 = diff -r 9f6461b1c9cc -r 95b8afcbb0ed src/Pure/tactical.ML --- 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; diff -r 9f6461b1c9cc -r 95b8afcbb0ed src/ZF/Tools/induct_tacs.ML --- 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