src/HOL/Nominal/nominal_datatype.ML
changeset 51122 386a117925db
parent 49835 31f32ec4d766
child 51671 0d142a78fb7c
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Thu Feb 14 16:35:32 2013 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Feb 14 16:36:21 2013 +0100
     1.3 @@ -197,7 +197,8 @@
     1.4  
     1.5      val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
     1.6  
     1.7 -    val (full_new_type_names',thy1) = Datatype.add_datatype config dts'' thy;
     1.8 +    val (full_new_type_names',thy1) = Datatype.add_datatype config dts'' thy
     1.9 +      ||> Theory.checkpoint;
    1.10  
    1.11      val {descr, induct, ...} = Datatype.the_info thy1 (hd full_new_type_names');
    1.12      fun nth_dtyp i = Datatype_Aux.typ_of_dtyp descr (Datatype.DtRec i);
    1.13 @@ -254,7 +255,8 @@
    1.14        Primrec.add_primrec_overloaded
    1.15          (map (fn (s, sT) => (s, sT, false))
    1.16             (List.take (perm_names' ~~ perm_names_types, length new_type_names)))
    1.17 -        (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs thy1;
    1.18 +        (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs thy1
    1.19 +      ||> Theory.checkpoint;
    1.20  
    1.21      (**** prove that permutation functions introduced by unfolding are ****)
    1.22      (**** equivalent to already existing permutation functions         ****)
    1.23 @@ -268,7 +270,7 @@
    1.24      val unfolded_perm_eq_thms =
    1.25        if length descr = length new_type_names then []
    1.26        else map Drule.export_without_context (List.drop (Datatype_Aux.split_conj_thm
    1.27 -        (Goal.prove_global thy2 [] []
    1.28 +        (Goal.prove_global_future thy2 [] []
    1.29            (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    1.30              (map (fn (c as (s, T), x) =>
    1.31                 let val [T1, T2] = binder_types T
    1.32 @@ -288,7 +290,7 @@
    1.33      val perm_empty_thms = maps (fn a =>
    1.34        let val permT = mk_permT (Type (a, []))
    1.35        in map Drule.export_without_context (List.take (Datatype_Aux.split_conj_thm
    1.36 -        (Goal.prove_global thy2 [] []
    1.37 +        (Goal.prove_global_future thy2 [] []
    1.38            (augment_sort thy2 [pt_class_of thy2 a]
    1.39              (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    1.40                (map (fn ((s, T), x) => HOLogic.mk_eq
    1.41 @@ -320,7 +322,7 @@
    1.42          val pt2' = pt_inst RS pt2;
    1.43          val pt2_ax = Global_Theory.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "2") a);
    1.44        in List.take (map Drule.export_without_context (Datatype_Aux.split_conj_thm
    1.45 -        (Goal.prove_global thy2 [] []
    1.46 +        (Goal.prove_global_future thy2 [] []
    1.47             (augment_sort thy2 [pt_class_of thy2 a]
    1.48               (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    1.49                  (map (fn ((s, T), x) =>
    1.50 @@ -355,7 +357,7 @@
    1.51          val pt3_rev' = at_inst RS (pt_inst RS pt3_rev);
    1.52          val pt3_ax = Global_Theory.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "3") a);
    1.53        in List.take (map Drule.export_without_context (Datatype_Aux.split_conj_thm
    1.54 -        (Goal.prove_global thy2 [] []
    1.55 +        (Goal.prove_global_future thy2 [] []
    1.56            (augment_sort thy2 [pt_class_of thy2 a] (Logic.mk_implies
    1.57               (HOLogic.mk_Trueprop (Const ("Nominal.prm_eq",
    1.58                  permT --> permT --> HOLogic.boolT) $ pi1 $ pi2),
    1.59 @@ -405,7 +407,7 @@
    1.60                  at_inst RS (pt_inst RS pt_perm_compose_rev) RS sym]
    1.61              end))
    1.62          val sort = Sign.minimize_sort thy (Sign.certify_sort thy (cp_class :: pt_class));
    1.63 -        val thms = Datatype_Aux.split_conj_thm (Goal.prove_global thy [] []
    1.64 +        val thms = Datatype_Aux.split_conj_thm (Goal.prove_global_future thy [] []
    1.65            (augment_sort thy sort
    1.66              (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    1.67                (map (fn ((s, T), x) =>
    1.68 @@ -427,6 +429,7 @@
    1.69              (s, map (inter_sort thy sort o snd) tvs, [cp_class])
    1.70              (Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac thms)) thy)
    1.71            (full_new_type_names' ~~ tyvars) thy
    1.72 +        |> Theory.checkpoint
    1.73        end;
    1.74  
    1.75      val (perm_thmss,thy3) = thy2 |>
    1.76 @@ -451,7 +454,8 @@
    1.77           ((Binding.name (space_implode "_" new_type_names ^ "_perm_append"),
    1.78            perm_append_thms), [Simplifier.simp_add]),
    1.79           ((Binding.name (space_implode "_" new_type_names ^ "_perm_eq"),
    1.80 -          perm_eq_thms), [Simplifier.simp_add])];
    1.81 +          perm_eq_thms), [Simplifier.simp_add])] ||>
    1.82 +      Theory.checkpoint;
    1.83  
    1.84      (**** Define representing sets ****)
    1.85  
    1.86 @@ -531,7 +535,8 @@
    1.87            (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
    1.88               (rep_set_names' ~~ recTs'))
    1.89            [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) []
    1.90 -      ||> Sign.restore_naming thy3;
    1.91 +      ||> Sign.restore_naming thy3
    1.92 +      ||> Theory.checkpoint;
    1.93  
    1.94      (**** Prove that representing set is closed under permutation ****)
    1.95  
    1.96 @@ -544,7 +549,7 @@
    1.97        (perm_indnames ~~ descr);
    1.98  
    1.99      fun mk_perm_closed name = map (fn th => Drule.export_without_context (th RS mp))
   1.100 -      (List.take (Datatype_Aux.split_conj_thm (Goal.prove_global thy4 [] []
   1.101 +      (List.take (Datatype_Aux.split_conj_thm (Goal.prove_global_future thy4 [] []
   1.102          (augment_sort thy4
   1.103            (pt_class_of thy4 name :: map (cp_class_of thy4 name) (remove (op =) name dt_atoms))
   1.104            (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
   1.105 @@ -593,7 +598,8 @@
   1.106                     (Const (Sign.intern_const thy ("Rep_" ^ Binding.name_of name), T --> U) $
   1.107                       Free ("x", T))))), [])] thy)
   1.108          end))
   1.109 -        (types_syntax ~~ tyvars ~~ List.take (rep_set_names'' ~~ recTs', length new_type_names));
   1.110 +        (types_syntax ~~ tyvars ~~ List.take (rep_set_names'' ~~ recTs', length new_type_names))
   1.111 +      ||> Theory.checkpoint;
   1.112  
   1.113      val perm_defs = map snd typedefs;
   1.114      val Abs_inverse_thms = map (collect_simp o #Abs_inverse o snd o fst) typedefs;
   1.115 @@ -622,6 +628,7 @@
   1.116                  [Rep RS perm_closed RS Abs_inverse]) 1,
   1.117                asm_full_simp_tac (HOL_basic_ss addsimps [Global_Theory.get_thm thy
   1.118                  ("pt_" ^ Long_Name.base_name atom ^ "3")]) 1]) thy
   1.119 +            |> Theory.checkpoint
   1.120            end)
   1.121          (Abs_inverse_thms ~~ Rep_inverse_thms ~~ Rep_thms ~~ perm_defs ~~
   1.122             new_type_names ~~ tyvars ~~ perm_closed_thms);
   1.123 @@ -660,7 +667,7 @@
   1.124      val thy7 = fold (fn x => fn thy => thy |>
   1.125        pt_instance x |>
   1.126        fold (cp_instance x) (atoms ~~ perm_closed_thmss))
   1.127 -        (atoms ~~ perm_closed_thmss) thy6;
   1.128 +        (atoms ~~ perm_closed_thmss) thy6 |> Theory.checkpoint;
   1.129  
   1.130      (**** constructors ****)
   1.131  
   1.132 @@ -760,7 +767,8 @@
   1.133          val def_name = (Long_Name.base_name cname) ^ "_def";
   1.134          val ([def_thm], thy') = thy |>
   1.135            Sign.add_consts_i [(cname', constrT, mx)] |>
   1.136 -          (Global_Theory.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)]
   1.137 +          (Global_Theory.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)] ||>
   1.138 +          Theory.checkpoint;
   1.139        in (thy', defs @ [def_thm], eqns @ [eqn]) end;
   1.140  
   1.141      fun dt_constr_defs ((((((_, (_, _, constrs)),
   1.142 @@ -774,7 +782,7 @@
   1.143          val (thy', defs', eqns') = fold (make_constr_def tname T T')
   1.144            (constrs ~~ constrs' ~~ constr_syntax) (Sign.add_path tname thy, defs, [])
   1.145        in
   1.146 -        (Sign.parent_path thy', defs', eqns @ [eqns'], dist_lemmas @ [dist])
   1.147 +        (Theory.checkpoint (Sign.parent_path thy'), defs', eqns @ [eqns'], dist_lemmas @ [dist])
   1.148        end;
   1.149  
   1.150      val (thy8, constr_defs, constr_rep_eqns, dist_lemmas) = fold dt_constr_defs
   1.151 @@ -792,7 +800,7 @@
   1.152        let
   1.153          val inj_thms = map (fn r => r RS iffD1) abs_inject_thms;
   1.154          val rewrites = constr_defs @ map mk_meta_eq Rep_inverse_thms
   1.155 -      in Goal.prove_global thy8 [] [] eqn (fn _ => EVERY
   1.156 +      in Goal.prove_global_future thy8 [] [] eqn (fn _ => EVERY
   1.157          [resolve_tac inj_thms 1,
   1.158           rewrite_goals_tac rewrites,
   1.159           rtac refl 3,
   1.160 @@ -811,7 +819,7 @@
   1.161          val permT = mk_permT (Type (atom, []));
   1.162          val pi = Free ("pi", permT);
   1.163        in
   1.164 -        Goal.prove_global thy8 [] []
   1.165 +        Goal.prove_global_future thy8 [] []
   1.166            (augment_sort thy8
   1.167              (pt_class_of thy8 atom :: map (cp_class_of thy8 atom) (remove (op =) atom dt_atoms))
   1.168              (HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.169 @@ -833,7 +841,7 @@
   1.170      fun prove_distinct_thms _ [] = []
   1.171        | prove_distinct_thms (p as (rep_thms, dist_lemma)) (t :: ts) =
   1.172            let
   1.173 -            val dist_thm = Goal.prove_global thy8 [] [] t (fn _ =>
   1.174 +            val dist_thm = Goal.prove_global_future thy8 [] [] t (fn _ =>
   1.175                simp_tac (global_simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1)
   1.176            in
   1.177              dist_thm :: Drule.export_without_context (dist_thm RS not_sym) ::
   1.178 @@ -876,7 +884,7 @@
   1.179            val (_, l_args, r_args) = fold_rev constr_arg dts (1, [], []);
   1.180            val c = Const (cname, map fastype_of l_args ---> T)
   1.181          in
   1.182 -          Goal.prove_global thy8 [] []
   1.183 +          Goal.prove_global_future thy8 [] []
   1.184              (augment_sort thy8
   1.185                (pt_class_of thy8 atom :: map (cp_class_of thy8 atom) (remove (op =) atom dt_atoms))
   1.186                (HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.187 @@ -932,7 +940,7 @@
   1.188            val Ts = map fastype_of args1;
   1.189            val c = Const (cname, Ts ---> T)
   1.190          in
   1.191 -          Goal.prove_global thy8 [] []
   1.192 +          Goal.prove_global_future thy8 [] []
   1.193              (augment_sort thy8 pt_cp_sort
   1.194                (HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.195                  (HOLogic.mk_eq (list_comb (c, args1), list_comb (c, args2)),
   1.196 @@ -975,7 +983,7 @@
   1.197            fun supp t =
   1.198              Const ("Nominal.supp", fastype_of t --> HOLogic.mk_setT atomT) $ t;
   1.199            fun fresh t = fresh_const atomT (fastype_of t) $ Free ("a", atomT) $ t;
   1.200 -          val supp_thm = Goal.prove_global thy8 [] []
   1.201 +          val supp_thm = Goal.prove_global_future thy8 [] []
   1.202              (augment_sort thy8 pt_cp_sort
   1.203                (HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.204                  (supp c,
   1.205 @@ -988,7 +996,7 @@
   1.206                   abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1)
   1.207          in
   1.208            (supp_thm,
   1.209 -           Goal.prove_global thy8 [] [] (augment_sort thy8 pt_cp_sort
   1.210 +           Goal.prove_global_future thy8 [] [] (augment_sort thy8 pt_cp_sort
   1.211               (HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.212                 (fresh c,
   1.213                  if null dts then @{term True}
   1.214 @@ -1017,7 +1025,7 @@
   1.215      val (indrule_lemma_prems, indrule_lemma_concls) =
   1.216        fold mk_indrule_lemma (descr'' ~~ recTs ~~ recTs') ([], []);
   1.217  
   1.218 -    val indrule_lemma = Goal.prove_global thy8 [] []
   1.219 +    val indrule_lemma = Goal.prove_global_future thy8 [] []
   1.220        (Logic.mk_implies
   1.221          (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj indrule_lemma_prems),
   1.222           HOLogic.mk_Trueprop (Datatype_Aux.mk_conj indrule_lemma_concls))) (fn _ => EVERY
   1.223 @@ -1035,7 +1043,7 @@
   1.224      val Abs_inverse_thms' = map (fn r => r RS subst) Abs_inverse_thms;
   1.225  
   1.226      val dt_induct_prop = Datatype_Prop.make_ind descr';
   1.227 -    val dt_induct = Goal.prove_global thy8 []
   1.228 +    val dt_induct = Goal.prove_global_future thy8 []
   1.229        (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
   1.230        (fn {prems, ...} => EVERY
   1.231          [rtac indrule_lemma' 1,
   1.232 @@ -1060,7 +1068,7 @@
   1.233      val finite_supp_thms = map (fn atom =>
   1.234        let val atomT = Type (atom, [])
   1.235        in map Drule.export_without_context (List.take
   1.236 -        (Datatype_Aux.split_conj_thm (Goal.prove_global thy8 [] []
   1.237 +        (Datatype_Aux.split_conj_thm (Goal.prove_global_future thy8 [] []
   1.238             (augment_sort thy8 (fs_class_of thy8 atom :: pt_cp_sort)
   1.239               (HOLogic.mk_Trueprop
   1.240                 (foldr1 HOLogic.mk_conj (map (fn (s, T) =>
   1.241 @@ -1100,7 +1108,8 @@
   1.242          in fold (fn Type (s, Ts) => AxClass.prove_arity
   1.243            (s, map (inter_sort thy sort o snd o dest_TFree) Ts, [class])
   1.244            (Class.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy
   1.245 -        end) (atoms ~~ finite_supp_thms);
   1.246 +        end) (atoms ~~ finite_supp_thms) ||>
   1.247 +      Theory.checkpoint;
   1.248  
   1.249      (**** strong induction theorem ****)
   1.250  
   1.251 @@ -1267,7 +1276,7 @@
   1.252  
   1.253      val _ = warning "proving strong induction theorem ...";
   1.254  
   1.255 -    val induct_aux = Goal.prove_global thy9 []
   1.256 +    val induct_aux = Goal.prove_global_future thy9 []
   1.257          (map (augment_sort thy9 fs_cp_sort) ind_prems')
   1.258          (augment_sort thy9 fs_cp_sort ind_concl') (fn {prems, context} =>
   1.259        let
   1.260 @@ -1368,7 +1377,7 @@
   1.261            cterm_of thy9 (Const ("Nominal.supp", fastype_of f')))
   1.262          end) fresh_fs) induct_aux;
   1.263  
   1.264 -    val induct = Goal.prove_global thy9 []
   1.265 +    val induct = Goal.prove_global_future thy9 []
   1.266        (map (augment_sort thy9 fs_cp_sort) ind_prems)
   1.267        (augment_sort thy9 fs_cp_sort ind_concl)
   1.268        (fn {prems, ...} => EVERY
   1.269 @@ -1381,7 +1390,8 @@
   1.270        Sign.add_path big_name |>
   1.271        Global_Theory.add_thms [((Binding.name "strong_induct'", induct_aux), [])] ||>>
   1.272        Global_Theory.add_thms [((Binding.name "strong_induct", induct), [case_names_induct])] ||>>
   1.273 -      Global_Theory.add_thmss [((Binding.name "strong_inducts", projections induct), [case_names_induct])];
   1.274 +      Global_Theory.add_thmss [((Binding.name "strong_inducts", projections induct), [case_names_induct])] ||>
   1.275 +      Theory.checkpoint;
   1.276  
   1.277      (**** recursion combinator ****)
   1.278  
   1.279 @@ -1489,7 +1499,8 @@
   1.280            (map dest_Free rec_fns)
   1.281            (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []
   1.282        ||> Global_Theory.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct")
   1.283 -      ||> Sign.restore_naming thy10;
   1.284 +      ||> Sign.restore_naming thy10
   1.285 +      ||> Theory.checkpoint;
   1.286  
   1.287      (** equivariance **)
   1.288  
   1.289 @@ -1512,7 +1523,7 @@
   1.290              (R $ x $ y, R' $ mk_perm [] pi x $ mk_perm [] pi y)
   1.291            end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ rec_sets_pi ~~ (1 upto length recTs));
   1.292          val ths = map (fn th => Drule.export_without_context (th RS mp)) (Datatype_Aux.split_conj_thm
   1.293 -          (Goal.prove_global thy11 [] []
   1.294 +          (Goal.prove_global_future thy11 [] []
   1.295              (augment_sort thy1 pt_cp_sort
   1.296                (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map HOLogic.mk_imp ps))))
   1.297              (fn _ => rtac rec_induct 1 THEN REPEAT
   1.298 @@ -1522,7 +1533,7 @@
   1.299                  (resolve_tac rec_intrs THEN_ALL_NEW
   1.300                   asm_simp_tac (HOL_ss addsimps (fresh_bij @ perm_bij))) 1))))
   1.301          val ths' = map (fn ((P, Q), th) =>
   1.302 -          Goal.prove_global thy11 [] []
   1.303 +          Goal.prove_global_future thy11 [] []
   1.304              (augment_sort thy1 pt_cp_sort
   1.305                (Logic.mk_implies (HOLogic.mk_Trueprop Q, HOLogic.mk_Trueprop P)))
   1.306              (fn _ => dtac (Thm.instantiate ([],
   1.307 @@ -1544,7 +1555,7 @@
   1.308              (rec_fns ~~ rec_fn_Ts)
   1.309        in
   1.310          map (fn th => Drule.export_without_context (th RS mp)) (Datatype_Aux.split_conj_thm
   1.311 -          (Goal.prove_global thy11 []
   1.312 +          (Goal.prove_global_future thy11 []
   1.313              (map (augment_sort thy11 fs_cp_sort) fins)
   1.314              (augment_sort thy11 fs_cp_sort
   1.315                (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
   1.316 @@ -1993,7 +2004,8 @@
   1.317            (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T)
   1.318             (Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T')
   1.319               (set $ Free ("x", T) $ Free ("y", T'))))))
   1.320 -               (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts));
   1.321 +               (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
   1.322 +      ||> Theory.checkpoint;
   1.323  
   1.324      (* prove characteristic equations for primrec combinators *)
   1.325  
   1.326 @@ -2009,7 +2021,7 @@
   1.327          fun solve rules prems = resolve_tac rules THEN_ALL_NEW
   1.328            (resolve_tac prems THEN_ALL_NEW atac)
   1.329        in
   1.330 -        Goal.prove_global thy12 []
   1.331 +        Goal.prove_global_future thy12 []
   1.332            (map (augment_sort thy12 fs_cp_sort) prems')
   1.333            (augment_sort thy12 fs_cp_sort concl')
   1.334            (fn {prems, ...} => EVERY
   1.335 @@ -2034,7 +2046,8 @@
   1.336           ((Binding.name "rec_unique", map Drule.export_without_context rec_unique_thms), []),
   1.337           ((Binding.name "recs", rec_thms), [])] ||>
   1.338        Sign.parent_path ||>
   1.339 -      map_nominal_datatypes (fold Symtab.update dt_infos);
   1.340 +      map_nominal_datatypes (fold Symtab.update dt_infos) ||>
   1.341 +      Theory.checkpoint;
   1.342  
   1.343    in
   1.344      thy13