really minimize sorts after certification -- looks like this is intended here;
authorwenzelm
Tue Apr 27 21:34:22 2010 +0200 (2010-04-27)
changeset 36428874843c1e96e
parent 36427 85bc9b7c4d18
child 36429 9d6b3be996d4
really minimize sorts after certification -- looks like this is intended here;
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Tue Apr 27 19:44:04 2010 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Tue Apr 27 21:34:22 2010 +0200
     1.3 @@ -215,7 +215,7 @@
     1.4  
     1.5      fun inter_sort thy S S' = Type.inter_sort (Sign.tsig_of thy) (S, S');
     1.6      fun augment_sort_typ thy S =
     1.7 -      let val S = Sign.certify_sort thy S
     1.8 +      let val S = Sign.minimize_sort thy (Sign.certify_sort thy S)
     1.9        in map_type_tfree (fn (s, S') => TFree (s,
    1.10          if member (op = o apsnd fst) sorts s then inter_sort thy S S' else S'))
    1.11        end;
    1.12 @@ -449,7 +449,7 @@
    1.13                  at_inst RS (pt_inst RS pt_perm_compose) RS sym,
    1.14                  at_inst RS (pt_inst RS pt_perm_compose_rev) RS sym]
    1.15              end))
    1.16 -        val sort = Sign.certify_sort thy (cp_class :: pt_class);
    1.17 +        val sort = Sign.minimize_sort thy (Sign.certify_sort thy (cp_class :: pt_class));
    1.18          val thms = split_conj_thm (Goal.prove_global thy [] []
    1.19            (augment_sort thy sort
    1.20              (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    1.21 @@ -654,8 +654,8 @@
    1.22          perm_def), name), tvs), perm_closed) => fn thy =>
    1.23            let
    1.24              val pt_class = pt_class_of thy atom;
    1.25 -            val sort = Sign.certify_sort thy
    1.26 -              (pt_class :: map (cp_class_of thy atom) (remove (op =) atom dt_atoms))
    1.27 +            val sort = Sign.minimize_sort thy (Sign.certify_sort thy
    1.28 +              (pt_class :: map (cp_class_of thy atom) (remove (op =) atom dt_atoms)))
    1.29            in AxClass.prove_arity
    1.30              (Sign.intern_type thy name,
    1.31                map (inter_sort thy sort o snd) tvs, [pt_class])
    1.32 @@ -678,10 +678,10 @@
    1.33      fun cp_instance (atom1, perm_closed_thms1) (atom2, perm_closed_thms2) thy =
    1.34        let
    1.35          val cp_class = cp_class_of thy atom1 atom2;
    1.36 -        val sort = Sign.certify_sort thy
    1.37 +        val sort = Sign.minimize_sort thy (Sign.certify_sort thy
    1.38            (pt_class_of thy atom1 :: map (cp_class_of thy atom1) (remove (op =) atom1 dt_atoms) @
    1.39             (if atom1 = atom2 then [cp_class_of thy atom1 atom1] else
    1.40 -            pt_class_of thy atom2 :: map (cp_class_of thy atom2) (remove (op =) atom2 dt_atoms)));
    1.41 +            pt_class_of thy atom2 :: map (cp_class_of thy atom2) (remove (op =) atom2 dt_atoms))));
    1.42          val cp1' = cp_inst_of thy atom1 atom2 RS cp1
    1.43        in fold (fn ((((((Abs_inverse, Rep),
    1.44          perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy =>
    1.45 @@ -1131,7 +1131,7 @@
    1.46        fold (fn (atom, ths) => fn thy =>
    1.47          let
    1.48            val class = fs_class_of thy atom;
    1.49 -          val sort = Sign.certify_sort thy (class :: pt_cp_sort)
    1.50 +          val sort = Sign.minimize_sort thy (Sign.certify_sort thy (class :: pt_cp_sort));
    1.51          in fold (fn Type (s, Ts) => AxClass.prove_arity
    1.52            (s, map (inter_sort thy sort o snd o dest_TFree) Ts, [class])
    1.53            (Class.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy
    1.54 @@ -1142,7 +1142,7 @@
    1.55      val pnames = if length descr'' = 1 then ["P"]
    1.56        else map (fn i => "P" ^ string_of_int i) (1 upto length descr'');
    1.57      val ind_sort = if null dt_atomTs then HOLogic.typeS
    1.58 -      else Sign.certify_sort thy9 (map (fs_class_of thy9) dt_atoms);
    1.59 +      else Sign.minimize_sort thy9 (Sign.certify_sort thy9 (map (fs_class_of thy9) dt_atoms));
    1.60      val fsT = TFree ("'n", ind_sort);
    1.61      val fsT' = TFree ("'n", HOLogic.typeS);
    1.62  
    1.63 @@ -1423,7 +1423,7 @@
    1.64      val (rec_result_Ts', rec_fn_Ts') = Datatype_Prop.make_primrec_Ts descr' sorts used;
    1.65  
    1.66      val rec_sort = if null dt_atomTs then HOLogic.typeS else
    1.67 -      Sign.certify_sort thy10 pt_cp_sort;
    1.68 +      Sign.minimize_sort thy10 (Sign.certify_sort thy10 pt_cp_sort);
    1.69  
    1.70      val rec_result_Ts = map (fn TFree (s, _) => TFree (s, rec_sort)) rec_result_Ts';
    1.71      val rec_fn_Ts = map (typ_subst_atomic (rec_result_Ts' ~~ rec_result_Ts)) rec_fn_Ts';
     2.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Tue Apr 27 19:44:04 2010 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Tue Apr 27 21:34:22 2010 +0200
     2.3 @@ -198,8 +198,8 @@
     2.4  
     2.5      val atomTs = distinct op = (maps (map snd o #2) prems);
     2.6      val ind_sort = if null atomTs then HOLogic.typeS
     2.7 -      else Sign.certify_sort thy (map (fn T => Sign.intern_class thy
     2.8 -        ("fs_" ^ Long_Name.base_name (fst (dest_Type T)))) atomTs);
     2.9 +      else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn T => Sign.intern_class thy
    2.10 +        ("fs_" ^ Long_Name.base_name (fst (dest_Type T)))) atomTs));
    2.11      val ([fs_ctxt_tyname], _) = Name.variants ["'n"] (Variable.names_of ctxt');
    2.12      val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
    2.13      val fsT = TFree (fs_ctxt_tyname, ind_sort);
     3.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Tue Apr 27 19:44:04 2010 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Tue Apr 27 21:34:22 2010 +0200
     3.3 @@ -223,8 +223,8 @@
     3.4      val atomTs = distinct op = (maps (map snd o #2) prems);
     3.5      val atoms = map (fst o dest_Type) atomTs;
     3.6      val ind_sort = if null atomTs then HOLogic.typeS
     3.7 -      else Sign.certify_sort thy (map (fn a => Sign.intern_class thy
     3.8 -        ("fs_" ^ Long_Name.base_name a)) atoms);
     3.9 +      else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn a => Sign.intern_class thy
    3.10 +        ("fs_" ^ Long_Name.base_name a)) atoms));
    3.11      val ([fs_ctxt_tyname], _) = Name.variants ["'n"] (Variable.names_of ctxt');
    3.12      val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
    3.13      val fsT = TFree (fs_ctxt_tyname, ind_sort);