equal
deleted
inserted
replaced
80 and TRM = trm / atrm |
80 and TRM = trm / atrm |
81 by (auto intro: alpha_equivps) |
81 by (auto intro: alpha_equivps) |
82 |
82 |
83 print_quotients |
83 print_quotients |
84 |
84 |
85 quotient_def |
85 quotient_def |
86 TYP :: "KIND" |
86 TYP :: "TYP :: KIND" |
87 where |
87 where |
88 "TYP \<equiv> Type" |
88 "Type" |
89 |
89 |
90 quotient_def |
90 quotient_def |
91 KPI :: "TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND" |
91 KPI :: "KPI :: TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND" |
92 where |
92 where |
93 "KPI \<equiv> KPi" |
93 "KPi" |
94 |
94 |
95 quotient_def |
95 quotient_def |
96 TCONST :: "ident \<Rightarrow> TY" |
96 TCONST :: "TCONST :: ident \<Rightarrow> TY" |
97 where |
97 where |
98 "TCONST \<equiv> TConst" |
98 "TConst" |
99 |
99 |
100 quotient_def |
100 quotient_def |
101 TAPP :: "TY \<Rightarrow> TRM \<Rightarrow> TY" |
101 TAPP :: "TAPP :: TY \<Rightarrow> TRM \<Rightarrow> TY" |
102 where |
102 where |
103 "TAPP \<equiv> TApp" |
103 "TApp" |
104 |
104 |
105 quotient_def |
105 quotient_def |
106 TPI :: "TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY" |
106 TPI :: "TPI :: TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY" |
107 where |
107 where |
108 "TPI \<equiv> TPi" |
108 "TPi" |
109 |
109 |
110 (* FIXME: does not work with CONST *) |
110 (* FIXME: does not work with CONST *) |
111 quotient_def |
111 quotient_def |
112 CONS :: "ident \<Rightarrow> TRM" |
112 CONS :: "CONS :: ident \<Rightarrow> TRM" |
113 where |
113 where |
114 "CONS \<equiv> Const" |
114 "Const" |
115 |
115 |
116 quotient_def |
116 quotient_def |
117 VAR :: "name \<Rightarrow> TRM" |
117 VAR :: "VAR :: name \<Rightarrow> TRM" |
118 where |
118 where |
119 "VAR \<equiv> Var" |
119 "Var" |
120 |
120 |
121 quotient_def |
121 quotient_def |
122 APP :: "TRM \<Rightarrow> TRM \<Rightarrow> TRM" |
122 APP :: "APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM" |
123 where |
123 where |
124 "APP \<equiv> App" |
124 "App" |
125 |
125 |
126 quotient_def |
126 quotient_def |
127 LAM :: "TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM" |
127 LAM :: "LAM :: TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM" |
128 where |
128 where |
129 "LAM \<equiv> Lam" |
129 "Lam" |
130 |
130 |
131 thm TYP_def |
131 thm TYP_def |
132 thm KPI_def |
132 thm KPI_def |
133 thm TCONST_def |
133 thm TCONST_def |
134 thm TAPP_def |
134 thm TAPP_def |
137 thm CONS_def |
137 thm CONS_def |
138 thm APP_def |
138 thm APP_def |
139 thm LAM_def |
139 thm LAM_def |
140 |
140 |
141 (* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *) |
141 (* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *) |
142 quotient_def |
142 quotient_def |
143 FV_kind :: "KIND \<Rightarrow> name set" |
143 FV_kind :: "FV_kind :: KIND \<Rightarrow> name set" |
144 where |
144 where |
145 "FV_kind \<equiv> fv_kind" |
145 "fv_kind" |
146 |
146 |
147 quotient_def |
147 quotient_def |
148 FV_ty :: "TY \<Rightarrow> name set" |
148 FV_ty :: "FV_ty :: TY \<Rightarrow> name set" |
149 where |
149 where |
150 "FV_ty \<equiv> fv_ty" |
150 "fv_ty" |
151 |
151 |
152 quotient_def |
152 quotient_def |
153 FV_trm :: "TRM \<Rightarrow> name set" |
153 FV_trm :: "FV_trm :: TRM \<Rightarrow> name set" |
154 where |
154 where |
155 "FV_trm \<equiv> fv_trm" |
155 "fv_trm" |
156 |
156 |
157 thm FV_kind_def |
157 thm FV_kind_def |
158 thm FV_ty_def |
158 thm FV_ty_def |
159 thm FV_trm_def |
159 thm FV_trm_def |
160 |
160 |
163 perm_kind \<equiv> "perm :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND" (unchecked) |
163 perm_kind \<equiv> "perm :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND" (unchecked) |
164 perm_ty \<equiv> "perm :: 'x prm \<Rightarrow> TY \<Rightarrow> TY" (unchecked) |
164 perm_ty \<equiv> "perm :: 'x prm \<Rightarrow> TY \<Rightarrow> TY" (unchecked) |
165 perm_trm \<equiv> "perm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM" (unchecked) |
165 perm_trm \<equiv> "perm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM" (unchecked) |
166 begin |
166 begin |
167 |
167 |
168 quotient_def |
168 quotient_def |
169 perm_kind :: "'x prm \<Rightarrow> KIND \<Rightarrow> KIND" |
169 perm_kind :: "perm_kind :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND" |
170 where |
170 where |
171 "perm_kind \<equiv> (perm::'x prm \<Rightarrow> kind \<Rightarrow> kind)" |
171 "(perm::'x prm \<Rightarrow> kind \<Rightarrow> kind)" |
172 |
172 |
173 quotient_def |
173 quotient_def |
174 perm_ty :: "'x prm \<Rightarrow> TY \<Rightarrow> TY" |
174 perm_ty :: "perm_ty :: 'x prm \<Rightarrow> TY \<Rightarrow> TY" |
175 where |
175 where |
176 "perm_ty \<equiv> (perm::'x prm \<Rightarrow> ty \<Rightarrow> ty)" |
176 "(perm::'x prm \<Rightarrow> ty \<Rightarrow> ty)" |
177 |
177 |
178 quotient_def |
178 quotient_def |
179 perm_trm :: "'x prm \<Rightarrow> TRM \<Rightarrow> TRM" |
179 perm_trm :: "perm_trm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM" |
180 where |
180 where |
181 "perm_trm \<equiv> (perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)" |
181 "(perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)" |
182 |
182 |
183 end |
183 end |
184 |
184 |
185 (* TODO/FIXME: Think whether these RSP theorems are true. *) |
185 (* TODO/FIXME: Think whether these RSP theorems are true. *) |
186 lemma kpi_rsp[quot_respect]: |
186 lemma kpi_rsp[quot_respect]: |
251 shows "((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and> |
251 shows "((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and> |
252 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> |
252 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> |
253 ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
253 ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
254 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 |
254 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 |
255 apply(lifting akind_aty_atrm.induct) |
255 apply(lifting akind_aty_atrm.induct) |
256 (* FIXME: with overloaded definitions *) |
|
257 apply(fold perm_kind_def perm_ty_def perm_trm_def) |
|
258 apply(cleaning) |
|
259 (* |
256 (* |
260 Profiling: |
257 Profiling: |
261 ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *} |
258 ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *} |
262 ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *} |
259 ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *} |
263 ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_equivps} 1) (ith 1)) *} |
260 ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_equivps} 1) (ith 1)) *} |