|
1 theory TypeSchemes |
|
2 imports "../Parser" |
|
3 begin |
|
4 |
|
5 section {*** Type Schemes ***} |
|
6 |
|
7 atom_decl name |
|
8 |
|
9 ML {* val _ = alpha_type := AlphaRes *} |
|
10 |
|
11 nominal_datatype ty = |
|
12 Var "name" |
|
13 | Fun "ty" "ty" |
|
14 and tys = |
|
15 All xs::"name fset" ty::"ty" bind xs in ty |
|
16 |
|
17 lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp] |
|
18 |
|
19 (* below we define manually the function for size *) |
|
20 |
|
21 lemma size_eqvt_raw: |
|
22 "size (pi \<bullet> t :: ty_raw) = size t" |
|
23 "size (pi \<bullet> ts :: tys_raw) = size ts" |
|
24 apply (induct rule: ty_raw_tys_raw.inducts) |
|
25 apply simp_all |
|
26 done |
|
27 |
|
28 instantiation ty and tys :: size |
|
29 begin |
|
30 |
|
31 quotient_definition |
|
32 "size_ty :: ty \<Rightarrow> nat" |
|
33 is |
|
34 "size :: ty_raw \<Rightarrow> nat" |
|
35 |
|
36 quotient_definition |
|
37 "size_tys :: tys \<Rightarrow> nat" |
|
38 is |
|
39 "size :: tys_raw \<Rightarrow> nat" |
|
40 |
|
41 lemma size_rsp: |
|
42 "alpha_ty_raw x y \<Longrightarrow> size x = size y" |
|
43 "alpha_tys_raw a b \<Longrightarrow> size a = size b" |
|
44 apply (induct rule: alpha_ty_raw_alpha_tys_raw.inducts) |
|
45 apply (simp_all only: ty_raw_tys_raw.size) |
|
46 apply (simp_all only: alphas) |
|
47 apply clarify |
|
48 apply (simp_all only: size_eqvt_raw) |
|
49 done |
|
50 |
|
51 lemma [quot_respect]: |
|
52 "(alpha_ty_raw ===> op =) size size" |
|
53 "(alpha_tys_raw ===> op =) size size" |
|
54 by (simp_all add: size_rsp) |
|
55 |
|
56 lemma [quot_preserve]: |
|
57 "(rep_ty ---> id) size = size" |
|
58 "(rep_tys ---> id) size = size" |
|
59 by (simp_all add: size_ty_def size_tys_def) |
|
60 |
|
61 instance |
|
62 by default |
|
63 |
|
64 end |
|
65 |
|
66 thm ty_raw_tys_raw.size(4)[quot_lifted] |
|
67 thm ty_raw_tys_raw.size(5)[quot_lifted] |
|
68 thm ty_raw_tys_raw.size(6)[quot_lifted] |
|
69 |
|
70 |
|
71 thm ty_tys.fv |
|
72 thm ty_tys.eq_iff |
|
73 thm ty_tys.bn |
|
74 thm ty_tys.perm |
|
75 thm ty_tys.inducts |
|
76 thm ty_tys.distinct |
|
77 |
|
78 ML {* Sign.of_sort @{theory} (@{typ ty}, @{sort fs}) *} |
|
79 |
|
80 lemma strong_induct: |
|
81 assumes a1: "\<And>name b. P b (Var name)" |
|
82 and a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)" |
|
83 and a3: "\<And>fset t b. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)" |
|
84 shows "P (a :: 'a :: pt) t \<and> P' (d :: 'b :: {fs}) ts " |
|
85 proof - |
|
86 have " (\<forall>p a. P a (p \<bullet> t)) \<and> (\<forall>p d. P' d (p \<bullet> ts))" |
|
87 apply (rule ty_tys.induct) |
|
88 apply (simp add: a1) |
|
89 apply (simp) |
|
90 apply (rule allI)+ |
|
91 apply (rule a2) |
|
92 apply simp |
|
93 apply simp |
|
94 apply (rule allI) |
|
95 apply (rule allI) |
|
96 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (fset_to_set (fmap atom (p \<bullet> fset)))) \<sharp>* d \<and> supp (p \<bullet> All fset ty) \<sharp>* pa)") |
|
97 apply clarify |
|
98 apply(rule_tac t="p \<bullet> All fset ty" and |
|
99 s="pa \<bullet> (p \<bullet> All fset ty)" in subst) |
|
100 apply (rule supp_perm_eq) |
|
101 apply assumption |
|
102 apply (simp only: ty_tys.perm) |
|
103 apply (rule a3) |
|
104 apply(erule_tac x="(pa + p)" in allE) |
|
105 apply simp |
|
106 apply (simp add: eqvts eqvts_raw) |
|
107 apply (rule at_set_avoiding2) |
|
108 apply (simp add: fin_fset_to_set) |
|
109 apply (simp add: finite_supp) |
|
110 apply (simp add: eqvts finite_supp) |
|
111 apply (subst atom_eqvt_raw[symmetric]) |
|
112 apply (subst fmap_eqvt[symmetric]) |
|
113 apply (subst fset_to_set_eqvt[symmetric]) |
|
114 apply (simp only: fresh_star_permute_iff) |
|
115 apply (simp add: fresh_star_def) |
|
116 apply clarify |
|
117 apply (simp add: fresh_def) |
|
118 apply (simp add: ty_tys_supp) |
|
119 done |
|
120 then have "P a (0 \<bullet> t) \<and> P' d (0 \<bullet> ts)" by blast |
|
121 then show ?thesis by simp |
|
122 qed |
|
123 |
|
124 lemma |
|
125 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))" |
|
126 apply(simp add: ty_tys.eq_iff) |
|
127 apply(rule_tac x="0::perm" in exI) |
|
128 apply(simp add: alphas) |
|
129 apply(simp add: fresh_star_def fresh_zero_perm) |
|
130 done |
|
131 |
|
132 lemma |
|
133 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))" |
|
134 apply(simp add: ty_tys.eq_iff) |
|
135 apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI) |
|
136 apply(simp add: alphas fresh_star_def eqvts) |
|
137 done |
|
138 |
|
139 lemma |
|
140 shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))" |
|
141 apply(simp add: ty_tys.eq_iff) |
|
142 apply(rule_tac x="0::perm" in exI) |
|
143 apply(simp add: alphas fresh_star_def eqvts ty_tys.eq_iff) |
|
144 done |
|
145 |
|
146 lemma |
|
147 assumes a: "a \<noteq> b" |
|
148 shows "\<not>(All {|a, b|} (Fun (Var a) (Var b)) = All {|c|} (Fun (Var c) (Var c)))" |
|
149 using a |
|
150 apply(simp add: ty_tys.eq_iff) |
|
151 apply(clarify) |
|
152 apply(simp add: alphas fresh_star_def eqvts ty_tys.eq_iff) |
|
153 apply auto |
|
154 done |
|
155 |
|
156 (* PROBLEM: |
|
157 Type schemes with separate datatypes |
|
158 |
|
159 nominal_datatype T = |
|
160 TVar "name" |
|
161 | TFun "T" "T" |
|
162 nominal_datatype TyS = |
|
163 TAll xs::"name list" ty::"T" bind xs in ty |
|
164 |
|
165 *** exception Datatype raised |
|
166 *** (line 218 of "/usr/local/src/Isabelle_16-Mar-2010/src/HOL/Tools/Datatype/datatype_aux.ML") |
|
167 *** At command "nominal_datatype". |
|
168 *) |
|
169 |
|
170 |
|
171 end |