merged
authorwenzelm
Mon Jul 27 23:41:57 2015 +0200 (2015-07-27)
changeset 60806622d45ca75ee
parent 60804 080a979a985b
parent 60805 4cc49ead6e75
child 60807 d7e6c7760db5
merged
     1.1 --- a/src/HOL/Eisbach/match_method.ML	Mon Jul 27 22:44:02 2015 +0200
     1.2 +++ b/src/HOL/Eisbach/match_method.ML	Mon Jul 27 23:41:57 2015 +0200
     1.3 @@ -504,7 +504,7 @@
     1.4        Subgoal.focus_params ctxt i bindings goal;
     1.5  
     1.6      val (inst, ctxt'') = Variable.import_inst true [Thm.term_of concl] ctxt';
     1.7 -    val (_, schematic_terms) = Thm.certify_inst ctxt'' inst;
     1.8 +    val schematic_terms = map (apsnd (Thm.cterm_of ctxt'')) (#2 inst);
     1.9  
    1.10      val goal'' = Thm.instantiate ([], schematic_terms) goal';
    1.11      val concl' = Thm.instantiate_cterm ([], schematic_terms) concl;
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Jul 27 22:44:02 2015 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Jul 27 23:41:57 2015 +0200
     2.3 @@ -947,9 +947,11 @@
     2.4      val U = TFree ("'u", @{sort type})
     2.5      val y = Free (yname, U)
     2.6      val f' = absdummy (U --> T') (Bound 0 $ y)
     2.7 -    val th' = Thm.certify_instantiate ctxt'
     2.8 -      ([(dest_TVar uninst_T, U --> T'), (dest_TVar uninst_T', T')],
     2.9 -       [((fst (dest_Var f), (U --> T') --> T'), f')]) th
    2.10 +    val th' =
    2.11 +      Thm.instantiate
    2.12 +        ([(dest_TVar uninst_T, Thm.ctyp_of ctxt' (U --> T')),
    2.13 +          (dest_TVar uninst_T', Thm.ctyp_of ctxt' T')],
    2.14 +         [((fst (dest_Var f), (U --> T') --> T'), Thm.cterm_of ctxt' f')]) th
    2.15      val [th'] = Variable.export (Variable.declare_thm th' ctxt') ctxt [th']
    2.16    in
    2.17      th'
    2.18 @@ -1075,10 +1077,10 @@
    2.19              val subst = Sign.typ_match thy (fastype_of pred', fastype_of pred) Vartab.empty
    2.20                handle Type.TYPE_MATCH =>
    2.21                  error ("Type mismatch of predicate " ^ fst (dest_Const pred) ^
    2.22 -                  " (trying to match " ^ Syntax.string_of_typ ctxt (fastype_of pred') ^
    2.23 -                  " and " ^ Syntax.string_of_typ ctxt (fastype_of pred) ^ ")" ^
    2.24 -                  " in " ^ Display.string_of_thm ctxt th)
    2.25 -          in map (fn (indexname, (s, T)) => ((indexname, s), T)) (Vartab.dest subst) end
    2.26 +                  " (trying to match " ^ Syntax.string_of_typ ctxt' (fastype_of pred') ^
    2.27 +                  " and " ^ Syntax.string_of_typ ctxt' (fastype_of pred) ^ ")" ^
    2.28 +                  " in " ^ Display.string_of_thm ctxt' th)
    2.29 +          in map (fn (xi, (S, T)) => ((xi, S), T)) (Vartab.dest subst) end
    2.30          fun instantiate_typ th =
    2.31            let
    2.32              val (pred', _) = strip_intro_concl th
    2.33 @@ -1086,13 +1088,13 @@
    2.34                if not (fst (dest_Const pred) = fst (dest_Const pred')) then
    2.35                  raise Fail "Trying to instantiate another predicate"
    2.36                else ()
    2.37 -          in Thm.certify_instantiate ctxt' (subst_of (pred', pred), []) th end
    2.38 +          in Thm.instantiate (map (apsnd (Thm.ctyp_of ctxt')) (subst_of (pred', pred)), []) th end
    2.39          fun instantiate_ho_args th =
    2.40            let
    2.41              val (_, args') =
    2.42                (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o Thm.prop_of) th
    2.43              val ho_args' = map dest_Var (ho_args_of_typ T args')
    2.44 -          in Thm.certify_instantiate ctxt' ([], ho_args' ~~ ho_args) th end
    2.45 +          in Thm.instantiate ([], ho_args' ~~ map (Thm.cterm_of ctxt') ho_args) th end
    2.46          val outp_pred =
    2.47            Term_Subst.instantiate (subst_of (inp_pred, pred), []) inp_pred
    2.48          val ((_, ths'), ctxt1) =
     3.1 --- a/src/HOL/Tools/Transfer/transfer.ML	Mon Jul 27 22:44:02 2015 +0200
     3.2 +++ b/src/HOL/Tools/Transfer/transfer.ML	Mon Jul 27 23:41:57 2015 +0200
     3.3 @@ -693,10 +693,11 @@
     3.4      val err_msg = "Transfer failed to convert goal to an object-logic formula"
     3.5      val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
     3.6      val thm1 = Drule.forall_intr_vars thm
     3.7 -    val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) [])
     3.8 -                |> map (fn v as ((a, _), S) => (v, TFree (a, S)))
     3.9 +    val instT =
    3.10 +      rev (Term.add_tvars (Thm.full_prop_of thm1) [])
    3.11 +      |> map (fn v as ((a, _), S) => (v, Thm.ctyp_of ctxt (TFree (a, S))))
    3.12      val thm2 = thm1
    3.13 -      |> Thm.certify_instantiate ctxt (instT, [])
    3.14 +      |> Thm.instantiate (instT, [])
    3.15        |> Raw_Simplifier.rewrite_rule ctxt pre_simps
    3.16      val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
    3.17      val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
    3.18 @@ -709,7 +710,7 @@
    3.19              THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1
    3.20          handle TERM (_, ts) => raise TERM (err_msg, ts)
    3.21      val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
    3.22 -    val tnames = map (fst o dest_TFree o snd) instT
    3.23 +    val tnames = map (fst o dest_TFree o Thm.typ_of o snd) instT
    3.24    in
    3.25      thm3
    3.26        |> Raw_Simplifier.rewrite_rule ctxt' post_simps
    3.27 @@ -729,10 +730,11 @@
    3.28      val err_msg = "Transfer failed to convert goal to an object-logic formula"
    3.29      val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
    3.30      val thm1 = Drule.forall_intr_vars thm
    3.31 -    val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) [])
    3.32 -                |> map (fn v as ((a, _), S) => (v, TFree (a, S)))
    3.33 +    val instT =
    3.34 +      rev (Term.add_tvars (Thm.full_prop_of thm1) [])
    3.35 +      |> map (fn v as ((a, _), S) => (v, Thm.ctyp_of ctxt (TFree (a, S))))
    3.36      val thm2 = thm1
    3.37 -      |> Thm.certify_instantiate ctxt (instT, [])
    3.38 +      |> Thm.instantiate (instT, [])
    3.39        |> Raw_Simplifier.rewrite_rule ctxt pre_simps
    3.40      val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
    3.41      val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
    3.42 @@ -745,7 +747,7 @@
    3.43              THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1
    3.44          handle TERM (_, ts) => raise TERM (err_msg, ts)
    3.45      val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
    3.46 -    val tnames = map (fst o dest_TFree o snd) instT
    3.47 +    val tnames = map (fst o dest_TFree o Thm.typ_of o snd) instT
    3.48    in
    3.49      thm3
    3.50        |> Raw_Simplifier.rewrite_rule ctxt' post_simps
     4.1 --- a/src/Pure/Isar/code.ML	Mon Jul 27 22:44:02 2015 +0200
     4.2 +++ b/src/Pure/Isar/code.ML	Mon Jul 27 23:41:57 2015 +0200
     4.3 @@ -638,14 +638,15 @@
     4.4  fun desymbolize_tvars thy thms =
     4.5    let
     4.6      val tvs = fold (Term.add_tvars o Thm.prop_of) thms [];
     4.7 -    val tvar_subst = mk_desymbolization (unprefix "'") (prefix "'") TVar tvs;
     4.8 -  in map (Thm.global_certify_instantiate thy (tvar_subst, [])) thms end;
     4.9 +    val instT =
    4.10 +      mk_desymbolization (unprefix "'") (prefix "'") (Thm.global_ctyp_of thy o TVar) tvs;
    4.11 +  in map (Thm.instantiate (instT, [])) thms end;
    4.12  
    4.13  fun desymbolize_vars thy thm =
    4.14    let
    4.15      val vs = Term.add_vars (Thm.prop_of thm) [];
    4.16 -    val var_subst = mk_desymbolization I I Var vs;
    4.17 -  in Thm.global_certify_instantiate thy ([], var_subst) thm end;
    4.18 +    val inst = mk_desymbolization I I (Thm.global_cterm_of thy o Var) vs;
    4.19 +  in Thm.instantiate ([], inst) thm end;
    4.20  
    4.21  fun canonize_thms thy = desymbolize_tvars thy #> same_arity thy #> map (desymbolize_vars thy);
    4.22  
    4.23 @@ -700,13 +701,13 @@
    4.24      val mapping = map2 (fn (v, sort) => fn sort' =>
    4.25        (v, Sorts.inter_sort (Sign.classes_of thy) (sort, sort'))) vs sorts;
    4.26      val inst = map2 (fn (v, sort) => fn (_, sort') =>
    4.27 -      (((v, 0), sort), TFree (v, sort'))) vs mapping;
    4.28 +      (((v, 0), sort), Thm.global_ctyp_of thy (TFree (v, sort')))) vs mapping;
    4.29      val subst = (map_types o map_type_tfree)
    4.30        (fn (v, _) => TFree (v, the (AList.lookup (op =) mapping v)));
    4.31    in
    4.32      thm
    4.33      |> Thm.varifyT_global
    4.34 -    |> Thm.global_certify_instantiate thy (inst, [])
    4.35 +    |> Thm.instantiate (inst, [])
    4.36      |> pair subst
    4.37    end;
    4.38  
    4.39 @@ -771,7 +772,7 @@
    4.40          val sorts = map_transpose inter_sorts vss;
    4.41          val vts = Name.invent_names Name.context Name.aT sorts;
    4.42          val thms' =
    4.43 -          map2 (fn vs => Thm.certify_instantiate ctxt (vs ~~ map TFree vts, [])) vss thms;
    4.44 +          map2 (fn vs => Thm.instantiate (vs ~~ map (Thm.ctyp_of ctxt o TFree) vts, [])) vss thms;
    4.45          val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms'))));
    4.46          fun head_conv ct = if can Thm.dest_comb ct
    4.47            then Conv.fun_conv head_conv ct
     5.1 --- a/src/Pure/Isar/subgoal.ML	Mon Jul 27 22:44:02 2015 +0200
     5.2 +++ b/src/Pure/Isar/subgoal.ML	Mon Jul 27 23:41:57 2015 +0200
     5.3 @@ -55,7 +55,7 @@
     5.4      val text = asms @ (if do_concl then [concl] else []);
     5.5  
     5.6      val (inst, ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2;
     5.7 -    val (_, schematic_terms) = Thm.certify_inst ctxt3 inst;
     5.8 +    val schematic_terms = map (apsnd (Thm.cterm_of ctxt3)) (#2 inst);
     5.9  
    5.10      val schematics = (schematic_types, schematic_terms);
    5.11      val asms' = map (Thm.instantiate_cterm schematics) asms;
     6.1 --- a/src/Pure/drule.ML	Mon Jul 27 22:44:02 2015 +0200
     6.2 +++ b/src/Pure/drule.ML	Mon Jul 27 23:41:57 2015 +0200
     6.3 @@ -206,10 +206,10 @@
     6.4      val Ts = map Term.fastype_of ps;
     6.5      val inst =
     6.6        Thm.fold_terms Term.add_vars th []
     6.7 -      |> map (fn (xi, T) => ((xi, T), Term.list_comb (Var (xi, Ts ---> T), ps)));
     6.8 +      |> map (fn (xi, T) => ((xi, T), Thm.cterm_of ctxt (Term.list_comb (Var (xi, Ts ---> T), ps))));
     6.9    in
    6.10      th
    6.11 -    |> Thm.certify_instantiate ctxt ([], inst)
    6.12 +    |> Thm.instantiate ([], inst)
    6.13      |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt) ps
    6.14    end;
    6.15  
    6.16 @@ -230,8 +230,11 @@
    6.17    | zero_var_indexes_list ths =
    6.18        let
    6.19          val thy = Theory.merge_list (map Thm.theory_of_thm ths);
    6.20 -        val insts = Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths);
    6.21 -      in map (Thm.adjust_maxidx_thm ~1 o Thm.global_certify_instantiate thy insts) ths end;
    6.22 +        val (instT, inst) = Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths);
    6.23 +        val insts' =
    6.24 +         (map (apsnd (Thm.global_ctyp_of thy)) instT,
    6.25 +          map (apsnd (Thm.global_cterm_of thy)) inst);
    6.26 +      in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate insts') ths end;
    6.27  
    6.28  val zero_var_indexes = singleton zero_var_indexes_list;
    6.29  
     7.1 --- a/src/Pure/more_thm.ML	Mon Jul 27 22:44:02 2015 +0200
     7.2 +++ b/src/Pure/more_thm.ML	Mon Jul 27 23:41:57 2015 +0200
     7.3 @@ -61,16 +61,6 @@
     7.4    val forall_elim_var: int -> thm -> thm
     7.5    val forall_elim_vars: int -> thm -> thm
     7.6    val instantiate': ctyp option list -> cterm option list -> thm -> thm
     7.7 -  val global_certify_inst: theory ->
     7.8 -    ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
     7.9 -    ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
    7.10 -  val global_certify_instantiate: theory ->
    7.11 -    ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm
    7.12 -  val certify_inst: Proof.context ->
    7.13 -    ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
    7.14 -    ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
    7.15 -  val certify_instantiate: Proof.context ->
    7.16 -    ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm
    7.17    val forall_intr_frees: thm -> thm
    7.18    val unvarify_global: thm -> thm
    7.19    val close_derivation: thm -> thm
    7.20 @@ -375,23 +365,6 @@
    7.21    in thm'' end;
    7.22  
    7.23  
    7.24 -(* certify_instantiate *)
    7.25 -
    7.26 -fun global_certify_inst thy (instT, inst) =
    7.27 - (map (apsnd (Thm.global_ctyp_of thy)) instT,
    7.28 -  map (apsnd (Thm.global_cterm_of thy)) inst);
    7.29 -
    7.30 -fun global_certify_instantiate thy insts th =
    7.31 -  Thm.instantiate (global_certify_inst thy insts) th;
    7.32 -
    7.33 -fun certify_inst ctxt (instT, inst) =
    7.34 - (map (apsnd (Thm.ctyp_of ctxt)) instT,
    7.35 -  map (apsnd (Thm.cterm_of ctxt)) inst);
    7.36 -
    7.37 -fun certify_instantiate ctxt insts th =
    7.38 -  Thm.instantiate (certify_inst ctxt insts) th;
    7.39 -
    7.40 -
    7.41  (* forall_intr_frees: generalization over all suitable Free variables *)
    7.42  
    7.43  fun forall_intr_frees th =
    7.44 @@ -417,8 +390,8 @@
    7.45      val instT = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S)));
    7.46      val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) =>
    7.47        let val T' = Term_Subst.instantiateT instT T
    7.48 -      in (((a, i), T'), Free ((a, T'))) end);
    7.49 -  in global_certify_instantiate thy (instT, inst) th end;
    7.50 +      in (((a, i), T'), Thm.global_cterm_of thy (Free ((a, T')))) end);
    7.51 +  in Thm.instantiate (map (apsnd (Thm.global_ctyp_of thy)) instT, inst) th end;
    7.52  
    7.53  
    7.54  (* close_derivation *)
     8.1 --- a/src/Pure/variable.ML	Mon Jul 27 22:44:02 2015 +0200
     8.2 +++ b/src/Pure/variable.ML	Mon Jul 27 23:41:57 2015 +0200
     8.3 @@ -600,8 +600,8 @@
     8.4  fun importT ths ctxt =
     8.5    let
     8.6      val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt;
     8.7 -    val insts' as (instT', _) = Thm.certify_inst ctxt' (instT, []);
     8.8 -    val ths' = map (Thm.instantiate insts') ths;
     8.9 +    val instT' = map (apsnd (Thm.ctyp_of ctxt')) instT;
    8.10 +    val ths' = map (Thm.instantiate (instT', [])) ths;
    8.11    in ((instT', ths'), ctxt') end;
    8.12  
    8.13  fun import_prf is_open prf ctxt =
    8.14 @@ -612,8 +612,10 @@
    8.15  
    8.16  fun import is_open ths ctxt =
    8.17    let
    8.18 -    val (insts, ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;
    8.19 -    val insts' = Thm.certify_inst ctxt' insts;
    8.20 +    val ((instT, inst), ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;
    8.21 +    val insts' =
    8.22 +     (map (apsnd (Thm.ctyp_of ctxt')) instT,
    8.23 +      map (apsnd (Thm.cterm_of ctxt')) inst);
    8.24      val ths' = map (Thm.instantiate insts') ths;
    8.25    in ((insts', ths'), ctxt') end;
    8.26  
     9.1 --- a/src/Tools/Code/code_preproc.ML	Mon Jul 27 22:44:02 2015 +0200
     9.2 +++ b/src/Tools/Code/code_preproc.ML	Mon Jul 27 23:41:57 2015 +0200
     9.3 @@ -168,17 +168,19 @@
     9.4  fun normalized_tfrees_sandwich ctxt ct =
     9.5    let
     9.6      val t = Thm.term_of ct;
     9.7 -    val vs_original = fold_term_types (K (fold_atyps (insert (eq_fst op =)
     9.8 -      o dest_TFree))) t [];
     9.9 +    val vs_original =
    9.10 +      fold_term_types (K (fold_atyps (insert (eq_fst op =) o dest_TFree))) t [];
    9.11      val vs_normalized = Name.invent_names Name.context Name.aT (map snd vs_original);
    9.12 -    val normalize = map_type_tfree (TFree o the o AList.lookup (op =) (vs_original ~~ vs_normalized));
    9.13 +    val normalize =
    9.14 +      map_type_tfree (TFree o the o AList.lookup (op =) (vs_original ~~ vs_normalized));
    9.15      val normalization =
    9.16 -      map2 (fn (v, sort) => fn (v', _) => (((v', 0), sort), TFree (v, sort))) vs_original vs_normalized;
    9.17 +      map2 (fn (v, sort) => fn (v', _) => (((v', 0), sort), Thm.ctyp_of ctxt (TFree (v, sort))))
    9.18 +        vs_original vs_normalized;
    9.19    in
    9.20      if eq_list (eq_fst (op =)) (vs_normalized, vs_original)
    9.21      then (I, ct)
    9.22      else
    9.23 -     (Thm.certify_instantiate ctxt (normalization, []) o Thm.varifyT_global,
    9.24 +     (Thm.instantiate (normalization, []) o Thm.varifyT_global,
    9.25        Thm.cterm_of ctxt (map_types normalize t))
    9.26    end;
    9.27