src/Tools/misc_legacy.ML
author wenzelm
Tue Jun 02 09:16:19 2015 +0200 (2015-06-02)
changeset 60358 aebfbcab1eb8
parent 59621 291934bac95e
child 60642 48dd1cefb4ae
permissions -rw-r--r--
clarified context;
     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: Proof.context -> (thm list -> tactic) -> int -> tactic
    26   val freeze_thaw_robust: Proof.context -> thm -> thm * (int -> thm -> thm)
    27   val freeze_thaw: Proof.context -> 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 ctxt tacf (prem,gno) state =
   162   let val (insts,params,hyps,concl) = metahyps_split_prem prem
   163       val maxidx = Thm.maxidx_of state
   164       val chyps = map (Thm.cterm_of ctxt) hyps
   165       val hypths = map Thm.assume chyps
   166       val subprems = map (Thm.forall_elim_vars 0) hypths
   167       val fparams = map Free params
   168       val cparams = map (Thm.cterm_of ctxt) fparams
   169       fun swap_ctpair (t, u) = apply2 (Thm.cterm_of ctxt) (u, t)
   170       (*Subgoal variables: make Free; lift type over params*)
   171       fun mk_subgoal_inst concl_vars (v, T) =
   172           if member (op =) concl_vars (v, T)
   173           then ((v, T), true, free_of "METAHYP2_" (v, T))
   174           else ((v, T), false, free_of "METAHYP2_" (v, map #2 params ---> T))
   175       (*Instantiate subgoal vars by Free applied to params*)
   176       fun mk_ctpair (v, in_concl, u) =
   177           if in_concl then apply2 (Thm.cterm_of ctxt) (Var v, u)
   178           else apply2 (Thm.cterm_of ctxt) (Var v, list_comb (u, fparams))
   179       (*Restore Vars with higher type and index*)
   180       fun mk_subgoal_swap_ctpair (((a, i), T), in_concl, u as Free (_, U)) =
   181           if in_concl then apply2 (Thm.cterm_of ctxt) (u, Var ((a, i), T))
   182           else apply2 (Thm.cterm_of ctxt) (u, Var ((a, i + maxidx), U))
   183       (*Embed B in the original context of params and hyps*)
   184       fun embed B = fold_rev Logic.all fparams (Logic.list_implies (hyps, B))
   185       (*Strip the context using elimination rules*)
   186       fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths
   187       (*A form of lifting that discharges assumptions.*)
   188       fun relift st =
   189         let val prop = Thm.prop_of st
   190             val subgoal_vars = (*Vars introduced in the subgoals*)
   191               fold Term.add_vars (Logic.strip_imp_prems prop) []
   192             and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) []
   193             val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
   194             val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st
   195             val emBs = map (Thm.cterm_of ctxt o embed) (Thm.prems_of st')
   196             val Cth  = implies_elim_list st' (map (elim o Thm.assume) emBs)
   197         in  (*restore the unknowns to the hypotheses*)
   198             free_instantiate (map swap_ctpair insts @
   199                               map mk_subgoal_swap_ctpair subgoal_insts)
   200                 (*discharge assumptions from state in same order*)
   201                 (implies_intr_list emBs
   202                   (forall_intr_list cparams (implies_intr_list chyps Cth)))
   203         end
   204       (*function to replace the current subgoal*)
   205       fun next st =
   206         Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = false}
   207           (false, relift st, Thm.nprems_of st) gno state
   208   in Seq.maps next (tacf subprems (Thm.trivial (Thm.cterm_of ctxt concl))) end;
   209 
   210 fun print_vars_terms ctxt n thm =
   211   let
   212     fun typed s ty = "  " ^ s ^ " has type: " ^ Syntax.string_of_typ ctxt ty;
   213     fun find_vars (Const (c, ty)) =
   214           if null (Term.add_tvarsT ty []) then I
   215           else insert (op =) (typed c ty)
   216       | find_vars (Var (xi, ty)) =
   217           insert (op =) (typed (Term.string_of_vname xi) ty)
   218       | find_vars (Free _) = I
   219       | find_vars (Bound _) = I
   220       | find_vars (Abs (_, _, t)) = find_vars t
   221       | find_vars (t1 $ t2) = find_vars t1 #> find_vars t2;
   222     val prem = Logic.nth_prem (n, Thm.prop_of thm)
   223     val tms = find_vars prem []
   224   in warning (cat_lines ("Found schematic vars in assumptions:" :: tms)) end;
   225 
   226 in
   227 
   228 fun METAHYPS ctxt tacf n thm = SUBGOAL (metahyps_aux_tac ctxt tacf) n thm
   229   handle THM ("assume: variables", _, _) => (print_vars_terms ctxt n thm; Seq.empty)
   230 
   231 end;
   232 
   233 
   234 (* generating identifiers -- often fresh *)
   235 
   236 local
   237 (*Maps 0-61 to A-Z, a-z, 0-9; exclude _ or ' to avoid clash with internal/unusual indentifiers*)
   238 fun gensym_char i =
   239   if i<26 then chr (ord "A" + i)
   240   else if i<52 then chr (ord "a" + i - 26)
   241   else chr (ord "0" + i - 52);
   242 
   243 val char_vec = Vector.tabulate (62, gensym_char);
   244 fun newid n = implode (map (fn i => Vector.sub (char_vec, i)) (radixpand (62, n)));
   245 
   246 val gensym_seed = Synchronized.var "gensym_seed" (0: int);
   247 
   248 in
   249   fun gensym pre =
   250     Synchronized.change_result gensym_seed (fn i => (pre ^ newid i, i + 1));
   251 end;
   252 
   253 
   254 (*Convert all Vars in a theorem to Frees.  Also return a function for
   255   reversing that operation.  DOES NOT WORK FOR TYPE VARIABLES.*)
   256 
   257 fun freeze_thaw_robust ctxt th =
   258  let val fth = Thm.legacy_freezeT th
   259  in
   260    case Thm.fold_terms Term.add_vars fth [] of
   261        [] => (fth, fn _ => fn x => x)   (*No vars: nothing to do!*)
   262      | vars =>
   263          let fun newName (ix,_) = (ix, gensym (string_of_indexname ix))
   264              val alist = map newName vars
   265              fun mk_inst (v,T) =
   266                  apply2 (Thm.cterm_of ctxt)
   267                   (Var (v, T), Free (the (AList.lookup (op =) alist v), T))
   268              val insts = map mk_inst vars
   269              fun thaw i th' = (*i is non-negative increment for Var indexes*)
   270                  th' |> forall_intr_list (map #2 insts)
   271                      |> forall_elim_list (map (Thm.incr_indexes_cterm i o #1) insts)
   272          in  (Thm.instantiate ([],insts) fth, thaw)  end
   273  end;
   274 
   275 (*Basic version of the function above. No option to rename Vars apart in thaw.
   276   The Frees created from Vars have nice names.*)
   277 fun freeze_thaw ctxt th =
   278  let val fth = Thm.legacy_freezeT th
   279  in
   280    case Thm.fold_terms Term.add_vars fth [] of
   281        [] => (fth, fn x => x)
   282      | vars =>
   283          let fun newName (ix, _) (pairs, used) =
   284                    let val v = singleton (Name.variant_list used) (string_of_indexname ix)
   285                    in  ((ix,v)::pairs, v::used)  end;
   286              val (alist, _) =
   287                  fold_rev newName vars ([], Thm.fold_terms Term.add_free_names fth [])
   288              fun mk_inst (v, T) =
   289                 apply2 (Thm.cterm_of ctxt) (Var (v, T), Free (the (AList.lookup (op =) alist v), T))
   290              val insts = map mk_inst vars
   291              fun thaw th' =
   292                  th' |> forall_intr_list (map #2 insts)
   293                      |> forall_elim_list (map #1 insts)
   294          in  (Thm.instantiate ([],insts) fth, thaw)  end
   295  end;
   296 
   297 end;