1 theory TypeSchemes2 |
|
2 imports "../Nominal2" |
|
3 begin |
|
4 |
|
5 section {*** Type Schemes defined as a single nominal datatype ***} |
|
6 |
|
7 atom_decl name |
|
8 |
|
9 nominal_datatype ty = |
|
10 Var "name" |
|
11 | Fun "ty" "ty" |
|
12 and tys = |
|
13 All xs::"name fset" ty::"ty" binds (set+) xs in ty |
|
14 |
|
15 thm ty_tys.distinct |
|
16 thm ty_tys.induct |
|
17 thm ty_tys.inducts |
|
18 thm ty_tys.exhaust |
|
19 thm ty_tys.strong_exhaust |
|
20 thm ty_tys.fv_defs |
|
21 thm ty_tys.bn_defs |
|
22 thm ty_tys.perm_simps |
|
23 thm ty_tys.eq_iff |
|
24 thm ty_tys.fv_bn_eqvt |
|
25 thm ty_tys.size_eqvt |
|
26 thm ty_tys.supports |
|
27 thm ty_tys.supp |
|
28 thm ty_tys.fresh |
|
29 |
|
30 fun |
|
31 lookup :: "(name \<times> ty) list \<Rightarrow> name \<Rightarrow> ty" |
|
32 where |
|
33 "lookup [] Y = Var Y" |
|
34 | "lookup ((X, T) # Ts) Y = (if X = Y then T else lookup Ts Y)" |
|
35 |
|
36 lemma lookup_eqvt[eqvt]: |
|
37 shows "(p \<bullet> lookup Ts T) = lookup (p \<bullet> Ts) (p \<bullet> T)" |
|
38 apply(induct Ts T rule: lookup.induct) |
|
39 apply(simp_all) |
|
40 done |
|
41 |
|
42 lemma TEST1: |
|
43 assumes "x = Inl y" |
|
44 shows "(p \<bullet> Sum_Type.Projl x) = Sum_Type.Projl (p \<bullet> x)" |
|
45 using assms by simp |
|
46 |
|
47 lemma TEST2: |
|
48 assumes "x = Inr y" |
|
49 shows "(p \<bullet> Sum_Type.Projr x) = Sum_Type.Projr (p \<bullet> x)" |
|
50 using assms by simp |
|
51 |
|
52 lemma test: |
|
53 assumes a: "\<exists>y. f x = Inl y" |
|
54 shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl ((p \<bullet> f) (p \<bullet> x))" |
|
55 using a |
|
56 apply clarify |
|
57 apply(frule_tac p="p" in permute_boolI) |
|
58 apply(simp (no_asm_use) only: eqvts) |
|
59 apply(subst (asm) permute_fun_app_eq) |
|
60 back |
|
61 apply(simp) |
|
62 done |
|
63 |
|
64 lemma test2: |
|
65 assumes a: "\<exists>y. f x = Inl y" |
|
66 shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl (p \<bullet> (f x))" |
|
67 using a |
|
68 apply clarify |
|
69 apply(frule_tac p="p" in permute_boolI) |
|
70 apply(simp (no_asm_use) only: eqvts) |
|
71 apply(subst (asm) permute_fun_app_eq) |
|
72 back |
|
73 apply(simp) |
|
74 done |
|
75 |
|
76 nominal_primrec (default "sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)") |
|
77 subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty" |
|
78 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" |
|
79 where |
|
80 "subst \<theta> (Var X) = lookup \<theta> X" |
|
81 | "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)" |
|
82 | "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)" |
|
83 apply(simp add: subst_substs_graph_aux_def eqvt_def) |
|
84 apply(rule TrueI) |
|
85 apply (case_tac x) |
|
86 apply simp apply clarify |
|
87 apply (rule_tac y="b" in ty_tys.exhaust(1)) |
|
88 apply (auto)[1] |
|
89 apply (auto)[1] |
|
90 apply simp apply clarify |
|
91 apply (rule_tac ya="b" and c="a" in ty_tys.strong_exhaust(2)) |
|
92 apply (auto)[1] |
|
93 apply (auto)[5] |
|
94 --"LAST GOAL" |
|
95 apply (simp add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff]) |
|
96 apply (subgoal_tac "eqvt_at (\<lambda>(l, r). subst l r) (\<theta>', T)") |
|
97 apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\<theta>', T))") |
|
98 apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\<theta>', Ta))") |
|
99 prefer 2 |
|
100 apply (simp add: eqvt_at_def subst_def) |
|
101 apply rule |
|
102 apply (subst test2) |
|
103 apply (simp add: subst_substs_sumC_def) |
|
104 apply (simp add: THE_default_def) |
|
105 apply (case_tac "Ex1 (subst_substs_graph (Inl (\<theta>', T)))") |
|
106 prefer 2 |
|
107 apply simp |
|
108 apply (simp add: the1_equality) |
|
109 apply auto[1] |
|
110 apply (erule_tac x="x" in allE) |
|
111 apply simp |
|
112 apply(cases rule: subst_substs_graph.cases) |
|
113 apply assumption |
|
114 apply (rule_tac x="lookup \<theta> X" in exI) |
|
115 apply clarify |
|
116 apply (rule the1_equality) |
|
117 apply blast apply assumption |
|
118 apply (rule_tac x="(Fun (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T1)))) |
|
119 (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T2)))))" in exI) |
|
120 apply clarify |
|
121 apply (rule the1_equality) |
|
122 apply blast apply assumption |
|
123 apply clarify |
|
124 apply simp |
|
125 --"-" |
|
126 apply clarify |
|
127 apply (frule supp_eqvt_at) |
|
128 apply (simp add: finite_supp) |
|
129 apply (erule Abs_res_fcb) |
|
130 apply (simp add: Abs_fresh_iff) |
|
131 apply (simp add: Abs_fresh_iff) |
|
132 apply auto[1] |
|
133 apply (simp add: fresh_def fresh_star_def) |
|
134 apply (erule contra_subsetD) |
|
135 apply (simp add: supp_Pair) |
|
136 apply blast |
|
137 apply clarify |
|
138 apply (simp) |
|
139 apply (simp add: eqvt_at_def) |
|
140 apply (subst Abs_eq_iff) |
|
141 apply (rule_tac x="0::perm" in exI) |
|
142 apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'") |
|
143 apply (simp add: alphas fresh_star_zero) |
|
144 apply (subgoal_tac "\<And>x. x \<in> supp (subst \<theta>' (p \<bullet> T)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset xs \<longleftrightarrow> x \<in> atom ` fset xsa") |
|
145 apply(simp) |
|
146 apply blast |
|
147 apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> T)") |
|
148 apply (simp add: supp_Pair eqvts eqvts_raw) |
|
149 apply auto[1] |
|
150 apply (subgoal_tac "(atom ` fset (p \<bullet> xs)) \<sharp>* \<theta>'") |
|
151 apply (simp add: fresh_star_def fresh_def) |
|
152 apply(drule_tac p1="p" in iffD2[OF fresh_star_permute_iff]) |
|
153 apply (simp add: eqvts eqvts_raw) |
|
154 apply (simp add: fresh_star_def fresh_def) |
|
155 apply (simp (no_asm) only: supp_eqvt[symmetric] Pair_eqvt[symmetric]) |
|
156 apply (subgoal_tac "p \<bullet> supp (subst \<theta>' T) \<subseteq> p \<bullet> supp (\<theta>', T)") |
|
157 apply (erule_tac subsetD) |
|
158 apply(simp only: supp_eqvt) |
|
159 apply(perm_simp) |
|
160 apply(drule_tac x="p" in spec) |
|
161 apply(simp) |
|
162 apply (metis permute_pure subset_eqvt) |
|
163 apply (rule perm_supp_eq) |
|
164 apply (simp add: fresh_def fresh_star_def) |
|
165 apply blast |
|
166 done |
|
167 |
|
168 |
|
169 termination (eqvt) by lexicographic_order |
|
170 |
|
171 text {* Some Tests about Alpha-Equality *} |
|
172 |
|
173 lemma |
|
174 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))" |
|
175 apply(simp add: Abs_eq_iff) |
|
176 apply(rule_tac x="0::perm" in exI) |
|
177 apply(simp add: alphas fresh_star_def ty_tys.supp supp_at_base) |
|
178 done |
|
179 |
|
180 lemma |
|
181 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))" |
|
182 apply(simp add: Abs_eq_iff) |
|
183 apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI) |
|
184 apply(simp add: alphas fresh_star_def supp_at_base ty_tys.supp) |
|
185 done |
|
186 |
|
187 lemma |
|
188 shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))" |
|
189 apply(simp add: Abs_eq_iff) |
|
190 apply(rule_tac x="0::perm" in exI) |
|
191 apply(simp add: alphas fresh_star_def ty_tys.supp supp_at_base) |
|
192 done |
|
193 |
|
194 lemma |
|
195 assumes a: "a \<noteq> b" |
|
196 shows "\<not>(All {|a, b|} (Fun (Var a) (Var b)) = All {|c|} (Fun (Var c) (Var c)))" |
|
197 using a |
|
198 apply(simp add: Abs_eq_iff) |
|
199 apply(clarify) |
|
200 apply(simp add: alphas fresh_star_def ty_tys.supp supp_at_base) |
|
201 apply auto |
|
202 done |
|
203 |
|
204 end |
|