17 |
17 |
18 nominal_datatype ty2 = |
18 nominal_datatype ty2 = |
19 Var2 "name" |
19 Var2 "name" |
20 | Fun2 "ty2" "ty2" |
20 | Fun2 "ty2" "ty2" |
21 |
21 |
22 |
|
23 nominal_datatype tys2 = |
22 nominal_datatype tys2 = |
24 All2 xs::"name fset" ty::"ty2" bind (res) xs in ty |
23 All2 xs::"name fset" ty::"ty2" bind (res) xs in ty |
25 |
24 |
26 |
25 |
27 lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp] |
26 (* |
28 |
|
29 |
|
30 |
|
31 (* below we define manually the function for size *) |
|
32 |
|
33 lemma size_eqvt_raw: |
|
34 "size (pi \<bullet> t :: ty_raw) = size t" |
|
35 "size (pi \<bullet> ts :: tys_raw) = size ts" |
|
36 apply (induct rule: ty_raw_tys_raw.inducts) |
|
37 apply simp_all |
|
38 done |
|
39 |
|
40 instantiation ty and tys :: size |
|
41 begin |
|
42 |
|
43 quotient_definition |
|
44 "size_ty :: ty \<Rightarrow> nat" |
|
45 is |
|
46 "size :: ty_raw \<Rightarrow> nat" |
|
47 |
|
48 quotient_definition |
|
49 "size_tys :: tys \<Rightarrow> nat" |
|
50 is |
|
51 "size :: tys_raw \<Rightarrow> nat" |
|
52 |
|
53 lemma size_rsp: |
|
54 "alpha_ty_raw x y \<Longrightarrow> size x = size y" |
|
55 "alpha_tys_raw a b \<Longrightarrow> size a = size b" |
|
56 apply (induct rule: alpha_ty_raw_alpha_tys_raw.inducts) |
|
57 apply (simp_all only: ty_raw_tys_raw.size) |
|
58 apply (simp_all only: alphas) |
|
59 apply clarify |
|
60 apply (simp_all only: size_eqvt_raw) |
|
61 done |
|
62 |
|
63 lemma [quot_respect]: |
|
64 "(alpha_ty_raw ===> op =) size size" |
|
65 "(alpha_tys_raw ===> op =) size size" |
|
66 by (simp_all add: size_rsp) |
|
67 |
|
68 lemma [quot_preserve]: |
|
69 "(rep_ty ---> id) size = size" |
|
70 "(rep_tys ---> id) size = size" |
|
71 by (simp_all add: size_ty_def size_tys_def) |
|
72 |
|
73 instance |
|
74 by default |
|
75 |
|
76 end |
|
77 |
|
78 thm ty_raw_tys_raw.size(4)[quot_lifted] |
|
79 thm ty_raw_tys_raw.size(5)[quot_lifted] |
|
80 thm ty_raw_tys_raw.size(6)[quot_lifted] |
|
81 |
|
82 |
|
83 thm ty_tys.fv |
|
84 thm ty_tys.eq_iff |
|
85 thm ty_tys.bn |
|
86 thm ty_tys.perm |
|
87 thm ty_tys.inducts |
|
88 thm ty_tys.distinct |
|
89 |
|
90 ML {* Sign.of_sort @{theory} (@{typ ty}, @{sort fs}) *} |
27 ML {* Sign.of_sort @{theory} (@{typ ty}, @{sort fs}) *} |
91 |
28 |
92 lemma strong_induct: |
29 lemma strong_induct: |
93 assumes a1: "\<And>name b. P b (Var name)" |
30 assumes a1: "\<And>name b. P b (Var name)" |
94 and a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)" |
31 and a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)" |