src/Tools/misc_legacy.ML
author wenzelm
Fri, 08 Apr 2011 13:31:16 +0200
changeset 42284 326f57825e1a
parent 39288 f1ae2493d93f
child 42361 23f352990944
permissions -rw-r--r--
explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37781
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
     1
(*  Title:      Tools/misc_legacy.ML
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
     2
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
     3
Misc legacy stuff -- to be phased out eventually.
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
     4
*)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
     5
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
     6
signature MISC_LEGACY =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
     7
sig
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
     8
  val mk_defpair: term * term -> string * term
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
     9
  val get_def: theory -> xstring -> thm
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    10
  val simple_read_term: theory -> typ -> string -> term
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    11
  val METAHYPS: (thm list -> tactic) -> int -> tactic
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    12
end;
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    13
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    14
structure Misc_Legacy: MISC_LEGACY =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    15
struct
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    16
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    17
fun mk_defpair (lhs, rhs) =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    18
  (case Term.head_of lhs of
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    19
    Const (name, _) =>
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    20
      (Long_Name.base_name name ^ "_def", Logic.mk_equals (lhs, rhs))
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    21
  | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    22
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    23
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    24
fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name;
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    25
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    26
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    27
fun simple_read_term thy T s =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    28
  let
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    29
    val ctxt = ProofContext.init_global thy
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    30
      |> ProofContext.allow_dummies
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    31
      |> ProofContext.set_mode ProofContext.mode_schematic;
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    32
    val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
39288
f1ae2493d93f eliminated aliases of Type.constraint;
wenzelm
parents: 37781
diff changeset
    33
  in parse ctxt s |> Type.constraint T |> Syntax.check_term ctxt end;
37781
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    34
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    35
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    36
(**** METAHYPS -- tactical for using hypotheses as meta-level assumptions
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    37
       METAHYPS (fn prems => tac prems) i
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    38
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    39
converts subgoal i, of the form !!x1...xm. [| A1;...;An] ==> A into a new
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    40
proof state A==>A, supplying A1,...,An as meta-level assumptions (in
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    41
"prems").  The parameters x1,...,xm become free variables.  If the
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    42
resulting proof state is [| B1;...;Bk] ==> C (possibly assuming A1,...,An)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    43
then it is lifted back into the original context, yielding k subgoals.
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    44
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    45
Replaces unknowns in the context by Frees having the prefix METAHYP_
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    46
New unknowns in [| B1;...;Bk] ==> C are lifted over x1,...,xm.
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    47
DOES NOT HANDLE TYPE UNKNOWNS.
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    48
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    49
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    50
NOTE: This version does not observe the proof context, and thus cannot
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    51
work reliably.  See also Subgoal.SUBPROOF and Subgoal.FOCUS for
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    52
properly localized variants of the same idea.
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    53
****)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    54
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    55
local
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    56
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    57
(*Strips assumptions in goal yielding  ( [x1,...,xm], [H1,...,Hn], B )
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    58
    H1,...,Hn are the hypotheses;  x1...xm are variants of the parameters.
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    59
  Main difference from strip_assums concerns parameters:
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    60
    it replaces the bound variables by free variables.  *)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    61
fun strip_context_aux (params, Hs, Const ("==>", _) $ H $ B) =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    62
      strip_context_aux (params, H :: Hs, B)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    63
  | strip_context_aux (params, Hs, Const ("all",_) $ Abs (a, T, t)) =
42284
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 39288
diff changeset
    64
      let val (b, u) = Syntax_Trans.variant_abs (a, T, t)
37781
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    65
      in strip_context_aux ((b, T) :: params, Hs, u) end
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    66
  | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    67
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    68
fun strip_context A = strip_context_aux ([], [], A);
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    69
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    70
(*Left-to-right replacements: ctpairs = [...,(vi,ti),...].
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    71
  Instantiates distinct free variables by terms of same type.*)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    72
fun free_instantiate ctpairs =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    73
  forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs);
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    74
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    75
fun free_of s ((a, i), T) =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    76
  Free (s ^ (case i of 0 => a | _ => a ^ "_" ^ string_of_int i), T)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    77
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    78
fun mk_inst v = (Var v, free_of "METAHYP1_" v)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    79
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    80
fun metahyps_split_prem prem =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    81
  let (*find all vars in the hyps -- should find tvars also!*)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    82
      val hyps_vars = fold Term.add_vars (Logic.strip_assums_hyp prem) []
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    83
      val insts = map mk_inst hyps_vars
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    84
      (*replace the hyps_vars by Frees*)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    85
      val prem' = subst_atomic insts prem
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    86
      val (params,hyps,concl) = strip_context prem'
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    87
  in (insts,params,hyps,concl)  end;
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    88
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    89
fun metahyps_aux_tac tacf (prem,gno) state =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    90
  let val (insts,params,hyps,concl) = metahyps_split_prem prem
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    91
      val maxidx = Thm.maxidx_of state
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    92
      val cterm = Thm.cterm_of (Thm.theory_of_thm state)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    93
      val chyps = map cterm hyps
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    94
      val hypths = map Thm.assume chyps
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    95
      val subprems = map (Thm.forall_elim_vars 0) hypths
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    96
      val fparams = map Free params
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    97
      val cparams = map cterm fparams
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    98
      fun swap_ctpair (t,u) = (cterm u, cterm t)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    99
      (*Subgoal variables: make Free; lift type over params*)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   100
      fun mk_subgoal_inst concl_vars (v, T) =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   101
          if member (op =) concl_vars (v, T)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   102
          then ((v, T), true, free_of "METAHYP2_" (v, T))
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   103
          else ((v, T), false, free_of "METAHYP2_" (v, map #2 params ---> T))
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   104
      (*Instantiate subgoal vars by Free applied to params*)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   105
      fun mk_ctpair (v, in_concl, u) =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   106
          if in_concl then (cterm (Var v), cterm u)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   107
          else (cterm (Var v), cterm (list_comb (u, fparams)))
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   108
      (*Restore Vars with higher type and index*)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   109
      fun mk_subgoal_swap_ctpair (((a, i), T), in_concl, u as Free (_, U)) =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   110
          if in_concl then (cterm u, cterm (Var ((a, i), T)))
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   111
          else (cterm u, cterm (Var ((a, i + maxidx), U)))
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   112
      (*Embed B in the original context of params and hyps*)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   113
      fun embed B = list_all_free (params, Logic.list_implies (hyps, B))
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   114
      (*Strip the context using elimination rules*)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   115
      fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   116
      (*A form of lifting that discharges assumptions.*)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   117
      fun relift st =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   118
        let val prop = Thm.prop_of st
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   119
            val subgoal_vars = (*Vars introduced in the subgoals*)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   120
              fold Term.add_vars (Logic.strip_imp_prems prop) []
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   121
            and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) []
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   122
            val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   123
            val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   124
            val emBs = map (cterm o embed) (prems_of st')
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   125
            val Cth  = implies_elim_list st' (map (elim o Thm.assume) emBs)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   126
        in  (*restore the unknowns to the hypotheses*)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   127
            free_instantiate (map swap_ctpair insts @
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   128
                              map mk_subgoal_swap_ctpair subgoal_insts)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   129
                (*discharge assumptions from state in same order*)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   130
                (implies_intr_list emBs
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   131
                  (forall_intr_list cparams (implies_intr_list chyps Cth)))
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   132
        end
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   133
      (*function to replace the current subgoal*)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   134
      fun next st = Thm.bicompose false (false, relift st, nprems_of st) gno state
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   135
  in Seq.maps next (tacf subprems (Thm.trivial (cterm concl))) end;
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   136
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   137
fun print_vars_terms n thm =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   138
  let
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   139
    val thy = theory_of_thm thm
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   140
    fun typed s ty =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   141
      "  " ^ s ^ " has type: " ^ Syntax.string_of_typ_global thy ty;
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   142
    fun find_vars (Const (c, ty)) =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   143
          if null (Term.add_tvarsT ty []) then I
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   144
          else insert (op =) (typed c ty)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   145
      | find_vars (Var (xi, ty)) =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   146
          insert (op =) (typed (Term.string_of_vname xi) ty)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   147
      | find_vars (Free _) = I
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   148
      | find_vars (Bound _) = I
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   149
      | find_vars (Abs (_, _, t)) = find_vars t
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   150
      | find_vars (t1 $ t2) = find_vars t1 #> find_vars t2;
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   151
    val prem = Logic.nth_prem (n, Thm.prop_of thm)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   152
    val tms = find_vars prem []
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   153
  in warning (cat_lines ("Found schematic vars in assumptions:" :: tms)) end;
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   154
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   155
in
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   156
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   157
fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   158
  handle THM("assume: variables",_,_) => (print_vars_terms n thm; Seq.empty)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   159
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   160
end;
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   161
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   162
end;
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   163