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