--- a/src/HOL/Nominal/nominal_atoms.ML Thu Feb 23 20:56:31 2006 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML Fri Feb 24 09:00:21 2006 +0100
@@ -390,18 +390,18 @@
val cls_name = Sign.full_name (sign_of thy') ("pt_"^ak_name);
val at_inst = PureThy.get_thm thy' (Name ("at_"^ak_name'^"_inst"));
- val proof1 = EVERY [AxClass.intro_classes_tac [],
+ val proof1 = EVERY [ClassPackage.intro_classes_tac [],
rtac ((at_inst RS at_pt_inst) RS pt1) 1,
rtac ((at_inst RS at_pt_inst) RS pt2) 1,
rtac ((at_inst RS at_pt_inst) RS pt3) 1,
atac 1];
val simp_s = HOL_basic_ss addsimps
PureThy.get_thmss thy' [Name (ak_name^"_prm_"^ak_name'^"_def")];
- val proof2 = EVERY [AxClass.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];
+ val proof2 = EVERY [ClassPackage.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];
in
thy'
- |> AxClass.add_inst_arity_i (qu_name,[],[cls_name])
+ |> AxClass.add_inst_arity_i I (qu_name,[],[cls_name])
(if ak_name = ak_name' then proof1 else proof2)
end) ak_names thy) ak_names thy12c;
@@ -422,7 +422,7 @@
val pt_inst = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));
fun pt_proof thm =
- EVERY [AxClass.intro_classes_tac [],
+ EVERY [ClassPackage.intro_classes_tac [],
rtac (thm RS pt1) 1, rtac (thm RS pt2) 1, rtac (thm RS pt3) 1, atac 1];
val pt_thm_fun = at_thm RS (pt_inst RS (pt_inst RS pt_fun_inst));
@@ -435,15 +435,15 @@
val pt_thm_set = pt_inst RS pt_set_inst
in
thy
- |> AxClass.add_inst_arity_i ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
- |> AxClass.add_inst_arity_i ("nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn)
- |> AxClass.add_inst_arity_i ("Datatype.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
- |> AxClass.add_inst_arity_i ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
- |> AxClass.add_inst_arity_i ("*",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
- |> AxClass.add_inst_arity_i ("nominal.nprod",[[cls_name],[cls_name]],[cls_name])
+ |> AxClass.add_inst_arity_i I ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
+ |> AxClass.add_inst_arity_i I ("nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn)
+ |> AxClass.add_inst_arity_i I ("Datatype.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
+ |> AxClass.add_inst_arity_i I ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
+ |> AxClass.add_inst_arity_i I ("*",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
+ |> AxClass.add_inst_arity_i I ("nominal.nprod",[[cls_name],[cls_name]],[cls_name])
(pt_proof pt_thm_nprod)
- |> AxClass.add_inst_arity_i ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit)
- |> AxClass.add_inst_arity_i ("set",[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
+ |> AxClass.add_inst_arity_i I ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit)
+ |> AxClass.add_inst_arity_i I ("set",[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
end) ak_names thy13;
(*<<<<<<< fs_<ak> class instances >>>>>>>*)
@@ -469,14 +469,14 @@
(if ak_name = ak_name'
then
let val at_thm = PureThy.get_thm thy' (Name ("at_"^ak_name^"_inst"));
- in EVERY [AxClass.intro_classes_tac [],
+ in EVERY [ClassPackage.intro_classes_tac [],
rtac ((at_thm RS fs_at_inst) RS fs1) 1] end
else
let val dj_inst = PureThy.get_thm thy' (Name ("dj_"^ak_name'^"_"^ak_name));
val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, Finites.emptyI];
- in EVERY [AxClass.intro_classes_tac [], asm_simp_tac simp_s 1] end)
+ in EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1] end)
in
- AxClass.add_inst_arity_i (qu_name,[],[qu_class]) proof thy'
+ AxClass.add_inst_arity_i I (qu_name,[],[qu_class]) proof thy'
end) ak_names thy) ak_names thy18;
(* shows that *)
@@ -491,7 +491,7 @@
let
val cls_name = Sign.full_name (sign_of thy) ("fs_"^ak_name);
val fs_inst = PureThy.get_thm thy (Name ("fs_"^ak_name^"_inst"));
- fun fs_proof thm = EVERY [AxClass.intro_classes_tac [], rtac (thm RS fs1) 1];
+ fun fs_proof thm = EVERY [ClassPackage.intro_classes_tac [], rtac (thm RS fs1) 1];
val fs_thm_unit = fs_unit_inst;
val fs_thm_prod = fs_inst RS (fs_inst RS fs_prod_inst);
@@ -500,12 +500,12 @@
val fs_thm_optn = fs_inst RS fs_option_inst;
in
thy
- |> AxClass.add_inst_arity_i ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit)
- |> AxClass.add_inst_arity_i ("*",[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod)
- |> AxClass.add_inst_arity_i ("nominal.nprod",[[cls_name],[cls_name]],[cls_name])
+ |> AxClass.add_inst_arity_i I ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit)
+ |> AxClass.add_inst_arity_i I ("*",[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod)
+ |> AxClass.add_inst_arity_i I ("nominal.nprod",[[cls_name],[cls_name]],[cls_name])
(fs_proof fs_thm_nprod)
- |> AxClass.add_inst_arity_i ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
- |> AxClass.add_inst_arity_i ("Datatype.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
+ |> AxClass.add_inst_arity_i I ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
+ |> AxClass.add_inst_arity_i I ("Datatype.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
end) ak_names thy20;
(*<<<<<<< cp_<ak>_<ai> class instances >>>>>>>*)
@@ -536,7 +536,7 @@
val pt_inst = PureThy.get_thm thy'' (Name ("pt_"^ak_name''^"_inst"));
val at_inst = PureThy.get_thm thy'' (Name ("at_"^ak_name''^"_inst"));
in
- EVERY [AxClass.intro_classes_tac [],
+ EVERY [ClassPackage.intro_classes_tac [],
rtac (at_inst RS (pt_inst RS pt_perm_compose)) 1]
end)
else
@@ -548,10 +548,10 @@
[Name (ak_name' ^"_prm_"^ak_name^"_def"),
Name (ak_name''^"_prm_"^ak_name^"_def")]));
in
- EVERY [AxClass.intro_classes_tac [], simp_tac simp_s 1]
+ EVERY [ClassPackage.intro_classes_tac [], simp_tac simp_s 1]
end))
in
- AxClass.add_inst_arity_i (name,[],[cls_name]) proof thy''
+ AxClass.add_inst_arity_i I (name,[],[cls_name]) proof thy''
end) ak_names thy') ak_names thy) ak_names thy24;
(* shows that *)
@@ -570,7 +570,7 @@
val pt_inst = PureThy.get_thm thy' (Name ("pt_"^ak_name^"_inst"));
val at_inst = PureThy.get_thm thy' (Name ("at_"^ak_name^"_inst"));
- fun cp_proof thm = EVERY [AxClass.intro_classes_tac [],rtac (thm RS cp1) 1];
+ fun cp_proof thm = EVERY [ClassPackage.intro_classes_tac [],rtac (thm RS cp1) 1];
val cp_thm_unit = cp_unit_inst;
val cp_thm_prod = cp_inst RS (cp_inst RS cp_prod_inst);
@@ -580,12 +580,12 @@
val cp_thm_noptn = cp_inst RS cp_noption_inst;
in
thy'
- |> AxClass.add_inst_arity_i ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit)
- |> AxClass.add_inst_arity_i ("*",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
- |> AxClass.add_inst_arity_i ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
- |> AxClass.add_inst_arity_i ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
- |> AxClass.add_inst_arity_i ("Datatype.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
- |> AxClass.add_inst_arity_i ("nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
+ |> AxClass.add_inst_arity_i I ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit)
+ |> AxClass.add_inst_arity_i I ("*",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
+ |> AxClass.add_inst_arity_i I ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
+ |> AxClass.add_inst_arity_i I ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
+ |> AxClass.add_inst_arity_i I ("Datatype.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
+ |> AxClass.add_inst_arity_i I ("nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
end) ak_names thy) ak_names thy25;
(* show that discrete nominal types are permutation types, finitely *)
@@ -599,9 +599,9 @@
let
val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);
val simp_s = HOL_basic_ss addsimps [defn];
- val proof = EVERY [AxClass.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];
+ val proof = EVERY [ClassPackage.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];
in
- AxClass.add_inst_arity_i (discrete_ty,[],[qu_class]) proof thy
+ AxClass.add_inst_arity_i I (discrete_ty,[],[qu_class]) proof thy
end) ak_names;
fun discrete_fs_inst discrete_ty defn =
@@ -610,9 +610,9 @@
val qu_class = Sign.full_name (sign_of thy) ("fs_"^ak_name);
val supp_def = thm "nominal.supp_def";
val simp_s = HOL_ss addsimps [supp_def,Collect_const,Finites.emptyI,defn];
- val proof = EVERY [AxClass.intro_classes_tac [], asm_simp_tac simp_s 1];
+ val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];
in
- AxClass.add_inst_arity_i (discrete_ty,[],[qu_class]) proof thy
+ AxClass.add_inst_arity_i I (discrete_ty,[],[qu_class]) proof thy
end) ak_names;
fun discrete_cp_inst discrete_ty defn =
@@ -621,9 +621,9 @@
val qu_class = Sign.full_name (sign_of thy) ("cp_"^ak_name^"_"^ak_name');
val supp_def = thm "nominal.supp_def";
val simp_s = HOL_ss addsimps [defn];
- val proof = EVERY [AxClass.intro_classes_tac [], asm_simp_tac simp_s 1];
+ val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];
in
- AxClass.add_inst_arity_i (discrete_ty,[],[qu_class]) proof thy
+ AxClass.add_inst_arity_i I (discrete_ty,[],[qu_class]) proof thy
end) ak_names)) ak_names;
in
--- a/src/HOL/Nominal/nominal_package.ML Thu Feb 23 20:56:31 2006 +0100
+++ b/src/HOL/Nominal/nominal_package.ML Fri Feb 24 09:00:21 2006 +0100
@@ -23,7 +23,7 @@
fun dt_cases (descr: descr) (_, args, constrs) =
let
fun the_bname i = Sign.base_name (#1 (valOf (AList.lookup (op =) descr i)));
- val bnames = map the_bname (distinct (List.concat (map dt_recs args)));
+ val bnames = map the_bname (distinct op = (List.concat (map dt_recs args)));
in map (fn (c, _) => space_implode "_" (Sign.base_name c :: bnames)) constrs end;
@@ -411,17 +411,17 @@
(fn _ => EVERY [indtac induction perm_indnames 1,
ALLGOALS (asm_full_simp_tac simps)])))
in
- foldl (fn ((s, tvs), thy) => AxClass.add_inst_arity_i
+ foldl (fn ((s, tvs), thy) => AxClass.add_inst_arity_i I
(s, replicate (length tvs) (cp_class :: classes), [cp_class])
- (AxClass.intro_classes_tac [] THEN ALLGOALS (resolve_tac thms)) thy)
+ (ClassPackage.intro_classes_tac [] THEN ALLGOALS (resolve_tac thms)) thy)
thy (full_new_type_names' ~~ tyvars)
end;
val (perm_thmss,thy3) = thy2 |>
fold (fn name1 => fold (composition_instance name1) atoms) atoms |>
curry (Library.foldr (fn ((i, (tyname, args, _)), thy) =>
- AxClass.add_inst_arity_i (tyname, replicate (length args) classes, classes)
- (AxClass.intro_classes_tac [] THEN REPEAT (EVERY
+ AxClass.add_inst_arity_i I (tyname, replicate (length args) classes, classes)
+ (ClassPackage.intro_classes_tac [] THEN REPEAT (EVERY
[resolve_tac perm_empty_thms 1,
resolve_tac perm_append_thms 1,
resolve_tac perm_eq_thms 1, assume_tac 1])) thy))
@@ -457,7 +457,7 @@
apfst (cons dt) (strip_option dt')
| strip_option dt = ([], dt);
- val dt_atomTs = distinct (map (typ_of_dtyp descr sorts')
+ val dt_atomTs = distinct op = (map (typ_of_dtyp descr sorts')
(List.concat (map (fn (_, (_, _, cs)) => List.concat
(map (List.concat o map (fst o strip_option) o snd) cs)) descr)));
@@ -585,10 +585,10 @@
fun pt_instance ((class, atom), perm_closed_thms) =
fold (fn (((({Abs_inverse, Rep_inverse, Rep, ...},
perm_def), name), tvs), perm_closed) => fn thy =>
- AxClass.add_inst_arity_i
+ AxClass.add_inst_arity_i I
(Sign.intern_type thy name,
replicate (length tvs) (classes @ cp_classes), [class])
- (EVERY [AxClass.intro_classes_tac [],
+ (EVERY [ClassPackage.intro_classes_tac [],
rewrite_goals_tac [perm_def],
asm_full_simp_tac (simpset_of thy addsimps [Rep_inverse]) 1,
asm_full_simp_tac (simpset_of thy addsimps
@@ -609,10 +609,10 @@
val cp1' = PureThy.get_thm thy (Name (name ^ "_inst")) RS cp1
in fold (fn ((((({Abs_inverse, Rep_inverse, Rep, ...},
perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy =>
- AxClass.add_inst_arity_i
+ AxClass.add_inst_arity_i I
(Sign.intern_type thy name,
replicate (length tvs) (classes @ cp_classes), [class])
- (EVERY [AxClass.intro_classes_tac [],
+ (EVERY [ClassPackage.intro_classes_tac [],
rewrite_goals_tac [perm_def],
asm_full_simp_tac (simpset_of thy addsimps
((Rep RS perm_closed1 RS Abs_inverse) ::
@@ -1086,10 +1086,10 @@
DatatypeAux.store_thmss_atts "fresh" new_type_names simp_atts fresh_thms ||>
fold (fn (atom, ths) => fn thy =>
let val class = Sign.intern_class thy ("fs_" ^ Sign.base_name atom)
- in fold (fn T => AxClass.add_inst_arity_i
+ in fold (fn T => AxClass.add_inst_arity_i I
(fst (dest_Type T),
replicate (length sorts) [class], [class])
- (AxClass.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy
+ (ClassPackage.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy
end) (atoms ~~ finite_supp_thms);
(**** strong induction theorem ****)