src/Tools/misc_legacy.ML
author wenzelm
Fri Aug 15 18:02:34 2014 +0200 (2014-08-15)
changeset 57944 fff8d328da56
parent 56245 84fc7dfa3cd4
child 58950 d07464875dd4
permissions -rw-r--r--
more informative Token.Name with history of morphisms;
tuned signature;
     1 (*  Title:      Tools/misc_legacy.ML
     2 
     3 Misc legacy stuff -- to be phased out eventually.
     4 *)
     5 
     6 signature MISC_LEGACY =
     7 sig
     8   val add_term_names: term * string list -> string list
     9   val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
    10   val add_typ_tfree_names: typ * string list -> string list
    11   val add_typ_tfrees: typ * (string * sort) list -> (string * sort) list
    12   val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
    13   val add_term_tfrees: term * (string * sort) list -> (string * sort) list
    14   val add_term_tfree_names: term * string list -> string list
    15   val typ_tfrees: typ -> (string * sort) list
    16   val typ_tvars: typ -> (indexname * sort) list
    17   val term_tfrees: term -> (string * sort) list
    18   val term_tvars: term -> (indexname * sort) list
    19   val add_term_vars: term * term list -> term list
    20   val term_vars: term -> term list
    21   val add_term_frees: term * term list -> term list
    22   val term_frees: term -> term list
    23   val mk_defpair: term * term -> string * term
    24   val get_def: theory -> xstring -> thm
    25   val METAHYPS: (thm list -> tactic) -> int -> tactic
    26   val freeze_thaw_robust: thm -> thm * (int -> thm -> thm)
    27   val freeze_thaw: thm -> thm * (thm -> thm)
    28 end;
    29 
    30 structure Misc_Legacy: MISC_LEGACY =
    31 struct
    32 
    33 (*iterate a function over all types in a term*)
    34 fun it_term_types f =
    35 let fun iter(Const(_,T), a) = f(T,a)
    36       | iter(Free(_,T), a) = f(T,a)
    37       | iter(Var(_,T), a) = f(T,a)
    38       | iter(Abs(_,T,t), a) = iter(t,f(T,a))
    39       | iter(f$u, a) = iter(f, iter(u, a))
    40       | iter(Bound _, a) = a
    41 in iter end
    42 
    43 (*Accumulates the names in the term, suppressing duplicates.
    44   Includes Frees and Consts.  For choosing unambiguous bound var names.*)
    45 fun add_term_names (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs
    46   | add_term_names (Free(a,_), bs) = insert (op =) a bs
    47   | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
    48   | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
    49   | add_term_names (_, bs) = bs;
    50 
    51 (*Accumulates the TVars in a type, suppressing duplicates.*)
    52 fun add_typ_tvars(Type(_,Ts),vs) = List.foldr add_typ_tvars vs Ts
    53   | add_typ_tvars(TFree(_),vs) = vs
    54   | add_typ_tvars(TVar(v),vs) = insert (op =) v vs;
    55 
    56 (*Accumulates the TFrees in a type, suppressing duplicates.*)
    57 fun add_typ_tfree_names(Type(_,Ts),fs) = List.foldr add_typ_tfree_names fs Ts
    58   | add_typ_tfree_names(TFree(f,_),fs) = insert (op =) f fs
    59   | add_typ_tfree_names(TVar(_),fs) = fs;
    60 
    61 fun add_typ_tfrees(Type(_,Ts),fs) = List.foldr add_typ_tfrees fs Ts
    62   | add_typ_tfrees(TFree(f),fs) = insert (op =) f fs
    63   | add_typ_tfrees(TVar(_),fs) = fs;
    64 
    65 (*Accumulates the TVars in a term, suppressing duplicates.*)
    66 val add_term_tvars = it_term_types add_typ_tvars;
    67 
    68 (*Accumulates the TFrees in a term, suppressing duplicates.*)
    69 val add_term_tfrees = it_term_types add_typ_tfrees;
    70 val add_term_tfree_names = it_term_types add_typ_tfree_names;
    71 
    72 (*Non-list versions*)
    73 fun typ_tfrees T = add_typ_tfrees(T,[]);
    74 fun typ_tvars T = add_typ_tvars(T,[]);
    75 fun term_tfrees t = add_term_tfrees(t,[]);
    76 fun term_tvars t = add_term_tvars(t,[]);
    77 
    78 
    79 (*Accumulates the Vars in the term, suppressing duplicates.*)
    80 fun add_term_vars (t, vars: term list) = case t of
    81     Var   _ => Ord_List.insert Term_Ord.term_ord t vars
    82   | Abs (_,_,body) => add_term_vars(body,vars)
    83   | f$t =>  add_term_vars (f, add_term_vars(t, vars))
    84   | _ => vars;
    85 
    86 fun term_vars t = add_term_vars(t,[]);
    87 
    88 (*Accumulates the Frees in the term, suppressing duplicates.*)
    89 fun add_term_frees (t, frees: term list) = case t of
    90     Free   _ => Ord_List.insert Term_Ord.term_ord t frees
    91   | Abs (_,_,body) => add_term_frees(body,frees)
    92   | f$t =>  add_term_frees (f, add_term_frees(t, frees))
    93   | _ => frees;
    94 
    95 fun term_frees t = add_term_frees(t,[]);
    96 
    97 
    98 fun mk_defpair (lhs, rhs) =
    99   (case Term.head_of lhs of
   100     Const (name, _) =>
   101       (Thm.def_name (Long_Name.base_name name), Logic.mk_equals (lhs, rhs))
   102   | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
   103 
   104 
   105 fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name;
   106 
   107 
   108 (**** METAHYPS -- tactical for using hypotheses as meta-level assumptions
   109        METAHYPS (fn prems => tac prems) i
   110 
   111 converts subgoal i, of the form !!x1...xm. [| A1;...;An] ==> A into a new
   112 proof state A==>A, supplying A1,...,An as meta-level assumptions (in
   113 "prems").  The parameters x1,...,xm become free variables.  If the
   114 resulting proof state is [| B1;...;Bk] ==> C (possibly assuming A1,...,An)
   115 then it is lifted back into the original context, yielding k subgoals.
   116 
   117 Replaces unknowns in the context by Frees having the prefix METAHYP_
   118 New unknowns in [| B1;...;Bk] ==> C are lifted over x1,...,xm.
   119 DOES NOT HANDLE TYPE UNKNOWNS.
   120 
   121 
   122 NOTE: This version does not observe the proof context, and thus cannot
   123 work reliably.  See also Subgoal.SUBPROOF and Subgoal.FOCUS for
   124 properly localized variants of the same idea.
   125 ****)
   126 
   127 local
   128 
   129 (*Strips assumptions in goal yielding  ( [x1,...,xm], [H1,...,Hn], B )
   130     H1,...,Hn are the hypotheses;  x1...xm are variants of the parameters.
   131   Main difference from strip_assums concerns parameters:
   132     it replaces the bound variables by free variables.  *)
   133 fun strip_context_aux (params, Hs, Const (@{const_name Pure.imp}, _) $ H $ B) =
   134       strip_context_aux (params, H :: Hs, B)
   135   | strip_context_aux (params, Hs, Const (@{const_name Pure.all},_) $ Abs (a, T, t)) =
   136       let val (b, u) = Syntax_Trans.variant_abs (a, T, t)
   137       in strip_context_aux ((b, T) :: params, Hs, u) end
   138   | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);
   139 
   140 fun strip_context A = strip_context_aux ([], [], A);
   141 
   142 (*Left-to-right replacements: ctpairs = [...,(vi,ti),...].
   143   Instantiates distinct free variables by terms of same type.*)
   144 fun free_instantiate ctpairs =
   145   forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs);
   146 
   147 fun free_of s ((a, i), T) =
   148   Free (s ^ (case i of 0 => a | _ => a ^ "_" ^ string_of_int i), T)
   149 
   150 fun mk_inst v = (Var v, free_of "METAHYP1_" v)
   151 
   152 fun metahyps_split_prem prem =
   153   let (*find all vars in the hyps -- should find tvars also!*)
   154       val hyps_vars = fold Term.add_vars (Logic.strip_assums_hyp prem) []
   155       val insts = map mk_inst hyps_vars
   156       (*replace the hyps_vars by Frees*)
   157       val prem' = subst_atomic insts prem
   158       val (params,hyps,concl) = strip_context prem'
   159   in (insts,params,hyps,concl)  end;
   160 
   161 fun metahyps_aux_tac tacf (prem,gno) state =
   162   let val (insts,params,hyps,concl) = metahyps_split_prem prem
   163       val maxidx = Thm.maxidx_of state
   164       val cterm = Thm.cterm_of (Thm.theory_of_thm state)
   165       val chyps = map cterm hyps
   166       val hypths = map Thm.assume chyps
   167       val subprems = map (Thm.forall_elim_vars 0) hypths
   168       val fparams = map Free params
   169       val cparams = map cterm fparams
   170       fun swap_ctpair (t,u) = (cterm u, cterm t)
   171       (*Subgoal variables: make Free; lift type over params*)
   172       fun mk_subgoal_inst concl_vars (v, T) =
   173           if member (op =) concl_vars (v, T)
   174           then ((v, T), true, free_of "METAHYP2_" (v, T))
   175           else ((v, T), false, free_of "METAHYP2_" (v, map #2 params ---> T))
   176       (*Instantiate subgoal vars by Free applied to params*)
   177       fun mk_ctpair (v, in_concl, u) =
   178           if in_concl then (cterm (Var v), cterm u)
   179           else (cterm (Var v), cterm (list_comb (u, fparams)))
   180       (*Restore Vars with higher type and index*)
   181       fun mk_subgoal_swap_ctpair (((a, i), T), in_concl, u as Free (_, U)) =
   182           if in_concl then (cterm u, cterm (Var ((a, i), T)))
   183           else (cterm u, cterm (Var ((a, i + maxidx), U)))
   184       (*Embed B in the original context of params and hyps*)
   185       fun embed B = fold_rev Logic.all fparams (Logic.list_implies (hyps, B))
   186       (*Strip the context using elimination rules*)
   187       fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths
   188       (*A form of lifting that discharges assumptions.*)
   189       fun relift st =
   190         let val prop = Thm.prop_of st
   191             val subgoal_vars = (*Vars introduced in the subgoals*)
   192               fold Term.add_vars (Logic.strip_imp_prems prop) []
   193             and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) []
   194             val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
   195             val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st
   196             val emBs = map (cterm o embed) (prems_of st')
   197             val Cth  = implies_elim_list st' (map (elim o Thm.assume) emBs)
   198         in  (*restore the unknowns to the hypotheses*)
   199             free_instantiate (map swap_ctpair insts @
   200                               map mk_subgoal_swap_ctpair subgoal_insts)
   201                 (*discharge assumptions from state in same order*)
   202                 (implies_intr_list emBs
   203                   (forall_intr_list cparams (implies_intr_list chyps Cth)))
   204         end
   205       (*function to replace the current subgoal*)
   206       fun next st =
   207         Thm.bicompose {flatten = true, match = false, incremented = false}
   208           (false, relift st, nprems_of st) gno state
   209   in Seq.maps next (tacf subprems (Thm.trivial (cterm concl))) end;
   210 
   211 fun print_vars_terms n thm =
   212   let
   213     val thy = theory_of_thm thm
   214     fun typed s ty =
   215       "  " ^ s ^ " has type: " ^ Syntax.string_of_typ_global thy ty;
   216     fun find_vars (Const (c, ty)) =
   217           if null (Term.add_tvarsT ty []) then I
   218           else insert (op =) (typed c ty)
   219       | find_vars (Var (xi, ty)) =
   220           insert (op =) (typed (Term.string_of_vname xi) ty)
   221       | find_vars (Free _) = I
   222       | find_vars (Bound _) = I
   223       | find_vars (Abs (_, _, t)) = find_vars t
   224       | find_vars (t1 $ t2) = find_vars t1 #> find_vars t2;
   225     val prem = Logic.nth_prem (n, Thm.prop_of thm)
   226     val tms = find_vars prem []
   227   in warning (cat_lines ("Found schematic vars in assumptions:" :: tms)) end;
   228 
   229 in
   230 
   231 fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm
   232   handle THM("assume: variables",_,_) => (print_vars_terms n thm; Seq.empty)
   233 
   234 end;
   235 
   236 
   237 (* generating identifiers -- often fresh *)
   238 
   239 local
   240 (*Maps 0-61 to A-Z, a-z, 0-9; exclude _ or ' to avoid clash with internal/unusual indentifiers*)
   241 fun gensym_char i =
   242   if i<26 then chr (ord "A" + i)
   243   else if i<52 then chr (ord "a" + i - 26)
   244   else chr (ord "0" + i - 52);
   245 
   246 val char_vec = Vector.tabulate (62, gensym_char);
   247 fun newid n = implode (map (fn i => Vector.sub (char_vec, i)) (radixpand (62, n)));
   248 
   249 val gensym_seed = Synchronized.var "gensym_seed" (0: int);
   250 
   251 in
   252   fun gensym pre =
   253     Synchronized.change_result gensym_seed (fn i => (pre ^ newid i, i + 1));
   254 end;
   255 
   256 
   257 (*Convert all Vars in a theorem to Frees.  Also return a function for
   258   reversing that operation.  DOES NOT WORK FOR TYPE VARIABLES.*)
   259 
   260 fun freeze_thaw_robust th =
   261  let val fth = Thm.legacy_freezeT th
   262      val thy = Thm.theory_of_thm fth
   263  in
   264    case Thm.fold_terms Term.add_vars fth [] of
   265        [] => (fth, fn _ => fn x => x)   (*No vars: nothing to do!*)
   266      | vars =>
   267          let fun newName (ix,_) = (ix, gensym (string_of_indexname ix))
   268              val alist = map newName vars
   269              fun mk_inst (v,T) =
   270                  (cterm_of thy (Var(v,T)),
   271                   cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
   272              val insts = map mk_inst vars
   273              fun thaw i th' = (*i is non-negative increment for Var indexes*)
   274                  th' |> forall_intr_list (map #2 insts)
   275                      |> forall_elim_list (map (Thm.incr_indexes_cterm i o #1) insts)
   276          in  (Thm.instantiate ([],insts) fth, thaw)  end
   277  end;
   278 
   279 (*Basic version of the function above. No option to rename Vars apart in thaw.
   280   The Frees created from Vars have nice names.*)
   281 fun freeze_thaw th =
   282  let val fth = Thm.legacy_freezeT th
   283      val thy = Thm.theory_of_thm fth
   284  in
   285    case Thm.fold_terms Term.add_vars fth [] of
   286        [] => (fth, fn x => x)
   287      | vars =>
   288          let fun newName (ix, _) (pairs, used) =
   289                    let val v = singleton (Name.variant_list used) (string_of_indexname ix)
   290                    in  ((ix,v)::pairs, v::used)  end;
   291              val (alist, _) =
   292                  fold_rev newName vars ([], Thm.fold_terms Term.add_free_names fth [])
   293              fun mk_inst (v, T) =
   294                  (cterm_of thy (Var(v,T)),
   295                   cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
   296              val insts = map mk_inst vars
   297              fun thaw th' =
   298                  th' |> forall_intr_list (map #2 insts)
   299                      |> forall_elim_list (map #1 insts)
   300          in  (Thm.instantiate ([],insts) fth, thaw)  end
   301  end;
   302 
   303 end;
   304