17870

1 
(* $Id$ *)


2 


3 
signature NOMINAL_PACKAGE =


4 
sig


5 
val create_nom_typedecls : string list > theory > theory


6 
val add_nominal_datatype : bool > string list > (string list * bstring * mixfix *


7 
(bstring * string list * mixfix) list) list > theory > theory *


8 
{distinct : thm list list,


9 
inject : thm list list,


10 
exhaustion : thm list,


11 
rec_thms : thm list,


12 
case_thms : thm list list,


13 
split_thms : (thm * thm) list,


14 
induction : thm,


15 
size : thm list,


16 
simps : thm list}


17 
val setup : (theory > theory) list


18 
end


19 


20 
structure NominalPackage (*: NOMINAL_PACKAGE *) =


21 
struct


22 


23 
open DatatypeAux;


24 


25 
(* data kind 'HOL/nominal' *)


26 


27 
structure NominalArgs =


28 
struct


29 
val name = "HOL/nominal";


30 
type T = unit Symtab.table;


31 


32 
val empty = Symtab.empty;


33 
val copy = I;


34 
val extend = I;


35 
fun merge _ x = Symtab.merge (K true) x;


36 


37 
fun print sg tab = ();


38 
end;


39 


40 
structure NominalData = TheoryDataFun(NominalArgs);


41 


42 
fun atoms_of thy = map fst (Symtab.dest (NominalData.get thy));


43 


44 
(* FIXME: add to hologic.ML ? *)


45 
fun mk_listT T = Type ("List.list", [T]);


46 
fun mk_permT T = mk_listT (HOLogic.mk_prodT (T, T));


47 


48 
fun mk_Cons x xs =


49 
let val T = fastype_of x


50 
in Const ("List.list.Cons", T > mk_listT T > mk_listT T) $ x $ xs end;


51 


52 


53 
(* this function sets up all matters related to atom *)


54 
(* kinds; the user specifies a list of atomkind names *)


55 
(* atom_decl <ak1> ... <akn> *)


56 
fun create_nom_typedecls ak_names thy =


57 
let


58 
(* declares a typedecl for every atomkind: *)


59 
(* that is typedecl <ak> *)


60 
val thy1 = TypedefPackage.add_typedecls (map (fn x => (x,[],NoSyn)) ak_names) thy;


61 


62 
(* produces a list consisting of pairs: *)


63 
(* fst component is the atomkind name *)


64 
(* snd component is its type *)


65 
val full_ak_names = map (Sign.intern_type (sign_of thy1)) ak_names;


66 
val ak_names_types = ak_names ~~ map (Type o rpair []) full_ak_names;


67 


68 
(* adds for every atomkind an axiom *)


69 
(* <ak>_infinite: infinite (UNIV::<ak_type> set) *)


70 
val (thy2,inf_axs) = PureThy.add_axioms_i (map (fn (ak_name, T) =>


71 
let


72 
val name = ak_name ^ "_infinite"


73 
val axiom = HOLogic.mk_Trueprop (HOLogic.mk_not


74 
(HOLogic.mk_mem (HOLogic.mk_UNIV T,


75 
Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT T)))))


76 
in


77 
((name, axiom), [])


78 
end) ak_names_types) thy1;


79 


80 
(* declares a swapping function for every atomkind, it is *)


81 
(* const swap_<ak> :: <akT> * <akT> => <akT> => <akT> *)


82 
(* swap_<ak> (a,b) c = (if a=c then b (else if b=c then a else c)) *)


83 
(* overloades then the general swapfunction *)


84 
val (thy3, swap_eqs) = foldl_map (fn (thy, (ak_name, T)) =>


85 
let


86 
val swapT = HOLogic.mk_prodT (T, T) > T > T;


87 
val swap_name = Sign.full_name (sign_of thy) ("swap_" ^ ak_name);


88 
val a = Free ("a", T);


89 
val b = Free ("b", T);


90 
val c = Free ("c", T);


91 
val ab = Free ("ab", HOLogic.mk_prodT (T, T))


92 
val cif = Const ("HOL.If", HOLogic.boolT > T > T > T);


93 
val cswap_akname = Const (swap_name, swapT);


94 
val cswap = Const ("nominal.swap", swapT)


95 


96 
val name = "swap_"^ak_name^"_def";


97 
val def1 = HOLogic.mk_Trueprop (HOLogic.mk_eq


98 
(cswap_akname $ HOLogic.mk_prod (a,b) $ c,


99 
cif $ HOLogic.mk_eq (a,c) $ b $ (cif $ HOLogic.mk_eq (b,c) $ a $ c)))


100 
val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c)


101 
in


102 
thy > Theory.add_consts_i [("swap_" ^ ak_name, swapT, NoSyn)]


103 
> (#1 o PureThy.add_defs_i true [((name, def2),[])])


104 
> PrimrecPackage.add_primrec_i "" [(("", def1),[])]


105 
end) (thy2, ak_names_types);


106 


107 
(* declares a permutation function for every atomkind acting *)


108 
(* on such atoms *)


109 
(* const <ak>_prm_<ak> :: (<akT> * <akT>)list => akT => akT *)


110 
(* <ak>_prm_<ak> [] a = a *)


111 
(* <ak>_prm_<ak> (x#xs) a = swap_<ak> x (perm xs a) *)


112 
val (thy4, prm_eqs) = foldl_map (fn (thy, (ak_name, T)) =>


113 
let


114 
val swapT = HOLogic.mk_prodT (T, T) > T > T;


115 
val swap_name = Sign.full_name (sign_of thy) ("swap_" ^ ak_name)


116 
val prmT = mk_permT T > T > T;


117 
val prm_name = ak_name ^ "_prm_" ^ ak_name;


118 
val qu_prm_name = Sign.full_name (sign_of thy) prm_name;


119 
val x = Free ("x", HOLogic.mk_prodT (T, T));


120 
val xs = Free ("xs", mk_permT T);


121 
val a = Free ("a", T) ;


122 


123 
val cnil = Const ("List.list.Nil", mk_permT T);


124 


125 
val def1 = HOLogic.mk_Trueprop (HOLogic.mk_eq (Const (qu_prm_name, prmT) $ cnil $ a, a));


126 


127 
val def2 = HOLogic.mk_Trueprop (HOLogic.mk_eq


128 
(Const (qu_prm_name, prmT) $ mk_Cons x xs $ a,


129 
Const (swap_name, swapT) $ x $ (Const (qu_prm_name, prmT) $ xs $ a)));


130 
in


131 
thy > Theory.add_consts_i [(prm_name, mk_permT T > T > T, NoSyn)]


132 
> PrimrecPackage.add_primrec_i "" [(("", def1), []),(("", def2), [])]


133 
end) (thy3, ak_names_types);


134 


135 
(* defines permutation functions for all combinations of atomkinds; *)


136 
(* there are a trivial cases and nontrivial cases *)


137 
(* nontrivial case: *)


138 
(* <ak>_prm_<ak>_def: perm pi a == <ak>_prm_<ak> pi a *)


139 
(* trivial case with <ak> != <ak'> *)


140 
(* <ak>_prm<ak'>_def[simp]: perm pi a == a *)


141 
(* *)


142 
(* the trivial cases are added to the simplifier, while the non *)


143 
(* have their own rules proved below *)


144 
val (thy5, perm_defs) = foldl_map (fn (thy, (ak_name, T)) =>


145 
foldl_map (fn (thy', (ak_name', T')) =>


146 
let


147 
val perm_def_name = ak_name ^ "_prm_" ^ ak_name';


148 
val pi = Free ("pi", mk_permT T);


149 
val a = Free ("a", T');


150 
val cperm = Const ("nominal.perm", mk_permT T > T' > T');


151 
val cperm_def = Const (Sign.full_name (sign_of thy') perm_def_name, mk_permT T > T' > T');


152 


153 
val name = ak_name ^ "_prm_" ^ ak_name' ^ "_def";


154 
val def = Logic.mk_equals


155 
(cperm $ pi $ a, if ak_name = ak_name' then cperm_def $ pi $ a else a)


156 
in


157 
thy' > PureThy.add_defs_i true [((name, def),[])]


158 
end) (thy, ak_names_types)) (thy4, ak_names_types);


159 


160 
(* proves that every atomkind is an instance of at *)


161 
(* lemma at_<ak>_inst: *)


162 
(* at TYPE(<ak>) *)


163 
val (thy6, prm_cons_thms) =


164 
thy5 > PureThy.add_thms (map (fn (ak_name, T) =>


165 
let


166 
val ak_name_qu = Sign.full_name (sign_of thy5) (ak_name);


167 
val i_type = Type(ak_name_qu,[]);


168 
val cat = Const ("nominal.at",(Term.itselfT i_type) > HOLogic.boolT);


169 
val at_type = Logic.mk_type i_type;


170 
val simp_s = HOL_basic_ss addsimps PureThy.get_thmss thy5


171 
[Name "at_def",


172 
Name (ak_name ^ "_prm_" ^ ak_name ^ "_def"),


173 
Name (ak_name ^ "_prm_" ^ ak_name ^ ".simps"),


174 
Name ("swap_" ^ ak_name ^ "_def"),


175 
Name ("swap_" ^ ak_name ^ ".simps"),


176 
Name (ak_name ^ "_infinite")]


177 


178 
val name = "at_"^ak_name^ "_inst";


179 
val statement = HOLogic.mk_Trueprop (cat $ at_type);


180 

18010

181 
val proof = fn _ => auto_tac (claset(),simp_s);

17870

182 


183 
in

18010

184 
((name, standard (Goal.prove thy5 [] [] statement proof)), [])

17870

185 
end) ak_names_types);


186 


187 
(* declares a permaxclass for every atomkind *)


188 
(* axclass pt_<ak> *)


189 
(* pt_<ak>1[simp]: perm [] x = x *)


190 
(* pt_<ak>2: perm (pi1@pi2) x = perm pi1 (perm pi2 x) *)


191 
(* pt_<ak>3: pi1 ~ pi2 ==> perm pi1 x = perm pi2 x *)


192 
val (thy7, pt_ax_classes) = foldl_map (fn (thy, (ak_name, T)) =>


193 
let


194 
val cl_name = "pt_"^ak_name;


195 
val ty = TFree("'a",["HOL.type"]);


196 
val x = Free ("x", ty);


197 
val pi1 = Free ("pi1", mk_permT T);


198 
val pi2 = Free ("pi2", mk_permT T);


199 
val cperm = Const ("nominal.perm", mk_permT T > ty > ty);


200 
val cnil = Const ("List.list.Nil", mk_permT T);


201 
val cappend = Const ("List.op @",mk_permT T > mk_permT T > mk_permT T);


202 
val cprm_eq = Const ("nominal.prm_eq",mk_permT T > mk_permT T > HOLogic.boolT);


203 
(* nil axiom *)


204 
val axiom1 = HOLogic.mk_Trueprop (HOLogic.mk_eq


205 
(cperm $ cnil $ x, x));


206 
(* append axiom *)


207 
val axiom2 = HOLogic.mk_Trueprop (HOLogic.mk_eq


208 
(cperm $ (cappend $ pi1 $ pi2) $ x, cperm $ pi1 $ (cperm $ pi2 $ x)));


209 
(* permeq axiom *)


210 
val axiom3 = Logic.mk_implies


211 
(HOLogic.mk_Trueprop (cprm_eq $ pi1 $ pi2),


212 
HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x)));


213 
in


214 
thy > AxClass.add_axclass_i (cl_name, ["HOL.type"])


215 
[((cl_name^"1", axiom1),[Simplifier.simp_add_global]),


216 
((cl_name^"2", axiom2),[]),


217 
((cl_name^"3", axiom3),[])]


218 
end) (thy6,ak_names_types);


219 


220 
(* proves that every pt_<ak>type together with <ak>type *)


221 
(* instance of pt *)


222 
(* lemma pt_<ak>_inst: *)


223 
(* pt TYPE('x::pt_<ak>) TYPE(<ak>) *)


224 
val (thy8, prm_inst_thms) =


225 
thy7 > PureThy.add_thms (map (fn (ak_name, T) =>


226 
let


227 
val ak_name_qu = Sign.full_name (sign_of thy7) (ak_name);


228 
val pt_name_qu = Sign.full_name (sign_of thy7) ("pt_"^ak_name);


229 
val i_type1 = TFree("'x",[pt_name_qu]);


230 
val i_type2 = Type(ak_name_qu,[]);


231 
val cpt = Const ("nominal.pt",(Term.itselfT i_type1)>(Term.itselfT i_type2)>HOLogic.boolT);


232 
val pt_type = Logic.mk_type i_type1;


233 
val at_type = Logic.mk_type i_type2;


234 
val simp_s = HOL_basic_ss addsimps PureThy.get_thmss thy7


235 
[Name "pt_def",


236 
Name ("pt_" ^ ak_name ^ "1"),


237 
Name ("pt_" ^ ak_name ^ "2"),


238 
Name ("pt_" ^ ak_name ^ "3")];


239 


240 
val name = "pt_"^ak_name^ "_inst";


241 
val statement = HOLogic.mk_Trueprop (cpt $ pt_type $ at_type);


242 

18010

243 
val proof = fn _ => auto_tac (claset(),simp_s);

17870

244 
in

18010

245 
((name, standard (Goal.prove thy7 [] [] statement proof)), [])

17870

246 
end) ak_names_types);


247 


248 
(* declares an fsaxclass for every atomkind *)


249 
(* axclass fs_<ak> *)


250 
(* fs_<ak>1: finite ((supp x)::<ak> set) *)


251 
val (thy11, fs_ax_classes) = foldl_map (fn (thy, (ak_name, T)) =>


252 
let


253 
val cl_name = "fs_"^ak_name;


254 
val pt_name = Sign.full_name (sign_of thy) ("pt_"^ak_name);


255 
val ty = TFree("'a",["HOL.type"]);


256 
val x = Free ("x", ty);


257 
val csupp = Const ("nominal.supp", ty > HOLogic.mk_setT T);


258 
val cfinites = Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT T))


259 


260 
val axiom1 = HOLogic.mk_Trueprop (HOLogic.mk_mem (csupp $ x, cfinites));


261 


262 
in


263 
thy > AxClass.add_axclass_i (cl_name, [pt_name]) [((cl_name^"1", axiom1),[])]


264 
end) (thy8,ak_names_types);


265 


266 
(* proves that every fs_<ak>type together with <ak>type *)


267 
(* instance of fstype *)


268 
(* lemma abst_<ak>_inst: *)


269 
(* fs TYPE('x::pt_<ak>) TYPE (<ak>) *)


270 
val (thy12, fs_inst_thms) =


271 
thy11 > PureThy.add_thms (map (fn (ak_name, T) =>


272 
let


273 
val ak_name_qu = Sign.full_name (sign_of thy11) (ak_name);


274 
val fs_name_qu = Sign.full_name (sign_of thy11) ("fs_"^ak_name);


275 
val i_type1 = TFree("'x",[fs_name_qu]);


276 
val i_type2 = Type(ak_name_qu,[]);


277 
val cfs = Const ("nominal.fs",


278 
(Term.itselfT i_type1)>(Term.itselfT i_type2)>HOLogic.boolT);


279 
val fs_type = Logic.mk_type i_type1;


280 
val at_type = Logic.mk_type i_type2;


281 
val simp_s = HOL_basic_ss addsimps PureThy.get_thmss thy11


282 
[Name "fs_def",


283 
Name ("fs_" ^ ak_name ^ "1")];


284 


285 
val name = "fs_"^ak_name^ "_inst";


286 
val statement = HOLogic.mk_Trueprop (cfs $ fs_type $ at_type);


287 

18010

288 
val proof = fn _ => auto_tac (claset(),simp_s);

17870

289 
in

18010

290 
((name, standard (Goal.prove thy11 [] [] statement proof)), [])

17870

291 
end) ak_names_types);


292 


293 
(* declares for every atomkind combination an axclass *)


294 
(* cp_<ak1>_<ak2> giving a composition property *)


295 
(* cp_<ak1>_<ak2>1: pi1 o pi2 o x = (pi1 o pi2) o (pi1 o x) *)


296 
val (thy12b,_) = foldl_map (fn (thy, (ak_name, T)) =>


297 
foldl_map (fn (thy', (ak_name', T')) =>


298 
let


299 
val cl_name = "cp_"^ak_name^"_"^ak_name';


300 
val ty = TFree("'a",["HOL.type"]);


301 
val x = Free ("x", ty);


302 
val pi1 = Free ("pi1", mk_permT T);


303 
val pi2 = Free ("pi2", mk_permT T');


304 
val cperm1 = Const ("nominal.perm", mk_permT T > ty > ty);


305 
val cperm2 = Const ("nominal.perm", mk_permT T' > ty > ty);


306 
val cperm3 = Const ("nominal.perm", mk_permT T > mk_permT T' > mk_permT T');


307 


308 
val ax1 = HOLogic.mk_Trueprop


309 
(HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x),


310 
cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x)));


311 
in


312 
(fst (AxClass.add_axclass_i (cl_name, ["HOL.type"]) [((cl_name^"1", ax1),[])] thy'),())


313 
end)


314 
(thy, ak_names_types)) (thy12, ak_names_types)


315 


316 
(* proves for every <ak>combination a cp_<ak1>_<ak2>_inst theorem; *)


317 
(* lemma cp_<ak1>_<ak2>_inst: *)


318 
(* cp TYPE('a::cp_<ak1>_<ak2>) TYPE(<ak1>) TYPE(<ak2>) *)


319 
val (thy12c, cp_thms) = foldl_map (fn (thy, (ak_name, T)) =>


320 
foldl_map (fn (thy', (ak_name', T')) =>


321 
let


322 
val ak_name_qu = Sign.full_name (sign_of thy') (ak_name);


323 
val ak_name_qu' = Sign.full_name (sign_of thy') (ak_name');


324 
val cp_name_qu = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');


325 
val i_type0 = TFree("'a",[cp_name_qu]);


326 
val i_type1 = Type(ak_name_qu,[]);


327 
val i_type2 = Type(ak_name_qu',[]);


328 
val ccp = Const ("nominal.cp",


329 
(Term.itselfT i_type0)>(Term.itselfT i_type1)>


330 
(Term.itselfT i_type2)>HOLogic.boolT);


331 
val at_type = Logic.mk_type i_type1;


332 
val at_type' = Logic.mk_type i_type2;


333 
val cp_type = Logic.mk_type i_type0;


334 
val simp_s = HOL_basic_ss addsimps PureThy.get_thmss thy' [(Name "cp_def")];


335 
val cp1 = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"1"));


336 


337 
val name = "cp_"^ak_name^ "_"^ak_name'^"_inst";


338 
val statement = HOLogic.mk_Trueprop (ccp $ cp_type $ at_type $ at_type');


339 

18010

340 
val proof = fn _ => EVERY [auto_tac (claset(),simp_s), rtac cp1 1];

17870

341 
in


342 
thy' > PureThy.add_thms

18010

343 
[((name, standard (Goal.prove thy' [] [] statement proof)), [])]

17870

344 
end)


345 
(thy, ak_names_types)) (thy12b, ak_names_types);


346 


347 
(* proves for every nontrivial <ak>combination a disjointness *)


348 
(* theorem; i.e. <ak1> != <ak2> *)


349 
(* lemma ds_<ak1>_<ak2>: *)


350 
(* dj TYPE(<ak1>) TYPE(<ak2>) *)


351 
val (thy12d, dj_thms) = foldl_map (fn (thy, (ak_name, T)) =>


352 
foldl_map (fn (thy', (ak_name', T')) =>


353 
(if not (ak_name = ak_name')


354 
then


355 
let


356 
val ak_name_qu = Sign.full_name (sign_of thy') (ak_name);


357 
val ak_name_qu' = Sign.full_name (sign_of thy') (ak_name');


358 
val i_type1 = Type(ak_name_qu,[]);


359 
val i_type2 = Type(ak_name_qu',[]);


360 
val cdj = Const ("nominal.disjoint",


361 
(Term.itselfT i_type1)>(Term.itselfT i_type2)>HOLogic.boolT);


362 
val at_type = Logic.mk_type i_type1;


363 
val at_type' = Logic.mk_type i_type2;


364 
val simp_s = HOL_basic_ss addsimps PureThy.get_thmss thy'


365 
[Name "disjoint_def",


366 
Name (ak_name^"_prm_"^ak_name'^"_def"),


367 
Name (ak_name'^"_prm_"^ak_name^"_def")];


368 


369 
val name = "dj_"^ak_name^"_"^ak_name';


370 
val statement = HOLogic.mk_Trueprop (cdj $ at_type $ at_type');


371 

18010

372 
val proof = fn _ => auto_tac (claset(),simp_s);

17870

373 
in


374 
thy' > PureThy.add_thms

18010

375 
[((name, standard (Goal.prove thy' [] [] statement proof)), []) ]

17870

376 
end


377 
else


378 
(thy',[]))) (* do nothing branch, if ak_name = ak_name' *)


379 
(thy, ak_names_types)) (thy12c, ak_names_types);


380 


381 
(*<<<<<<< pt_<ak> class instances >>>>>>>*)


382 
(*=========================================*)


383 


384 
(* some frequently used theorems *)


385 
val pt1 = PureThy.get_thm thy12c (Name "pt1");


386 
val pt2 = PureThy.get_thm thy12c (Name "pt2");


387 
val pt3 = PureThy.get_thm thy12c (Name "pt3");


388 
val at_pt_inst = PureThy.get_thm thy12c (Name "at_pt_inst");


389 
val pt_bool_inst = PureThy.get_thm thy12c (Name "pt_bool_inst");


390 
val pt_set_inst = PureThy.get_thm thy12c (Name "pt_set_inst");


391 
val pt_unit_inst = PureThy.get_thm thy12c (Name "pt_unit_inst");


392 
val pt_prod_inst = PureThy.get_thm thy12c (Name "pt_prod_inst");


393 
val pt_list_inst = PureThy.get_thm thy12c (Name "pt_list_inst");


394 
val pt_optn_inst = PureThy.get_thm thy12c (Name "pt_option_inst");


395 
val pt_noptn_inst = PureThy.get_thm thy12c (Name "pt_noption_inst");


396 
val pt_fun_inst = PureThy.get_thm thy12c (Name "pt_fun_inst");


397 


398 
(* for all atomkind combination shows that *)


399 
(* every <ak> is an instance of pt_<ai> *)


400 
val (thy13,_) = foldl_map (fn (thy, (ak_name, T)) =>


401 
foldl_map (fn (thy', (ak_name', T')) =>


402 
(if ak_name = ak_name'


403 
then


404 
let


405 
val qu_name = Sign.full_name (sign_of thy') ak_name;


406 
val qu_class = Sign.full_name (sign_of thy') ("pt_"^ak_name);


407 
val at_inst = PureThy.get_thm thy' (Name ("at_"^ak_name ^"_inst"));


408 
val proof = EVERY [AxClass.intro_classes_tac [],


409 
rtac ((at_inst RS at_pt_inst) RS pt1) 1,


410 
rtac ((at_inst RS at_pt_inst) RS pt2) 1,


411 
rtac ((at_inst RS at_pt_inst) RS pt3) 1,


412 
atac 1];


413 
in


414 
(AxClass.add_inst_arity_i (qu_name,[],[qu_class]) proof thy',())


415 
end


416 
else


417 
let


418 
val qu_name' = Sign.full_name (sign_of thy') ak_name';


419 
val qu_class = Sign.full_name (sign_of thy') ("pt_"^ak_name);


420 
val simp_s = HOL_basic_ss addsimps


421 
PureThy.get_thmss thy' [Name (ak_name^"_prm_"^ak_name'^"_def")];


422 
val proof = EVERY [AxClass.intro_classes_tac [], auto_tac (claset(),simp_s)];


423 
in


424 
(AxClass.add_inst_arity_i (qu_name',[],[qu_class]) proof thy',())


425 
end))


426 
(thy, ak_names_types)) (thy12c, ak_names_types);


427 


428 
(* shows that bool is an instance of pt_<ak> *)


429 
(* uses the theorem pt_bool_inst *)


430 
val (thy14,_) = foldl_map (fn (thy, (ak_name, T)) =>


431 
let


432 
val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);


433 
val proof = EVERY [AxClass.intro_classes_tac [],


434 
rtac (pt_bool_inst RS pt1) 1,


435 
rtac (pt_bool_inst RS pt2) 1,


436 
rtac (pt_bool_inst RS pt3) 1,


437 
atac 1];


438 
in


439 
(AxClass.add_inst_arity_i ("bool",[],[qu_class]) proof thy,())


440 
end) (thy13,ak_names_types);


441 


442 
(* shows that set(pt_<ak>) is an instance of pt_<ak> *)


443 
(* unfolds the permutation definition and applies pt_<ak>i *)


444 
val (thy15,_) = foldl_map (fn (thy, (ak_name, T)) =>


445 
let


446 
val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);


447 
val pt_inst = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));


448 
val proof = EVERY [AxClass.intro_classes_tac [],


449 
rtac ((pt_inst RS pt_set_inst) RS pt1) 1,


450 
rtac ((pt_inst RS pt_set_inst) RS pt2) 1,


451 
rtac ((pt_inst RS pt_set_inst) RS pt3) 1,


452 
atac 1];


453 
in


454 
(AxClass.add_inst_arity_i ("set",[[qu_class]],[qu_class]) proof thy,())


455 
end) (thy14,ak_names_types);


456 


457 
(* shows that unit is an instance of pt_<ak> *)


458 
val (thy16,_) = foldl_map (fn (thy, (ak_name, T)) =>


459 
let


460 
val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);


461 
val proof = EVERY [AxClass.intro_classes_tac [],


462 
rtac (pt_unit_inst RS pt1) 1,


463 
rtac (pt_unit_inst RS pt2) 1,


464 
rtac (pt_unit_inst RS pt3) 1,


465 
atac 1];


466 
in


467 
(AxClass.add_inst_arity_i ("Product_Type.unit",[],[qu_class]) proof thy,())


468 
end) (thy15,ak_names_types);


469 


470 
(* shows that *(pt_<ak>,pt_<ak>) is an instance of pt_<ak> *)


471 
(* uses the theorem pt_prod_inst and pt_<ak>_inst *)


472 
val (thy17,_) = foldl_map (fn (thy, (ak_name, T)) =>


473 
let


474 
val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);


475 
val pt_inst = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));


476 
val proof = EVERY [AxClass.intro_classes_tac [],


477 
rtac ((pt_inst RS (pt_inst RS pt_prod_inst)) RS pt1) 1,


478 
rtac ((pt_inst RS (pt_inst RS pt_prod_inst)) RS pt2) 1,


479 
rtac ((pt_inst RS (pt_inst RS pt_prod_inst)) RS pt3) 1,


480 
atac 1];


481 
in


482 
(AxClass.add_inst_arity_i ("*",[[qu_class],[qu_class]],[qu_class]) proof thy,())


483 
end) (thy16,ak_names_types);


484 


485 
(* shows that list(pt_<ak>) is an instance of pt_<ak> *)


486 
(* uses the theorem pt_list_inst and pt_<ak>_inst *)


487 
val (thy18,_) = foldl_map (fn (thy, (ak_name, T)) =>


488 
let


489 
val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);


490 
val pt_inst = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));


491 
val proof = EVERY [AxClass.intro_classes_tac [],


492 
rtac ((pt_inst RS pt_list_inst) RS pt1) 1,


493 
rtac ((pt_inst RS pt_list_inst) RS pt2) 1,


494 
rtac ((pt_inst RS pt_list_inst) RS pt3) 1,


495 
atac 1];


496 
in


497 
(AxClass.add_inst_arity_i ("List.list",[[qu_class]],[qu_class]) proof thy,())


498 
end) (thy17,ak_names_types);


499 


500 
(* shows that option(pt_<ak>) is an instance of pt_<ak> *)


501 
(* uses the theorem pt_option_inst and pt_<ak>_inst *)


502 
val (thy18a,_) = foldl_map (fn (thy, (ak_name, T)) =>


503 
let


504 
val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);


505 
val pt_inst = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));


506 
val proof = EVERY [AxClass.intro_classes_tac [],


507 
rtac ((pt_inst RS pt_optn_inst) RS pt1) 1,


508 
rtac ((pt_inst RS pt_optn_inst) RS pt2) 1,


509 
rtac ((pt_inst RS pt_optn_inst) RS pt3) 1,


510 
atac 1];


511 
in


512 
(AxClass.add_inst_arity_i ("Datatype.option",[[qu_class]],[qu_class]) proof thy,())


513 
end) (thy18,ak_names_types);


514 


515 
(* shows that nOption(pt_<ak>) is an instance of pt_<ak> *)


516 
(* uses the theorem pt_option_inst and pt_<ak>_inst *)


517 
val (thy18b,_) = foldl_map (fn (thy, (ak_name, T)) =>


518 
let


519 
val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);


520 
val pt_inst = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));


521 
val proof = EVERY [AxClass.intro_classes_tac [],


522 
rtac ((pt_inst RS pt_noptn_inst) RS pt1) 1,


523 
rtac ((pt_inst RS pt_noptn_inst) RS pt2) 1,


524 
rtac ((pt_inst RS pt_noptn_inst) RS pt3) 1,


525 
atac 1];


526 
in


527 
(AxClass.add_inst_arity_i ("nominal.nOption",[[qu_class]],[qu_class]) proof thy,())


528 
end) (thy18a,ak_names_types);


529 


530 


531 
(* shows that fun(pt_<ak>,pt_<ak>) is an instance of pt_<ak> *)


532 
(* uses the theorem pt_list_inst and pt_<ak>_inst *)


533 
val (thy19,_) = foldl_map (fn (thy, (ak_name, T)) =>


534 
let


535 
val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);


536 
val at_thm = PureThy.get_thm thy (Name ("at_"^ak_name^"_inst"));


537 
val pt_inst = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));


538 
val proof = EVERY [AxClass.intro_classes_tac [],


539 
rtac ((at_thm RS (pt_inst RS (pt_inst RS pt_fun_inst))) RS pt1) 1,


540 
rtac ((at_thm RS (pt_inst RS (pt_inst RS pt_fun_inst))) RS pt2) 1,


541 
rtac ((at_thm RS (pt_inst RS (pt_inst RS pt_fun_inst))) RS pt3) 1,


542 
atac 1];


543 
in


544 
(AxClass.add_inst_arity_i ("fun",[[qu_class],[qu_class]],[qu_class]) proof thy,())


545 
end) (thy18b,ak_names_types);


546 


547 
(*<<<<<<< fs_<ak> class instances >>>>>>>*)


548 
(*=========================================*)


549 
val fs1 = PureThy.get_thm thy19 (Name "fs1");


550 
val fs_at_inst = PureThy.get_thm thy19 (Name "fs_at_inst");


551 
val fs_unit_inst = PureThy.get_thm thy19 (Name "fs_unit_inst");


552 
val fs_bool_inst = PureThy.get_thm thy19 (Name "fs_bool_inst");


553 
val fs_prod_inst = PureThy.get_thm thy19 (Name "fs_prod_inst");


554 
val fs_list_inst = PureThy.get_thm thy19 (Name "fs_list_inst");


555 


556 
(* shows that <ak> is an instance of fs_<ak> *)


557 
(* uses the theorem at_<ak>_inst *)


558 
val (thy20,_) = foldl_map (fn (thy, (ak_name, T)) =>


559 
let


560 
val qu_name = Sign.full_name (sign_of thy) ak_name;


561 
val qu_class = Sign.full_name (sign_of thy) ("fs_"^ak_name);


562 
val at_thm = PureThy.get_thm thy (Name ("at_"^ak_name^"_inst"));


563 
val proof = EVERY [AxClass.intro_classes_tac [],


564 
rtac ((at_thm RS fs_at_inst) RS fs1) 1];


565 
in


566 
(AxClass.add_inst_arity_i (qu_name,[],[qu_class]) proof thy,())


567 
end) (thy19,ak_names_types);


568 


569 
(* shows that unit is an instance of fs_<ak> *)


570 
(* uses the theorem fs_unit_inst *)


571 
val (thy21,_) = foldl_map (fn (thy, (ak_name, T)) =>


572 
let


573 
val qu_class = Sign.full_name (sign_of thy) ("fs_"^ak_name);


574 
val proof = EVERY [AxClass.intro_classes_tac [],


575 
rtac (fs_unit_inst RS fs1) 1];


576 
in


577 
(AxClass.add_inst_arity_i ("Product_Type.unit",[],[qu_class]) proof thy,())


578 
end) (thy20,ak_names_types);


579 


580 
(* shows that bool is an instance of fs_<ak> *)


581 
(* uses the theorem fs_bool_inst *)


582 
val (thy22,_) = foldl_map (fn (thy, (ak_name, T)) =>


583 
let


584 
val qu_class = Sign.full_name (sign_of thy) ("fs_"^ak_name);


585 
val proof = EVERY [AxClass.intro_classes_tac [],


586 
rtac (fs_bool_inst RS fs1) 1];


587 
in


588 
(AxClass.add_inst_arity_i ("bool",[],[qu_class]) proof thy,())


589 
end) (thy21,ak_names_types);


590 


591 
(* shows that *(fs_<ak>,fs_<ak>) is an instance of fs_<ak> *)


592 
(* uses the theorem fs_prod_inst *)


593 
val (thy23,_) = foldl_map (fn (thy, (ak_name, T)) =>


594 
let


595 
val qu_class = Sign.full_name (sign_of thy) ("fs_"^ak_name);


596 
val fs_inst = PureThy.get_thm thy (Name ("fs_"^ak_name^"_inst"));


597 
val proof = EVERY [AxClass.intro_classes_tac [],


598 
rtac ((fs_inst RS (fs_inst RS fs_prod_inst)) RS fs1) 1];


599 
in


600 
(AxClass.add_inst_arity_i ("*",[[qu_class],[qu_class]],[qu_class]) proof thy,())


601 
end) (thy22,ak_names_types);


602 


603 
(* shows that list(fs_<ak>) is an instance of fs_<ak> *)


604 
(* uses the theorem fs_list_inst *)


605 
val (thy24,_) = foldl_map (fn (thy, (ak_name, T)) =>


606 
let


607 
val qu_class = Sign.full_name (sign_of thy) ("fs_"^ak_name);


608 
val fs_inst = PureThy.get_thm thy (Name ("fs_"^ak_name^"_inst"));


609 
val proof = EVERY [AxClass.intro_classes_tac [],


610 
rtac ((fs_inst RS fs_list_inst) RS fs1) 1];


611 
in


612 
(AxClass.add_inst_arity_i ("List.list",[[qu_class]],[qu_class]) proof thy,())


613 
end) (thy23,ak_names_types);


614 


615 
(*<<<<<<< cp_<ak>_<ai> class instances >>>>>>>*)


616 
(*==============================================*)


617 
val cp1 = PureThy.get_thm thy24 (Name "cp1");


618 
val cp_unit_inst = PureThy.get_thm thy24 (Name "cp_unit_inst");


619 
val cp_bool_inst = PureThy.get_thm thy24 (Name "cp_bool_inst");


620 
val cp_prod_inst = PureThy.get_thm thy24 (Name "cp_prod_inst");


621 
val cp_list_inst = PureThy.get_thm thy24 (Name "cp_list_inst");


622 
val cp_fun_inst = PureThy.get_thm thy24 (Name "cp_fun_inst");


623 
val cp_option_inst = PureThy.get_thm thy24 (Name "cp_option_inst");


624 
val cp_noption_inst = PureThy.get_thm thy24 (Name "cp_noption_inst");


625 
val pt_perm_compose = PureThy.get_thm thy24 (Name "pt_perm_compose");


626 
val dj_pp_forget = PureThy.get_thm thy24 (Name "dj_perm_perm_forget");


627 


628 
(* shows that <aj> is an instance of cp_<ak>_<ai> *)


629 
(* that needs a threenested loop *)


630 
val (thy25,_) = foldl_map (fn (thy, (ak_name, T)) =>


631 
foldl_map (fn (thy', (ak_name', T')) =>


632 
foldl_map (fn (thy'', (ak_name'', T'')) =>


633 
let


634 
val qu_name = Sign.full_name (sign_of thy'') ak_name;


635 
val qu_class = Sign.full_name (sign_of thy'') ("cp_"^ak_name'^"_"^ak_name'');


636 
val proof =


637 
(if (ak_name'=ak_name'') then


638 
(let


639 
val pt_inst = PureThy.get_thm thy'' (Name ("pt_"^ak_name''^"_inst"));


640 
val at_inst = PureThy.get_thm thy'' (Name ("at_"^ak_name''^"_inst"));


641 
in


642 
EVERY [AxClass.intro_classes_tac [],


643 
rtac (at_inst RS (pt_inst RS pt_perm_compose)) 1]


644 
end)


645 
else


646 
(let


647 
val dj_inst = PureThy.get_thm thy'' (Name ("dj_"^ak_name''^"_"^ak_name'));


648 
val simp_s = HOL_basic_ss addsimps


649 
((dj_inst RS dj_pp_forget)::


650 
(PureThy.get_thmss thy''


651 
[Name (ak_name' ^"_prm_"^ak_name^"_def"),


652 
Name (ak_name''^"_prm_"^ak_name^"_def")]));


653 
in


654 
EVERY [AxClass.intro_classes_tac [], simp_tac simp_s 1]


655 
end))


656 
in


657 
(AxClass.add_inst_arity_i (qu_name,[],[qu_class]) proof thy'',())


658 
end)


659 
(thy', ak_names_types)) (thy, ak_names_types)) (thy24, ak_names_types);


660 


661 
(* shows that unit is an instance of cp_<ak>_<ai> *)


662 
(* for every <ak>combination *)


663 
val (thy26,_) = foldl_map (fn (thy, (ak_name, T)) =>


664 
foldl_map (fn (thy', (ak_name', T')) =>


665 
let


666 
val qu_class = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');


667 
val proof = EVERY [AxClass.intro_classes_tac [],rtac (cp_unit_inst RS cp1) 1];


668 
in


669 
(AxClass.add_inst_arity_i ("Product_Type.unit",[],[qu_class]) proof thy',())


670 
end)


671 
(thy, ak_names_types)) (thy25, ak_names_types);


672 


673 
(* shows that bool is an instance of cp_<ak>_<ai> *)


674 
(* for every <ak>combination *)


675 
val (thy27,_) = foldl_map (fn (thy, (ak_name, T)) =>


676 
foldl_map (fn (thy', (ak_name', T')) =>


677 
let


678 
val qu_class = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');


679 
val proof = EVERY [AxClass.intro_classes_tac [], rtac (cp_bool_inst RS cp1) 1];


680 
in


681 
(AxClass.add_inst_arity_i ("bool",[],[qu_class]) proof thy',())


682 
end)


683 
(thy, ak_names_types)) (thy26, ak_names_types);


684 


685 
(* shows that prod is an instance of cp_<ak>_<ai> *)


686 
(* for every <ak>combination *)


687 
val (thy28,_) = foldl_map (fn (thy, (ak_name, T)) =>


688 
foldl_map (fn (thy', (ak_name', T')) =>


689 
let


690 
val qu_class = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');


691 
val cp_inst = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));


692 
val proof = EVERY [AxClass.intro_classes_tac [],


693 
rtac ((cp_inst RS (cp_inst RS cp_prod_inst)) RS cp1) 1];


694 
in


695 
(AxClass.add_inst_arity_i ("*",[[qu_class],[qu_class]],[qu_class]) proof thy',())


696 
end)


697 
(thy, ak_names_types)) (thy27, ak_names_types);


698 


699 
(* shows that list is an instance of cp_<ak>_<ai> *)


700 
(* for every <ak>combination *)


701 
val (thy29,_) = foldl_map (fn (thy, (ak_name, T)) =>


702 
foldl_map (fn (thy', (ak_name', T')) =>


703 
let


704 
val qu_class = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');


705 
val cp_inst = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));


706 
val proof = EVERY [AxClass.intro_classes_tac [],


707 
rtac ((cp_inst RS cp_list_inst) RS cp1) 1];


708 
in


709 
(AxClass.add_inst_arity_i ("List.list",[[qu_class]],[qu_class]) proof thy',())


710 
end)


711 
(thy, ak_names_types)) (thy28, ak_names_types);


712 


713 
(* shows that function is an instance of cp_<ak>_<ai> *)


714 
(* for every <ak>combination *)


715 
val (thy30,_) = foldl_map (fn (thy, (ak_name, T)) =>


716 
foldl_map (fn (thy', (ak_name', T')) =>


717 
let


718 
val qu_class = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');


719 
val cp_inst = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));


720 
val pt_inst = PureThy.get_thm thy' (Name ("pt_"^ak_name^"_inst"));


721 
val at_inst = PureThy.get_thm thy' (Name ("at_"^ak_name^"_inst"));


722 
val proof = EVERY [AxClass.intro_classes_tac [],


723 
rtac ((at_inst RS (pt_inst RS (cp_inst RS (cp_inst RS cp_fun_inst)))) RS cp1) 1];


724 
in


725 
(AxClass.add_inst_arity_i ("fun",[[qu_class],[qu_class]],[qu_class]) proof thy',())


726 
end)


727 
(thy, ak_names_types)) (thy29, ak_names_types);


728 


729 
(* shows that option is an instance of cp_<ak>_<ai> *)


730 
(* for every <ak>combination *)


731 
val (thy31,_) = foldl_map (fn (thy, (ak_name, T)) =>


732 
foldl_map (fn (thy', (ak_name', T')) =>


733 
let


734 
val qu_class = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');


735 
val cp_inst = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));


736 
val proof = EVERY [AxClass.intro_classes_tac [],


737 
rtac ((cp_inst RS cp_option_inst) RS cp1) 1];


738 
in


739 
(AxClass.add_inst_arity_i ("Datatype.option",[[qu_class]],[qu_class]) proof thy',())


740 
end)


741 
(thy, ak_names_types)) (thy30, ak_names_types);


742 


743 
(* shows that nOption is an instance of cp_<ak>_<ai> *)


744 
(* for every <ak>combination *)


745 
val (thy32,_) = foldl_map (fn (thy, (ak_name, T)) =>


746 
foldl_map (fn (thy', (ak_name', T')) =>


747 
let


748 
val qu_class = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');


749 
val cp_inst = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));


750 
val proof = EVERY [AxClass.intro_classes_tac [],


751 
rtac ((cp_inst RS cp_noption_inst) RS cp1) 1];


752 
in


753 
(AxClass.add_inst_arity_i ("nominal.nOption",[[qu_class]],[qu_class]) proof thy',())


754 
end)


755 
(thy, ak_names_types)) (thy31, ak_names_types);


756 


757 
(* abbreviations for some collection of rules *)


758 
(*============================================*)


759 
val abs_fun_pi = PureThy.get_thm thy32 (Name ("nominal.abs_fun_pi"));


760 
val abs_fun_pi_ineq = PureThy.get_thm thy32 (Name ("nominal.abs_fun_pi_ineq"));


761 
val abs_fun_eq = PureThy.get_thm thy32 (Name ("nominal.abs_fun_eq"));


762 
val dj_perm_forget = PureThy.get_thm thy32 (Name ("nominal.dj_perm_forget"));


763 
val dj_pp_forget = PureThy.get_thm thy32 (Name ("nominal.dj_perm_perm_forget"));


764 
val fresh_iff = PureThy.get_thm thy32 (Name ("nominal.fresh_abs_fun_iff"));


765 
val fresh_iff_ineq = PureThy.get_thm thy32 (Name ("nominal.fresh_abs_fun_iff_ineq"));


766 
val abs_fun_supp = PureThy.get_thm thy32 (Name ("nominal.abs_fun_supp"));


767 
val abs_fun_supp_ineq = PureThy.get_thm thy32 (Name ("nominal.abs_fun_supp_ineq"));


768 
val pt_swap_bij = PureThy.get_thm thy32 (Name ("nominal.pt_swap_bij"));


769 
val pt_fresh_fresh = PureThy.get_thm thy32 (Name ("nominal.pt_fresh_fresh"));


770 
val pt_bij = PureThy.get_thm thy32 (Name ("nominal.pt_bij"));


771 
val pt_perm_compose = PureThy.get_thm thy32 (Name ("nominal.pt_perm_compose"));


772 
val perm_eq_app = PureThy.get_thm thy32 (Name ("nominal.perm_eq_app"));


773 


774 
(* abs_perm collects all lemmas for simplifying a permutation *)


775 
(* in front of an abs_fun *)


776 
val (thy33,_) =


777 
let


778 
val name = "abs_perm"


779 
val thm_list = Library.flat (map (fn (ak_name, T) =>


780 
let


781 
val at_inst = PureThy.get_thm thy32 (Name ("at_"^ak_name^"_inst"));


782 
val pt_inst = PureThy.get_thm thy32 (Name ("pt_"^ak_name^"_inst"));


783 
val thm = [pt_inst, at_inst] MRS abs_fun_pi


784 
val thm_list = map (fn (ak_name', T') =>


785 
let


786 
val cp_inst = PureThy.get_thm thy32 (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));


787 
in


788 
[pt_inst, pt_inst, at_inst, cp_inst] MRS abs_fun_pi_ineq


789 
end) ak_names_types;


790 
in thm::thm_list end) (ak_names_types))


791 
in


792 
(PureThy.add_thmss [((name, thm_list),[])] thy32)


793 
end;


794 


795 
(* alpha collects all lemmas analysing an equation *)


796 
(* between abs_funs *)


797 
(*val (thy34,_) =


798 
let


799 
val name = "alpha"


800 
val thm_list = map (fn (ak_name, T) =>


801 
let


802 
val at_inst = PureThy.get_thm thy33 (Name ("at_"^ak_name^"_inst"));


803 
val pt_inst = PureThy.get_thm thy33 (Name ("pt_"^ak_name^"_inst"));


804 
in


805 
[pt_inst, at_inst] MRS abs_fun_eq


806 
end) ak_names_types


807 
in


808 
(PureThy.add_thmss [((name, thm_list),[])] thy33)


809 
end;*)


810 


811 
val (thy34,_) =


812 
let


813 
fun inst_pt_at thm ak_name =


814 
let


815 
val at_inst = PureThy.get_thm thy33 (Name ("at_"^ak_name^"_inst"));


816 
val pt_inst = PureThy.get_thm thy33 (Name ("pt_"^ak_name^"_inst"));


817 
in


818 
[pt_inst, at_inst] MRS thm


819 
end


820 


821 
in


822 
thy33


823 
> PureThy.add_thmss [(("alpha", map (inst_pt_at abs_fun_eq) ak_names),[])]


824 
>>> PureThy.add_thmss [(("perm_swap", map (inst_pt_at pt_swap_bij) ak_names),[])]


825 
>>> PureThy.add_thmss [(("perm_fresh_fresh", map (inst_pt_at pt_fresh_fresh) ak_names),[])]


826 
>>> PureThy.add_thmss [(("perm_bij", map (inst_pt_at pt_bij) ak_names),[])]


827 
>>> PureThy.add_thmss [(("perm_compose", map (inst_pt_at pt_perm_compose) ak_names),[])]


828 
>>> PureThy.add_thmss [(("perm_app_eq", map (inst_pt_at perm_eq_app) ak_names),[])]


829 
end;


830 


831 
(* perm_dj collects all lemmas that forget an permutation *)


832 
(* when it acts on an atom of different type *)


833 
val (thy35,_) =


834 
let


835 
val name = "perm_dj"


836 
val thm_list = Library.flat (map (fn (ak_name, T) =>


837 
Library.flat (map (fn (ak_name', T') =>


838 
if not (ak_name = ak_name')


839 
then


840 
let


841 
val dj_inst = PureThy.get_thm thy34 (Name ("dj_"^ak_name^"_"^ak_name'));


842 
in


843 
[dj_inst RS dj_perm_forget, dj_inst RS dj_pp_forget]


844 
end


845 
else []) ak_names_types)) ak_names_types)


846 
in


847 
(PureThy.add_thmss [((name, thm_list),[])] thy34)


848 
end;


849 


850 
(* abs_fresh collects all lemmas for simplifying a freshness *)


851 
(* proposition involving an abs_fun *)


852 


853 
val (thy36,_) =


854 
let


855 
val name = "abs_fresh"


856 
val thm_list = Library.flat (map (fn (ak_name, T) =>


857 
let


858 
val at_inst = PureThy.get_thm thy35 (Name ("at_"^ak_name^"_inst"));


859 
val pt_inst = PureThy.get_thm thy35 (Name ("pt_"^ak_name^"_inst"));


860 
val fs_inst = PureThy.get_thm thy35 (Name ("fs_"^ak_name^"_inst"));


861 
val thm = [pt_inst, at_inst, (fs_inst RS fs1)] MRS fresh_iff


862 
val thm_list = Library.flat (map (fn (ak_name', T') =>


863 
(if (not (ak_name = ak_name'))


864 
then


865 
let


866 
val cp_inst = PureThy.get_thm thy35 (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));


867 
val dj_inst = PureThy.get_thm thy35 (Name ("dj_"^ak_name'^"_"^ak_name));


868 
in


869 
[[pt_inst, pt_inst, at_inst, cp_inst, dj_inst] MRS fresh_iff_ineq]


870 
end


871 
else [])) ak_names_types);


872 
in thm::thm_list end) (ak_names_types))


873 
in


874 
(PureThy.add_thmss [((name, thm_list),[])] thy35)


875 
end;


876 


877 
(* abs_supp collects all lemmas for simplifying *)


878 
(* support proposition involving an abs_fun *)


879 


880 
val (thy37,_) =


881 
let


882 
val name = "abs_supp"


883 
val thm_list = Library.flat (map (fn (ak_name, T) =>


884 
let


885 
val at_inst = PureThy.get_thm thy36 (Name ("at_"^ak_name^"_inst"));


886 
val pt_inst = PureThy.get_thm thy36 (Name ("pt_"^ak_name^"_inst"));


887 
val fs_inst = PureThy.get_thm thy36 (Name ("fs_"^ak_name^"_inst"));


888 
val thm1 = [pt_inst, at_inst, (fs_inst RS fs1)] MRS abs_fun_supp


889 
val thm2 = [pt_inst, at_inst] MRS abs_fun_supp


890 
val thm_list = Library.flat (map (fn (ak_name', T') =>


891 
(if (not (ak_name = ak_name'))


892 
then


893 
let


894 
val cp_inst = PureThy.get_thm thy36 (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));


895 
val dj_inst = PureThy.get_thm thy36 (Name ("dj_"^ak_name'^"_"^ak_name));


896 
in


897 
[[pt_inst, pt_inst, at_inst, cp_inst, dj_inst] MRS abs_fun_supp_ineq]


898 
end


899 
else [])) ak_names_types);


900 
in thm1::thm2::thm_list end) (ak_names_types))


901 
in


902 
(PureThy.add_thmss [((name, thm_list),[])] thy36)


903 
end;


904 


905 
in NominalData.put (fold Symtab.update (map (rpair ()) full_ak_names)


906 
(NominalData.get thy11)) thy37


907 
end;


908 


909 


910 
(* syntax und parsing *)


911 
structure P = OuterParse and K = OuterKeyword;


912 


913 
val atom_declP =


914 
OuterSyntax.command "atom_decl" "Declare new kinds of atoms" K.thy_decl


915 
(Scan.repeat1 P.name >> (Toplevel.theory o create_nom_typedecls));


916 


917 
val _ = OuterSyntax.add_parsers [atom_declP];


918 


919 
val setup = [NominalData.init];


920 


921 
(*=======================================================================*)


922 

18016

923 
(** FIXME: DatatypePackage should export this function **)


924 


925 
local


926 


927 
fun dt_recs (DtTFree _) = []


928 
 dt_recs (DtType (_, dts)) = List.concat (map dt_recs dts)


929 
 dt_recs (DtRec i) = [i];


930 


931 
fun dt_cases (descr: descr) (_, args, constrs) =


932 
let


933 
fun the_bname i = Sign.base_name (#1 (valOf (AList.lookup (op =) descr i)));


934 
val bnames = map the_bname (distinct (List.concat (map dt_recs args)));


935 
in map (fn (c, _) => space_implode "_" (Sign.base_name c :: bnames)) constrs end;


936 


937 


938 
fun induct_cases descr =


939 
DatatypeProp.indexify_names (List.concat (map (dt_cases descr) (map #2 descr)));


940 


941 
fun exhaust_cases descr i = dt_cases descr (valOf (AList.lookup (op =) descr i));


942 


943 
in


944 


945 
fun mk_case_names_induct descr = RuleCases.case_names (induct_cases descr);


946 


947 
fun mk_case_names_exhausts descr new =


948 
map (RuleCases.case_names o exhaust_cases descr o #1)


949 
(List.filter (fn ((_, (name, _, _))) => name mem_string new) descr);


950 


951 
end;


952 


953 
(*******************************)


954 

17870

955 
val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);


956 


957 
fun read_typ sign ((Ts, sorts), str) =


958 
let


959 
val T = Type.no_tvars (Sign.read_typ (sign, (AList.lookup op =)


960 
(map (apfst (rpair ~1)) sorts)) str) handle TYPE (msg, _, _) => error msg


961 
in (Ts @ [T], add_typ_tfrees (T, sorts)) end;


962 


963 
(** taken from HOL/Tools/datatype_aux.ML **)


964 


965 
fun indtac indrule indnames i st =


966 
let


967 
val ts = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule));


968 
val ts' = HOLogic.dest_conj (HOLogic.dest_Trueprop


969 
(Logic.strip_imp_concl (List.nth (prems_of st, i  1))));


970 
val getP = if can HOLogic.dest_imp (hd ts) then


971 
(apfst SOME) o HOLogic.dest_imp else pair NONE;


972 
fun abstr (t1, t2) = (case t1 of


973 
NONE => (case filter (fn Free (s, _) => s mem indnames  _ => false)


974 
(term_frees t2) of


975 
[Free (s, T)] => absfree (s, T, t2)


976 
 _ => sys_error "indtac")


977 
 SOME (_ $ t' $ _) => Abs ("x", fastype_of t', abstract_over (t', t2)))


978 
val cert = cterm_of (Thm.sign_of_thm st);


979 
val Ps = map (cert o head_of o snd o getP) ts;


980 
val indrule' = cterm_instantiate (Ps ~~


981 
(map (cert o abstr o getP) ts')) indrule


982 
in


983 
rtac indrule' i st


984 
end;


985 


986 
fun gen_add_nominal_datatype prep_typ err flat_names new_type_names dts thy =


987 
let


988 
(* this theory is used just for parsing *)


989 


990 
val tmp_thy = thy >


991 
Theory.copy >


992 
Theory.add_types (map (fn (tvs, tname, mx, _) =>


993 
(tname, length tvs, mx)) dts);


994 


995 
val sign = Theory.sign_of tmp_thy;


996 


997 
val atoms = atoms_of thy;


998 
val classes = map (NameSpace.map_base (fn s => "pt_" ^ s)) atoms;


999 
val cp_classes = List.concat (map (fn atom1 => map (fn atom2 =>


1000 
Sign.intern_class thy ("cp_" ^ Sign.base_name atom1 ^ "_" ^


1001 
Sign.base_name atom2)) atoms) atoms);


1002 
fun augment_sort S = S union classes;


1003 
val augment_sort_typ = map_type_tfree (fn (s, S) => TFree (s, augment_sort S));


1004 


1005 
fun prep_constr ((constrs, sorts), (cname, cargs, mx)) =


1006 
let val (cargs', sorts') = Library.foldl (prep_typ sign) (([], sorts), cargs)


1007 
in (constrs @ [(cname, cargs', mx)], sorts') end


1008 


1009 
fun prep_dt_spec ((dts, sorts), (tvs, tname, mx, constrs)) =


1010 
let val (constrs', sorts') = Library.foldl prep_constr (([], sorts), constrs)


1011 
in (dts @ [(tvs, tname, mx, constrs')], sorts') end


1012 


1013 
val (dts', sorts) = Library.foldl prep_dt_spec (([], []), dts);


1014 
val sorts' = map (apsnd augment_sort) sorts;


1015 
val tyvars = map #1 dts';


1016 


1017 
val types_syntax = map (fn (tvs, tname, mx, constrs) => (tname, mx)) dts';


1018 
val constr_syntax = map (fn (tvs, tname, mx, constrs) =>


1019 
map (fn (cname, cargs, mx) => (cname, mx)) constrs) dts';


1020 


1021 
val ps = map (fn (_, n, _, _) =>


1022 
(Sign.full_name sign n, Sign.full_name sign (n ^ "_Rep"))) dts;


1023 
val rps = map Library.swap ps;


1024 


1025 
fun replace_types (Type ("nominal.ABS", [T, U])) =


1026 
Type ("fun", [T, Type ("nominal.nOption", [replace_types U])])


1027 
 replace_types (Type (s, Ts)) =


1028 
Type (getOpt (AList.lookup op = ps s, s), map replace_types Ts)


1029 
 replace_types T = T;


1030 


1031 
fun replace_types' (Type (s, Ts)) =


1032 
Type (getOpt (AList.lookup op = rps s, s), map replace_types' Ts)


1033 
 replace_types' T = T;


1034 


1035 
val dts'' = map (fn (tvs, tname, mx, constrs) => (tvs, tname ^ "_Rep", NoSyn,


1036 
map (fn (cname, cargs, mx) => (cname,


1037 
map (augment_sort_typ o replace_types) cargs, NoSyn)) constrs)) dts';


1038 


1039 
val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;


1040 
val full_new_type_names' = map (Sign.full_name (sign_of thy)) new_type_names';


1041 

18045

1042 
val ({induction, ...},thy1) =

17870

1043 
DatatypePackage.add_datatype_i err flat_names new_type_names' dts'' thy;


1044 


1045 
val SOME {descr, ...} = Symtab.lookup


1046 
(DatatypePackage.get_datatypes thy1) (hd full_new_type_names');


1047 
val typ_of_dtyp = typ_of_dtyp descr sorts';


1048 
fun nth_dtyp i = typ_of_dtyp (DtRec i);


1049 


1050 
(**** define permutation functions ****)


1051 


1052 
val permT = mk_permT (TFree ("'x", HOLogic.typeS));


1053 
val pi = Free ("pi", permT);


1054 
val perm_types = map (fn (i, _) =>


1055 
let val T = nth_dtyp i


1056 
in permT > T > T end) descr;


1057 
val perm_names = replicate (length new_type_names) "nominal.perm" @


1058 
DatatypeProp.indexify_names (map (fn i => Sign.full_name (sign_of thy1)


1059 
("perm_" ^ name_of_typ (nth_dtyp i)))


1060 
(length new_type_names upto length descr  1));


1061 
val perm_names_types = perm_names ~~ perm_types;


1062 


1063 
val perm_eqs = List.concat (map (fn (i, (_, _, constrs)) =>


1064 
let val T = nth_dtyp i


1065 
in map (fn (cname, dts) =>


1066 
let


1067 
val Ts = map typ_of_dtyp dts;


1068 
val names = DatatypeProp.make_tnames Ts;


1069 
val args = map Free (names ~~ Ts);


1070 
val c = Const (cname, Ts > T);


1071 
fun perm_arg (dt, x) =


1072 
let val T = type_of x


1073 
in if is_rec_type dt then


1074 
let val (Us, _) = strip_type T


1075 
in list_abs (map (pair "x") Us,


1076 
Const (List.nth (perm_names_types, body_index dt)) $ pi $


1077 
list_comb (x, map (fn (i, U) =>


1078 
Const ("nominal.perm", permT > U > U) $


1079 
(Const ("List.rev", permT > permT) $ pi) $


1080 
Bound i) ((length Us  1 downto 0) ~~ Us)))


1081 
end


1082 
else Const ("nominal.perm", permT > T > T) $ pi $ x


1083 
end;


1084 
in


1085 
(("", HOLogic.mk_Trueprop (HOLogic.mk_eq


1086 
(Const (List.nth (perm_names_types, i)) $


1087 
Free ("pi", mk_permT (TFree ("'x", HOLogic.typeS))) $


1088 
list_comb (c, args),


1089 
list_comb (c, map perm_arg (dts ~~ args))))), [])


1090 
end) constrs


1091 
end) descr);


1092 


1093 
val (thy2, perm_simps) = thy1 >


1094 
Theory.add_consts_i (map (fn (s, T) => (Sign.base_name s, T, NoSyn))


1095 
(List.drop (perm_names_types, length new_type_names))) >


1096 
PrimrecPackage.add_primrec_i "" perm_eqs;


1097 


1098 
(**** prove that permutation functions introduced by unfolding are ****)


1099 
(**** equivalent to already existing permutation functions ****)


1100 


1101 
val _ = warning ("length descr: " ^ string_of_int (length descr));


1102 
val _ = warning ("length new_type_names: " ^ string_of_int (length new_type_names));


1103 


1104 
val perm_indnames = DatatypeProp.make_tnames (map body_type perm_types);


1105 
val perm_fun_def = PureThy.get_thm thy2 (Name "perm_fun_def");


1106 


1107 
val unfolded_perm_eq_thms =


1108 
if length descr = length new_type_names then []


1109 
else map standard (List.drop (split_conj_thm

18010

1110 
(Goal.prove thy2 [] []

17870

1111 
(HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj


1112 
(map (fn (c as (s, T), x) =>


1113 
let val [T1, T2] = binder_types T


1114 
in HOLogic.mk_eq (Const c $ pi $ Free (x, T2),


1115 
Const ("nominal.perm", T) $ pi $ Free (x, T2))


1116 
end)

18010

1117 
(perm_names_types ~~ perm_indnames))))


1118 
(fn _ => EVERY [indtac induction perm_indnames 1,

17870

1119 
ALLGOALS (asm_full_simp_tac


1120 
(simpset_of thy2 addsimps [perm_fun_def]))])),


1121 
length new_type_names));


1122 


1123 
(**** prove [] \<bullet> t = t ****)


1124 


1125 
val _ = warning "perm_empty_thms";


1126 


1127 
val perm_empty_thms = List.concat (map (fn a =>


1128 
let val permT = mk_permT (Type (a, []))


1129 
in map standard (List.take (split_conj_thm

18010

1130 
(Goal.prove thy2 [] []

17870

1131 
(HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj


1132 
(map (fn ((s, T), x) => HOLogic.mk_eq


1133 
(Const (s, permT > T > T) $


1134 
Const ("List.list.Nil", permT) $ Free (x, T),


1135 
Free (x, T)))


1136 
(perm_names ~~

18010

1137 
map body_type perm_types ~~ perm_indnames))))


1138 
(fn _ => EVERY [indtac induction perm_indnames 1,

17870

1139 
ALLGOALS (asm_full_simp_tac (simpset_of thy2))])),


1140 
length new_type_names))


1141 
end)


1142 
atoms);


1143 


1144 
(**** prove (pi1 @ pi2) \<bullet> t = pi1 \<bullet> (pi2 \<bullet> t) ****)


1145 


1146 
val _ = warning "perm_append_thms";


1147 


1148 
(*FIXME: these should be looked up statically*)


1149 
val at_pt_inst = PureThy.get_thm thy2 (Name "at_pt_inst");


1150 
val pt2 = PureThy.get_thm thy2 (Name "pt2");


1151 


1152 
val perm_append_thms = List.concat (map (fn a =>


1153 
let


1154 
val permT = mk_permT (Type (a, []));


1155 
val pi1 = Free ("pi1", permT);


1156 
val pi2 = Free ("pi2", permT);


1157 
val pt_inst = PureThy.get_thm thy2 (Name ("pt_" ^ Sign.base_name a ^ "_inst"));


1158 
val pt2' = pt_inst RS pt2;


1159 
val pt2_ax = PureThy.get_thm thy2


1160 
(Name (NameSpace.map_base (fn s => "pt_" ^ s ^ "2") a));


1161 
in List.take (map standard (split_conj_thm

18010

1162 
(Goal.prove thy2 [] []

17870

1163 
(HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj


1164 
(map (fn ((s, T), x) =>


1165 
let val perm = Const (s, permT > T > T)


1166 
in HOLogic.mk_eq


1167 
(perm $ (Const ("List.op @", permT > permT > permT) $


1168 
pi1 $ pi2) $ Free (x, T),


1169 
perm $ pi1 $ (perm $ pi2 $ Free (x, T)))


1170 
end)


1171 
(perm_names ~~

18010

1172 
map body_type perm_types ~~ perm_indnames))))


1173 
(fn _ => EVERY [indtac induction perm_indnames 1,

17870

1174 
ALLGOALS (asm_full_simp_tac (simpset_of thy2 addsimps [pt2', pt2_ax]))]))),


1175 
length new_type_names)


1176 
end) atoms);


1177 


1178 
(**** prove pi1 ~ pi2 ==> pi1 \<bullet> t = pi2 \<bullet> t ****)


1179 


1180 
val _ = warning "perm_eq_thms";


1181 


1182 
val pt3 = PureThy.get_thm thy2 (Name "pt3");


1183 
val pt3_rev = PureThy.get_thm thy2 (Name "pt3_rev");


1184 


1185 
val perm_eq_thms = List.concat (map (fn a =>


1186 
let


1187 
val permT = mk_permT (Type (a, []));


1188 
val pi1 = Free ("pi1", permT);


1189 
val pi2 = Free ("pi2", permT);


1190 
(*FIXME: not robust  better access these theorems using NominalData?*)


1191 
val at_inst = PureThy.get_thm thy2 (Name ("at_" ^ Sign.base_name a ^ "_inst"));


1192 
val pt_inst = PureThy.get_thm thy2 (Name ("pt_" ^ Sign.base_name a ^ "_inst"));


1193 
val pt3' = pt_inst RS pt3;


1194 
val pt3_rev' = at_inst RS (pt_inst RS pt3_rev);


1195 
val pt3_ax = PureThy.get_thm thy2


1196 
(Name (NameSpace.map_base (fn s => "pt_" ^ s ^ "3") a));


1197 
in List.take (map standard (split_conj_thm

18010

1198 
(Goal.prove thy2 [] [] (Logic.mk_implies

17870

1199 
(HOLogic.mk_Trueprop (Const ("nominal.prm_eq",


1200 
permT > permT > HOLogic.boolT) $ pi1 $ pi2),


1201 
HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj


1202 
(map (fn ((s, T), x) =>


1203 
let val perm = Const (s, permT > T > T)


1204 
in HOLogic.mk_eq


1205 
(perm $ pi1 $ Free (x, T),


1206 
perm $ pi2 $ Free (x, T))


1207 
end)


1208 
(perm_names ~~

18010

1209 
map body_type perm_types ~~ perm_indnames)))))


1210 
(fn _ => EVERY [indtac induction perm_indnames 1,

17870

1211 
ALLGOALS (asm_full_simp_tac (simpset_of thy2 addsimps [pt3', pt3_rev', pt3_ax]))]))),


1212 
length new_type_names)


1213 
end) atoms);


1214 


1215 
(**** prove pi1 \<bullet> (pi2 \<bullet> t) = (pi1 \<bullet> pi2) \<bullet> (pi1 \<bullet> t) ****)


1216 


1217 
val cp1 = PureThy.get_thm thy2 (Name "cp1");


1218 
val dj_cp = PureThy.get_thm thy2 (Name "dj_cp");


1219 
val pt_perm_compose = PureThy.get_thm thy2 (Name "pt_perm_compose");


1220 
val pt_perm_compose_rev = PureThy.get_thm thy2 (Name "pt_perm_compose_rev");


1221 
val dj_perm_perm_forget = PureThy.get_thm thy2 (Name "dj_perm_perm_forget");


1222 


1223 
fun composition_instance name1 name2 thy =


1224 
let


1225 
val name1' = Sign.base_name name1;


1226 
val name2' = Sign.base_name name2;


1227 
val cp_class = Sign.intern_class thy ("cp_" ^ name1' ^ "_" ^ name2');


1228 
val permT1 = mk_permT (Type (name1, []));


1229 
val permT2 = mk_permT (Type (name2, []));


1230 
val augment = map_type_tfree


1231 
(fn (x, S) => TFree (x, cp_class :: S));


1232 
val Ts = map (augment o body_type) perm_types;


1233 
val cp_inst = PureThy.get_thm thy


1234 
(Name ("cp_" ^ name1' ^ "_" ^ name2' ^ "_inst"));


1235 
val simps = simpset_of thy addsimps (perm_fun_def ::


1236 
(if name1 <> name2 then


1237 
let val dj = PureThy.get_thm thy (Name ("dj_" ^ name2' ^ "_" ^ name1'))


1238 
in [dj RS (cp_inst RS dj_cp), dj RS dj_perm_perm_forget] end


1239 
else


1240 
let


1241 
val at_inst = PureThy.get_thm thy (Name ("at_" ^ name1' ^ "_inst"));


1242 
val pt_inst = PureThy.get_thm thy (Name ("pt_" ^ name1' ^ "_inst"))


1243 
in


1244 
[cp_inst RS cp1 RS sym,


1245 
at_inst RS (pt_inst RS pt_perm_compose) RS sym,


1246 
at_inst RS (pt_inst RS pt_perm_compose_rev) RS sym]


1247 
end))

18010

1248 
val thms = split_conj_thm (standard (Goal.prove thy [] []

17870

1249 
(HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj


1250 
(map (fn ((s, T), x) =>


1251 
let


1252 
val pi1 = Free ("pi1", permT1);


1253 
val pi2 = Free ("pi2", permT2);


1254 
val perm1 = Const (s, permT1 > T > T);


1255 
val perm2 = Const (s, permT2 > T > T);


1256 
val perm3 = Const ("nominal.perm", permT1 > permT2 > permT2)


1257 
in HOLogic.mk_eq


1258 
(perm1 $ pi1 $ (perm2 $ pi2 $ Free (x, T)),


1259 
perm2 $ (perm3 $ pi1 $ pi2) $ (perm1 $ pi1 $ Free (x, T)))


1260 
end)

18010

1261 
(perm_names ~~ Ts ~~ perm_indnames))))


1262 
(fn _ => EVERY [indtac induction perm_indnames 1,


1263 
ALLGOALS (asm_full_simp_tac simps)])))

17870

1264 
in


1265 
foldl (fn ((s, tvs), thy) => AxClass.add_inst_arity_i


1266 
(s, replicate (length tvs) (cp_class :: classes), [cp_class])


1267 
(AxClass.intro_classes_tac [] THEN ALLGOALS (resolve_tac thms)) thy)


1268 
thy (full_new_type_names' ~~ tyvars)


1269 
end;


1270 


1271 
val (thy3, perm_thmss) = thy2 >


1272 
fold (fn name1 => fold (composition_instance name1) atoms) atoms >


1273 
curry (Library.foldr (fn ((i, (tyname, args, _)), thy) =>


1274 
AxClass.add_inst_arity_i (tyname, replicate (length args) classes, classes)


1275 
(AxClass.intro_classes_tac [] THEN REPEAT (EVERY


1276 
[resolve_tac perm_empty_thms 1,


1277 
resolve_tac perm_append_thms 1,


1278 
resolve_tac perm_eq_thms 1, assume_tac 1])) thy))


1279 
(List.take (descr, length new_type_names)) >


1280 
PureThy.add_thmss


1281 
[((space_implode "_" new_type_names ^ "_unfolded_perm_eq",


1282 
unfolded_perm_eq_thms), [Simplifier.simp_add_global]),


1283 
((space_implode "_" new_type_names ^ "_perm_empty",


1284 
perm_empty_thms), [Simplifier.simp_add_global]),


1285 
((space_implode "_" new_type_names ^ "_perm_append",


1286 
perm_append_thms), [Simplifier.simp_add_global]),


1287 
((space_implode "_" new_type_names ^ "_perm_eq",


1288 
perm_eq_thms), [Simplifier.simp_add_global])];


1289 


1290 
(**** Define representing sets ****)


1291 


1292 
val _ = warning "representing sets";


1293 


1294 
val rep_set_names = map (Sign.full_name thy3) (DatatypeProp.indexify_names


1295 
(map (fn (i, _) => name_of_typ (nth_dtyp i) ^ "_set") descr));


1296 
val big_rep_name =


1297 
space_implode "_" (DatatypeProp.indexify_names (List.mapPartial


1298 
(fn (i, ("nominal.nOption", _, _)) => NONE


1299 
 (i, _) => SOME (name_of_typ (nth_dtyp i))) descr)) ^ "_set";


1300 
val _ = warning ("big_rep_name: " ^ big_rep_name);


1301 


1302 
fun strip_option (dtf as DtType ("fun", [dt, DtRec i])) =


1303 
(case AList.lookup op = descr i of


1304 
SOME ("nominal.nOption", _, [(_, [dt']), _]) =>


1305 
apfst (cons dt) (strip_option dt')


1306 
 _ => ([], dtf))


1307 
 strip_option dt = ([], dt);


1308 


1309 
fun make_intr s T (cname, cargs) =


1310 
let


1311 
fun mk_prem (dt, (j, j', prems, ts)) =


1312 
let


1313 
val (dts, dt') = strip_option dt;


1314 
val (dts', dt'') = strip_dtyp dt';


1315 
val Ts = map typ_of_dtyp dts;


1316 
val Us = map typ_of_dtyp dts';


1317 
val T = typ_of_dtyp dt'';


1318 
val free = mk_Free "x" (Us > T) j;


1319 
val free' = app_bnds free (length Us);


1320 
fun mk_abs_fun (T, (i, t)) =


1321 
let val U = fastype_of t


1322 
in (i + 1, Const ("nominal.abs_fun", [T, U, T] >


1323 
Type ("nominal.nOption", [U])) $ mk_Free "y" T i $ t)


1324 
end


1325 
in (j + 1, j' + length Ts,


1326 
case dt'' of


1327 
DtRec k => list_all (map (pair "x") Us,


1328 
HOLogic.mk_Trueprop (HOLogic.mk_mem (free',


1329 
Const (List.nth (rep_set_names, k),


1330 
HOLogic.mk_setT T)))) :: prems


1331 
 _ => prems,


1332 
snd (foldr mk_abs_fun (j', free) Ts) :: ts)


1333 
end;


1334 


1335 
val (_, _, prems, ts) = foldr mk_prem (1, 1, [], []) cargs;


1336 
val concl = HOLogic.mk_Trueprop (HOLogic.mk_mem


1337 
(list_comb (Const (cname, map fastype_of ts > T), ts),


1338 
Const (s, HOLogic.mk_setT T)))


1339 
in Logic.list_implies (prems, concl)


1340 
end;


1341 


1342 
val (intr_ts, ind_consts) =


1343 
apfst List.concat (ListPair.unzip (List.mapPartial


1344 
(fn ((_, ("nominal.nOption", _, _)), _) => NONE


1345 
 ((i, (_, _, constrs)), rep_set_name) =>


1346 
let val T = nth_dtyp i


1347 
in SOME (map (make_intr rep_set_name T) constrs,


1348 
Const (rep_set_name, HOLogic.mk_setT T))


1349 
end)


1350 
(descr ~~ rep_set_names)));


1351 


1352 
val (thy4, {raw_induct = rep_induct, intrs = rep_intrs, ...}) =


1353 
setmp InductivePackage.quiet_mode false


1354 
(InductivePackage.add_inductive_i false true big_rep_name false true false


1355 
ind_consts (map (fn x => (("", x), [])) intr_ts) []) thy3;


1356 


1357 
(**** Prove that representing set is closed under permutation ****)


1358 


1359 
val _ = warning "proving closure under permutation...";


1360 


1361 
val perm_indnames' = List.mapPartial


1362 
(fn (x, (_, ("nominal.nOption", _, _))) => NONE  (x, _) => SOME x)


1363 
(perm_indnames ~~ descr);


1364 


1365 
fun mk_perm_closed name = map (fn th => standard (th RS mp))

18010

1366 
(List.take (split_conj_thm (Goal.prove thy4 [] []

17870

1367 
(HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map


1368 
(fn (S, x) =>


1369 
let


1370 
val S = map_term_types (map_type_tfree


1371 
(fn (s, cs) => TFree (s, cs union cp_classes))) S;


1372 
val T = HOLogic.dest_setT (fastype_of S);


1373 
val permT = mk_permT (Type (name, []))


1374 
in HOLogic.mk_imp (HOLogic.mk_mem (Free (x, T), S),


1375 
HOLogic.mk_mem (Const ("nominal.perm", permT > T > T) $


1376 
Free ("pi", permT) $ Free (x, T), S))

18010

1377 
end) (ind_consts ~~ perm_indnames'))))


1378 
(fn _ => EVERY (* CU: added perm_fun_def in the final tactic in order to deal with funs *)

17870

1379 
[indtac rep_induct [] 1,


1380 
ALLGOALS (simp_tac (simpset_of thy4 addsimps


1381 
(symmetric perm_fun_def :: PureThy.get_thms thy4 (Name ("abs_perm"))))),


1382 
ALLGOALS (resolve_tac rep_intrs


1383 
THEN_ALL_NEW (asm_full_simp_tac (simpset_of thy4 addsimps [perm_fun_def])))])),


1384 
length new_type_names));


1385 


1386 
(* FIXME: theorems are stored in database for testing only *)


1387 
val perm_closed_thmss = map mk_perm_closed atoms;


1388 
val (thy5, _) = PureThy.add_thmss [(("perm_closed",


1389 
List.concat perm_closed_thmss), [])] thy4;


1390 


1391 
(**** typedef ****)


1392 


1393 
val _ = warning "defining type...";


1394 


1395 
val (thy6, typedefs) =


1396 
foldl_map (fn (thy, ((((name, mx), tvs), c), name')) =>


1397 
setmp TypedefPackage.quiet_mode true


1398 
(TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx) c NONE


1399 
(rtac exI 1 THEN


1400 
QUIET_BREADTH_FIRST (has_fewer_prems 1)


1401 
(resolve_tac rep_intrs 1))) thy > (fn (thy, r) =>


1402 
let


1403 
val permT = mk_permT (TFree (variant tvs "'a", HOLogic.typeS));


1404 
val pi = Free ("pi", permT);


1405 
val tvs' = map (fn s => TFree (s, the (AList.lookup op = sorts' s))) tvs;


1406 
val T = Type (Sign.intern_type thy name, tvs');


1407 
val Const (_, Type (_, [U])) = c


1408 
in apsnd (pair r o hd)


1409 
(PureThy.add_defs_i true [(("prm_" ^ name ^ "_def", Logic.mk_equals


1410 
(Const ("nominal.perm", permT > T > T) $ pi $ Free ("x", T),


1411 
Const (Sign.intern_const thy ("Abs_" ^ name), U > T) $


1412 
(Const ("nominal.perm", permT > U > U) $ pi $


1413 
(Const (Sign.intern_const thy ("Rep_" ^ name), T > U) $


1414 
Free ("x", T))))), [])] thy)


1415 
end))


1416 
(thy5, types_syntax ~~ tyvars ~~


1417 
(List.take (ind_consts, length new_type_names)) ~~ new_type_names);


1418 


1419 
val perm_defs = map snd typedefs;


1420 
val Abs_inverse_thms = map (#Abs_inverse o fst) typedefs;

18016

1421 
val Rep_inverse_thms = map (#Rep_inverse o fst) typedefs;

17870

1422 
val Rep_thms = map (#Rep o fst) typedefs;


1423 

18016

1424 
val big_name = space_implode "_" new_type_names;


1425 


1426 

17870

1427 
(** prove that new types are in class pt_<name> **)


1428 


1429 
val _ = warning "prove that new types are in class pt_<name> ...";


1430 


1431 
fun pt_instance ((class, atom), perm_closed_thms) =


1432 
fold (fn (((({Abs_inverse, Rep_inverse, Rep, ...},


1433 
perm_def), name), tvs), perm_closed) => fn thy =>


1434 
AxClass.add_inst_arity_i


1435 
(Sign.intern_type thy name,


1436 
replicate (length tvs) (classes @ cp_classes), [class])


1437 
(EVERY [AxClass.intro_classes_tac [],


1438 
rewrite_goals_tac [perm_def],


1439 
asm_full_simp_tac (simpset_of thy addsimps [Rep_inverse]) 1,


1440 
asm_full_simp_tac (simpset_of thy addsimps


1441 
[Rep RS perm_closed RS Abs_inverse]) 1,


1442 
asm_full_simp_tac (HOL_basic_ss addsimps [PureThy.get_thm thy


1443 
(Name ("pt_" ^ Sign.base_name atom ^ "3"))]) 1]) thy)


1444 
(typedefs ~~ new_type_names ~~ tyvars ~~ perm_closed_thms);


1445 


1446 


1447 
(** prove that new types are in class cp_<name1>_<name2> **)


1448 


1449 
val _ = warning "prove that new types are in class cp_<name1>_<name2> ...";


1450 


1451 
fun cp_instance (atom1, perm_closed_thms1) (atom2, perm_closed_thms2) thy =

