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