27 |
27 |
28 instantiation int :: predomain |
28 instantiation int :: predomain |
29 begin |
29 begin |
30 |
30 |
31 definition |
31 definition |
32 "(liftemb :: int u \<rightarrow> udom) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)" |
32 "(liftemb :: int u \<rightarrow> udom u) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)" |
33 |
33 |
34 definition |
34 definition |
35 "(liftprj :: udom \<rightarrow> int u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj" |
35 "(liftprj :: udom u \<rightarrow> int u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj" |
36 |
36 |
37 definition |
37 definition |
38 "liftdefl \<equiv> (\<lambda>(t::int itself). LIFTDEFL(int discr))" |
38 "liftdefl \<equiv> (\<lambda>(t::int itself). LIFTDEFL(int discr))" |
39 |
39 |
40 instance proof |
40 instance proof |
41 show "ep_pair liftemb (liftprj :: udom \<rightarrow> int u)" |
41 show "ep_pair liftemb (liftprj :: udom u \<rightarrow> int u)" |
42 unfolding liftemb_int_def liftprj_int_def |
42 unfolding liftemb_int_def liftprj_int_def |
43 apply (rule ep_pair_comp) |
43 apply (rule ep_pair_comp) |
44 apply (rule ep_pair_u_map) |
44 apply (rule ep_pair_u_map) |
45 apply (simp add: ep_pair.intro) |
45 apply (simp add: ep_pair.intro) |
46 apply (rule predomain_ep) |
46 apply (rule predomain_ep) |
47 done |
47 done |
48 show "cast\<cdot>LIFTDEFL(int) = liftemb oo (liftprj :: udom \<rightarrow> int u)" |
48 show "cast\<cdot>LIFTDEFL(int) = liftemb oo (liftprj :: udom u \<rightarrow> int u)" |
49 unfolding liftemb_int_def liftprj_int_def liftdefl_int_def |
49 unfolding liftemb_int_def liftprj_int_def liftdefl_int_def |
50 apply (simp add: cast_liftdefl cfcomp1 u_map_map) |
50 apply (simp add: cast_liftdefl cfcomp1 u_map_map) |
51 apply (simp add: ID_def [symmetric] u_map_ID) |
51 apply (simp add: ID_def [symmetric] u_map_ID) |
52 done |
52 done |
53 qed |
53 qed |