merged
authorwenzelm
Mon Jul 27 22:25:29 2009 +0200 (2009-07-27 ago)
changeset 32239d2a99fdddd69
parent 32235 8f9b8d14fc9f
parent 32231 95b8afcbb0ed
child 32240 2a3ffaf00de4
merged
     1.1 --- a/src/HOL/Tools/cnf_funcs.ML	Mon Jul 27 21:47:41 2009 +0200
     1.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Mon Jul 27 22:25:29 2009 +0200
     1.3 @@ -520,7 +520,7 @@
     1.4  
     1.5  fun cnf_rewrite_tac i =
     1.6  	(* cut the CNF formulas as new premises *)
     1.7 -	METAHYPS (fn prems =>
     1.8 +	OldGoals.METAHYPS (fn prems =>
     1.9  		let
    1.10  			val cnf_thms = map (fn pr => make_cnf_thm (theory_of_thm pr) ((HOLogic.dest_Trueprop o prop_of) pr)) prems
    1.11  			val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems)
    1.12 @@ -544,7 +544,7 @@
    1.13  
    1.14  fun cnfx_rewrite_tac i =
    1.15  	(* cut the CNF formulas as new premises *)
    1.16 -	METAHYPS (fn prems =>
    1.17 +	OldGoals.METAHYPS (fn prems =>
    1.18  		let
    1.19  			val cnfx_thms = map (fn pr => make_cnfx_thm (theory_of_thm pr) ((HOLogic.dest_Trueprop o prop_of) pr)) prems
    1.20  			val cut_thms  = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems)
     2.1 --- a/src/HOL/Tools/meson.ML	Mon Jul 27 21:47:41 2009 +0200
     2.2 +++ b/src/HOL/Tools/meson.ML	Mon Jul 27 22:25:29 2009 +0200
     2.3 @@ -132,7 +132,7 @@
     2.4                  Display.string_of_thm_without_context st ::
     2.5                  "Premises:" :: map Display.string_of_thm_without_context prems))
     2.6    in
     2.7 -    case Seq.pull (ALLGOALS (METAHYPS forward_tacf) st)
     2.8 +    case Seq.pull (ALLGOALS (OldGoals.METAHYPS forward_tacf) st)
     2.9      of SOME(th,_) => th
    2.10       | NONE => raise THM("forward_res", 0, [st])
    2.11    end;
    2.12 @@ -226,7 +226,7 @@
    2.13  fun forward_res2 nf hyps st =
    2.14    case Seq.pull
    2.15          (REPEAT
    2.16 -         (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
    2.17 +         (OldGoals.METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
    2.18           st)
    2.19    of SOME(th,_) => th
    2.20     | NONE => raise THM("forward_res2", 0, [st]);
    2.21 @@ -335,8 +335,8 @@
    2.22                (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
    2.23                  all combinations of converting P, Q to CNF.*)
    2.24                let val tac =
    2.25 -                  (METAHYPS (resop cnf_nil) 1) THEN
    2.26 -                   (fn st' => st' |> METAHYPS (resop cnf_nil) 1)
    2.27 +                  (OldGoals.METAHYPS (resop cnf_nil) 1) THEN
    2.28 +                   (fn st' => st' |> OldGoals.METAHYPS (resop cnf_nil) 1)
    2.29                in  Seq.list_of (tac (th RS disj_forward)) @ ths  end
    2.30            | _ => nodups th :: ths  (*no work to do*)
    2.31        and cnf_nil th = cnf_aux (th,[])
    2.32 @@ -584,9 +584,9 @@
    2.33    SELECT_GOAL
    2.34      (EVERY [ObjectLogic.atomize_prems_tac 1,
    2.35              rtac ccontr 1,
    2.36 -            METAHYPS (fn negs =>
    2.37 +            OldGoals.METAHYPS (fn negs =>
    2.38                        EVERY1 [skolemize_prems_tac negs,
    2.39 -                              METAHYPS (cltac o mkcl)]) 1]) i st
    2.40 +                              OldGoals.METAHYPS (cltac o mkcl)]) 1]) i st
    2.41    handle THM _ => no_tac st;    (*probably from make_meta_clause, not first-order*)
    2.42  
    2.43  (** Best-first search versions **)
    2.44 @@ -698,7 +698,7 @@
    2.45  fun skolemize_tac i st =
    2.46    let val ts = Logic.strip_assums_hyp (List.nth (prems_of st, i-1))
    2.47    in
    2.48 -     EVERY' [METAHYPS
    2.49 +     EVERY' [OldGoals.METAHYPS
    2.50              (fn hyps => (cut_facts_tac (skolemize_nnf_list hyps) 1
    2.51                           THEN REPEAT (etac exE 1))),
    2.52              REPEAT_DETERM_N (length ts) o (etac thin_rl)] i st
     3.1 --- a/src/HOL/Tools/res_axioms.ML	Mon Jul 27 21:47:41 2009 +0200
     3.2 +++ b/src/HOL/Tools/res_axioms.ML	Mon Jul 27 22:25:29 2009 +0200
     3.3 @@ -503,8 +503,8 @@
     3.4  
     3.5  fun neg_conjecture_clauses st0 n =
     3.6    let val st = Seq.hd (neg_skolemize_tac n st0)
     3.7 -      val (params,_,_) = strip_context (Logic.nth_prem (n, Thm.prop_of st))
     3.8 -  in (neg_clausify (the (metahyps_thms n st)), params) end
     3.9 +      val (params,_,_) = OldGoals.strip_context (Logic.nth_prem (n, Thm.prop_of st))
    3.10 +  in (neg_clausify (the (OldGoals.metahyps_thms n st)), params) end
    3.11    handle Option => error "unable to Skolemize subgoal";
    3.12  
    3.13  (*Conversion of a subgoal to conjecture clauses. Each clause has
    3.14 @@ -515,7 +515,7 @@
    3.15      (fn (prop,_) =>
    3.16       let val ts = Logic.strip_assums_hyp prop
    3.17       in EVERY1
    3.18 -         [METAHYPS
    3.19 +         [OldGoals.METAHYPS
    3.20              (fn hyps =>
    3.21                (Method.insert_tac
    3.22                  (map forall_intr_vars (neg_clausify hyps)) 1)),
     4.1 --- a/src/HOL/Tools/sat_funcs.ML	Mon Jul 27 21:47:41 2009 +0200
     4.2 +++ b/src/HOL/Tools/sat_funcs.ML	Mon Jul 27 22:25:29 2009 +0200
     4.3 @@ -410,7 +410,7 @@
     4.4  (*      or "True"                                                            *)
     4.5  (* ------------------------------------------------------------------------- *)
     4.6  
     4.7 -fun rawsat_tac i = METAHYPS (fn prems => rtac (rawsat_thm (map cprop_of prems)) 1) i;
     4.8 +fun rawsat_tac i = OldGoals.METAHYPS (fn prems => rtac (rawsat_thm (map cprop_of prems)) 1) i;
     4.9  
    4.10  (* ------------------------------------------------------------------------- *)
    4.11  (* pre_cnf_tac: converts the i-th subgoal                                    *)
     5.1 --- a/src/Pure/old_goals.ML	Mon Jul 27 21:47:41 2009 +0200
     5.2 +++ b/src/Pure/old_goals.ML	Mon Jul 27 22:25:29 2009 +0200
     5.3 @@ -10,6 +10,9 @@
     5.4  
     5.5  signature OLD_GOALS =
     5.6  sig
     5.7 +  val strip_context: term -> (string * typ) list * term list * term
     5.8 +  val metahyps_thms: int -> thm -> thm list option
     5.9 +  val METAHYPS: (thm list -> tactic) -> int -> tactic
    5.10    val simple_read_term: theory -> typ -> string -> term
    5.11    val read_term: theory -> string -> term
    5.12    val read_prop: theory -> string -> term
    5.13 @@ -62,6 +65,147 @@
    5.14  structure OldGoals: OLD_GOALS =
    5.15  struct
    5.16  
    5.17 +(**** METAHYPS -- tactical for using hypotheses as meta-level assumptions
    5.18 +       METAHYPS (fn prems => tac prems) i
    5.19 +
    5.20 +converts subgoal i, of the form !!x1...xm. [| A1;...;An] ==> A into a new
    5.21 +proof state A==>A, supplying A1,...,An as meta-level assumptions (in
    5.22 +"prems").  The parameters x1,...,xm become free variables.  If the
    5.23 +resulting proof state is [| B1;...;Bk] ==> C (possibly assuming A1,...,An)
    5.24 +then it is lifted back into the original context, yielding k subgoals.
    5.25 +
    5.26 +Replaces unknowns in the context by Frees having the prefix METAHYP_
    5.27 +New unknowns in [| B1;...;Bk] ==> C are lifted over x1,...,xm.
    5.28 +DOES NOT HANDLE TYPE UNKNOWNS.
    5.29 +
    5.30 +
    5.31 +NOTE: This version does not observe the proof context, and thus cannot
    5.32 +work reliably.  See also Subgoal.SUBPROOF and Subgoal.FOCUS for
    5.33 +properly localized variants of the same idea.
    5.34 +****)
    5.35 +
    5.36 +(*Strips assumptions in goal yielding  ( [x1,...,xm], [H1,...,Hn], B )
    5.37 +    H1,...,Hn are the hypotheses;  x1...xm are variants of the parameters.
    5.38 +  Main difference from strip_assums concerns parameters:
    5.39 +    it replaces the bound variables by free variables.  *)
    5.40 +fun strip_context_aux (params, Hs, Const ("==>", _) $ H $ B) =
    5.41 +      strip_context_aux (params, H :: Hs, B)
    5.42 +  | strip_context_aux (params, Hs, Const ("all",_) $ Abs (a, T, t)) =
    5.43 +      let val (b, u) = Syntax.variant_abs (a, T, t)
    5.44 +      in strip_context_aux ((b, T) :: params, Hs, u) end
    5.45 +  | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);
    5.46 +
    5.47 +fun strip_context A = strip_context_aux ([], [], A);
    5.48 +
    5.49 +local
    5.50 +
    5.51 +  (*Left-to-right replacements: ctpairs = [...,(vi,ti),...].
    5.52 +    Instantiates distinct free variables by terms of same type.*)
    5.53 +  fun free_instantiate ctpairs =
    5.54 +    forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs);
    5.55 +
    5.56 +  fun free_of s ((a, i), T) =
    5.57 +    Free (s ^ (case i of 0 => a | _ => a ^ "_" ^ string_of_int i), T)
    5.58 +
    5.59 +  fun mk_inst v = (Var v, free_of "METAHYP1_" v)
    5.60 +in
    5.61 +
    5.62 +(*Common code for METAHYPS and metahyps_thms*)
    5.63 +fun metahyps_split_prem prem =
    5.64 +  let (*find all vars in the hyps -- should find tvars also!*)
    5.65 +      val hyps_vars = fold Term.add_vars (Logic.strip_assums_hyp prem) []
    5.66 +      val insts = map mk_inst hyps_vars
    5.67 +      (*replace the hyps_vars by Frees*)
    5.68 +      val prem' = subst_atomic insts prem
    5.69 +      val (params,hyps,concl) = strip_context prem'
    5.70 +  in (insts,params,hyps,concl)  end;
    5.71 +
    5.72 +fun metahyps_aux_tac tacf (prem,gno) state =
    5.73 +  let val (insts,params,hyps,concl) = metahyps_split_prem prem
    5.74 +      val maxidx = Thm.maxidx_of state
    5.75 +      val cterm = Thm.cterm_of (Thm.theory_of_thm state)
    5.76 +      val chyps = map cterm hyps
    5.77 +      val hypths = map assume chyps
    5.78 +      val subprems = map (Thm.forall_elim_vars 0) hypths
    5.79 +      val fparams = map Free params
    5.80 +      val cparams = map cterm fparams
    5.81 +      fun swap_ctpair (t,u) = (cterm u, cterm t)
    5.82 +      (*Subgoal variables: make Free; lift type over params*)
    5.83 +      fun mk_subgoal_inst concl_vars (v, T) =
    5.84 +          if member (op =) concl_vars (v, T)
    5.85 +          then ((v, T), true, free_of "METAHYP2_" (v, T))
    5.86 +          else ((v, T), false, free_of "METAHYP2_" (v, map #2 params ---> T))
    5.87 +      (*Instantiate subgoal vars by Free applied to params*)
    5.88 +      fun mk_ctpair (v, in_concl, u) =
    5.89 +          if in_concl then (cterm (Var v), cterm u)
    5.90 +          else (cterm (Var v), cterm (list_comb (u, fparams)))
    5.91 +      (*Restore Vars with higher type and index*)
    5.92 +      fun mk_subgoal_swap_ctpair (((a, i), T), in_concl, u as Free (_, U)) =
    5.93 +          if in_concl then (cterm u, cterm (Var ((a, i), T)))
    5.94 +          else (cterm u, cterm (Var ((a, i + maxidx), U)))
    5.95 +      (*Embed B in the original context of params and hyps*)
    5.96 +      fun embed B = list_all_free (params, Logic.list_implies (hyps, B))
    5.97 +      (*Strip the context using elimination rules*)
    5.98 +      fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths
    5.99 +      (*A form of lifting that discharges assumptions.*)
   5.100 +      fun relift st =
   5.101 +        let val prop = Thm.prop_of st
   5.102 +            val subgoal_vars = (*Vars introduced in the subgoals*)
   5.103 +              fold Term.add_vars (Logic.strip_imp_prems prop) []
   5.104 +            and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) []
   5.105 +            val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
   5.106 +            val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st
   5.107 +            val emBs = map (cterm o embed) (prems_of st')
   5.108 +            val Cth  = implies_elim_list st' (map (elim o assume) emBs)
   5.109 +        in  (*restore the unknowns to the hypotheses*)
   5.110 +            free_instantiate (map swap_ctpair insts @
   5.111 +                              map mk_subgoal_swap_ctpair subgoal_insts)
   5.112 +                (*discharge assumptions from state in same order*)
   5.113 +                (implies_intr_list emBs
   5.114 +                  (forall_intr_list cparams (implies_intr_list chyps Cth)))
   5.115 +        end
   5.116 +      (*function to replace the current subgoal*)
   5.117 +      fun next st = Thm.bicompose false (false, relift st, nprems_of st) gno state
   5.118 +  in Seq.maps next (tacf subprems (trivial (cterm concl))) end;
   5.119 +
   5.120 +end;
   5.121 +
   5.122 +(*Returns the theorem list that METAHYPS would supply to its tactic*)
   5.123 +fun metahyps_thms i state =
   5.124 +  let val prem = Logic.nth_prem (i, Thm.prop_of state)
   5.125 +      and cterm = cterm_of (Thm.theory_of_thm state)
   5.126 +      val (_,_,hyps,_) = metahyps_split_prem prem
   5.127 +  in SOME (map (Thm.forall_elim_vars 0 o Thm.assume o cterm) hyps) end
   5.128 +  handle TERM ("nth_prem", [A]) => NONE;
   5.129 +
   5.130 +local
   5.131 +
   5.132 +fun print_vars_terms thy (n,thm) =
   5.133 +  let
   5.134 +    fun typed ty = " has type: " ^ Syntax.string_of_typ_global thy ty;
   5.135 +    fun find_vars thy (Const (c, ty)) =
   5.136 +          if null (Term.add_tvarsT ty []) then I
   5.137 +          else insert (op =) (c ^ typed ty)
   5.138 +      | find_vars thy (Var (xi, ty)) = insert (op =) (Term.string_of_vname xi ^ typed ty)
   5.139 +      | find_vars _ (Free _) = I
   5.140 +      | find_vars _ (Bound _) = I
   5.141 +      | find_vars thy (Abs (_, _, t)) = find_vars thy t
   5.142 +      | find_vars thy (t1 $ t2) =
   5.143 +          find_vars thy t1 #> find_vars thy t1;
   5.144 +    val prem = Logic.nth_prem (n, Thm.prop_of thm)
   5.145 +    val tms = find_vars thy prem []
   5.146 +  in
   5.147 +    (warning "Found schematic vars in assumptions:"; warning (cat_lines tms))
   5.148 +  end;
   5.149 +
   5.150 +in
   5.151 +
   5.152 +fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm
   5.153 +  handle THM("assume: variables",_,_) => (print_vars_terms (theory_of_thm thm) (n,thm); Seq.empty)
   5.154 +
   5.155 +end;
   5.156 +
   5.157 +
   5.158  (* old ways of reading terms *)
   5.159  
   5.160  fun simple_read_term thy T s =
     6.1 --- a/src/Pure/tactical.ML	Mon Jul 27 21:47:41 2009 +0200
     6.2 +++ b/src/Pure/tactical.ML	Mon Jul 27 22:25:29 2009 +0200
     6.3 @@ -60,9 +60,6 @@
     6.4    val CHANGED_GOAL: (int -> tactic) -> int -> tactic
     6.5    val THEN_ALL_NEW: (int -> tactic) * (int -> tactic) -> int -> tactic
     6.6    val REPEAT_ALL_NEW: (int -> tactic) -> int -> tactic
     6.7 -  val strip_context: term -> (string * typ) list * term list * term
     6.8 -  val metahyps_thms: int -> thm -> thm list option
     6.9 -  val METAHYPS: (thm list -> tactic) -> int -> tactic
    6.10    val PRIMSEQ: (thm -> thm Seq.seq) -> tactic
    6.11    val PRIMITIVE: (thm -> thm) -> tactic
    6.12    val SINGLE: tactic -> thm -> thm option
    6.13 @@ -366,143 +363,6 @@
    6.14  fun REPEAT_ALL_NEW tac =
    6.15    tac THEN_ALL_NEW (TRY o (fn i => REPEAT_ALL_NEW tac i));
    6.16  
    6.17 -
    6.18 -(*Strips assumptions in goal yielding  ( [x1,...,xm], [H1,...,Hn], B )
    6.19 -    H1,...,Hn are the hypotheses;  x1...xm are variants of the parameters.
    6.20 -  Main difference from strip_assums concerns parameters:
    6.21 -    it replaces the bound variables by free variables.  *)
    6.22 -fun strip_context_aux (params, Hs, Const("==>", _) $ H $ B) =
    6.23 -        strip_context_aux (params, H::Hs, B)
    6.24 -  | strip_context_aux (params, Hs, Const("all",_)$Abs(a,T,t)) =
    6.25 -        let val (b,u) = Syntax.variant_abs(a,T,t)
    6.26 -        in  strip_context_aux ((b,T)::params, Hs, u)  end
    6.27 -  | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);
    6.28 -
    6.29 -fun strip_context A = strip_context_aux ([],[],A);
    6.30 -
    6.31 -
    6.32 -(**** METAHYPS -- tactical for using hypotheses as meta-level assumptions
    6.33 -       METAHYPS (fn prems => tac prems) i
    6.34 -
    6.35 -converts subgoal i, of the form !!x1...xm. [| A1;...;An] ==> A into a new
    6.36 -proof state A==>A, supplying A1,...,An as meta-level assumptions (in
    6.37 -"prems").  The parameters x1,...,xm become free variables.  If the
    6.38 -resulting proof state is [| B1;...;Bk] ==> C (possibly assuming A1,...,An)
    6.39 -then it is lifted back into the original context, yielding k subgoals.
    6.40 -
    6.41 -Replaces unknowns in the context by Frees having the prefix METAHYP_
    6.42 -New unknowns in [| B1;...;Bk] ==> C are lifted over x1,...,xm.
    6.43 -DOES NOT HANDLE TYPE UNKNOWNS.
    6.44 -****)
    6.45 -
    6.46 -local
    6.47 -
    6.48 -  (*Left-to-right replacements: ctpairs = [...,(vi,ti),...].
    6.49 -    Instantiates distinct free variables by terms of same type.*)
    6.50 -  fun free_instantiate ctpairs =
    6.51 -    forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs);
    6.52 -
    6.53 -  fun free_of s ((a, i), T) =
    6.54 -    Free (s ^ (case i of 0 => a | _ => a ^ "_" ^ string_of_int i), T)
    6.55 -
    6.56 -  fun mk_inst v = (Var v, free_of "METAHYP1_" v)
    6.57 -in
    6.58 -
    6.59 -(*Common code for METAHYPS and metahyps_thms*)
    6.60 -fun metahyps_split_prem prem =
    6.61 -  let (*find all vars in the hyps -- should find tvars also!*)
    6.62 -      val hyps_vars = fold Term.add_vars (Logic.strip_assums_hyp prem) []
    6.63 -      val insts = map mk_inst hyps_vars
    6.64 -      (*replace the hyps_vars by Frees*)
    6.65 -      val prem' = subst_atomic insts prem
    6.66 -      val (params,hyps,concl) = strip_context prem'
    6.67 -  in (insts,params,hyps,concl)  end;
    6.68 -
    6.69 -fun metahyps_aux_tac tacf (prem,gno) state =
    6.70 -  let val (insts,params,hyps,concl) = metahyps_split_prem prem
    6.71 -      val maxidx = Thm.maxidx_of state
    6.72 -      val cterm = Thm.cterm_of (Thm.theory_of_thm state)
    6.73 -      val chyps = map cterm hyps
    6.74 -      val hypths = map assume chyps
    6.75 -      val subprems = map (Thm.forall_elim_vars 0) hypths
    6.76 -      val fparams = map Free params
    6.77 -      val cparams = map cterm fparams
    6.78 -      fun swap_ctpair (t,u) = (cterm u, cterm t)
    6.79 -      (*Subgoal variables: make Free; lift type over params*)
    6.80 -      fun mk_subgoal_inst concl_vars (v, T) =
    6.81 -          if member (op =) concl_vars (v, T)
    6.82 -          then ((v, T), true, free_of "METAHYP2_" (v, T))
    6.83 -          else ((v, T), false, free_of "METAHYP2_" (v, map #2 params ---> T))
    6.84 -      (*Instantiate subgoal vars by Free applied to params*)
    6.85 -      fun mk_ctpair (v, in_concl, u) =
    6.86 -          if in_concl then (cterm (Var v), cterm u)
    6.87 -          else (cterm (Var v), cterm (list_comb (u, fparams)))
    6.88 -      (*Restore Vars with higher type and index*)
    6.89 -      fun mk_subgoal_swap_ctpair (((a, i), T), in_concl, u as Free (_, U)) =
    6.90 -          if in_concl then (cterm u, cterm (Var ((a, i), T)))
    6.91 -          else (cterm u, cterm (Var ((a, i + maxidx), U)))
    6.92 -      (*Embed B in the original context of params and hyps*)
    6.93 -      fun embed B = list_all_free (params, Logic.list_implies (hyps, B))
    6.94 -      (*Strip the context using elimination rules*)
    6.95 -      fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths
    6.96 -      (*A form of lifting that discharges assumptions.*)
    6.97 -      fun relift st =
    6.98 -        let val prop = Thm.prop_of st
    6.99 -            val subgoal_vars = (*Vars introduced in the subgoals*)
   6.100 -              fold Term.add_vars (Logic.strip_imp_prems prop) []
   6.101 -            and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) []
   6.102 -            val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
   6.103 -            val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st
   6.104 -            val emBs = map (cterm o embed) (prems_of st')
   6.105 -            val Cth  = implies_elim_list st' (map (elim o assume) emBs)
   6.106 -        in  (*restore the unknowns to the hypotheses*)
   6.107 -            free_instantiate (map swap_ctpair insts @
   6.108 -                              map mk_subgoal_swap_ctpair subgoal_insts)
   6.109 -                (*discharge assumptions from state in same order*)
   6.110 -                (implies_intr_list emBs
   6.111 -                  (forall_intr_list cparams (implies_intr_list chyps Cth)))
   6.112 -        end
   6.113 -      (*function to replace the current subgoal*)
   6.114 -      fun next st = Thm.bicompose false (false, relift st, nprems_of st) gno state
   6.115 -  in Seq.maps next (tacf subprems (trivial (cterm concl))) end;
   6.116 -
   6.117 -end;
   6.118 -
   6.119 -(*Returns the theorem list that METAHYPS would supply to its tactic*)
   6.120 -fun metahyps_thms i state =
   6.121 -  let val prem = Logic.nth_prem (i, Thm.prop_of state)
   6.122 -      and cterm = cterm_of (Thm.theory_of_thm state)
   6.123 -      val (_,_,hyps,_) = metahyps_split_prem prem
   6.124 -  in SOME (map (Thm.forall_elim_vars 0 o Thm.assume o cterm) hyps) end
   6.125 -  handle TERM ("nth_prem", [A]) => NONE;
   6.126 -
   6.127 -local
   6.128 -
   6.129 -fun print_vars_terms thy (n,thm) =
   6.130 -  let
   6.131 -    fun typed ty = " has type: " ^ Syntax.string_of_typ_global thy ty;
   6.132 -    fun find_vars thy (Const (c, ty)) =
   6.133 -          if null (Term.add_tvarsT ty []) then I
   6.134 -          else insert (op =) (c ^ typed ty)
   6.135 -      | find_vars thy (Var (xi, ty)) = insert (op =) (Term.string_of_vname xi ^ typed ty)
   6.136 -      | find_vars _ (Free _) = I
   6.137 -      | find_vars _ (Bound _) = I
   6.138 -      | find_vars thy (Abs (_, _, t)) = find_vars thy t
   6.139 -      | find_vars thy (t1 $ t2) =
   6.140 -          find_vars thy t1 #> find_vars thy t1;
   6.141 -    val prem = Logic.nth_prem (n, Thm.prop_of thm)
   6.142 -    val tms = find_vars thy prem []
   6.143 -  in
   6.144 -    (warning "Found schematic vars in assumptions:"; warning (cat_lines tms))
   6.145 -  end;
   6.146 -
   6.147 -in
   6.148 -
   6.149 -fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm
   6.150 -  handle THM("assume: variables",_,_) => (print_vars_terms (theory_of_thm thm) (n,thm); Seq.empty)
   6.151 -
   6.152 -end;
   6.153 -
   6.154  (*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)
   6.155  fun PRIMSEQ thmfun st =  thmfun st handle THM _ => Seq.empty;
   6.156  
     7.1 --- a/src/ZF/Tools/induct_tacs.ML	Mon Jul 27 21:47:41 2009 +0200
     7.2 +++ b/src/ZF/Tools/induct_tacs.ML	Mon Jul 27 22:25:29 2009 +0200
     7.3 @@ -75,7 +75,7 @@
     7.4               (v, #1 (dest_Const (head_of A)))
     7.5          | mk_pair _ = raise Match
     7.6        val pairs = List.mapPartial (try (mk_pair o FOLogic.dest_Trueprop))
     7.7 -          (#2 (strip_context Bi))
     7.8 +          (#2 (OldGoals.strip_context Bi))
     7.9    in case AList.lookup (op =) pairs var of
    7.10         NONE => raise Find_tname ("Cannot determine datatype of " ^ quote var)
    7.11       | SOME t => t