author  berghofe 
Wed, 15 Mar 2006 17:59:33 +0100  
changeset 19275  3d10de7a8ca7 
parent 19251  6bc0dda66f32 
child 19322  bf84bdf05f14 
permissions  rwrr 
17870  1 
(* $Id$ *) 
2 

3 
signature NOMINAL_PACKAGE = 

4 
sig 

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

18068  6 
(bstring * string list * mixfix) list) list > theory > theory 
17870  7 
end 
8 

18068  9 
structure NominalPackage : NOMINAL_PACKAGE = 
17870  10 
struct 
11 

12 
open DatatypeAux; 

18068  13 
open NominalAtoms; 
17870  14 

18016  15 
(** FIXME: DatatypePackage should export this function **) 
16 

17 
local 

18 

19 
fun dt_recs (DtTFree _) = [] 

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

21 
 dt_recs (DtRec i) = [i]; 

22 

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

24 
let 

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

19133
7e84a1a3741c
Adapted to Florian's recent changes to the AxClass package.
berghofe
parents:
18759
diff
changeset

26 
val bnames = map the_bname (distinct op = (List.concat (map dt_recs args))); 
18016  27 
in map (fn (c, _) => space_implode "_" (Sign.base_name c :: bnames)) constrs end; 
28 

29 

30 
fun induct_cases descr = 

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

32 

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

34 

35 
in 

36 

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

38 

39 
fun mk_case_names_exhausts descr new = 

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

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

42 

43 
end; 

44 

45 
(*******************************) 

46 

17870  47 
val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma); 
48 

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

50 
let 

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

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

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

54 

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

56 

57 
fun indtac indrule indnames i st = 

58 
let 

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

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

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

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

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

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

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

66 
(term_frees t2) of 

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

68 
 _ => sys_error "indtac") 

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

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

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

72 
val indrule' = cterm_instantiate (Ps ~~ 

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

74 
in 

75 
rtac indrule' i st 

76 
end; 

77 

18658  78 
fun mk_subgoal i f st = 
79 
let 

80 
val cg = List.nth (cprems_of st, i  1); 

81 
val g = term_of cg; 

82 
val revcut_rl' = Thm.lift_rule cg revcut_rl; 

83 
val v = head_of (Logic.strip_assums_concl (hd (prems_of revcut_rl'))); 

84 
val ps = Logic.strip_params g; 

85 
val cert = cterm_of (sign_of_thm st); 

86 
in 

87 
compose_tac (false, 

88 
Thm.instantiate ([], [(cert v, cert (list_abs (ps, 

89 
f (rev ps) (Logic.strip_assums_hyp g) (Logic.strip_assums_concl g))))]) 

90 
revcut_rl', 2) i st 

91 
end; 

92 

93 
(** simplification procedure for sorting permutations **) 

94 

95 
val dj_cp = thm "dj_cp"; 

96 

97 
fun dest_permT (Type ("fun", [Type ("List.list", [Type ("*", [T, _])]), 

98 
Type ("fun", [_, U])])) = (T, U); 

99 

100 
fun permTs_of (Const ("nominal.perm", T) $ t $ u) = fst (dest_permT T) :: permTs_of u 

101 
 permTs_of _ = []; 

102 

103 
fun perm_simproc' thy ss (Const ("nominal.perm", T) $ t $ (u as Const ("nominal.perm", U) $ r $ s)) = 

104 
let 

105 
val (aT as Type (a, []), S) = dest_permT T; 

106 
val (bT as Type (b, []), _) = dest_permT U 

107 
in if aT mem permTs_of u andalso aT <> bT then 

108 
let 

109 
val a' = Sign.base_name a; 

110 
val b' = Sign.base_name b; 

111 
val cp = PureThy.get_thm thy (Name ("cp_" ^ a' ^ "_" ^ b' ^ "_inst")); 

112 
val dj = PureThy.get_thm thy (Name ("dj_" ^ b' ^ "_" ^ a')); 

113 
val dj_cp' = [cp, dj] MRS dj_cp; 

114 
val cert = SOME o cterm_of thy 

115 
in 

116 
SOME (mk_meta_eq (Drule.instantiate' [SOME (ctyp_of thy S)] 

117 
[cert t, cert r, cert s] dj_cp')) 

118 
end 

119 
else NONE 

120 
end 

121 
 perm_simproc' thy ss _ = NONE; 

122 

123 
val perm_simproc = 

124 
Simplifier.simproc (the_context ()) "perm_simp" ["pi1 \\<bullet> (pi2 \\<bullet> x)"] perm_simproc'; 

125 

126 
val allE_Nil = read_instantiate_sg (the_context()) [("x", "[]")] allE; 

127 

128 
val meta_spec = thm "meta_spec"; 

129 

18582
4f4cc426b440
provide projections of induct_weak, induct_unsafe;
wenzelm
parents:
18579
diff
changeset

130 
fun projections rule = 
4f4cc426b440
provide projections of induct_weak, induct_unsafe;
wenzelm
parents:
18579
diff
changeset

131 
ProjectRule.projections rule 
4f4cc426b440
provide projections of induct_weak, induct_unsafe;
wenzelm
parents:
18579
diff
changeset

132 
> map (standard #> RuleCases.save rule); 
4f4cc426b440
provide projections of induct_weak, induct_unsafe;
wenzelm
parents:
18579
diff
changeset

133 

18658  134 
fun norm_sort thy = Sorts.norm_sort (snd (#classes (Type.rep_tsig (Sign.tsig_of thy)))); 
135 

17870  136 
fun gen_add_nominal_datatype prep_typ err flat_names new_type_names dts thy = 
137 
let 

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

139 

140 
val tmp_thy = thy > 

141 
Theory.copy > 

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

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

144 

145 
val sign = Theory.sign_of tmp_thy; 

146 

147 
val atoms = atoms_of thy; 

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

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

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

151 
Sign.base_name atom2)) atoms) atoms); 

152 
fun augment_sort S = S union classes; 

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

154 

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

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

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

158 

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

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

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

162 

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

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

165 
val tyvars = map #1 dts'; 

166 

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

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

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

170 

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

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

173 
val rps = map Library.swap ps; 

174 

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

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

176 
Type ("fun", [T, Type ("nominal.noption", [replace_types U])]) 
17870  177 
 replace_types (Type (s, Ts)) = 
178 
Type (getOpt (AList.lookup op = ps s, s), map replace_types Ts) 

179 
 replace_types T = T; 

180 

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

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

183 
 replace_types' T = T; 

184 

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

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

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

188 

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

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

191 

18045  192 
val ({induction, ...},thy1) = 
17870  193 
DatatypePackage.add_datatype_i err flat_names new_type_names' dts'' thy; 
194 

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

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

18107
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

197 
fun nth_dtyp i = typ_of_dtyp descr sorts' (DtRec i); 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

198 

17870  199 
(**** define permutation functions ****) 
200 

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

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

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

204 
let val T = nth_dtyp i 

205 
in permT > T > T end) descr; 

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

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

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

209 
(length new_type_names upto length descr  1)); 

210 
val perm_names_types = perm_names ~~ perm_types; 

211 

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

213 
let val T = nth_dtyp i 

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

215 
let 

18107
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

216 
val Ts = map (typ_of_dtyp descr sorts') dts; 
17870  217 
val names = DatatypeProp.make_tnames Ts; 
218 
val args = map Free (names ~~ Ts); 

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

220 
fun perm_arg (dt, x) = 

221 
let val T = type_of x 

222 
in if is_rec_type dt then 

223 
let val (Us, _) = strip_type T 

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

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

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

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

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

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

230 
end 

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

232 
end; 

233 
in 

234 
(("", HOLogic.mk_Trueprop (HOLogic.mk_eq 

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

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

237 
list_comb (c, args), 

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

239 
end) constrs 

240 
end) descr); 

241 

242 
val (thy2, perm_simps) = thy1 > 

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

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

245 
PrimrecPackage.add_primrec_i "" perm_eqs; 

246 

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

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

249 

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

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

252 

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

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

255 

256 
val unfolded_perm_eq_thms = 

257 
if length descr = length new_type_names then [] 

258 
else map standard (List.drop (split_conj_thm 

18010  259 
(Goal.prove thy2 [] [] 
17870  260 
(HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj 
261 
(map (fn (c as (s, T), x) => 

262 
let val [T1, T2] = binder_types T 

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

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

265 
end) 

18010  266 
(perm_names_types ~~ perm_indnames)))) 
267 
(fn _ => EVERY [indtac induction perm_indnames 1, 

17870  268 
ALLGOALS (asm_full_simp_tac 
269 
(simpset_of thy2 addsimps [perm_fun_def]))])), 

270 
length new_type_names)); 

271 

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

273 

274 
val _ = warning "perm_empty_thms"; 

275 

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

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

278 
in map standard (List.take (split_conj_thm 

18010  279 
(Goal.prove thy2 [] [] 
17870  280 
(HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj 
281 
(map (fn ((s, T), x) => HOLogic.mk_eq 

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

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

284 
Free (x, T))) 

285 
(perm_names ~~ 

18010  286 
map body_type perm_types ~~ perm_indnames)))) 
287 
(fn _ => EVERY [indtac induction perm_indnames 1, 

17870  288 
ALLGOALS (asm_full_simp_tac (simpset_of thy2))])), 
289 
length new_type_names)) 

290 
end) 

291 
atoms); 

292 

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

294 

295 
val _ = warning "perm_append_thms"; 

296 

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

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

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

300 

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

302 
let 

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

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

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

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

307 
val pt2' = pt_inst RS pt2; 

308 
val pt2_ax = PureThy.get_thm thy2 

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

310 
in List.take (map standard (split_conj_thm 

18010  311 
(Goal.prove thy2 [] [] 
17870  312 
(HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj 
313 
(map (fn ((s, T), x) => 

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

315 
in HOLogic.mk_eq 

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

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

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

319 
end) 

320 
(perm_names ~~ 

18010  321 
map body_type perm_types ~~ perm_indnames)))) 
322 
(fn _ => EVERY [indtac induction perm_indnames 1, 

17870  323 
ALLGOALS (asm_full_simp_tac (simpset_of thy2 addsimps [pt2', pt2_ax]))]))), 
324 
length new_type_names) 

325 
end) atoms); 

326 

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

328 

329 
val _ = warning "perm_eq_thms"; 

330 

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

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

333 

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

335 
let 

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

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

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

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

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

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

342 
val pt3' = pt_inst RS pt3; 

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

344 
val pt3_ax = PureThy.get_thm thy2 

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

346 
in List.take (map standard (split_conj_thm 

18010  347 
(Goal.prove thy2 [] [] (Logic.mk_implies 
17870  348 
(HOLogic.mk_Trueprop (Const ("nominal.prm_eq", 
349 
permT > permT > HOLogic.boolT) $ pi1 $ pi2), 

350 
HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj 

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

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

353 
in HOLogic.mk_eq 

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

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

356 
end) 

357 
(perm_names ~~ 

18010  358 
map body_type perm_types ~~ perm_indnames))))) 
359 
(fn _ => EVERY [indtac induction perm_indnames 1, 

17870  360 
ALLGOALS (asm_full_simp_tac (simpset_of thy2 addsimps [pt3', pt3_rev', pt3_ax]))]))), 
361 
length new_type_names) 

362 
end) atoms); 

363 

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

365 

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

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

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

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

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

371 

372 
fun composition_instance name1 name2 thy = 

373 
let 

374 
val name1' = Sign.base_name name1; 

375 
val name2' = Sign.base_name name2; 

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

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

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

379 
val augment = map_type_tfree 

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

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

382 
val cp_inst = PureThy.get_thm thy 

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

384 
val simps = simpset_of thy addsimps (perm_fun_def :: 

385 
(if name1 <> name2 then 

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

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

388 
else 

389 
let 

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

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

392 
in 

393 
[cp_inst RS cp1 RS sym, 

394 
at_inst RS (pt_inst RS pt_perm_compose) RS sym, 

395 
at_inst RS (pt_inst RS pt_perm_compose_rev) RS sym] 

396 
end)) 

18010  397 
val thms = split_conj_thm (standard (Goal.prove thy [] [] 
17870  398 
(HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj 
399 
(map (fn ((s, T), x) => 

400 
let 

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

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

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

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

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

406 
in HOLogic.mk_eq 

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

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

409 
end) 

18010  410 
(perm_names ~~ Ts ~~ perm_indnames)))) 
411 
(fn _ => EVERY [indtac induction perm_indnames 1, 

412 
ALLGOALS (asm_full_simp_tac simps)]))) 

17870  413 
in 
19275  414 
foldl (fn ((s, tvs), thy) => AxClass.prove_arity 
17870  415 
(s, replicate (length tvs) (cp_class :: classes), [cp_class]) 
19133
7e84a1a3741c
Adapted to Florian's recent changes to the AxClass package.
berghofe
parents:
18759
diff
changeset

416 
(ClassPackage.intro_classes_tac [] THEN ALLGOALS (resolve_tac thms)) thy) 
17870  417 
thy (full_new_type_names' ~~ tyvars) 
418 
end; 

419 

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

420 
val (perm_thmss,thy3) = thy2 > 
17870  421 
fold (fn name1 => fold (composition_instance name1) atoms) atoms > 
422 
curry (Library.foldr (fn ((i, (tyname, args, _)), thy) => 

19275  423 
AxClass.prove_arity (tyname, replicate (length args) classes, classes) 
19133
7e84a1a3741c
Adapted to Florian's recent changes to the AxClass package.
berghofe
parents:
18759
diff
changeset

424 
(ClassPackage.intro_classes_tac [] THEN REPEAT (EVERY 
17870  425 
[resolve_tac perm_empty_thms 1, 
426 
resolve_tac perm_append_thms 1, 

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

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

429 
PureThy.add_thmss 

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

18759  431 
unfolded_perm_eq_thms), [Simplifier.simp_add]), 
17870  432 
((space_implode "_" new_type_names ^ "_perm_empty", 
18759  433 
perm_empty_thms), [Simplifier.simp_add]), 
17870  434 
((space_implode "_" new_type_names ^ "_perm_append", 
18759  435 
perm_append_thms), [Simplifier.simp_add]), 
17870  436 
((space_implode "_" new_type_names ^ "_perm_eq", 
18759  437 
perm_eq_thms), [Simplifier.simp_add])]; 
17870  438 

439 
(**** Define representing sets ****) 

440 

441 
val _ = warning "representing sets"; 

442 

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

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

445 
val big_rep_name = 

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

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

447 
(fn (i, ("nominal.noption", _, _)) => NONE 
17870  448 
 (i, _) => SOME (name_of_typ (nth_dtyp i))) descr)) ^ "_set"; 
449 
val _ = warning ("big_rep_name: " ^ big_rep_name); 

450 

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

452 
(case AList.lookup op = descr i of 

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

453 
SOME ("nominal.noption", _, [(_, [dt']), _]) => 
17870  454 
apfst (cons dt) (strip_option dt') 
455 
 _ => ([], dtf)) 

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

456 
 strip_option (DtType ("fun", [dt, DtType ("nominal.noption", [dt'])])) = 
18261
1318955d57ac
Corrected treatment of nonrecursive abstraction types.
berghofe
parents:
18246
diff
changeset

457 
apfst (cons dt) (strip_option dt') 
17870  458 
 strip_option dt = ([], dt); 
459 

19133
7e84a1a3741c
Adapted to Florian's recent changes to the AxClass package.
berghofe
parents:
18759
diff
changeset

460 
val dt_atomTs = distinct op = (map (typ_of_dtyp descr sorts') 
18280
45e139675daf
Corrected atom class constraints in strong induction rule.
berghofe
parents:
18261
diff
changeset

461 
(List.concat (map (fn (_, (_, _, cs)) => List.concat 
45e139675daf
Corrected atom class constraints in strong induction rule.
berghofe
parents:
18261
diff
changeset

462 
(map (List.concat o map (fst o strip_option) o snd) cs)) descr))); 
45e139675daf
Corrected atom class constraints in strong induction rule.
berghofe
parents:
18261
diff
changeset

463 

17870  464 
fun make_intr s T (cname, cargs) = 
465 
let 

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

467 
let 

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

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

18107
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

470 
val Ts = map (typ_of_dtyp descr sorts') dts; 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

471 
val Us = map (typ_of_dtyp descr sorts') dts'; 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

472 
val T = typ_of_dtyp descr sorts' dt''; 
17870  473 
val free = mk_Free "x" (Us > T) j; 
474 
val free' = app_bnds free (length Us); 

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

476 
let val U = fastype_of t 

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

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

478 
Type ("nominal.noption", [U])) $ mk_Free "y" T i $ t) 
17870  479 
end 
480 
in (j + 1, j' + length Ts, 

481 
case dt'' of 

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

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

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

485 
HOLogic.mk_setT T)))) :: prems 

486 
 _ => prems, 

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

488 
end; 

489 

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

491 
val concl = HOLogic.mk_Trueprop (HOLogic.mk_mem 

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

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

494 
in Logic.list_implies (prems, concl) 

495 
end; 

496 

497 
val (intr_ts, ind_consts) = 

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

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

499 
(fn ((_, ("nominal.noption", _, _)), _) => NONE 
17870  500 
 ((i, (_, _, constrs)), rep_set_name) => 
501 
let val T = nth_dtyp i 

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

503 
Const (rep_set_name, HOLogic.mk_setT T)) 

504 
end) 

505 
(descr ~~ rep_set_names))); 

506 

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

508 
setmp InductivePackage.quiet_mode false 

509 
(InductivePackage.add_inductive_i false true big_rep_name false true false 

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

511 

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

513 

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

515 

516 
val perm_indnames' = List.mapPartial 

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

517 
(fn (x, (_, ("nominal.noption", _, _))) => NONE  (x, _) => SOME x) 
17870  518 
(perm_indnames ~~ descr); 
519 

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

18010  521 
(List.take (split_conj_thm (Goal.prove thy4 [] [] 
17870  522 
(HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map 
523 
(fn (S, x) => 

524 
let 

525 
val S = map_term_types (map_type_tfree 

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

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

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

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

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

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

18010  532 
end) (ind_consts ~~ perm_indnames')))) 
533 
(fn _ => EVERY (* CU: added perm_fun_def in the final tactic in order to deal with funs *) 

17870  534 
[indtac rep_induct [] 1, 
535 
ALLGOALS (simp_tac (simpset_of thy4 addsimps 

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

537 
ALLGOALS (resolve_tac rep_intrs 

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

539 
length new_type_names)); 

540 

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

542 
val perm_closed_thmss = map mk_perm_closed atoms; 

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

543 
val (_,thy5) = PureThy.add_thmss [(("perm_closed", List.concat perm_closed_thmss), [])] thy4; 
17870  544 

545 
(**** typedef ****) 

546 

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

548 

18366  549 
val (typedefs, thy6) = 
550 
fold_map (fn ((((name, mx), tvs), c), name') => fn thy => 

17870  551 
setmp TypedefPackage.quiet_mode true 
552 
(TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx) c NONE 

553 
(rtac exI 1 THEN 

554 
QUIET_BREADTH_FIRST (has_fewer_prems 1) 

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

556 
let 

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

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

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

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

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

18366  562 
in apfst (pair r o hd) 
17870  563 
(PureThy.add_defs_i true [(("prm_" ^ name ^ "_def", Logic.mk_equals 
564 
(Const ("nominal.perm", permT > T > T) $ pi $ Free ("x", T), 

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

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

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

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

569 
end)) 

18366  570 
(types_syntax ~~ tyvars ~~ 
571 
(List.take (ind_consts, length new_type_names)) ~~ new_type_names) thy5; 

17870  572 

573 
val perm_defs = map snd typedefs; 

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

18016  575 
val Rep_inverse_thms = map (#Rep_inverse o fst) typedefs; 
17870  576 
val Rep_thms = map (#Rep o fst) typedefs; 
577 

18016  578 
val big_name = space_implode "_" new_type_names; 
579 

580 

17870  581 
(** prove that new types are in class pt_<name> **) 
582 

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

584 

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

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

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

19275  588 
AxClass.prove_arity 
17870  589 
(Sign.intern_type thy name, 
590 
replicate (length tvs) (classes @ cp_classes), [class]) 

19133
7e84a1a3741c
Adapted to Florian's recent changes to the AxClass package.
berghofe
parents:
18759
diff
changeset

591 
(EVERY [ClassPackage.intro_classes_tac [], 
17870  592 
rewrite_goals_tac [perm_def], 
593 
asm_full_simp_tac (simpset_of thy addsimps [Rep_inverse]) 1, 

594 
asm_full_simp_tac (simpset_of thy addsimps 

595 
[Rep RS perm_closed RS Abs_inverse]) 1, 

596 
asm_full_simp_tac (HOL_basic_ss addsimps [PureThy.get_thm thy 

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

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

599 

600 

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

602 

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

604 

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

606 
let 

607 
val name = "cp_" ^ Sign.base_name atom1 ^ "_" ^ Sign.base_name atom2; 

608 
val class = Sign.intern_class thy name; 

609 
val cp1' = PureThy.get_thm thy (Name (name ^ "_inst")) RS cp1 

610 
in fold (fn ((((({Abs_inverse, Rep_inverse, Rep, ...}, 

611 
perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy => 

19275  612 
AxClass.prove_arity 
17870  613 
(Sign.intern_type thy name, 
614 
replicate (length tvs) (classes @ cp_classes), [class]) 

19133
7e84a1a3741c
Adapted to Florian's recent changes to the AxClass package.
berghofe
parents:
18759
diff
changeset

615 
(EVERY [ClassPackage.intro_classes_tac [], 
17870  616 
rewrite_goals_tac [perm_def], 
617 
asm_full_simp_tac (simpset_of thy addsimps 

618 
((Rep RS perm_closed1 RS Abs_inverse) :: 

619 
(if atom1 = atom2 then [] 

620 
else [Rep RS perm_closed2 RS Abs_inverse]))) 1, 

18016  621 
cong_tac 1, 
17870  622 
rtac refl 1, 
623 
rtac cp1' 1]) thy) 

624 
(typedefs ~~ new_type_names ~~ tyvars ~~ perm_closed_thms1 ~~ 

625 
perm_closed_thms2) thy 

626 
end; 

627 

628 
val thy7 = fold (fn x => fn thy => thy > 

629 
pt_instance x > 

630 
fold (cp_instance (apfst snd x)) (atoms ~~ perm_closed_thmss)) 

631 
(classes ~~ atoms ~~ perm_closed_thmss) thy6; 

632 

633 
(**** constructors ****) 

634 

635 
fun mk_abs_fun (x, t) = 

636 
let 

637 
val T = fastype_of x; 

638 
val U = fastype_of t 

639 
in 

640 
Const ("nominal.abs_fun", T > U > T > 

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

641 
Type ("nominal.noption", [U])) $ x $ t 
17870  642 
end; 
643 

18016  644 
val (ty_idxs, _) = foldl 
18579
002d371401f5
changed the name of the type "nOption" to "noption".
urbanc
parents:
18381
diff
changeset

645 
(fn ((i, ("nominal.noption", _, _)), p) => p 
18016  646 
 ((i, _), (ty_idxs, j)) => (ty_idxs @ [(i, j)], j + 1)) ([], 0) descr; 
647 

648 
fun reindex (DtType (s, dts)) = DtType (s, map reindex dts) 

649 
 reindex (DtRec i) = DtRec (the (AList.lookup op = ty_idxs i)) 

650 
 reindex dt = dt; 

651 

652 
fun strip_suffix i s = implode (List.take (explode s, size s  i)); 

653 

654 
(** strips the "_Rep" in type names *) 

18045  655 
fun strip_nth_name i s = 
656 
let val xs = NameSpace.unpack s; 

657 
in NameSpace.pack (Library.nth_map (length xs  i) (strip_suffix 4) xs) end; 

18016  658 

18107
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

659 
val (descr'', ndescr) = ListPair.unzip (List.mapPartial 
18579
002d371401f5
changed the name of the type "nOption" to "noption".
urbanc
parents:
18381
diff
changeset

660 
(fn (i, ("nominal.noption", _, _)) => NONE 
18107
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

661 
 (i, (s, dts, constrs)) => 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

662 
let 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

663 
val SOME index = AList.lookup op = ty_idxs i; 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

664 
val (constrs1, constrs2) = ListPair.unzip 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

665 
(map (fn (cname, cargs) => apfst (pair (strip_nth_name 2 cname)) 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

666 
(foldl_map (fn (dts, dt) => 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

667 
let val (dts', dt') = strip_option dt 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

668 
in (dts @ dts' @ [reindex dt'], (length dts, length dts')) end) 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

669 
([], cargs))) constrs) 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

670 
in SOME ((index, (strip_nth_name 1 s, map reindex dts, constrs1)), 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

671 
(index, constrs2)) 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

672 
end) descr); 
18045  673 

18016  674 
val (descr1, descr2) = splitAt (length new_type_names, descr''); 
675 
val descr' = [descr1, descr2]; 

676 

18107
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

677 
val typ_of_dtyp' = replace_types' o typ_of_dtyp descr sorts'; 
17870  678 

679 
val rep_names = map (fn s => 

680 
Sign.intern_const thy7 ("Rep_" ^ s)) new_type_names; 

681 
val abs_names = map (fn s => 

682 
Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names; 

683 

18016  684 
val recTs' = List.mapPartial 
18579
002d371401f5
changed the name of the type "nOption" to "noption".
urbanc
parents:
18381
diff
changeset

685 
(fn ((_, ("nominal.noption", _, _)), T) => NONE 
18016  686 
 (_, T) => SOME T) (descr ~~ get_rec_types descr sorts'); 
18107
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

687 
val recTs = get_rec_types descr'' sorts'; 
18016  688 
val newTs' = Library.take (length new_type_names, recTs'); 
689 
val newTs = Library.take (length new_type_names, recTs); 

17870  690 

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

692 

693 
fun make_constr_def tname T T' ((thy, defs, eqns), ((cname, cargs), (cname', mx))) = 

694 
let 

695 
fun constr_arg (dt, (j, l_args, r_args)) = 

696 
let 

697 
val x' = mk_Free "x" (typ_of_dtyp' dt) j; 

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

699 
val xs = map (fn (dt, i) => mk_Free "x" (typ_of_dtyp' dt) i) 

700 
(dts ~~ (j upto j + length dts  1)) 

701 
val x = mk_Free "x" (typ_of_dtyp' dt') (j + length dts) 

702 
val (dts', dt'') = strip_dtyp dt' 

18261
1318955d57ac
Corrected treatment of nonrecursive abstraction types.
berghofe
parents:
18246
diff
changeset

703 
in 
1318955d57ac
Corrected treatment of nonrecursive abstraction types.
berghofe
parents:
18246
diff
changeset

704 
(j + length dts + 1, 
1318955d57ac
Corrected treatment of nonrecursive abstraction types.
berghofe
parents:
18246
diff
changeset

705 
xs @ x :: l_args, 
1318955d57ac
Corrected treatment of nonrecursive abstraction types.
berghofe
parents:
18246
diff
changeset

706 
foldr mk_abs_fun 
1318955d57ac
Corrected treatment of nonrecursive abstraction types.
berghofe
parents:
18246
diff
changeset

707 
(case dt'' of 
1318955d57ac
Corrected treatment of nonrecursive abstraction types.
berghofe
parents:
18246
diff
changeset

708 
DtRec k => if k < length new_type_names then 
1318955d57ac
Corrected treatment of nonrecursive abstraction types.
berghofe
parents:
18246
diff
changeset

709 
list_abs (map (pair "z" o typ_of_dtyp') dts', 
1318955d57ac
Corrected treatment of nonrecursive abstraction types.
berghofe
parents:
18246
diff
changeset

710 
Const (List.nth (rep_names, k), typ_of_dtyp' dt'' > 
1318955d57ac
Corrected treatment of nonrecursive abstraction types.
berghofe
parents:
18246
diff
changeset

711 
typ_of_dtyp descr sorts' dt'') $ app_bnds x (length dts')) 
1318955d57ac
Corrected treatment of nonrecursive abstraction types.
berghofe
parents:
18246
diff
changeset

712 
else error "nested recursion not (yet) supported" 
1318955d57ac
Corrected treatment of nonrecursive abstraction types.
berghofe
parents:
18246
diff
changeset

713 
 _ => x) xs :: r_args) 
17870  714 
end 
715 

716 
val (_, l_args, r_args) = foldr constr_arg (1, [], []) cargs; 

717 
val abs_name = Sign.intern_const (Theory.sign_of thy) ("Abs_" ^ tname); 

718 
val rep_name = Sign.intern_const (Theory.sign_of thy) ("Rep_" ^ tname); 

719 
val constrT = map fastype_of l_args > T; 

720 
val lhs = list_comb (Const (Sign.full_name thy (Sign.base_name cname), 

721 
constrT), l_args); 

722 
val rhs = list_comb (Const (cname, map fastype_of r_args > T'), r_args); 

723 
val def = Logic.mk_equals (lhs, Const (abs_name, T' > T) $ rhs); 

724 
val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq 

725 
(Const (rep_name, T > T') $ lhs, rhs)); 

726 
val def_name = (Sign.base_name cname) ^ "_def"; 

18366  727 
val ([def_thm], thy') = thy > 
17870  728 
Theory.add_consts_i [(cname', constrT, mx)] > 
729 
(PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)] 

730 
in (thy', defs @ [def_thm], eqns @ [eqn]) end; 

731 

732 
fun dt_constr_defs ((thy, defs, eqns, dist_lemmas), 

733 
(((((_, (_, _, constrs)), tname), T), T'), constr_syntax)) = 

734 
let 

735 
val rep_const = cterm_of thy 

736 
(Const (Sign.intern_const thy ("Rep_" ^ tname), T > T')); 

737 
val dist = standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma); 

738 
val (thy', defs', eqns') = Library.foldl (make_constr_def tname T T') 

739 
((Theory.add_path tname thy, defs, []), constrs ~~ constr_syntax) 

740 
in 

741 
(parent_path flat_names thy', defs', eqns @ [eqns'], dist_lemmas @ [dist]) 

742 
end; 

743 

744 
val (thy8, constr_defs, constr_rep_eqns, dist_lemmas) = Library.foldl dt_constr_defs 

745 
((thy7, [], [], []), List.take (descr, length new_type_names) ~~ 

746 
new_type_names ~~ newTs ~~ newTs' ~~ constr_syntax); 

747 

748 
val abs_inject_thms = map (fn tname => 

749 
PureThy.get_thm thy8 (Name ("Abs_" ^ tname ^ "_inject"))) new_type_names; 

750 

751 
val rep_inject_thms = map (fn tname => 

752 
PureThy.get_thm thy8 (Name ("Rep_" ^ tname ^ "_inject"))) new_type_names; 

753 

754 
val rep_thms = map (fn tname => 

755 
PureThy.get_thm thy8 (Name ("Rep_" ^ tname))) new_type_names; 

756 

757 
val rep_inverse_thms = map (fn tname => 

758 
PureThy.get_thm thy8 (Name ("Rep_" ^ tname ^ "_inverse"))) new_type_names; 

759 

760 
(* prove theorem Rep_i (Constr_j ...) = Constr'_j ... *) 

761 

762 
fun prove_constr_rep_thm eqn = 

763 
let 

764 
val inj_thms = map (fn r => r RS iffD1) abs_inject_thms; 

765 
val rewrites = constr_defs @ map mk_meta_eq rep_inverse_thms 

18010  766 
in standard (Goal.prove thy8 [] [] eqn (fn _ => EVERY 
17870  767 
[resolve_tac inj_thms 1, 
768 
rewrite_goals_tac rewrites, 

769 
rtac refl 3, 

770 
resolve_tac rep_intrs 2, 

18010  771 
REPEAT (resolve_tac rep_thms 1)])) 
17870  772 
end; 
773 

774 
val constr_rep_thmss = map (map prove_constr_rep_thm) constr_rep_eqns; 

775 

776 
(* prove theorem pi \<bullet> Rep_i x = Rep_i (pi \<bullet> x) *) 

777 

778 
fun prove_perm_rep_perm (atom, perm_closed_thms) = map (fn th => 

779 
let 

780 
val _ $ (_ $ (Rep $ x) $ _) = Logic.unvarify (prop_of th); 

781 
val Type ("fun", [T, U]) = fastype_of Rep; 

782 
val permT = mk_permT (Type (atom, [])); 

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

784 
in 

18010  785 
standard (Goal.prove thy8 [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq 
17870  786 
(Const ("nominal.perm", permT > U > U) $ pi $ (Rep $ x), 
18010  787 
Rep $ (Const ("nominal.perm", permT > T > T) $ pi $ x)))) 
788 
(fn _ => simp_tac (HOL_basic_ss addsimps (perm_defs @ Abs_inverse_thms @ 

789 
perm_closed_thms @ Rep_thms)) 1)) 

17870  790 
end) Rep_thms; 
791 

792 
val perm_rep_perm_thms = List.concat (map prove_perm_rep_perm 

793 
(atoms ~~ perm_closed_thmss)); 

794 

795 
(* prove distinctness theorems *) 

796 

18016  797 
val distinct_props = setmp DatatypeProp.dtK 1000 
798 
(DatatypeProp.make_distincts new_type_names descr' sorts') thy8; 

17870  799 

800 
val dist_rewrites = map (fn (rep_thms, dist_lemma) => 

801 
dist_lemma::(rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0])) 

802 
(constr_rep_thmss ~~ dist_lemmas); 

803 

804 
fun prove_distinct_thms (_, []) = [] 

805 
 prove_distinct_thms (p as (rep_thms, dist_lemma), t::ts) = 

806 
let 

18010  807 
val dist_thm = standard (Goal.prove thy8 [] [] t (fn _ => 
808 
simp_tac (simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1)) 

17870  809 
in dist_thm::(standard (dist_thm RS not_sym)):: 
810 
(prove_distinct_thms (p, ts)) 

811 
end; 

812 

813 
val distinct_thms = map prove_distinct_thms 

814 
(constr_rep_thmss ~~ dist_lemmas ~~ distinct_props); 

815 

816 
(** prove equations for permutation functions **) 

817 

818 
val abs_perm = PureThy.get_thms thy8 (Name "abs_perm"); (* FIXME *) 

819 

820 
val perm_simps' = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) => 

821 
let val T = replace_types' (nth_dtyp i) 

822 
in List.concat (map (fn (atom, perm_closed_thms) => 

823 
map (fn ((cname, dts), constr_rep_thm) => 

824 
let 

825 
val cname = Sign.intern_const thy8 

826 
(NameSpace.append tname (Sign.base_name cname)); 

827 
val permT = mk_permT (Type (atom, [])); 

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

829 

830 
fun perm t = 

831 
let val T = fastype_of t 

832 
in Const ("nominal.perm", permT > T > T) $ pi $ t end; 

833 

834 
fun constr_arg (dt, (j, l_args, r_args)) = 

835 
let 

836 
val x' = mk_Free "x" (typ_of_dtyp' dt) j; 

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

838 
val Ts = map typ_of_dtyp' dts; 

839 
val xs = map (fn (T, i) => mk_Free "x" T i) 

840 
(Ts ~~ (j upto j + length dts  1)) 

841 
val x = mk_Free "x" (typ_of_dtyp' dt') (j + length dts); 

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

18261
1318955d57ac
Corrected treatment of nonrecursive abstraction types.
berghofe
parents:
18246
diff
changeset

843 
in 
1318955d57ac
Corrected treatment of nonrecursive abstraction types.
berghofe
parents:
18246
diff
changeset

844 
(j + length dts + 1, 
1318955d57ac
Corrected treatment of nonrecursive abstraction types.
berghofe
parents:
18246
diff
changeset

845 
xs @ x :: l_args, 
1318955d57ac
Corrected treatment of nonrecursive abstraction types.
berghofe
parents:
18246
diff
changeset

846 
map perm (xs @ [x]) @ r_args) 
17870  847 
end 
848 

849 
val (_, l_args, r_args) = foldr constr_arg (1, [], []) dts; 

850 
val c = Const (cname, map fastype_of l_args > T) 

851 
in 

18010  852 
standard (Goal.prove thy8 [] [] 
17870  853 
(HOLogic.mk_Trueprop (HOLogic.mk_eq 
18010  854 
(perm (list_comb (c, l_args)), list_comb (c, r_args)))) 
855 
(fn _ => EVERY 

17870  856 
[simp_tac (simpset_of thy8 addsimps (constr_rep_thm :: perm_defs)) 1, 
857 
simp_tac (HOL_basic_ss addsimps (Rep_thms @ Abs_inverse_thms @ 

858 
constr_defs @ perm_closed_thms)) 1, 

859 
TRY (simp_tac (HOL_basic_ss addsimps 

860 
(symmetric perm_fun_def :: abs_perm)) 1), 

861 
TRY (simp_tac (HOL_basic_ss addsimps 

862 
(perm_fun_def :: perm_defs @ Rep_thms @ Abs_inverse_thms @ 

18010  863 
perm_closed_thms)) 1)])) 
17870  864 
end) (constrs ~~ constr_rep_thms)) (atoms ~~ perm_closed_thmss)) 
865 
end) (List.take (descr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss); 

866 

867 
(** prove injectivity of constructors **) 

868 

869 
val rep_inject_thms' = map (fn th => th RS sym) rep_inject_thms; 

870 
val alpha = PureThy.get_thms thy8 (Name "alpha"); 

871 
val abs_fresh = PureThy.get_thms thy8 (Name "abs_fresh"); 

872 
val fresh_def = PureThy.get_thm thy8 (Name "fresh_def"); 

873 
val supp_def = PureThy.get_thm thy8 (Name "supp_def"); 

874 

875 
val inject_thms = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) => 

876 
let val T = replace_types' (nth_dtyp i) 

877 
in List.mapPartial (fn ((cname, dts), constr_rep_thm) => 

878 
if null dts then NONE else SOME 

879 
let 

880 
val cname = Sign.intern_const thy8 

881 
(NameSpace.append tname (Sign.base_name cname)); 

882 

883 
fun make_inj (dt, (j, args1, args2, eqs)) = 

884 
let 

885 
val x' = mk_Free "x" (typ_of_dtyp' dt) j; 

886 
val y' = mk_Free "y" (typ_of_dtyp' dt) j; 

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

888 
val Ts_idx = map typ_of_dtyp' dts ~~ (j upto j + length dts  1); 

889 
val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx; 

890 
val ys = map (fn (T, i) => mk_Free "y" T i) Ts_idx; 

891 
val x = mk_Free "x" (typ_of_dtyp' dt') (j + length dts); 

892 
val y = mk_Free "y" (typ_of_dtyp' dt') (j + length dts); 

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

18261
1318955d57ac
Corrected treatment of nonrecursive abstraction types.
berghofe
parents:
18246
diff
changeset

894 
in 
1318955d57ac
Corrected treatment of nonrecursive abstraction types.
berghofe
parents:
18246
diff
changeset

895 
(j + length dts + 1, 
1318955d57ac
Corrected treatment of nonrecursive abstraction types.
berghofe
parents:
18246
diff
changeset

896 
xs @ (x :: args1), ys @ (y :: args2), 
1318955d57ac
Corrected treatment of nonrecursive abstraction types.
berghofe
parents:
18246
diff
changeset

897 
HOLogic.mk_eq 
1318955d57ac
Corrected treatment of nonrecursive abstraction types.
berghofe
parents:
18246
diff
changeset

898 
(foldr mk_abs_fun x xs, foldr mk_abs_fun y ys) :: eqs) 
17870  899 
end; 
900 

901 
val (_, args1, args2, eqs) = foldr make_inj (1, [], [], []) dts; 

902 
val Ts = map fastype_of args1; 

903 
val c = Const (cname, Ts > T) 

904 
in 

18010  905 
standard (Goal.prove thy8 [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq 
17870  906 
(HOLogic.mk_eq (list_comb (c, args1), list_comb (c, args2)), 
18010  907 
foldr1 HOLogic.mk_conj eqs))) 
908 
(fn _ => EVERY 

17870  909 
[asm_full_simp_tac (simpset_of thy8 addsimps (constr_rep_thm :: 
910 
rep_inject_thms')) 1, 

911 
TRY (asm_full_simp_tac (HOL_basic_ss addsimps (fresh_def :: supp_def :: 

912 
alpha @ abs_perm @ abs_fresh @ rep_inject_thms @ 

17874
8be65cf94d2e
Improved proof of injectivity theorems to make it work on
berghofe
parents:
17873
diff
changeset

913 
perm_rep_perm_thms)) 1), 
8be65cf94d2e
Improved proof of injectivity theorems to make it work on
berghofe
parents:
17873
diff
changeset

914 
TRY (asm_full_simp_tac (HOL_basic_ss addsimps (perm_fun_def :: 
18010  915 
expand_fun_eq :: rep_inject_thms @ perm_rep_perm_thms)) 1)])) 
17870  916 
end) (constrs ~~ constr_rep_thms) 
917 
end) (List.take (descr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss); 

918 

17872
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

919 
(** equations for support and freshness **) 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

920 

f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

921 
val Un_assoc = PureThy.get_thm thy8 (Name "Un_assoc"); 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

922 
val de_Morgan_conj = PureThy.get_thm thy8 (Name "de_Morgan_conj"); 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

923 
val Collect_disj_eq = PureThy.get_thm thy8 (Name "Collect_disj_eq"); 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

924 
val finite_Un = PureThy.get_thm thy8 (Name "finite_Un"); 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

925 

f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

926 
val (supp_thms, fresh_thms) = ListPair.unzip (map ListPair.unzip 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

927 
(map (fn ((((i, (_, _, constrs)), tname), inject_thms'), perm_thms') => 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

928 
let val T = replace_types' (nth_dtyp i) 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

929 
in List.concat (map (fn (cname, dts) => map (fn atom => 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

930 
let 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

931 
val cname = Sign.intern_const thy8 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

932 
(NameSpace.append tname (Sign.base_name cname)); 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

933 
val atomT = Type (atom, []); 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

934 

f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

935 
fun process_constr (dt, (j, args1, args2)) = 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

936 
let 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

937 
val x' = mk_Free "x" (typ_of_dtyp' dt) j; 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

938 
val (dts, dt') = strip_option dt; 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

939 
val Ts_idx = map typ_of_dtyp' dts ~~ (j upto j + length dts  1); 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

940 
val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx; 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

941 
val x = mk_Free "x" (typ_of_dtyp' dt') (j + length dts); 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

942 
val (dts', dt'') = strip_dtyp dt'; 
18261
1318955d57ac
Corrected treatment of nonrecursive abstraction types.
berghofe
parents:
18246
diff
changeset

943 
in 
1318955d57ac
Corrected treatment of nonrecursive abstraction types.
berghofe
parents:
18246
diff
changeset

944 
(j + length dts + 1, 
1318955d57ac
Corrected treatment of nonrecursive abstraction types.
berghofe
parents:
18246
diff
changeset

945 
xs @ (x :: args1), foldr mk_abs_fun x xs :: args2) 
17872
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

946 
end; 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

947 

f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

948 
val (_, args1, args2) = foldr process_constr (1, [], []) dts; 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

949 
val Ts = map fastype_of args1; 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

950 
val c = list_comb (Const (cname, Ts > T), args1); 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

951 
fun supp t = 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

952 
Const ("nominal.supp", fastype_of t > HOLogic.mk_setT atomT) $ t; 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

953 
fun fresh t = 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

954 
Const ("nominal.fresh", atomT > fastype_of t > HOLogic.boolT) $ 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

955 
Free ("a", atomT) $ t; 
18010  956 
val supp_thm = standard (Goal.prove thy8 [] [] 
17872
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

957 
(HOLogic.mk_Trueprop (HOLogic.mk_eq 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

958 
(supp c, 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

959 
if null dts then Const ("{}", HOLogic.mk_setT atomT) 
18010  960 
else foldr1 (HOLogic.mk_binop "op Un") (map supp args2)))) 
17872
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

961 
(fn _ => 
18010  962 
simp_tac (HOL_basic_ss addsimps (supp_def :: 
17872
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

963 
Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un :: 
17874
8be65cf94d2e
Improved proof of injectivity theorems to make it work on
berghofe
parents:
17873
diff
changeset

964 
symmetric empty_def :: Finites.emptyI :: simp_thms @ 
18010  965 
abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1)) 
17872
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

966 
in 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

967 
(supp_thm, 
18010  968 
standard (Goal.prove thy8 [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq 
17872
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

969 
(fresh c, 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

970 
if null dts then HOLogic.true_const 
18010  971 
else foldr1 HOLogic.mk_conj (map fresh args2)))) 
17872
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

972 
(fn _ => 
18010  973 
simp_tac (simpset_of thy8 addsimps [fresh_def, supp_thm]) 1))) 
17872
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

974 
end) atoms) constrs) 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

975 
end) (List.take (descr, length new_type_names) ~~ new_type_names ~~ inject_thms ~~ perm_simps'))); 
f08fc98a164a
Implemented proofs for support and freshness theorems.
berghofe
parents:
17870
diff
changeset

976 

18107
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

977 
(**** weak induction theorem ****) 
18016  978 

18107
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

979 
val arities = get_arities descr''; 
18016  980 

981 
fun mk_funs_inv thm = 

982 
let 

983 
val {sign, prop, ...} = rep_thm thm; 

984 
val _ $ (_ $ (Const (_, Type (_, [U, _])) $ _ $ S)) $ 

985 
(_ $ (_ $ (r $ (a $ _)) $ _)) = Type.freeze prop; 

986 
val used = add_term_tfree_names (a, []); 

987 

988 
fun mk_thm i = 

989 
let 

990 
val Ts = map (TFree o rpair HOLogic.typeS) 

991 
(variantlist (replicate i "'t", used)); 

992 
val f = Free ("f", Ts > U) 

993 
in standard (Goal.prove sign [] [] (Logic.mk_implies 

994 
(HOLogic.mk_Trueprop (HOLogic.list_all 

995 
(map (pair "x") Ts, HOLogic.mk_mem (app_bnds f i, S))), 

996 
HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts, 

997 
r $ (a $ app_bnds f i)), f)))) 

998 
(fn _ => EVERY [REPEAT (rtac ext 1), REPEAT (etac allE 1), rtac thm 1, atac 1])) 

999 
end 

1000 
in map (fn r => r RS subst) (thm :: map mk_thm arities) end; 

1001 

1002 
fun mk_indrule_lemma ((prems, concls), (((i, _), T), U)) = 

1003 
let 

1004 
val Rep_t = Const (List.nth (rep_names, i), T > U) $ 

1005 
mk_Free "x" T i; 

1006 

1007 
val Abs_t = Const (List.nth (abs_names, i), U > T) 

1008 

1009 
in (prems @ [HOLogic.imp $ HOLogic.mk_mem (Rep_t, 

1010 
Const (List.nth (rep_set_names, i), HOLogic.mk_setT U)) $ 

1011 
(mk_Free "P" (T > HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))], 

1012 
concls @ [mk_Free "P" (T > HOLogic.boolT) (i + 1) $ mk_Free "x" T i]) 

1013 
end; 

1014 

1015 
val (indrule_lemma_prems, indrule_lemma_concls) = 

18107
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1016 
Library.foldl mk_indrule_lemma (([], []), (descr'' ~~ recTs ~~ recTs')); 
18016  1017 

1018 
val indrule_lemma = standard (Goal.prove thy8 [] [] 

1019 
(Logic.mk_implies 

1020 
(HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems), 

1021 
HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls))) (fn _ => EVERY 

1022 
[REPEAT (etac conjE 1), 

1023 
REPEAT (EVERY 

1024 
[TRY (rtac conjI 1), full_simp_tac (HOL_basic_ss addsimps Rep_inverse_thms) 1, 

1025 
etac mp 1, resolve_tac Rep_thms 1])])); 

1026 

1027 
val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule_lemma))); 

1028 
val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else 

1029 
map (Free o apfst fst o dest_Var) Ps; 

1030 
val indrule_lemma' = cterm_instantiate 

1031 
(map (cterm_of thy8) Ps ~~ map (cterm_of thy8) frees) indrule_lemma; 

1032 

1033 
val Abs_inverse_thms' = List.concat (map mk_funs_inv Abs_inverse_thms); 

1034 

1035 
val dt_induct_prop = DatatypeProp.make_ind descr' sorts'; 

1036 
val dt_induct = standard (Goal.prove thy8 [] 

1037 
(Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop) 

1038 
(fn prems => EVERY 

1039 
[rtac indrule_lemma' 1, 

1040 
(DatatypeAux.indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1, 

1041 
EVERY (map (fn (prem, r) => (EVERY 

1042 
[REPEAT (eresolve_tac Abs_inverse_thms' 1), 

1043 
simp_tac (HOL_basic_ss addsimps [symmetric r]) 1, 

1044 
DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)])) 

1045 
(prems ~~ constr_defs))])); 

1046 

18107
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1047 
val case_names_induct = mk_case_names_induct descr''; 
18016  1048 

18066
d1e47ee13070
Added code for proving that new datatype has finite support.
berghofe
parents:
18054
diff
changeset

1049 
(**** prove that new datatypes have finite support ****) 
d1e47ee13070
Added code for proving that new datatype has finite support.
berghofe
parents:
18054
diff
changeset

1050 

18246
676d2e625d98
added fsub.thy (poplmark challenge) to the examples
urbanc
parents:
18245
diff
changeset

1051 
val _ = warning "proving finite support for the new datatype"; 
676d2e625d98
added fsub.thy (poplmark challenge) to the examples
urbanc
parents:
18245
diff
changeset

1052 

18066
d1e47ee13070
Added code for proving that new datatype has finite support.
berghofe
parents:
18054
diff
changeset

1053 
val indnames = DatatypeProp.make_tnames recTs; 
d1e47ee13070
Added code for proving that new datatype has finite support.
berghofe
parents:
18054
diff
changeset

1054 

d1e47ee13070
Added code for proving that new datatype has finite support.
berghofe
parents:
18054
diff
changeset

1055 
val abs_supp = PureThy.get_thms thy8 (Name "abs_supp"); 
18067  1056 
val supp_atm = PureThy.get_thms thy8 (Name "supp_atm"); 
18066
d1e47ee13070
Added code for proving that new datatype has finite support.
berghofe
parents:
18054
diff
changeset

1057 

d1e47ee13070
Added code for proving that new datatype has finite support.
berghofe
parents:
18054
diff
changeset

1058 
val finite_supp_thms = map (fn atom => 
d1e47ee13070
Added code for proving that new datatype has finite support.
berghofe
parents:
18054
diff
changeset

1059 
let val atomT = Type (atom, []) 
d1e47ee13070
Added code for proving that new datatype has finite support.
berghofe
parents:
18054
diff
changeset

1060 
in map standard (List.take 
d1e47ee13070
Added code for proving that new datatype has finite support.
berghofe
parents:
18054
diff
changeset

1061 
(split_conj_thm (Goal.prove thy8 [] [] (HOLogic.mk_Trueprop 
d1e47ee13070
Added code for proving that new datatype has finite support.
berghofe
parents:
18054
diff
changeset

1062 
(foldr1 HOLogic.mk_conj (map (fn (s, T) => HOLogic.mk_mem 
d1e47ee13070
Added code for proving that new datatype has finite support.
berghofe
parents:
18054
diff
changeset

1063 
(Const ("nominal.supp", T > HOLogic.mk_setT atomT) $ Free (s, T), 
d1e47ee13070
Added code for proving that new datatype has finite support.
berghofe
parents:
18054
diff
changeset

1064 
Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT atomT)))) 
d1e47ee13070
Added code for proving that new datatype has finite support.
berghofe
parents:
18054
diff
changeset

1065 
(indnames ~~ recTs)))) 
d1e47ee13070
Added code for proving that new datatype has finite support.
berghofe
parents:
18054
diff
changeset

1066 
(fn _ => indtac dt_induct indnames 1 THEN 
d1e47ee13070
Added code for proving that new datatype has finite support.
berghofe
parents:
18054
diff
changeset

1067 
ALLGOALS (asm_full_simp_tac (simpset_of thy8 addsimps 
18067  1068 
(abs_supp @ supp_atm @ 
18066
d1e47ee13070
Added code for proving that new datatype has finite support.
berghofe
parents:
18054
diff
changeset

1069 
PureThy.get_thms thy8 (Name ("fs_" ^ Sign.base_name atom ^ "1")) @ 
d1e47ee13070
Added code for proving that new datatype has finite support.
berghofe
parents:
18054
diff
changeset

1070 
List.concat supp_thms))))), 
d1e47ee13070
Added code for proving that new datatype has finite support.
berghofe
parents:
18054
diff
changeset

1071 
length new_type_names)) 
d1e47ee13070
Added code for proving that new datatype has finite support.
berghofe
parents:
18054
diff
changeset

1072 
end) atoms; 
d1e47ee13070
Added code for proving that new datatype has finite support.
berghofe
parents:
18054
diff
changeset

1073 

18759  1074 
val simp_atts = replicate (length new_type_names) [Simplifier.simp_add]; 
18658  1075 

1076 
val (_, thy9) = thy8 > 

1077 
Theory.add_path big_name > 

1078 
PureThy.add_thms [(("induct_weak", dt_induct), [case_names_induct])] >> 

1079 
PureThy.add_thmss [(("inducts_weak", projections dt_induct), [case_names_induct])] > 

1080 
Theory.parent_path >> 

1081 
DatatypeAux.store_thmss_atts "distinct" new_type_names simp_atts distinct_thms >> 

1082 
DatatypeAux.store_thmss "constr_rep" new_type_names constr_rep_thmss >> 

1083 
DatatypeAux.store_thmss_atts "perm" new_type_names simp_atts perm_simps' >> 

1084 
DatatypeAux.store_thmss "inject" new_type_names inject_thms >> 

1085 
DatatypeAux.store_thmss "supp" new_type_names supp_thms >> 

1086 
DatatypeAux.store_thmss_atts "fresh" new_type_names simp_atts fresh_thms > 

1087 
fold (fn (atom, ths) => fn thy => 

1088 
let val class = Sign.intern_class thy ("fs_" ^ Sign.base_name atom) 

19275  1089 
in fold (fn T => AxClass.prove_arity 
18658  1090 
(fst (dest_Type T), 
1091 
replicate (length sorts) [class], [class]) 

19133
7e84a1a3741c
Adapted to Florian's recent changes to the AxClass package.
berghofe
parents:
18759
diff
changeset

1092 
(ClassPackage.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy 
18658  1093 
end) (atoms ~~ finite_supp_thms); 
1094 

18107
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1095 
(**** strong induction theorem ****) 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1096 

ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1097 
val pnames = if length descr'' = 1 then ["P"] 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1098 
else map (fn i => "P" ^ string_of_int i) (1 upto length descr''); 
18245
65e60434b3c2
Fixed problem with strong induction theorem for datatypes containing
berghofe
parents:
18142
diff
changeset

1099 
val ind_sort = if null dt_atomTs then HOLogic.typeS 
18658  1100 
else norm_sort thy9 (map (fn T => Sign.intern_class thy9 ("fs_" ^ 
1101 
Sign.base_name (fst (dest_Type T)))) dt_atomTs); 

18107
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1102 
val fsT = TFree ("'n", ind_sort); 
18658  1103 
val fsT' = TFree ("'n", HOLogic.typeS); 
18107
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1104 

18658  1105 
val fresh_fs = map (fn (s, T) => (T, Free (s, fsT' > HOLogic.mk_setT T))) 
1106 
(DatatypeProp.indexify_names (replicate (length dt_atomTs) "f") ~~ dt_atomTs); 

1107 

1108 
fun make_pred fsT i T = 

18302
577e5d19b33c
Changed order of predicate arguments and quantifiers in strong induction rule.
berghofe
parents:
18280
diff
changeset

1109 
Free (List.nth (pnames, i), fsT > T > HOLogic.boolT); 
18107
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1110 

18658  1111 
fun make_ind_prem fsT f k T ((cname, cargs), idxs) = 
18107
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1112 
let 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1113 
val recs = List.filter is_rec_type cargs; 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1114 
val Ts = map (typ_of_dtyp descr'' sorts') cargs; 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1115 
val recTs' = map (typ_of_dtyp descr'' sorts') recs; 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1116 
val tnames = variantlist (DatatypeProp.make_tnames Ts, pnames); 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1117 
val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs)); 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1118 
val frees = tnames ~~ Ts; 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1119 
val z = (variant tnames "z", fsT); 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1120 

ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1121 
fun mk_prem ((dt, s), T) = 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1122 
let 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1123 
val (Us, U) = strip_type T; 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1124 
val l = length Us 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1125 
in list_all (z :: map (pair "x") Us, HOLogic.mk_Trueprop 
18658  1126 
(make_pred fsT (body_index dt) U $ Bound l $ app_bnds (Free (s, T)) l)) 
18107
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1127 
end; 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1128 

ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1129 
val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs'); 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1130 
val prems' = map (fn p as (_, T) => HOLogic.mk_Trueprop 
18658  1131 
(f T (Free p) (Free z))) 
18107
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1132 
(map (curry List.nth frees) (List.concat (map (fn (m, n) => 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1133 
m upto m + n  1) idxs))) 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1134 

18302
577e5d19b33c
Changed order of predicate arguments and quantifiers in strong induction rule.
berghofe
parents:
18280
diff
changeset

1135 
in list_all_free (frees @ [z], Logic.list_implies (prems' @ prems, 
18658  1136 
HOLogic.mk_Trueprop (make_pred fsT k T $ Free z $ 
18302
577e5d19b33c
Changed order of predicate arguments and quantifiers in strong induction rule.
berghofe
parents:
18280
diff
changeset

1137 
list_comb (Const (cname, Ts > T), map Free frees)))) 
18107
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1138 
end; 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1139 

ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1140 
val ind_prems = List.concat (map (fn (((i, (_, _, constrs)), (_, idxss)), T) => 
18658  1141 
map (make_ind_prem fsT (fn T => fn t => fn u => 
1142 
Const ("nominal.fresh", T > fsT > HOLogic.boolT) $ t $ u) i T) 

1143 
(constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs)); 

18107
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1144 
val tnames = DatatypeProp.make_tnames recTs; 
18658  1145 
val zs = variantlist (replicate (length descr'') "z", tnames); 
18107
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1146 
val ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &") 
18658  1147 
(map (fn ((((i, _), T), tname), z) => 
1148 
make_pred fsT i T $ Free (z, fsT) $ Free (tname, T)) 

1149 
(descr'' ~~ recTs ~~ tnames ~~ zs))); 

18107
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1150 
val induct = Logic.list_implies (ind_prems, ind_concl); 
ee6b4d3af498
Added strong induction theorem (currently only axiomatized!).
berghofe
parents:
18104
diff
changeset

1151 

18658  1152 
val ind_prems' = 
1153 
map (fn (_, f as Free (_, T)) => list_all_free ([("x", fsT')], 

1154 
HOLogic.mk_Trueprop (HOLogic.mk_mem (f $ Free ("x", fsT'), 

1155 
Const ("Finite_Set.Finites", HOLogic.mk_setT (body_type T)))))) fresh_fs @ 

1156 
List.concat (map (fn (((i, (_, _, constrs)), (_, idxss)), T) => 

1157 
map (make_ind_prem fsT' (fn T => fn t => fn u => HOLogic.Not $ 

1158 
HOLogic.mk_mem (t, the (AList.lookup op = fresh_fs T) $ u)) i T) 

1159 
(constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs)); 

1160 
val ind_concl' = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &") 

1161 
(map (fn ((((i, _), T), tname), z) => 

1162 
make_pred fsT' i T $ Free (z, fsT') $ Free (tname, T)) 

1163 
(descr'' ~~ recTs ~~ tnames ~~ zs))); 

1164 
val induct' = Logic.list_implies (ind_prems', ind_concl'); 

1165 

1166 
fun mk_perm Ts (t, u) = 

1167 
let 

1168 
val T = fastype_of1 (Ts, t); 

1169 
val U = fastype_of1 (Ts, u) 

1170 
in Const ("nominal.perm", T > U > U) $ t $ u end; 

1171 

1172 
val aux_ind_vars = 

1173 
(DatatypeProp.indexify_names (replicate (length dt_atomTs) "pi") ~~ 

1174 
map mk_permT dt_atomTs) @ [("z", fsT')]; 

1175 
val aux_ind_Ts = rev (map snd aux_ind_vars); 

1176 
val aux_ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &") 

1177 
(map (fn (((i, _), T), tname) => 

1178 
HOLogic.list_all (aux_ind_vars, make_pred fsT' i T $ Bound 0 $ 

1179 
foldr (mk_perm aux_ind_Ts) (Free (tname, T)) 

1180 
(map Bound (length dt_atomTs downto 1)))) 

1181 
(descr'' ~~ recTs ~~ tnames))); 

1182 

1183 
fun mk_ind_perm i k p l vs j = 

1184 
let 

1185 
val n = length vs; 

1186 
val Ts = map snd vs; 

1187 
val T = List.nth (Ts, i  j); 

1188 
val pT = NominalAtoms.mk_permT T 

1189 
in 

1190 
Const ("List.list.Cons", HOLogic.mk_prodT (T, T) > pT > pT) $ 

1191 
(HOLogic.pair_const T T $ Bound (l  j) $ foldr (mk_perm Ts) 

1192 
(Bound (i  j)) 

1193 
(map (mk_ind_perm i k p l vs) (j  1 downto 0) @ 

1194 
map Bound (n  k  1 downto n  k  p))) $ 

1195 
Const ("List.list.Nil", pT) 

1196 
end; 

1197 

1198 
fun mk_fresh i i' j k p l vs _ _ = 

1199 
let 

1200 
val n = length vs; 

1201 
val Ts = map snd vs; 

1202 
val T = List.nth (Ts, n  i  1  j); 

1203 
val f = the (AList.lookup op = fresh_fs T); 

1204 
val U = List.nth (Ts, n  i'  1); 

1205 
val S = HOLogic.mk_setT T; 

1206 
val prms = map (mk_ind_perm (n  i) k p (n  l) (("a", T) :: vs)) 

1207 
(j  1 downto 0) @ 

1208 
map Bound (n  k downto n  k  p + 1) 

1209 
in 

1210 
HOLogic.mk_Trueprop (Const ("Ex", (T > HOLogic.boolT) > HOLogic.boolT) $ 

1211 
Abs ("a", T, HOLogic.Not $ 

1212 
(Const ("op :", T > S > HOLogic.boolT) $ Bound 0 $ 

1213 
(Const ("insert", T > S > S) $ 

1214 
(foldr (mk_perm (T :: Ts)) (Bound (n  i  j)) prms) $ 

1215 
(Const ("op Un", S > S > S) $ (f $ Bound (n  k  p)) $ 

1216 
(Const ("nominal.supp", U > S) $ 

1217 
foldr (mk_perm (T :: Ts)) (Bound (n  i')) prms)))))) 

1218 
end; 

18104
dbe58b104cb9
added thms perm, distinct and fresh to the simplifier.
urbanc
parents:
18068
diff
changeset

1219 

18658  1220 
fun mk_fresh_constr is p vs _ concl = 
1221 
let 

1222 
val n = length vs; 

1223 
val Ts = map snd vs; 

1224 
val _ $ (_ $ _ $ t) = concl; 

1225 
val c = head_of t; 

1226 
val T = body_type (fastype_of c); 

1227 
val k = foldr op + 0 (map (fn (_, i) => i + 1) is); 

1228 
val ps = map Bound (n  k  1 downto n  k  p); 

1229 
val (_, _, ts, us) = foldl (fn ((_, i), (m, n, ts, us)) => 

1230 
(m  i  1, n  i, 

1231 
ts @ map Bound (n downto n  i + 1) @ 

1232 
[foldr (mk_perm Ts) (Bound (m  i)) 

1233 
(map (mk_ind_perm m k p n vs) (i  1 downto 0) @ ps)], 

1234 
us @ map (fn j => foldr (mk_perm Ts) (Bound j) ps) (m downto m  i))) 

1235 
(n  1, n  k  p  2, [], []) is 

1236 
in 

1237 
HOLogic.mk_Trueprop (HOLogic.eq_const T $ list_comb (c, ts) $ list_comb (c, us)) 

1238 
end; 

1239 

1240 
val abs_fun_finite_supp = PureThy.get_thm thy9 (Name "abs_fun_finite_supp"); 

1241 

1242 
val at_finite_select = PureThy.get_thm thy9 (Name "at_finite_select"); 

1243 

1244 
val induct_aux_lemmas = List.concat (map (fn Type (s, _) => 

1245 
[PureThy.get_thm thy9 (Name ("pt_" ^ Sign.base_name s ^ "_inst")), 

1246 
PureThy.get_thm thy9 (Name ("fs_" ^ Sign.base_name s ^ "1")), 

1247 
PureThy.get_thm thy9 (Name ("at_" ^ Sign.base_name s ^ "_inst"))]) dt_atomTs); 

1248 

1249 
val induct_aux_lemmas' = map (fn Type (s, _) => 

1250 
PureThy.get_thm thy9 (Name ("pt_" ^ Sign.base_name s ^ "2")) RS sym) dt_atomTs; 

1251 

1252 
val induct_aux = standard (Goal.prove thy9 [] ind_prems' ind_concl' 

1253 
(fn prems => EVERY 

1254 
([mk_subgoal 1 (K (K (K aux_ind_concl))), 

1255 
indtac dt_induct tnames 1] @ 

1256 
List.concat (map (fn ((_, (_, _, constrs)), (_, constrs')) => 

1257 
List.concat (map (fn ((cname, cargs), is) => 

1258 
[simp_tac (HOL_basic_ss addsimps List.concat perm_simps') 1, 

1259 
REPEAT (rtac allI 1)] @ 

1260 
List.concat (map 

1261 
(fn ((_, 0), _) => [] 

1262 
 ((i, j), k) => List.concat (map (fn j' => 

1263 
let 

1264 
val DtType (tname, _) = List.nth (cargs, i + j'); 

1265 
val atom = Sign.base_name tname 

1266 
in 

1267 
[mk_subgoal 1 (mk_fresh i (i + j) j' 

1268 
(length cargs) (length dt_atomTs) 

1269 
(length cargs + length dt_atomTs + 1 + i  k)), 

1270 
rtac at_finite_select 1, 

1271 
rtac (PureThy.get_thm thy9 (Name ("at_" ^ atom ^ "_inst"))) 1, 

1272 
asm_full_simp_tac (simpset_of thy9 addsimps 

1273 
[PureThy.get_thm thy9 (Name ("fs_" ^ atom ^ "1"))]) 1, 

1274 
resolve_tac prems 1, 

1275 
etac exE 1, 

1276 
asm_full_simp_tac (simpset_of thy9 addsimps 

1277 
[symmetric fresh_def]) 1] 

1278 
end) (0 upto j  1))) (is ~~ (0 upto length is  1))) @ 

1279 
(if exists (not o equal 0 o snd) is then 

1280 
[mk_subgoal 1 (mk_fresh_constr is (length dt_atomTs)), 

1281 
asm_full_simp_tac (simpset_of thy9 addsimps 

1282 
(List.concat inject_thms @ 

1283 
alpha @ abs_perm @ abs_fresh @ [abs_fun_finite_supp] @ 

1284 
induct_aux_lemmas)) 1, 

1285 
dtac sym 1, 

1286 
asm_full_simp_tac (simpset_of thy9 

1287 
addsimps induct_aux_lemmas' 

1288 
addsimprocs [perm_simproc]) 1, 

1289 
REPEAT (etac conjE 1)] 

1290 
else 

1291 
[]) @ 

1292 
[(resolve_tac prems THEN_ALL_NEW 

1293 
(atac ORELSE' ((REPEAT o etac allE) THEN' atac))) 1]) 

1294 
(constrs ~~ constrs'))) (descr'' ~~ ndescr)) @ 

1295 
[REPEAT (eresolve_tac [conjE, allE_Nil] 1), 

1296 
REPEAT (etac allE 1), 

1297 
REPEAT (TRY (rtac conjI 1) THEN asm_full_simp_tac (simpset_of thy9) 1)]))); 

1298 

1299 
val induct_aux' = Thm.instantiate ([], 

1300 
map (fn (s, T) => 

1301 
let val pT = TVar (("'n", 0), HOLogic.typeS) > T > HOLogic.boolT 

1302 
in (cterm_of thy9 (Var ((s, 0), pT)), cterm_of thy9 (Free (s, pT))) end) 

1303 
(pnames ~~ recTs) @ 

1304 
map (fn (_, f) => 

1305 
let val f' = Logic.varify f 

1306 
in (cterm_of thy9 f', 

1307 
cterm_of thy9 (Const ("nominal.supp", fastype_of f'))) 

1308 
end) fresh_fs) induct_aux; 

1309 

1310 
val induct = standard (Goal.prove thy9 [] ind_prems ind_concl 

1311 
(fn prems => EVERY 

1312 
[rtac induct_aux' 1, 

1313 
REPEAT (resolve_tac induct_aux_lemmas 1), 

1314 
REPEAT ((resolve_tac prems THEN_ALL_NEW 

1315 
(etac meta_spec ORELSE' full_simp_tac (HOL_basic_ss addsimps [fresh_def]))) 1)])) 

1316 

1317 
val (_, thy10) = thy9 > 

18016  1318 
Theory.add_path big_name > 
18658  1319 
PureThy.add_thms [(("induct'", induct_aux), [])] >> 
1320 
PureThy.add_thms [(("induct", induct), [case_names_induct])] >> 

1321 
PureThy.add_thmss [(("inducts", projections induct), [case_names_induct])] > 

1322 
Theory.parent_path; 

1323 

19251
6bc0dda66f32
First version of function for defining graph of iteration combinator.
berghofe
parents:
19134
diff
changeset

1324 
(**** iteration combinator ****) 
6bc0dda66f32
First version of function for defining graph of iteration combinator.
berghofe
parents:
19134
diff
changeset

1325 

6bc0dda66f32
First version of function for defining graph of iteration combinator.
berghofe
parents:
19134
diff
changeset

1326 
val _ = warning "defining iteration combinator ..."; 
6bc0dda66f32
First version of function for defining graph of iteration combinator.
berghofe
parents:
19134
diff
changeset

1327 

6bc0dda66f32
First version of function for defining graph of iteration combinator.
berghofe
parents:
19134
diff
changeset

1328 
val used = foldr add_typ_tfree_names [] recTs; 
6bc0dda66f32
First version of function for defining graph of iteration combinator.
berghofe
parents:
19134
diff
changeset

1329 
val rec_result_Ts = map TFree (variantlist (replicate (length descr'') "'t", used) ~~ 
6bc0dda66f32
First version of function for defining graph of iteration combinator.
berghofe
parents:
19134
diff
changeset

1330 
replicate (length descr'') HOLogic.typeS); 
6bc0dda66f32
First version of function for defining graph of iteration combinator.
berghofe
parents:
19134
diff
changeset

1331 

6bc0dda66f32
First version of function for defining graph of iteration combinator.
berghofe
parents:
19134
diff
changeset

1332 
val iter_fn_Ts = List.concat (map (fn (i, (_, _, constrs)) => 
6bc0dda66f32
First version of function for defining graph of 