author  urbanc 
Sun, 23 Sep 2007 22:10:27 +0200  
changeset 24677  c6295d2dce48 
parent 24569  c80e1871098b 
child 24712  64ed05609568 
permissions  rwrr 
19494  1 
(* Title: HOL/Nominal/nominal_atoms.ML 
2 
ID: $Id$ 

3 
Author: Christian Urban and Stefan Berghofer, TU Muenchen 

4 

5 
Declaration of atom types to be used in nominal datatypes. 

6 
*) 

18068  7 

8 
signature NOMINAL_ATOMS = 

9 
sig 

10 
val create_nom_typedecls : string list > theory > theory 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

11 
type atom_info 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

12 
val get_atom_infos : theory > atom_info Symtab.table 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

13 
val get_atom_info : theory > string > atom_info option 
18068  14 
val atoms_of : theory > string list 
15 
val mk_permT : typ > typ 

16 
end 

17 

18 
structure NominalAtoms : NOMINAL_ATOMS = 

19 
struct 

20 

23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

21 
val finite_emptyI = @{thm "finite.emptyI"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

22 
val Collect_const = @{thm "Collect_const"}; 
21669  23 

24569  24 
val inductive_forall_def = @{thm "induct_forall_def"}; 
25 

21669  26 

22846  27 
(* theory data *) 
18068  28 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

29 
type atom_info = 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

30 
{pt_class : string, 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

31 
fs_class : string, 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

32 
cp_classes : (string * string) list}; 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

33 

22846  34 
structure NominalData = TheoryDataFun 
35 
( 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

36 
type T = atom_info Symtab.table; 
18068  37 
val empty = Symtab.empty; 
38 
val copy = I; 

39 
val extend = I; 

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

22846  41 
); 
18068  42 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

43 
fun make_atom_info ((pt_class, fs_class), cp_classes) = 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

44 
{pt_class = pt_class, 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

45 
fs_class = fs_class, 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

46 
cp_classes = cp_classes}; 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

47 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

48 
val get_atom_infos = NominalData.get; 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

49 
val get_atom_info = Symtab.lookup o NominalData.get; 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

50 

18068  51 
fun atoms_of thy = map fst (Symtab.dest (NominalData.get thy)); 
52 

20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

53 
fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T)); 
18068  54 

55 
fun mk_Cons x xs = 

56 
let val T = fastype_of x 

20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

57 
in Const ("List.list.Cons", T > HOLogic.listT T > HOLogic.listT T) $ x $ xs end; 
18068  58 

59 

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

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

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

63 
fun create_nom_typedecls ak_names thy = 

64 
let 

24527
888d56a8d9d3
modified proofs so that they are not using claset()
urbanc
parents:
24218
diff
changeset

65 

24677
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

66 
val (_,thy1) = 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

67 
fold_map (fn ak => fn thy => 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

68 
let val dt = ([],ak,NoSyn,[(ak,[@{typ nat}],NoSyn)]) 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

69 
val ({inject,case_thms,...},thy1) = DatatypePackage.add_datatype_i true false [ak] [dt] thy 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

70 
val inject_flat = Library.flat inject 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

71 
val ak_type = Type (Sign.intern_type thy1 ak,[]) 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

72 
val ak_sign = Sign.intern_const thy1 ak 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

73 

c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

74 
val inj_type = @{typ nat}>ak_type 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

75 
val inj_on_type = inj_type>(@{typ "nat set"})>@{typ bool} 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

76 

c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

77 
(* first statement *) 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

78 
val stmnt1 = HOLogic.mk_Trueprop 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

79 
(Const (@{const_name "inj_on"},inj_on_type) $ 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

80 
Const (ak_sign,inj_type) $ HOLogic.mk_UNIV @{typ nat}) 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

81 

c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

82 
val simp1 = @{thm inj_on_def}::inject_flat 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

83 

c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

84 
val proof1 = fn _ => EVERY [simp_tac (HOL_basic_ss addsimps simp1) 1, 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

85 
rtac @{thm ballI} 1, 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

86 
rtac @{thm ballI} 1, 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

87 
rtac @{thm impI} 1, 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

88 
atac 1] 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

89 

c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

90 
val (inj_thm,thy2) = 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

91 
PureThy.add_thms [((ak^"_inj",Goal.prove_global thy1 [] [] stmnt1 proof1), [])] thy1 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

92 

c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

93 
(* second statement *) 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

94 
val y = Free ("y",ak_type) 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

95 
val stmnt2 = HOLogic.mk_Trueprop 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

96 
(HOLogic.mk_exists ("x",@{typ nat},HOLogic.mk_eq (y,Const (ak_sign,inj_type) $ Bound 0))) 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

97 

c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

98 
val proof2 = fn _ => EVERY [case_tac "y" 1, 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

99 
asm_simp_tac (HOL_basic_ss addsimps simp1) 1, 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

100 
rtac @{thm exI} 1, 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

101 
rtac @{thm refl} 1] 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

102 

c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

103 
(* third statement *) 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

104 
val (inject_thm,thy3) = 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

105 
PureThy.add_thms [((ak^"_injection",Goal.prove_global thy2 [] [] stmnt2 proof2), [])] thy2 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

106 

c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

107 
val stmnt3 = HOLogic.mk_Trueprop 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

108 
(HOLogic.mk_not 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

109 
(Const ("Finite_Set.finite", HOLogic.mk_setT ak_type > HOLogic.boolT) $ 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

110 
HOLogic.mk_UNIV ak_type)) 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

111 

c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

112 
val simp2 = [@{thm image_def},@{thm bex_UNIV}]@inject_thm 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

113 
val simp3 = [@{thm UNIV_def}] 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

114 

c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

115 
val proof3 = fn _ => EVERY [cut_facts_tac inj_thm 1, 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

116 
dtac @{thm range_inj_infinite} 1, 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

117 
asm_full_simp_tac (HOL_basic_ss addsimps simp2) 1, 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

118 
simp_tac (HOL_basic_ss addsimps simp3) 1] 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

119 

c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

120 
val (inf_thm,thy4) = 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

121 
PureThy.add_thms [((ak^"_infinite",Goal.prove_global thy1 [] [] stmnt3 proof3), [])] thy3 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

122 
in 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

123 
((inj_thm,inject_thm,inf_thm),thy4) 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

124 
end) ak_names thy 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

125 

18068  126 
(* produces a list consisting of pairs: *) 
127 
(* fst component is the atomkind name *) 

128 
(* snd component is its type *) 

21289
920b7b893d9c
deleted all uses of sign_of as it's now the identity function
urbanc
parents:
20377
diff
changeset

129 
val full_ak_names = map (Sign.intern_type thy1) ak_names; 
18068  130 
val ak_names_types = ak_names ~~ map (Type o rpair []) full_ak_names; 
131 

132 
(* adds for every atomkind an axiom *) 

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

18381
246807ef6dfb
changed the types in accordance with Florian's changes
urbanc
parents:
18366
diff
changeset

134 
val (inf_axs,thy2) = PureThy.add_axioms_i (map (fn (ak_name, T) => 
18068  135 
let 
20179  136 
val name = ak_name ^ "_infinite" 
18068  137 
val axiom = HOLogic.mk_Trueprop (HOLogic.mk_not 
22274  138 
(Const ("Finite_Set.finite", HOLogic.mk_setT T > HOLogic.boolT) $ 
139 
HOLogic.mk_UNIV T)) 

18068  140 
in 
20179  141 
((name, axiom), []) 
18068  142 
end) ak_names_types) thy1; 
143 

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

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

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

147 
(* overloades then the general swapfunction *) 

20179  148 
val (swap_eqs, thy3) = fold_map (fn (ak_name, T) => fn thy => 
18068  149 
let 
150 
val swapT = HOLogic.mk_prodT (T, T) > T > T; 

21289
920b7b893d9c
deleted all uses of sign_of as it's now the identity function
urbanc
parents:
20377
diff
changeset

151 
val swap_name = Sign.full_name thy ("swap_" ^ ak_name); 
18068  152 
val a = Free ("a", T); 
153 
val b = Free ("b", T); 

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

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

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

157 
val cswap_akname = Const (swap_name, swapT); 

19494  158 
val cswap = Const ("Nominal.swap", swapT) 
18068  159 

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

161 
val def1 = HOLogic.mk_Trueprop (HOLogic.mk_eq 

20179  162 
(cswap_akname $ HOLogic.mk_prod (a,b) $ c, 
18068  163 
cif $ HOLogic.mk_eq (a,c) $ b $ (cif $ HOLogic.mk_eq (b,c) $ a $ c))) 
164 
val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c) 

165 
in 

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

20179  167 
> PureThy.add_defs_unchecked_i true [((name, def2),[])] 
168 
> snd 

169 
> PrimrecPackage.add_primrec_unchecked_i "" [(("", def1),[])] 

170 
end) ak_names_types thy2; 

18068  171 

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

173 
(* on such atoms *) 

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

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

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

20179  177 
val (prm_eqs, thy4) = fold_map (fn (ak_name, T) => fn thy => 
18068  178 
let 
179 
val swapT = HOLogic.mk_prodT (T, T) > T > T; 

21289
920b7b893d9c
deleted all uses of sign_of as it's now the identity function
urbanc
parents:
20377
diff
changeset

180 
val swap_name = Sign.full_name thy ("swap_" ^ ak_name) 
18068  181 
val prmT = mk_permT T > T > T; 
182 
val prm_name = ak_name ^ "_prm_" ^ ak_name; 

21289
920b7b893d9c
deleted all uses of sign_of as it's now the identity function
urbanc
parents:
20377
diff
changeset

183 
val qu_prm_name = Sign.full_name thy prm_name; 
18068  184 
val x = Free ("x", HOLogic.mk_prodT (T, T)); 
185 
val xs = Free ("xs", mk_permT T); 

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

187 

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

189 

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

191 

192 
val def2 = HOLogic.mk_Trueprop (HOLogic.mk_eq 

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

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

195 
in 

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

19635  197 
> PrimrecPackage.add_primrec_unchecked_i "" [(("", def1), []),(("", def2), [])] 
20179  198 
end) ak_names_types thy3; 
18068  199 

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

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

202 
(* nontrivial case: *) 

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

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

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

206 
(* *) 

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

208 
(* have their own rules proved below *) 

18366  209 
val (perm_defs, thy5) = fold_map (fn (ak_name, T) => fn thy => 
210 
fold_map (fn (ak_name', T') => fn thy' => 

18068  211 
let 
212 
val perm_def_name = ak_name ^ "_prm_" ^ ak_name'; 

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

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

19494  215 
val cperm = Const ("Nominal.perm", mk_permT T > T' > T'); 
21289
920b7b893d9c
deleted all uses of sign_of as it's now the identity function
urbanc
parents:
20377
diff
changeset

216 
val cperm_def = Const (Sign.full_name thy' perm_def_name, mk_permT T > T' > T'); 
18068  217 

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

219 
val def = Logic.mk_equals 

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

221 
in 

19635  222 
PureThy.add_defs_unchecked_i true [((name, def),[])] thy' 
18366  223 
end) ak_names_types thy) ak_names_types thy4; 
18068  224 

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

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

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

18381
246807ef6dfb
changed the types in accordance with Florian's changes
urbanc
parents:
18366
diff
changeset

228 
val (prm_cons_thms,thy6) = 
18068  229 
thy5 > PureThy.add_thms (map (fn (ak_name, T) => 
230 
let 

21289
920b7b893d9c
deleted all uses of sign_of as it's now the identity function
urbanc
parents:
20377
diff
changeset

231 
val ak_name_qu = Sign.full_name thy5 (ak_name); 
18068  232 
val i_type = Type(ak_name_qu,[]); 
19494  233 
val cat = Const ("Nominal.at",(Term.itselfT i_type) > HOLogic.boolT); 
18068  234 
val at_type = Logic.mk_type i_type; 
24527
888d56a8d9d3
modified proofs so that they are not using claset()
urbanc
parents:
24218
diff
changeset

235 
val simp_s = HOL_ss addsimps PureThy.get_thmss thy5 
18068  236 
[Name "at_def", 
237 
Name (ak_name ^ "_prm_" ^ ak_name ^ "_def"), 

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

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

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

241 
Name (ak_name ^ "_infinite")] 

242 

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

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

245 

24527
888d56a8d9d3
modified proofs so that they are not using claset()
urbanc
parents:
24218
diff
changeset

246 
val proof = fn _ => simp_tac simp_s 1 
18068  247 

248 
in 

20046  249 
((name, Goal.prove_global thy5 [] [] statement proof), []) 
18068  250 
end) ak_names_types); 
251 

252 
(* declares a permaxclass for every atomkind *) 

253 
(* axclass pt_<ak> *) 

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

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

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

18438
b8d867177916
made the changes according to Florian's rearranging of
urbanc
parents:
18437
diff
changeset

257 
val (pt_ax_classes,thy7) = fold_map (fn (ak_name, T) => fn thy => 
18068  258 
let 
259 
val cl_name = "pt_"^ak_name; 

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

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

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

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

19494  264 
val cperm = Const ("Nominal.perm", mk_permT T > ty > ty); 
18068  265 
val cnil = Const ("List.list.Nil", mk_permT T); 
23029  266 
val cappend = Const ("List.append",mk_permT T > mk_permT T > mk_permT T); 
19494  267 
val cprm_eq = Const ("Nominal.prm_eq",mk_permT T > mk_permT T > HOLogic.boolT); 
18068  268 
(* nil axiom *) 
269 
val axiom1 = HOLogic.mk_Trueprop (HOLogic.mk_eq 

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

271 
(* append axiom *) 

272 
val axiom2 = HOLogic.mk_Trueprop (HOLogic.mk_eq 

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

274 
(* permeq axiom *) 

275 
val axiom3 = Logic.mk_implies 

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

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

278 
in 

22745  279 
AxClass.define_class (cl_name, ["HOL.type"]) [] 
19488  280 
[((cl_name ^ "1", [Simplifier.simp_add]), [axiom1]), 
281 
((cl_name ^ "2", []), [axiom2]), 

282 
((cl_name ^ "3", []), [axiom3])] thy 

18438
b8d867177916
made the changes according to Florian's rearranging of
urbanc
parents:
18437
diff
changeset

283 
end) ak_names_types thy6; 
18068  284 

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

286 
(* instance of pt *) 

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

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

18381
246807ef6dfb
changed the types in accordance with Florian's changes
urbanc
parents:
18366
diff
changeset

289 
val (prm_inst_thms,thy8) = 
18068  290 
thy7 > PureThy.add_thms (map (fn (ak_name, T) => 
291 
let 

21289
920b7b893d9c
deleted all uses of sign_of as it's now the identity function
urbanc
parents:
20377
diff
changeset

292 
val ak_name_qu = Sign.full_name thy7 ak_name; 
920b7b893d9c
deleted all uses of sign_of as it's now the identity function
urbanc
parents:
20377
diff
changeset

293 
val pt_name_qu = Sign.full_name thy7 ("pt_"^ak_name); 
18068  294 
val i_type1 = TFree("'x",[pt_name_qu]); 
295 
val i_type2 = Type(ak_name_qu,[]); 

19494  296 
val cpt = Const ("Nominal.pt",(Term.itselfT i_type1)>(Term.itselfT i_type2)>HOLogic.boolT); 
18068  297 
val pt_type = Logic.mk_type i_type1; 
298 
val at_type = Logic.mk_type i_type2; 

24527
888d56a8d9d3
modified proofs so that they are not using claset()
urbanc
parents:
24218
diff
changeset

299 
val simp_s = HOL_ss addsimps PureThy.get_thmss thy7 
18068  300 
[Name "pt_def", 
301 
Name ("pt_" ^ ak_name ^ "1"), 

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

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

304 

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

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

307 

24527
888d56a8d9d3
modified proofs so that they are not using claset()
urbanc
parents:
24218
diff
changeset

308 
val proof = fn _ => simp_tac simp_s 1; 
18068  309 
in 
20046  310 
((name, Goal.prove_global thy7 [] [] statement proof), []) 
18068  311 
end) ak_names_types); 
312 

313 
(* declares an fsaxclass for every atomkind *) 

314 
(* axclass fs_<ak> *) 

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

18438
b8d867177916
made the changes according to Florian's rearranging of
urbanc
parents:
18437
diff
changeset

316 
val (fs_ax_classes,thy11) = fold_map (fn (ak_name, T) => fn thy => 
18068  317 
let 
318 
val cl_name = "fs_"^ak_name; 

21289
920b7b893d9c
deleted all uses of sign_of as it's now the identity function
urbanc
parents:
20377
diff
changeset

319 
val pt_name = Sign.full_name thy ("pt_"^ak_name); 
18068  320 
val ty = TFree("'a",["HOL.type"]); 
321 
val x = Free ("x", ty); 

19494  322 
val csupp = Const ("Nominal.supp", ty > HOLogic.mk_setT T); 
22274  323 
val cfinite = Const ("Finite_Set.finite", HOLogic.mk_setT T > HOLogic.boolT) 
18068  324 

22274  325 
val axiom1 = HOLogic.mk_Trueprop (cfinite $ (csupp $ x)); 
18068  326 

327 
in 

22745  328 
AxClass.define_class (cl_name, [pt_name]) [] [((cl_name ^ "1", []), [axiom1])] thy 
18438
b8d867177916
made the changes according to Florian's rearranging of
urbanc
parents:
18437
diff
changeset

329 
end) ak_names_types thy8; 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

330 

18068  331 
(* proves that every fs_<ak>type together with <ak>type *) 
332 
(* instance of fstype *) 

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

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

18381
246807ef6dfb
changed the types in accordance with Florian's changes
urbanc
parents:
18366
diff
changeset

335 
val (fs_inst_thms,thy12) = 
18068  336 
thy11 > PureThy.add_thms (map (fn (ak_name, T) => 
337 
let 

21289
920b7b893d9c
deleted all uses of sign_of as it's now the identity function
urbanc
parents:
20377
diff
changeset

338 
val ak_name_qu = Sign.full_name thy11 ak_name; 
920b7b893d9c
deleted all uses of sign_of as it's now the identity function
urbanc
parents:
20377
diff
changeset

339 
val fs_name_qu = Sign.full_name thy11 ("fs_"^ak_name); 
18068  340 
val i_type1 = TFree("'x",[fs_name_qu]); 
341 
val i_type2 = Type(ak_name_qu,[]); 

19494  342 
val cfs = Const ("Nominal.fs", 
18068  343 
(Term.itselfT i_type1)>(Term.itselfT i_type2)>HOLogic.boolT); 
344 
val fs_type = Logic.mk_type i_type1; 

345 
val at_type = Logic.mk_type i_type2; 

24527
888d56a8d9d3
modified proofs so that they are not using claset()
urbanc
parents:
24218
diff
changeset

346 
val simp_s = HOL_ss addsimps PureThy.get_thmss thy11 
18068  347 
[Name "fs_def", 
348 
Name ("fs_" ^ ak_name ^ "1")]; 

349 

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

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

352 

24527
888d56a8d9d3
modified proofs so that they are not using claset()
urbanc
parents:
24218
diff
changeset

353 
val proof = fn _ => simp_tac simp_s 1; 
18068  354 
in 
20046  355 
((name, Goal.prove_global thy11 [] [] statement proof), []) 
18068  356 
end) ak_names_types); 
357 

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

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

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

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

361 
val (cp_ax_classes,thy12b) = fold_map (fn (ak_name, T) => fn thy => 
18438
b8d867177916
made the changes according to Florian's rearranging of
urbanc
parents:
18437
diff
changeset

362 
fold_map (fn (ak_name', T') => fn thy' => 
18068  363 
let 
364 
val cl_name = "cp_"^ak_name^"_"^ak_name'; 

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

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

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

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

19494  369 
val cperm1 = Const ("Nominal.perm", mk_permT T > ty > ty); 
370 
val cperm2 = Const ("Nominal.perm", mk_permT T' > ty > ty); 

371 
val cperm3 = Const ("Nominal.perm", mk_permT T > mk_permT T' > mk_permT T'); 

18068  372 

373 
val ax1 = HOLogic.mk_Trueprop 

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

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

376 
in 

22745  377 
AxClass.define_class (cl_name, ["HOL.type"]) [] [((cl_name ^ "1", []), [ax1])] thy' 
18438
b8d867177916
made the changes according to Florian's rearranging of
urbanc
parents:
18437
diff
changeset

378 
end) ak_names_types thy) ak_names_types thy12; 
18068  379 

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

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

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

18381
246807ef6dfb
changed the types in accordance with Florian's changes
urbanc
parents:
18366
diff
changeset

383 
val (cp_thms,thy12c) = fold_map (fn (ak_name, T) => fn thy => 
246807ef6dfb
changed the types in accordance with Florian's changes
urbanc
parents:
18366
diff
changeset

384 
fold_map (fn (ak_name', T') => fn thy' => 
18068  385 
let 
21289
920b7b893d9c
deleted all uses of sign_of as it's now the identity function
urbanc
parents:
20377
diff
changeset

386 
val ak_name_qu = Sign.full_name thy' (ak_name); 
920b7b893d9c
deleted all uses of sign_of as it's now the identity function
urbanc
parents:
20377
diff
changeset

387 
val ak_name_qu' = Sign.full_name thy' (ak_name'); 
920b7b893d9c
deleted all uses of sign_of as it's now the identity function
urbanc
parents:
20377
diff
changeset

388 
val cp_name_qu = Sign.full_name thy' ("cp_"^ak_name^"_"^ak_name'); 
18068  389 
val i_type0 = TFree("'a",[cp_name_qu]); 
390 
val i_type1 = Type(ak_name_qu,[]); 

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

19494  392 
val ccp = Const ("Nominal.cp", 
18068  393 
(Term.itselfT i_type0)>(Term.itselfT i_type1)> 
394 
(Term.itselfT i_type2)>HOLogic.boolT); 

395 
val at_type = Logic.mk_type i_type1; 

396 
val at_type' = Logic.mk_type i_type2; 

397 
val cp_type = Logic.mk_type i_type0; 

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

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

400 

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

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

403 

24527
888d56a8d9d3
modified proofs so that they are not using claset()
urbanc
parents:
24218
diff
changeset

404 
val proof = fn _ => EVERY [simp_tac simp_s 1, 
888d56a8d9d3
modified proofs so that they are not using claset()
urbanc
parents:
24218
diff
changeset

405 
rtac allI 1, rtac allI 1, rtac allI 1, 
888d56a8d9d3
modified proofs so that they are not using claset()
urbanc
parents:
24218
diff
changeset

406 
rtac cp1 1]; 
18068  407 
in 
20046  408 
PureThy.add_thms [((name, Goal.prove_global thy' [] [] statement proof), [])] thy' 
18068  409 
end) 
18381
246807ef6dfb
changed the types in accordance with Florian's changes
urbanc
parents:
18366
diff
changeset

410 
ak_names_types thy) ak_names_types thy12b; 
18068  411 

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

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

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

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

18381
246807ef6dfb
changed the types in accordance with Florian's changes
urbanc
parents:
18366
diff
changeset

416 
val (dj_thms, thy12d) = fold_map (fn (ak_name,T) => fn thy => 
246807ef6dfb
changed the types in accordance with Florian's changes
urbanc
parents:
18366
diff
changeset

417 
fold_map (fn (ak_name',T') => fn thy' => 
18068  418 
(if not (ak_name = ak_name') 
419 
then 

420 
let 

21289
920b7b893d9c
deleted all uses of sign_of as it's now the identity function
urbanc
parents:
20377
diff
changeset

421 
val ak_name_qu = Sign.full_name thy' ak_name; 
920b7b893d9c
deleted all uses of sign_of as it's now the identity function
urbanc
parents:
20377
diff
changeset

422 
val ak_name_qu' = Sign.full_name thy' ak_name'; 
18068  423 
val i_type1 = Type(ak_name_qu,[]); 
424 
val i_type2 = Type(ak_name_qu',[]); 

19494  425 
val cdj = Const ("Nominal.disjoint", 
18068  426 
(Term.itselfT i_type1)>(Term.itselfT i_type2)>HOLogic.boolT); 
427 
val at_type = Logic.mk_type i_type1; 

428 
val at_type' = Logic.mk_type i_type2; 

24527
888d56a8d9d3
modified proofs so that they are not using claset()
urbanc
parents:
24218
diff
changeset

429 
val simp_s = HOL_ss addsimps PureThy.get_thmss thy' 
18068  430 
[Name "disjoint_def", 
431 
Name (ak_name^"_prm_"^ak_name'^"_def"), 

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

433 

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

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

436 

24527
888d56a8d9d3
modified proofs so that they are not using claset()
urbanc
parents:
24218
diff
changeset

437 
val proof = fn _ => simp_tac simp_s 1; 
18068  438 
in 
20046  439 
PureThy.add_thms [((name, Goal.prove_global thy' [] [] statement proof), [])] thy' 
18068  440 
end 
441 
else 

18381
246807ef6dfb
changed the types in accordance with Florian's changes
urbanc
parents:
18366
diff
changeset

442 
([],thy'))) (* do nothing branch, if ak_name = ak_name' *) 
246807ef6dfb
changed the types in accordance with Florian's changes
urbanc
parents:
18366
diff
changeset

443 
ak_names_types thy) ak_names_types thy12c; 
18068  444 

20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

445 
(******** pt_<ak> class instances ********) 
18068  446 
(*=========================================*) 
18279
f7a18e2b10fc
made some of the theorem lookups static (by using
urbanc
parents:
18262
diff
changeset

447 
(* some abbreviations for theorems *) 
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

448 
val pt1 = @{thm "pt1"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

449 
val pt2 = @{thm "pt2"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

450 
val pt3 = @{thm "pt3"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

451 
val at_pt_inst = @{thm "at_pt_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

452 
val pt_set_inst = @{thm "pt_set_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

453 
val pt_unit_inst = @{thm "pt_unit_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

454 
val pt_prod_inst = @{thm "pt_prod_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

455 
val pt_nprod_inst = @{thm "pt_nprod_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

456 
val pt_list_inst = @{thm "pt_list_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

457 
val pt_optn_inst = @{thm "pt_option_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

458 
val pt_noptn_inst = @{thm "pt_noption_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

459 
val pt_fun_inst = @{thm "pt_fun_inst"}; 
18068  460 

18435  461 
(* for all atomkind combinations <ak>/<ak'> show that *) 
462 
(* every <ak> is an instance of pt_<ak'>; the proof for *) 

463 
(* ak!=ak' is by definition; the case ak=ak' uses at_pt_inst. *) 

18431  464 
val thy13 = fold (fn ak_name => fn thy => 
465 
fold (fn ak_name' => fn thy' => 

466 
let 

21289
920b7b893d9c
deleted all uses of sign_of as it's now the identity function
urbanc
parents:
20377
diff
changeset

467 
val qu_name = Sign.full_name thy' ak_name'; 
920b7b893d9c
deleted all uses of sign_of as it's now the identity function
urbanc
parents:
20377
diff
changeset

468 
val cls_name = Sign.full_name thy' ("pt_"^ak_name); 
18431  469 
val at_inst = PureThy.get_thm thy' (Name ("at_"^ak_name'^"_inst")); 
470 

24218  471 
val proof1 = EVERY [Class.intro_classes_tac [], 
18068  472 
rtac ((at_inst RS at_pt_inst) RS pt1) 1, 
473 
rtac ((at_inst RS at_pt_inst) RS pt2) 1, 

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

475 
atac 1]; 

18431  476 
val simp_s = HOL_basic_ss addsimps 
477 
PureThy.get_thmss thy' [Name (ak_name^"_prm_"^ak_name'^"_def")]; 

24218  478 
val proof2 = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)]; 
18431  479 

480 
in 

481 
thy' 

19275  482 
> AxClass.prove_arity (qu_name,[],[cls_name]) 
18431  483 
(if ak_name = ak_name' then proof1 else proof2) 
484 
end) ak_names thy) ak_names thy12c; 

18068  485 

18430  486 
(* show that *) 
487 
(* fun(pt_<ak>,pt_<ak>) *) 

18579
002d371401f5
changed the name of the type "nOption" to "noption".
urbanc
parents:
18438
diff
changeset

488 
(* noption(pt_<ak>) *) 
18430  489 
(* option(pt_<ak>) *) 
490 
(* list(pt_<ak>) *) 

491 
(* *(pt_<ak>,pt_<ak>) *) 

18600  492 
(* nprod(pt_<ak>,pt_<ak>) *) 
18430  493 
(* unit *) 
494 
(* set(pt_<ak>) *) 

495 
(* are instances of pt_<ak> *) 

18431  496 
val thy18 = fold (fn ak_name => fn thy => 
18068  497 
let 
21289
920b7b893d9c
deleted all uses of sign_of as it's now the identity function
urbanc
parents:
20377
diff
changeset

498 
val cls_name = Sign.full_name thy ("pt_"^ak_name); 
18068  499 
val at_thm = PureThy.get_thm thy (Name ("at_"^ak_name^"_inst")); 
500 
val pt_inst = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst")); 

20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

501 

18430  502 
fun pt_proof thm = 
24218  503 
EVERY [Class.intro_classes_tac [], 
18430  504 
rtac (thm RS pt1) 1, rtac (thm RS pt2) 1, rtac (thm RS pt3) 1, atac 1]; 
505 

506 
val pt_thm_fun = at_thm RS (pt_inst RS (pt_inst RS pt_fun_inst)); 

507 
val pt_thm_noptn = pt_inst RS pt_noptn_inst; 

508 
val pt_thm_optn = pt_inst RS pt_optn_inst; 

509 
val pt_thm_list = pt_inst RS pt_list_inst; 

510 
val pt_thm_prod = pt_inst RS (pt_inst RS pt_prod_inst); 

18600  511 
val pt_thm_nprod = pt_inst RS (pt_inst RS pt_nprod_inst); 
18430  512 
val pt_thm_unit = pt_unit_inst; 
513 
val pt_thm_set = pt_inst RS pt_set_inst 

20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

514 
in 
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

515 
thy 
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

516 
> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun) 
19494  517 
> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
24194  518 
> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn) 
19275  519 
> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list) 
520 
> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod) 

19494  521 
> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
18600  522 
(pt_proof pt_thm_nprod) 
19275  523 
> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit) 
524 
> AxClass.prove_arity ("set",[[cls_name]],[cls_name]) (pt_proof pt_thm_set) 

18430  525 
end) ak_names thy13; 
18068  526 

20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

527 
(******** fs_<ak> class instances ********) 
18068  528 
(*=========================================*) 
18279
f7a18e2b10fc
made some of the theorem lookups static (by using
urbanc
parents:
18262
diff
changeset

529 
(* abbreviations for some lemmas *) 
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

530 
val fs1 = @{thm "fs1"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

531 
val fs_at_inst = @{thm "fs_at_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

532 
val fs_unit_inst = @{thm "fs_unit_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

533 
val fs_prod_inst = @{thm "fs_prod_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

534 
val fs_nprod_inst = @{thm "fs_nprod_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

535 
val fs_list_inst = @{thm "fs_list_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

536 
val fs_option_inst = @{thm "fs_option_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

537 
val dj_supp = @{thm "dj_supp"}; 
18068  538 

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

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

18431  541 
val thy20 = fold (fn ak_name => fn thy => 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

542 
fold (fn ak_name' => fn thy' => 
18437
ee0283e5dfe3
added proofs to show that every atomkind combination
urbanc
parents:
18436
diff
changeset

543 
let 
21289
920b7b893d9c
deleted all uses of sign_of as it's now the identity function
urbanc
parents:
20377
diff
changeset

544 
val qu_name = Sign.full_name thy' ak_name'; 
920b7b893d9c
deleted all uses of sign_of as it's now the identity function
urbanc
parents:
20377
diff
changeset

545 
val qu_class = Sign.full_name thy' ("fs_"^ak_name); 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

546 
val proof = 
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

547 
(if ak_name = ak_name' 
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

548 
then 
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

549 
let val at_thm = PureThy.get_thm thy' (Name ("at_"^ak_name^"_inst")); 
24218  550 
in EVERY [Class.intro_classes_tac [], 
18437
ee0283e5dfe3
added proofs to show that every atomkind combination
urbanc
parents:
18436
diff
changeset

551 
rtac ((at_thm RS fs_at_inst) RS fs1) 1] end 
ee0283e5dfe3
added proofs to show that every atomkind combination
urbanc
parents:
18436
diff
changeset

552 
else 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

553 
let val dj_inst = PureThy.get_thm thy' (Name ("dj_"^ak_name'^"_"^ak_name)); 
22274  554 
val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, finite_emptyI]; 
24218  555 
in EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1] end) 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

556 
in 
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

557 
AxClass.prove_arity (qu_name,[],[qu_class]) proof thy' 
18437
ee0283e5dfe3
added proofs to show that every atomkind combination
urbanc
parents:
18436
diff
changeset

558 
end) ak_names thy) ak_names thy18; 
18068  559 

18431  560 
(* shows that *) 
561 
(* unit *) 

562 
(* *(fs_<ak>,fs_<ak>) *) 

18600  563 
(* nprod(fs_<ak>,fs_<ak>) *) 
18431  564 
(* list(fs_<ak>) *) 
565 
(* option(fs_<ak>) *) 

566 
(* are instances of fs_<ak> *) 

18068  567 

18431  568 
val thy24 = fold (fn ak_name => fn thy => 
569 
let 

21289
920b7b893d9c
deleted all uses of sign_of as it's now the identity function
urbanc
parents:
20377
diff
changeset

570 
val cls_name = Sign.full_name thy ("fs_"^ak_name); 
18068  571 
val fs_inst = PureThy.get_thm thy (Name ("fs_"^ak_name^"_inst")); 
24218  572 
fun fs_proof thm = EVERY [Class.intro_classes_tac [], rtac (thm RS fs1) 1]; 
18068  573 

18600  574 
val fs_thm_unit = fs_unit_inst; 
575 
val fs_thm_prod = fs_inst RS (fs_inst RS fs_prod_inst); 

576 
val fs_thm_nprod = fs_inst RS (fs_inst RS fs_nprod_inst); 

577 
val fs_thm_list = fs_inst RS fs_list_inst; 

578 
val fs_thm_optn = fs_inst RS fs_option_inst; 

18431  579 
in 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

580 
thy 
19275  581 
> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit) 
582 
> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) 

19494  583 
> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
18600  584 
(fs_proof fs_thm_nprod) 
19275  585 
> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list) 
24194  586 
> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn) 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

587 
end) ak_names thy20; 
18431  588 

20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

589 
(******** cp_<ak>_<ai> class instances ********) 
18068  590 
(*==============================================*) 
18279
f7a18e2b10fc
made some of the theorem lookups static (by using
urbanc
parents:
18262
diff
changeset

591 
(* abbreviations for some lemmas *) 
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

592 
val cp1 = @{thm "cp1"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

593 
val cp_unit_inst = @{thm "cp_unit_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

594 
val cp_bool_inst = @{thm "cp_bool_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

595 
val cp_prod_inst = @{thm "cp_prod_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

596 
val cp_list_inst = @{thm "cp_list_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

597 
val cp_fun_inst = @{thm "cp_fun_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

598 
val cp_option_inst = @{thm "cp_option_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

599 
val cp_noption_inst = @{thm "cp_noption_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

600 
val cp_set_inst = @{thm "cp_set_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

601 
val pt_perm_compose = @{thm "pt_perm_compose"}; 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

602 

23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

603 
val dj_pp_forget = @{thm "dj_perm_perm_forget"}; 
18068  604 

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

18432  606 
(* for every <ak>/<ai>combination *) 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

607 
val thy25 = fold (fn ak_name => fn thy => 
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

608 
fold (fn ak_name' => fn thy' => 
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

609 
fold (fn ak_name'' => fn thy'' => 
18068  610 
let 
21289
920b7b893d9c
deleted all uses of sign_of as it's now the identity function
urbanc
parents:
20377
diff
changeset

611 
val name = Sign.full_name thy'' ak_name; 
920b7b893d9c
deleted all uses of sign_of as it's now the identity function
urbanc
parents:
20377
diff
changeset

612 
val cls_name = Sign.full_name thy'' ("cp_"^ak_name'^"_"^ak_name''); 
18068  613 
val proof = 
614 
(if (ak_name'=ak_name'') then 

20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

615 
(let 
18068  616 
val pt_inst = PureThy.get_thm thy'' (Name ("pt_"^ak_name''^"_inst")); 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

617 
val at_inst = PureThy.get_thm thy'' (Name ("at_"^ak_name''^"_inst")); 
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

618 
in 
24218  619 
EVERY [Class.intro_classes_tac [], 
18068  620 
rtac (at_inst RS (pt_inst RS pt_perm_compose)) 1] 
621 
end) 

622 
else 

20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

623 
(let 
18068  624 
val dj_inst = PureThy.get_thm thy'' (Name ("dj_"^ak_name''^"_"^ak_name')); 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

625 
val simp_s = HOL_basic_ss addsimps 
18068  626 
((dj_inst RS dj_pp_forget):: 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

627 
(PureThy.get_thmss thy'' 
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

628 
[Name (ak_name' ^"_prm_"^ak_name^"_def"), 
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

629 
Name (ak_name''^"_prm_"^ak_name^"_def")])); 
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

630 
in 
24218  631 
EVERY [Class.intro_classes_tac [], simp_tac simp_s 1] 
18068  632 
end)) 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

633 
in 
19275  634 
AxClass.prove_arity (name,[],[cls_name]) proof thy'' 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

635 
end) ak_names thy') ak_names thy) ak_names thy24; 
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

636 

18432  637 
(* shows that *) 
638 
(* units *) 

639 
(* products *) 

640 
(* lists *) 

641 
(* functions *) 

642 
(* options *) 

643 
(* noptions *) 

22536
35debf264656
made the type sets instance of the "cp" typeclass
urbanc
parents:
22535
diff
changeset

644 
(* sets *) 
18432  645 
(* are instances of cp_<ak>_<ai> for every <ak>/<ai>combination *) 
646 
val thy26 = fold (fn ak_name => fn thy => 

647 
fold (fn ak_name' => fn thy' => 

648 
let 

21289
920b7b893d9c
deleted all uses of sign_of as it's now the identity function
urbanc
parents:
20377
diff
changeset

649 
val cls_name = Sign.full_name thy' ("cp_"^ak_name^"_"^ak_name'); 
18068  650 
val cp_inst = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"_inst")); 
651 
val pt_inst = PureThy.get_thm thy' (Name ("pt_"^ak_name^"_inst")); 

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

18432  653 

24218  654 
fun cp_proof thm = EVERY [Class.intro_classes_tac [],rtac (thm RS cp1) 1]; 
18432  655 

656 
val cp_thm_unit = cp_unit_inst; 

657 
val cp_thm_prod = cp_inst RS (cp_inst RS cp_prod_inst); 

658 
val cp_thm_list = cp_inst RS cp_list_inst; 

659 
val cp_thm_fun = at_inst RS (pt_inst RS (cp_inst RS (cp_inst RS cp_fun_inst))); 

660 
val cp_thm_optn = cp_inst RS cp_option_inst; 

661 
val cp_thm_noptn = cp_inst RS cp_noption_inst; 

22536
35debf264656
made the type sets instance of the "cp" typeclass
urbanc
parents:
22535
diff
changeset

662 
val cp_thm_set = cp_inst RS cp_set_inst; 
18432  663 
in 
664 
thy' 

19275  665 
> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit) 
666 
> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod) 

667 
> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list) 

668 
> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun) 

24194  669 
> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn) 
19494  670 
> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn) 
22536
35debf264656
made the type sets instance of the "cp" typeclass
urbanc
parents:
22535
diff
changeset

671 
> AxClass.prove_arity ("set",[[cls_name]],[cls_name]) (cp_proof cp_thm_set) 
18432  672 
end) ak_names thy) ak_names thy25; 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

673 

be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

674 
(* show that discrete nominal types are permutation types, finitely *) 
18432  675 
(* supported and have the commutation property *) 
676 
(* discrete types have a permutation operation defined as pi o x = x; *) 

20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

677 
(* which renders the proofs to be simple "simp_all"proofs. *) 
18432  678 
val thy32 = 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

679 
let 
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

680 
fun discrete_pt_inst discrete_ty defn = 
18432  681 
fold (fn ak_name => fn thy => 
682 
let 

21289
920b7b893d9c
deleted all uses of sign_of as it's now the identity function
urbanc
parents:
20377
diff
changeset

683 
val qu_class = Sign.full_name thy ("pt_"^ak_name); 
18432  684 
val simp_s = HOL_basic_ss addsimps [defn]; 
24218  685 
val proof = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)]; 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

686 
in 
19275  687 
AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy 
18432  688 
end) ak_names; 
18068  689 

18432  690 
fun discrete_fs_inst discrete_ty defn = 
691 
fold (fn ak_name => fn thy => 

692 
let 

21289
920b7b893d9c
deleted all uses of sign_of as it's now the identity function
urbanc
parents:
20377
diff
changeset

693 
val qu_class = Sign.full_name thy ("fs_"^ak_name); 
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

694 
val supp_def = @{thm "Nominal.supp_def"}; 
22274  695 
val simp_s = HOL_ss addsimps [supp_def,Collect_const,finite_emptyI,defn]; 
24218  696 
val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1]; 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

697 
in 
19275  698 
AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

699 
end) ak_names; 
18068  700 

18432  701 
fun discrete_cp_inst discrete_ty defn = 
702 
fold (fn ak_name' => (fold (fn ak_name => fn thy => 

703 
let 

21289
920b7b893d9c
deleted all uses of sign_of as it's now the identity function
urbanc
parents:
20377
diff
changeset

704 
val qu_class = Sign.full_name thy ("cp_"^ak_name^"_"^ak_name'); 
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

705 
val supp_def = @{thm "Nominal.supp_def"}; 
18432  706 
val simp_s = HOL_ss addsimps [defn]; 
24218  707 
val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1]; 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

708 
in 
19275  709 
AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

710 
end) ak_names)) ak_names; 
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

711 

18432  712 
in 
713 
thy26 

23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

714 
> discrete_pt_inst "nat" @{thm "perm_nat_def"} 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

715 
> discrete_fs_inst "nat" @{thm "perm_nat_def"} 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

716 
> discrete_cp_inst "nat" @{thm "perm_nat_def"} 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

717 
> discrete_pt_inst "bool" @{thm "perm_bool"} 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

718 
> discrete_fs_inst "bool" @{thm "perm_bool"} 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

719 
> discrete_cp_inst "bool" @{thm "perm_bool"} 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

720 
> discrete_pt_inst "IntDef.int" @{thm "perm_int_def"} 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

721 
> discrete_fs_inst "IntDef.int" @{thm "perm_int_def"} 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

722 
> discrete_cp_inst "IntDef.int" @{thm "perm_int_def"} 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

723 
> discrete_pt_inst "List.char" @{thm "perm_char_def"} 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

724 
> discrete_fs_inst "List.char" @{thm "perm_char_def"} 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

725 
> discrete_cp_inst "List.char" @{thm "perm_char_def"} 
18432  726 
end; 
727 

20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

728 

18262  729 
(* abbreviations for some lemmas *) 
730 
(*===============================*) 

23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

731 
val abs_fun_pi = @{thm "Nominal.abs_fun_pi"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

732 
val abs_fun_pi_ineq = @{thm "Nominal.abs_fun_pi_ineq"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

733 
val abs_fun_eq = @{thm "Nominal.abs_fun_eq"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

734 
val abs_fun_eq' = @{thm "Nominal.abs_fun_eq'"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

735 
val abs_fun_fresh = @{thm "Nominal.abs_fun_fresh"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

736 
val abs_fun_fresh' = @{thm "Nominal.abs_fun_fresh'"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

737 
val dj_perm_forget = @{thm "Nominal.dj_perm_forget"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

738 
val dj_pp_forget = @{thm "Nominal.dj_perm_perm_forget"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

739 
val fresh_iff = @{thm "Nominal.fresh_abs_fun_iff"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

740 
val fresh_iff_ineq = @{thm "Nominal.fresh_abs_fun_iff_ineq"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

741 
val abs_fun_supp = @{thm "Nominal.abs_fun_supp"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

742 
val abs_fun_supp_ineq = @{thm "Nominal.abs_fun_supp_ineq"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

743 
val pt_swap_bij = @{thm "Nominal.pt_swap_bij"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

744 
val pt_swap_bij' = @{thm "Nominal.pt_swap_bij'"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

745 
val pt_fresh_fresh = @{thm "Nominal.pt_fresh_fresh"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

746 
val pt_bij = @{thm "Nominal.pt_bij"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

747 
val pt_perm_compose = @{thm "Nominal.pt_perm_compose"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

748 
val pt_perm_compose' = @{thm "Nominal.pt_perm_compose'"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

749 
val perm_app = @{thm "Nominal.pt_fun_app_eq"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

750 
val at_fresh = @{thm "Nominal.at_fresh"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

751 
val at_fresh_ineq = @{thm "Nominal.at_fresh_ineq"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

752 
val at_calc = @{thms "Nominal.at_calc"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

753 
val at_swap_simps = @{thms "Nominal.at_swap_simps"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

754 
val at_supp = @{thm "Nominal.at_supp"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

755 
val dj_supp = @{thm "Nominal.dj_supp"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

756 
val fresh_left_ineq = @{thm "Nominal.pt_fresh_left_ineq"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

757 
val fresh_left = @{thm "Nominal.pt_fresh_left"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

758 
val fresh_right_ineq = @{thm "Nominal.pt_fresh_right_ineq"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

759 
val fresh_right = @{thm "Nominal.pt_fresh_right"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

760 
val fresh_bij_ineq = @{thm "Nominal.pt_fresh_bij_ineq"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

761 
val fresh_bij = @{thm "Nominal.pt_fresh_bij"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

762 
val fresh_eqvt = @{thm "Nominal.pt_fresh_eqvt"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

763 
val fresh_eqvt_ineq = @{thm "Nominal.pt_fresh_eqvt_ineq"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

764 
val set_diff_eqvt = @{thm "Nominal.pt_set_diff_eqvt"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

765 
val in_eqvt = @{thm "Nominal.pt_in_eqvt"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

766 
val eq_eqvt = @{thm "Nominal.pt_eq_eqvt"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

767 
val all_eqvt = @{thm "Nominal.pt_all_eqvt"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

768 
val ex_eqvt = @{thm "Nominal.pt_ex_eqvt"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

769 
val pt_pi_rev = @{thm "Nominal.pt_pi_rev"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

770 
val pt_rev_pi = @{thm "Nominal.pt_rev_pi"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

771 
val at_exists_fresh = @{thm "Nominal.at_exists_fresh"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

772 
val at_exists_fresh' = @{thm "Nominal.at_exists_fresh'"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

773 
val fresh_perm_app_ineq = @{thm "Nominal.pt_fresh_perm_app_ineq"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

774 
val fresh_perm_app = @{thm "Nominal.pt_fresh_perm_app"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

775 
val fresh_aux = @{thm "Nominal.pt_fresh_aux"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

776 
val pt_perm_supp_ineq = @{thm "Nominal.pt_perm_supp_ineq"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

777 
val pt_perm_supp = @{thm "Nominal.pt_perm_supp"}; 
22786  778 

18262  779 
(* Now we collect and instantiate some lemmas w.r.t. all atom *) 
780 
(* types; this allows for example to use abs_perm (which is a *) 

781 
(* collection of theorems) instead of thm abs_fun_pi with explicit *) 

782 
(* instantiations. *) 

20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

783 
val (_, thy33) = 
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

784 
let 
18651
0cb5a8f501aa
added the thmscollection "pt_id" (collection of all pt_<ak>1 lemmas)
urbanc
parents:
18626
diff
changeset

785 

18279
f7a18e2b10fc
made some of the theorem lookups static (by using
urbanc
parents:
18262
diff
changeset

786 
(* takes a theorem thm and a list of theorems [t1,..,tn] *) 
f7a18e2b10fc
made some of the theorem lookups static (by using
urbanc
parents:
18262
diff
changeset

787 
(* produces a list of theorems of the form [t1 RS thm,..,tn RS thm] *) 
18262  788 
fun instR thm thms = map (fn ti => ti RS thm) thms; 
18068  789 

18262  790 
(* takes two theorem lists (hopefully of the same length ;o) *) 
791 
(* produces a list of theorems of the form *) 

792 
(* [t1 RS m1,..,tn RS mn] where [t1,..,tn] is thms1 and [m1,..,mn] is thms2 *) 

18279
f7a18e2b10fc
made some of the theorem lookups static (by using
urbanc
parents:
18262
diff
changeset

793 
fun inst_zip thms1 thms2 = map (fn (t1,t2) => t1 RS t2) (thms1 ~~ thms2); 
18068  794 

18262  795 
(* takes a theorem list of the form [l1,...,ln] *) 
796 
(* and a list of theorem lists of the form *) 

797 
(* [[h11,...,h1m],....,[hk1,....,hkm] *) 

798 
(* produces the list of theorem lists *) 

799 
(* [[l1 RS h11,...,l1 RS h1m],...,[ln RS hk1,...,ln RS hkm]] *) 

18279
f7a18e2b10fc
made some of the theorem lookups static (by using
urbanc
parents:
18262
diff
changeset

800 
fun inst_mult thms thmss = map (fn (t,ts) => instR t ts) (thms ~~ thmss); 
f7a18e2b10fc
made some of the theorem lookups static (by using
urbanc
parents:
18262
diff
changeset

801 

f7a18e2b10fc
made some of the theorem lookups static (by using
urbanc
parents:
18262
diff
changeset

802 
(* FIXME: these lists do not need to be created dynamically again *) 
18262  803 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

804 

18068  805 
(* list of all at_insttheorems *) 
18262  806 
val ats = map (fn ak => PureThy.get_thm thy32 (Name ("at_"^ak^"_inst"))) ak_names 
18068  807 
(* list of all pt_insttheorems *) 
18262  808 
val pts = map (fn ak => PureThy.get_thm thy32 (Name ("pt_"^ak^"_inst"))) ak_names 
809 
(* list of all cp_insttheorems as a collection of lists*) 

18068  810 
val cps = 
18262  811 
let fun cps_fun ak1 ak2 = PureThy.get_thm thy32 (Name ("cp_"^ak1^"_"^ak2^"_inst")) 
812 
in map (fn aki => (map (cps_fun aki) ak_names)) ak_names end; 

813 
(* list of all cp_insttheorems that have different atom types *) 

814 
val cps' = 

815 
let fun cps'_fun ak1 ak2 = 

816 
if ak1=ak2 then NONE else SOME(PureThy.get_thm thy32 (Name ("cp_"^ak1^"_"^ak2^"_inst"))) 

817 
in map (fn aki => (List.mapPartial I (map (cps'_fun aki) ak_names))) ak_names end; 

18068  818 
(* list of all dj_insttheorems *) 
819 
val djs = 

820 
let fun djs_fun (ak1,ak2) = 

18262  821 
if ak1=ak2 then NONE else SOME(PureThy.get_thm thy32 (Name ("dj_"^ak2^"_"^ak1))) 
822 
in List.mapPartial I (map djs_fun (Library.product ak_names ak_names)) end; 

823 
(* list of all fs_insttheorems *) 

824 
val fss = map (fn ak => PureThy.get_thm thy32 (Name ("fs_"^ak^"_inst"))) ak_names 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

825 
(* list of all at_insttheorems *) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

826 
val fs_axs = map (fn ak => PureThy.get_thm thy32 (Name ("fs_"^ak^"1"))) ak_names 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

827 

be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

828 
fun inst_pt thms = Library.flat (map (fn ti => instR ti pts) thms); 
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

829 
fun inst_at thms = Library.flat (map (fn ti => instR ti ats) thms); 
18262  830 
fun inst_fs thms = Library.flat (map (fn ti => instR ti fss) thms); 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

831 
fun inst_cp thms cps = Library.flat (inst_mult thms cps); 
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

832 
fun inst_pt_at thms = inst_zip ats (inst_pt thms); 
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

833 
fun inst_dj thms = Library.flat (map (fn ti => instR ti djs) thms); 
18436
9649e24bc10e
added thms to perm_compose (so far only composition
urbanc
parents:
18435
diff
changeset

834 
fun inst_pt_pt_at_cp thms = inst_cp (inst_zip ats (inst_zip pts (inst_pt thms))) cps; 
18262  835 
fun inst_pt_at_fs thms = inst_zip (inst_fs [fs1]) (inst_zip ats (inst_pt thms)); 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

836 
fun inst_pt_pt_at_cp thms = 
18279
f7a18e2b10fc
made some of the theorem lookups static (by using
urbanc
parents:
18262
diff
changeset

837 
let val i_pt_pt_at = inst_zip ats (inst_zip pts (inst_pt thms)); 
18436
9649e24bc10e
added thms to perm_compose (so far only composition
urbanc
parents:
18435
diff
changeset

838 
val i_pt_pt_at_cp = inst_cp i_pt_pt_at cps'; 
18396
b3e7da94b51f
added a fresh_left lemma that contains all instantiation
urbanc
parents:
18381
diff
changeset

839 
in i_pt_pt_at_cp end; 
b3e7da94b51f
added a fresh_left lemma that contains all instantiation
urbanc
parents:
18381
diff
changeset

840 
fun inst_pt_pt_at_cp_dj thms = inst_zip djs (inst_pt_pt_at_cp thms); 
18068  841 
in 
18262  842 
thy32 
18652
3930a060d71b
rolled back the last addition since these lemmas were already
urbanc
parents:
18651
diff
changeset

843 
> PureThy.add_thmss [(("alpha", inst_pt_at [abs_fun_eq]),[])] 
19562
e56b3c967ae8
added the lemma abs_fun_eq' to the nominal theory,
urbanc
parents:
19548
diff
changeset

844 
>> PureThy.add_thmss [(("alpha'", inst_pt_at [abs_fun_eq']),[])] 
23158
749b6870b1a1
introduced symmetric variants of the lemmas for alphaequivalence
urbanc
parents:
23029
diff
changeset

845 
>> PureThy.add_thmss [(("alpha_fresh", inst_pt_at [abs_fun_fresh]),[])] 
749b6870b1a1
introduced symmetric variants of the lemmas for alphaequivalence
urbanc
parents:
23029
diff
changeset

846 
>> PureThy.add_thmss [(("alpha_fresh'", inst_pt_at [abs_fun_fresh']),[])] 
22557
6775c71f1da0
added pt_bij' to the collection perm_swap and also added abs_perm to the collection of equivariance lemmas
urbanc
parents:
22536
diff
changeset

847 
>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij] @ inst_pt_at [pt_swap_bij']),[])] 
22610  848 
>> PureThy.add_thmss [(("swap_simps", inst_at at_swap_simps),[])] 
19139  849 
>> PureThy.add_thmss 
850 
let val thms1 = inst_pt_at [pt_pi_rev]; 

851 
val thms2 = inst_pt_at [pt_rev_pi]; 

852 
in [(("perm_pi_simp",thms1 @ thms2),[])] end 

18381
246807ef6dfb
changed the types in accordance with Florian's changes
urbanc
parents:
18366
diff
changeset

853 
>> PureThy.add_thmss [(("perm_fresh_fresh", inst_pt_at [pt_fresh_fresh]),[])] 
246807ef6dfb
changed the types in accordance with Florian's changes
urbanc
parents:
18366
diff
changeset

854 
>> PureThy.add_thmss [(("perm_bij", inst_pt_at [pt_bij]),[])] 
18436
9649e24bc10e
added thms to perm_compose (so far only composition
urbanc
parents:
18435
diff
changeset

855 
>> PureThy.add_thmss 
9649e24bc10e
added thms to perm_compose (so far only composition
urbanc
parents:
18435
diff
changeset

856 
let val thms1 = inst_pt_at [pt_perm_compose]; 
9649e24bc10e
added thms to perm_compose (so far only composition
urbanc
parents:
18435
diff
changeset

857 
val thms2 = instR cp1 (Library.flat cps'); 
9649e24bc10e
added thms to perm_compose (so far only composition
urbanc
parents:
18435
diff
changeset

858 
in [(("perm_compose",thms1 @ thms2),[])] end 
19139  859 
>> PureThy.add_thmss [(("perm_compose'",inst_pt_at [pt_perm_compose']),[])] 
860 
>> PureThy.add_thmss [(("perm_app", inst_pt_at [perm_app]),[])] 

18381
246807ef6dfb
changed the types in accordance with Florian's changes
urbanc
parents:
18366
diff
changeset

861 
>> PureThy.add_thmss [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])] 
19972
89c5afe4139a
added more infrastructure for the recursion combinator
urbanc
parents:
19638
diff
changeset

862 
>> PureThy.add_thmss [(("exists_fresh", inst_at [at_exists_fresh]),[])] 
21377
c29146dc14f1
replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents:
21289
diff
changeset

863 
>> PureThy.add_thmss [(("exists_fresh'", inst_at [at_exists_fresh']),[])] 
24569  864 
>> PureThy.add_thmss 
865 
let 

866 
val thms1 = inst_pt_at [all_eqvt]; 

867 
val thms2 = map (fold_rule [inductive_forall_def]) thms1 

868 
in 

869 
[(("all_eqvt", thms1 @ thms2), [NominalThmDecls.eqvt_force_add])] 

870 
end 

22715
381e6c45f13b
improved the equivariance lemmas for the quantifiers; had to export the lemma eqvt_force_add and eqvt_force_del in the thmdecls
urbanc
parents:
22611
diff
changeset

871 
>> PureThy.add_thmss [(("ex_eqvt", inst_pt_at [ex_eqvt]),[NominalThmDecls.eqvt_force_add])] 
19972
89c5afe4139a
added more infrastructure for the recursion combinator
urbanc
parents:
19638
diff
changeset

872 
>> PureThy.add_thmss 
89c5afe4139a
added more infrastructure for the recursion combinator
urbanc
parents:
19638
diff
changeset

873 
let val thms1 = inst_at [at_fresh] 
89c5afe4139a
added more infrastructure for the recursion combinator
urbanc
parents:
19638
diff
changeset

874 
val thms2 = inst_dj [at_fresh_ineq] 
89c5afe4139a
added more infrastructure for the recursion combinator
urbanc
parents:
19638
diff
changeset

875 
in [(("fresh_atm", thms1 @ thms2),[])] end 
19992  876 
>> PureThy.add_thmss 
20377
3baf326b2b5f
Removed nontrivial definitions from calc_atm theorem list.
berghofe
parents:
20179
diff
changeset

877 
let val thms1 = filter 
3baf326b2b5f
Removed nontrivial definitions from calc_atm theorem list.
berghofe
parents:
20179
diff
changeset

878 
(fn th => case prop_of th of _ $ _ $ Var _ => true  _ => false) 
3baf326b2b5f
Removed nontrivial definitions from calc_atm theorem list.
berghofe
parents:
20179
diff
changeset

879 
(List.concat (List.concat perm_defs)) 
19993
e0a5783d708f
added simplification rules to the fresh_guess tactic
urbanc
parents:
19992
diff
changeset

880 
in [(("calc_atm", (inst_at at_calc) @ thms1),[])] end 
18381
246807ef6dfb
changed the types in accordance with Florian's changes
urbanc
parents:
18366
diff
changeset

881 
>> PureThy.add_thmss 
18279
f7a18e2b10fc
made some of the theorem lookups static (by using
urbanc
parents:
18262
diff
changeset

882 
let val thms1 = inst_pt_at [abs_fun_pi] 
f7a18e2b10fc
made some of the theorem lookups static (by using
urbanc
parents:
18262
diff
changeset

883 
and thms2 = inst_pt_pt_at_cp [abs_fun_pi_ineq] 
22557
6775c71f1da0
added pt_bij' to the collection perm_swap and also added abs_perm to the collection of equivariance lemmas
urbanc
parents:
22536
diff
changeset

884 
in [(("abs_perm", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end 
18381
246807ef6dfb
changed the types in accordance with Florian's changes
urbanc
parents:
18366
diff
changeset

885 
>> PureThy.add_thmss 
18279
f7a18e2b10fc
made some of the theorem lookups static (by using
urbanc
parents:
18262
diff
changeset

886 
let val thms1 = inst_dj [dj_perm_forget] 
f7a18e2b10fc
made some of the theorem lookups static (by using
urbanc
parents:
18262
diff
changeset

887 
and thms2 = inst_dj [dj_pp_forget] 
f7a18e2b10fc
made some of the theorem lookups static (by using
urbanc
parents:
18262
diff
changeset

888 
in [(("perm_dj", thms1 @ thms2),[])] end 
18381
246807ef6dfb
changed the types in accordance with Florian's changes
urbanc
parents:
18366
diff
changeset

889 
>> PureThy.add_thmss 
18279
f7a18e2b10fc
made some of the theorem lookups static (by using
urbanc
parents:
18262
diff
changeset

890 
let val thms1 = inst_pt_at_fs [fresh_iff] 
18626  891 
and thms2 = inst_pt_at [fresh_iff] 
892 
and thms3 = inst_pt_pt_at_cp_dj [fresh_iff_ineq] 

893 
in [(("abs_fresh", thms1 @ thms2 @ thms3),[])] end 

18381
246807ef6dfb
changed the types in accordance with Florian's changes
urbanc
parents:
18366
diff
changeset

894 
>> PureThy.add_thmss 
18279
f7a18e2b10fc
made some of the theorem lookups static (by using
urbanc
parents:
18262
diff
changeset

895 
let val thms1 = inst_pt_at [abs_fun_supp] 
f7a18e2b10fc
made some of the theorem lookups static (by using
urbanc
parents:
18262
diff
changeset

896 
and thms2 = inst_pt_at_fs [abs_fun_supp] 
f7a18e2b10fc
made some of the theorem lookups static (by using
urbanc
parents:
18262
diff
changeset

897 
and thms3 = inst_pt_pt_at_cp_dj [abs_fun_supp_ineq] 
f7a18e2b10fc
made some of the theorem lookups static (by using
urbanc
parents:
18262
diff
changeset

898 
in [(("abs_supp", thms1 @ thms2 @ thms3),[])] end 
18396
b3e7da94b51f
added a fresh_left lemma that contains all instantiation
urbanc
parents:
18381
diff
changeset

899 
>> PureThy.add_thmss 
b3e7da94b51f
added a fresh_left lemma that contains all instantiation
urbanc
parents:
18381
diff
changeset

900 
let val thms1 = inst_pt_at [fresh_left] 
b3e7da94b51f
added a fresh_left lemma that contains all instantiation
urbanc
parents:
18381
diff
changeset

901 
and thms2 = inst_pt_pt_at_cp [fresh_left_ineq] 
b3e7da94b51f
added a fresh_left lemma that contains all instantiation
urbanc
parents:
18381
diff
changeset

902 
in [(("fresh_left", thms1 @ thms2),[])] end 
18426  903 
>> PureThy.add_thmss 
19548  904 
let val thms1 = inst_pt_at [fresh_right] 
905 
and thms2 = inst_pt_pt_at_cp [fresh_right_ineq] 

906 
in [(("fresh_right", thms1 @ thms2),[])] end 

907 
>> PureThy.add_thmss 

18426  908 
let val thms1 = inst_pt_at [fresh_bij] 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

909 
and thms2 = inst_pt_pt_at_cp [fresh_bij_ineq] 
19972
89c5afe4139a
added more infrastructure for the recursion combinator
urbanc
parents:
19638
diff
changeset

910 
in [(("fresh_bij", thms1 @ thms2),[])] end 
89c5afe4139a
added more infrastructure for the recursion combinator
urbanc
parents:
19638
diff
changeset

911 
>> PureThy.add_thmss 
89c5afe4139a
added more infrastructure for the recursion combinator
urbanc
parents:
19638
diff
changeset

912 
let val thms1 = inst_pt_at [fresh_eqvt] 
22535
cbee450f88a6
added extended the lemma for equivariance of freshness
urbanc
parents:
22418
diff
changeset

913 
and thms2 = inst_pt_pt_at_cp_dj [fresh_eqvt_ineq] 
cbee450f88a6
added extended the lemma for equivariance of freshness
urbanc
parents:
22418
diff
changeset

914 
in [(("fresh_eqvt", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

915 
>> PureThy.add_thmss 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

916 
let val thms1 = inst_pt_at [in_eqvt] 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

917 
in [(("in_eqvt", thms1),[NominalThmDecls.eqvt_add])] end 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

918 
>> PureThy.add_thmss 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

919 
let val thms1 = inst_pt_at [eq_eqvt] 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

920 
in [(("eq_eqvt", thms1),[NominalThmDecls.eqvt_add])] end 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

921 
>> PureThy.add_thmss 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

922 
let val thms1 = inst_pt_at [set_diff_eqvt] 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

923 
in [(("set_diff_eqvt", thms1),[NominalThmDecls.eqvt_add])] end 
19638
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19635
diff
changeset

924 
>> PureThy.add_thmss 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19635
diff
changeset

925 
let val thms1 = inst_pt_at [fresh_aux] 
22786  926 
and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq] 
927 
in [(("fresh_aux", thms1 @ thms2),[])] end 

22785
fab155c8ce46
add two lemmas dealing with freshness on permutations.
narboux
parents:
22768
diff
changeset

928 
>> PureThy.add_thmss 
fab155c8ce46
add two lemmas dealing with freshness on permutations.
narboux
parents:
22768
diff
changeset

929 
let val thms1 = inst_pt_at [fresh_perm_app] 
22786  930 
and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq] 
22794
d0f483fd57dd
add the lemma supp_eqvt and put the right attribute
narboux
parents:
22786
diff
changeset

931 
in [(("fresh_perm_app", thms1 @ thms2),[])] end 
d0f483fd57dd
add the lemma supp_eqvt and put the right attribute
narboux
parents:
22786
diff
changeset

932 
>> PureThy.add_thmss 
d0f483fd57dd
add the lemma supp_eqvt and put the right attribute
narboux
parents:
22786
diff
changeset

933 
let val thms1 = inst_pt_at [pt_perm_supp] 
d0f483fd57dd
add the lemma supp_eqvt and put the right attribute
narboux
parents:
22786
diff
changeset

934 
and thms2 = inst_pt_pt_at_cp [pt_perm_supp_ineq] 
d0f483fd57dd
add the lemma supp_eqvt and put the right attribute
narboux
parents:
22786
diff
changeset

935 
in [(("supp_eqvt", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

936 
>> PureThy.add_thmss [(("fin_supp",fs_axs),[])] 
18068  937 
end; 
938 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

939 
in 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

940 
NominalData.map (fold Symtab.update (full_ak_names ~~ map make_atom_info 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

941 
(pt_ax_classes ~~ 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

942 
fs_ax_classes ~~ 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

943 
map (fn cls => full_ak_names ~~ cls) cp_ax_classes))) thy33 
18068  944 
end; 
945 

946 

947 
(* syntax und parsing *) 

948 
structure P = OuterParse and K = OuterKeyword; 

949 

950 
val atom_declP = 

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

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

953 

954 
val _ = OuterSyntax.add_parsers [atom_declP]; 

955 

956 
end; 