73 as |
73 as |
74 "(perm::'x prm \<Rightarrow> rmethod \<Rightarrow> rmethod)" |
74 "(perm::'x prm \<Rightarrow> rmethod \<Rightarrow> rmethod)" |
75 |
75 |
76 end |
76 end |
77 |
77 |
|
78 |
|
79 |
78 lemma tolift: |
80 lemma tolift: |
79 "\<forall> fvar. |
81 "\<forall> fvar. |
80 \<forall> fobj\<in>Respects (op = ===> list_rel (prod_rel (op =) alpha_method) ===> op =). |
82 \<forall> fobj\<in>Respects (op = ===> list_rel (prod_rel (op =) alpha_method) ===> op =). |
81 \<forall> fnvk\<in>Respects (op = ===> alpha_obj ===> op =). |
83 \<forall> fnvk\<in>Respects (op = ===> alpha_obj ===> op =). |
82 \<forall> fupd\<in>Respects (op = ===> op = ===> alpha_obj ===> op = ===> alpha_method ===> op =). |
84 \<forall> fupd\<in>Respects (op = ===> op = ===> alpha_obj ===> op = ===> alpha_method ===> op =). |
83 \<forall> fcns\<in>Respects (op = ===> op = ===> prod_rel (op =) alpha_method ===> list_rel (prod_rel (op =) alpha_method) ===> op =). |
85 \<forall> fcns\<in>Respects (op = ===> op = ===> prod_rel (op =) alpha_method ===> list_rel (prod_rel (op =) alpha_method) ===> op =). |
84 \<forall> fnil. |
86 \<forall> fnil. |
85 \<forall> fpar\<in>Respects (op = ===> op = ===> alpha_method ===> op =). |
87 \<forall> fpar\<in>Respects (op = ===> op = ===> alpha_method ===> op =). |
86 \<forall> fsgm\<in>Respects (op = ===> (op = ===> alpha_obj) ===> op =). |
88 \<forall> fsgm\<in>Respects (op = ===> (op = ===> alpha_obj) ===> op =). |
87 |
89 |
88 Bex1 |
90 Ex1 (\<lambda>x. |
89 (Respects (prod_rel (alpha_obj ===> op =) |
91 (x \<in> (Respects (prod_rel (alpha_obj ===> op =) |
90 (prod_rel (list_rel (prod_rel (op =) alpha_method) ===> op =) |
92 (prod_rel (list_rel (prod_rel (op =) alpha_method) ===> op =) |
91 (prod_rel ((prod_rel (op =) alpha_method) ===> op =) |
93 (prod_rel ((prod_rel (op =) alpha_method) ===> op =) |
92 (alpha_method ===> op =) |
94 (alpha_method ===> op =) |
93 ) |
95 ) |
94 ) |
96 )))) \<and> |
95 )) |
|
96 (\<lambda> (hom_o\<Colon>robj \<Rightarrow> 'a, hom_d\<Colon>(char list \<times> rmethod) list \<Rightarrow> 'b, hom_e\<Colon>char list \<times> rmethod \<Rightarrow> 'c, hom_m\<Colon>rmethod \<Rightarrow> 'd). |
97 (\<lambda> (hom_o\<Colon>robj \<Rightarrow> 'a, hom_d\<Colon>(char list \<times> rmethod) list \<Rightarrow> 'b, hom_e\<Colon>char list \<times> rmethod \<Rightarrow> 'c, hom_m\<Colon>rmethod \<Rightarrow> 'd). |
97 |
98 |
98 |
99 ((\<forall>x. hom_o (rVar x) = fvar x) \<and> |
99 (\<forall>x. hom_o (rVar x) = fvar x) \<and> |
|
100 (\<forall>d. hom_o (rObj d) = fobj (hom_d d) d) \<and> |
100 (\<forall>d. hom_o (rObj d) = fobj (hom_d d) d) \<and> |
101 (\<forall>a l. hom_o (rInv a l) = fnvk (hom_o a) a l) \<and> |
101 (\<forall>a l. hom_o (rInv a l) = fnvk (hom_o a) a l) \<and> |
102 (\<forall>a l m. hom_o (rUpd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and> |
102 (\<forall>a l m. hom_o (rUpd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and> |
103 (\<forall>e d. hom_d (e # d) = fcns (hom_e e) (hom_d d) e d) \<and> |
103 (\<forall>e d. hom_d (e # d) = fcns (hom_e e) (hom_d d) e d) \<and> |
104 (hom_d [] = fnil) \<and> |
104 (hom_d [] = fnil) \<and> |
105 (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and> |
105 (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and> |
106 (\<forall>x a. hom_m (rSig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a)) |
106 (\<forall>x a. hom_m (rSig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a)) |
107 )" |
107 )) x) " |
108 sorry |
108 sorry |
109 |
109 |
110 syntax |
110 lemma test_to: "Ex1 (\<lambda>x. (x \<in> (Respects alpha_obj)) \<and> P x)" |
|
111 ML_prf {* prop_of (#goal (Isar.goal ())) *} |
|
112 sorry |
|
113 lemma test_tod: "Ex1 (P :: obj \<Rightarrow> bool)" |
|
114 apply (lifting test_to) |
|
115 done |
|
116 |
|
117 |
|
118 |
|
119 |
|
120 (*syntax |
111 "_expttrn" :: "pttrn => bool => bool" ("(3\<exists>\<exists> _./ _)" [0, 10] 10) |
121 "_expttrn" :: "pttrn => bool => bool" ("(3\<exists>\<exists> _./ _)" [0, 10] 10) |
112 |
122 |
113 translations |
123 translations |
114 "\<exists>\<exists> x. P" == "Ex (%x. P)" |
124 "\<exists>\<exists> x. P" == "Ex (%x. P)" |
|
125 *) |
115 |
126 |
116 lemma rvar_rsp[quot_respect]: "(op = ===> alpha_obj) rVar rVar" |
127 lemma rvar_rsp[quot_respect]: "(op = ===> alpha_obj) rVar rVar" |
117 by (simp add: a1) |
128 by (simp add: a1) |
118 |
129 |
119 lemma robj_rsp[quot_respect]: "(list_rel (prod_rel op = alpha_method) ===> alpha_obj) rObj rObj" |
130 lemma robj_rsp[quot_respect]: "(list_rel (prod_rel op = alpha_method) ===> alpha_obj) rObj rObj" |
150 (hom_d [] = fnil) \<and> |
161 (hom_d [] = fnil) \<and> |
151 (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and> |
162 (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and> |
152 (\<forall>x a. hom_m (Sig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a)) |
163 (\<forall>x a. hom_m (Sig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a)) |
153 )" |
164 )" |
154 apply (lifting tolift) |
165 apply (lifting tolift) |
155 done |
|
156 |
|
157 done |
166 done |
158 |
167 |
159 lemma tolift': |
168 lemma tolift': |
160 "\<forall> fvar. |
169 "\<forall> fvar. |
161 \<forall> fobj\<in>Respects (op = ===> list_rel (prod_rel (op =) alpha_method) ===> op =). |
170 \<forall> fobj\<in>Respects (op = ===> list_rel (prod_rel (op =) alpha_method) ===> op =). |