equal
deleted
inserted
replaced
169 use "quotient.ML" |
169 use "quotient.ML" |
170 |
170 |
171 |
171 |
172 (* lifting of constants *) |
172 (* lifting of constants *) |
173 use "quotient_def.ML" |
173 use "quotient_def.ML" |
174 |
|
175 section {* Bounded abstraction *} |
|
176 |
|
177 definition |
|
178 Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
|
179 where |
|
180 "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)" |
|
181 |
174 |
182 section {* Simset setup *} |
175 section {* Simset setup *} |
183 |
176 |
184 (* since HOL_basic_ss is too "big", we need to set up *) |
177 (* since HOL_basic_ss is too "big", we need to set up *) |
185 (* our own minimal simpset *) |
178 (* our own minimal simpset *) |
416 |
409 |
417 fun regularize_trm lthy rtrm qtrm = |
410 fun regularize_trm lthy rtrm qtrm = |
418 case (rtrm, qtrm) of |
411 case (rtrm, qtrm) of |
419 (Abs (x, ty, t), Abs (x', ty', t')) => |
412 (Abs (x, ty, t), Abs (x', ty', t')) => |
420 let |
413 let |
421 val subtrm = regularize_trm lthy t t' |
414 val subtrm = Abs(x, ty, regularize_trm lthy t t') |
422 in |
415 in |
423 if ty = ty' |
416 if ty = ty' |
424 then Abs (x, ty, subtrm) |
417 then subtrm |
425 else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm |
418 else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm |
426 end |
419 end |
427 |
420 |
428 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
421 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
429 let |
422 let |