101 assumes type: "type_definition Rep Abs (defl_set t)" |
101 assumes type: "type_definition Rep Abs (defl_set t)" |
102 assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
102 assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
103 assumes emb: "emb \<equiv> (\<Lambda> x. Rep x)" |
103 assumes emb: "emb \<equiv> (\<Lambda> x. Rep x)" |
104 assumes prj: "prj \<equiv> (\<Lambda> x. Abs (cast\<cdot>t\<cdot>x))" |
104 assumes prj: "prj \<equiv> (\<Lambda> x. Abs (cast\<cdot>t\<cdot>x))" |
105 assumes defl: "defl \<equiv> (\<lambda> a::'a itself. t)" |
105 assumes defl: "defl \<equiv> (\<lambda> a::'a itself. t)" |
106 assumes liftemb: "(liftemb :: 'a u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb" |
106 assumes liftemb: "(liftemb :: 'a u \<rightarrow> udom) \<equiv> u_emb oo u_map\<cdot>emb" |
107 assumes liftprj: "(liftprj :: udom \<rightarrow> 'a u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx" |
107 assumes liftprj: "(liftprj :: udom \<rightarrow> 'a u) \<equiv> u_map\<cdot>prj oo u_prj" |
108 assumes liftdefl: "(liftdefl :: 'a itself \<Rightarrow> _) \<equiv> (\<lambda>t. u_defl\<cdot>DEFL('a))" |
108 assumes liftdefl: "(liftdefl :: 'a itself \<Rightarrow> _) \<equiv> (\<lambda>t. u_defl\<cdot>DEFL('a))" |
109 shows "OFCLASS('a, liftdomain_class)" |
109 shows "OFCLASS('a, liftdomain_class)" |
110 using liftemb [THEN meta_eq_to_obj_eq] |
110 using liftemb [THEN meta_eq_to_obj_eq] |
111 using liftprj [THEN meta_eq_to_obj_eq] |
111 using liftprj [THEN meta_eq_to_obj_eq] |
112 proof (rule liftdomain_class_intro) |
112 proof (rule liftdomain_class_intro) |