src/Pure/old_goals.ML
changeset 32231 95b8afcbb0ed
parent 32187 cca43ca13f4f
child 32432 64f30bdd3ba1
     1.1 --- a/src/Pure/old_goals.ML	Mon Jul 27 17:36:30 2009 +0200
     1.2 +++ b/src/Pure/old_goals.ML	Mon Jul 27 20:45:40 2009 +0200
     1.3 @@ -10,6 +10,9 @@
     1.4  
     1.5  signature OLD_GOALS =
     1.6  sig
     1.7 +  val strip_context: term -> (string * typ) list * term list * term
     1.8 +  val metahyps_thms: int -> thm -> thm list option
     1.9 +  val METAHYPS: (thm list -> tactic) -> int -> tactic
    1.10    val simple_read_term: theory -> typ -> string -> term
    1.11    val read_term: theory -> string -> term
    1.12    val read_prop: theory -> string -> term
    1.13 @@ -62,6 +65,147 @@
    1.14  structure OldGoals: OLD_GOALS =
    1.15  struct
    1.16  
    1.17 +(**** METAHYPS -- tactical for using hypotheses as meta-level assumptions
    1.18 +       METAHYPS (fn prems => tac prems) i
    1.19 +
    1.20 +converts subgoal i, of the form !!x1...xm. [| A1;...;An] ==> A into a new
    1.21 +proof state A==>A, supplying A1,...,An as meta-level assumptions (in
    1.22 +"prems").  The parameters x1,...,xm become free variables.  If the
    1.23 +resulting proof state is [| B1;...;Bk] ==> C (possibly assuming A1,...,An)
    1.24 +then it is lifted back into the original context, yielding k subgoals.
    1.25 +
    1.26 +Replaces unknowns in the context by Frees having the prefix METAHYP_
    1.27 +New unknowns in [| B1;...;Bk] ==> C are lifted over x1,...,xm.
    1.28 +DOES NOT HANDLE TYPE UNKNOWNS.
    1.29 +
    1.30 +
    1.31 +NOTE: This version does not observe the proof context, and thus cannot
    1.32 +work reliably.  See also Subgoal.SUBPROOF and Subgoal.FOCUS for
    1.33 +properly localized variants of the same idea.
    1.34 +****)
    1.35 +
    1.36 +(*Strips assumptions in goal yielding  ( [x1,...,xm], [H1,...,Hn], B )
    1.37 +    H1,...,Hn are the hypotheses;  x1...xm are variants of the parameters.
    1.38 +  Main difference from strip_assums concerns parameters:
    1.39 +    it replaces the bound variables by free variables.  *)
    1.40 +fun strip_context_aux (params, Hs, Const ("==>", _) $ H $ B) =
    1.41 +      strip_context_aux (params, H :: Hs, B)
    1.42 +  | strip_context_aux (params, Hs, Const ("all",_) $ Abs (a, T, t)) =
    1.43 +      let val (b, u) = Syntax.variant_abs (a, T, t)
    1.44 +      in strip_context_aux ((b, T) :: params, Hs, u) end
    1.45 +  | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);
    1.46 +
    1.47 +fun strip_context A = strip_context_aux ([], [], A);
    1.48 +
    1.49 +local
    1.50 +
    1.51 +  (*Left-to-right replacements: ctpairs = [...,(vi,ti),...].
    1.52 +    Instantiates distinct free variables by terms of same type.*)
    1.53 +  fun free_instantiate ctpairs =
    1.54 +    forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs);
    1.55 +
    1.56 +  fun free_of s ((a, i), T) =
    1.57 +    Free (s ^ (case i of 0 => a | _ => a ^ "_" ^ string_of_int i), T)
    1.58 +
    1.59 +  fun mk_inst v = (Var v, free_of "METAHYP1_" v)
    1.60 +in
    1.61 +
    1.62 +(*Common code for METAHYPS and metahyps_thms*)
    1.63 +fun metahyps_split_prem prem =
    1.64 +  let (*find all vars in the hyps -- should find tvars also!*)
    1.65 +      val hyps_vars = fold Term.add_vars (Logic.strip_assums_hyp prem) []
    1.66 +      val insts = map mk_inst hyps_vars
    1.67 +      (*replace the hyps_vars by Frees*)
    1.68 +      val prem' = subst_atomic insts prem
    1.69 +      val (params,hyps,concl) = strip_context prem'
    1.70 +  in (insts,params,hyps,concl)  end;
    1.71 +
    1.72 +fun metahyps_aux_tac tacf (prem,gno) state =
    1.73 +  let val (insts,params,hyps,concl) = metahyps_split_prem prem
    1.74 +      val maxidx = Thm.maxidx_of state
    1.75 +      val cterm = Thm.cterm_of (Thm.theory_of_thm state)
    1.76 +      val chyps = map cterm hyps
    1.77 +      val hypths = map assume chyps
    1.78 +      val subprems = map (Thm.forall_elim_vars 0) hypths
    1.79 +      val fparams = map Free params
    1.80 +      val cparams = map cterm fparams
    1.81 +      fun swap_ctpair (t,u) = (cterm u, cterm t)
    1.82 +      (*Subgoal variables: make Free; lift type over params*)
    1.83 +      fun mk_subgoal_inst concl_vars (v, T) =
    1.84 +          if member (op =) concl_vars (v, T)
    1.85 +          then ((v, T), true, free_of "METAHYP2_" (v, T))
    1.86 +          else ((v, T), false, free_of "METAHYP2_" (v, map #2 params ---> T))
    1.87 +      (*Instantiate subgoal vars by Free applied to params*)
    1.88 +      fun mk_ctpair (v, in_concl, u) =
    1.89 +          if in_concl then (cterm (Var v), cterm u)
    1.90 +          else (cterm (Var v), cterm (list_comb (u, fparams)))
    1.91 +      (*Restore Vars with higher type and index*)
    1.92 +      fun mk_subgoal_swap_ctpair (((a, i), T), in_concl, u as Free (_, U)) =
    1.93 +          if in_concl then (cterm u, cterm (Var ((a, i), T)))
    1.94 +          else (cterm u, cterm (Var ((a, i + maxidx), U)))
    1.95 +      (*Embed B in the original context of params and hyps*)
    1.96 +      fun embed B = list_all_free (params, Logic.list_implies (hyps, B))
    1.97 +      (*Strip the context using elimination rules*)
    1.98 +      fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths
    1.99 +      (*A form of lifting that discharges assumptions.*)
   1.100 +      fun relift st =
   1.101 +        let val prop = Thm.prop_of st
   1.102 +            val subgoal_vars = (*Vars introduced in the subgoals*)
   1.103 +              fold Term.add_vars (Logic.strip_imp_prems prop) []
   1.104 +            and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) []
   1.105 +            val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
   1.106 +            val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st
   1.107 +            val emBs = map (cterm o embed) (prems_of st')
   1.108 +            val Cth  = implies_elim_list st' (map (elim o assume) emBs)
   1.109 +        in  (*restore the unknowns to the hypotheses*)
   1.110 +            free_instantiate (map swap_ctpair insts @
   1.111 +                              map mk_subgoal_swap_ctpair subgoal_insts)
   1.112 +                (*discharge assumptions from state in same order*)
   1.113 +                (implies_intr_list emBs
   1.114 +                  (forall_intr_list cparams (implies_intr_list chyps Cth)))
   1.115 +        end
   1.116 +      (*function to replace the current subgoal*)
   1.117 +      fun next st = Thm.bicompose false (false, relift st, nprems_of st) gno state
   1.118 +  in Seq.maps next (tacf subprems (trivial (cterm concl))) end;
   1.119 +
   1.120 +end;
   1.121 +
   1.122 +(*Returns the theorem list that METAHYPS would supply to its tactic*)
   1.123 +fun metahyps_thms i state =
   1.124 +  let val prem = Logic.nth_prem (i, Thm.prop_of state)
   1.125 +      and cterm = cterm_of (Thm.theory_of_thm state)
   1.126 +      val (_,_,hyps,_) = metahyps_split_prem prem
   1.127 +  in SOME (map (Thm.forall_elim_vars 0 o Thm.assume o cterm) hyps) end
   1.128 +  handle TERM ("nth_prem", [A]) => NONE;
   1.129 +
   1.130 +local
   1.131 +
   1.132 +fun print_vars_terms thy (n,thm) =
   1.133 +  let
   1.134 +    fun typed ty = " has type: " ^ Syntax.string_of_typ_global thy ty;
   1.135 +    fun find_vars thy (Const (c, ty)) =
   1.136 +          if null (Term.add_tvarsT ty []) then I
   1.137 +          else insert (op =) (c ^ typed ty)
   1.138 +      | find_vars thy (Var (xi, ty)) = insert (op =) (Term.string_of_vname xi ^ typed ty)
   1.139 +      | find_vars _ (Free _) = I
   1.140 +      | find_vars _ (Bound _) = I
   1.141 +      | find_vars thy (Abs (_, _, t)) = find_vars thy t
   1.142 +      | find_vars thy (t1 $ t2) =
   1.143 +          find_vars thy t1 #> find_vars thy t1;
   1.144 +    val prem = Logic.nth_prem (n, Thm.prop_of thm)
   1.145 +    val tms = find_vars thy prem []
   1.146 +  in
   1.147 +    (warning "Found schematic vars in assumptions:"; warning (cat_lines tms))
   1.148 +  end;
   1.149 +
   1.150 +in
   1.151 +
   1.152 +fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm
   1.153 +  handle THM("assume: variables",_,_) => (print_vars_terms (theory_of_thm thm) (n,thm); Seq.empty)
   1.154 +
   1.155 +end;
   1.156 +
   1.157 +
   1.158  (* old ways of reading terms *)
   1.159  
   1.160  fun simple_read_term thy T s =