equal
deleted
inserted
replaced
111 "_expttrn" :: "pttrn => bool => bool" ("(3\<exists>\<exists> _./ _)" [0, 10] 10) |
111 "_expttrn" :: "pttrn => bool => bool" ("(3\<exists>\<exists> _./ _)" [0, 10] 10) |
112 |
112 |
113 translations |
113 translations |
114 "\<exists>\<exists> x. P" == "Ex (%x. P)" |
114 "\<exists>\<exists> x. P" == "Ex (%x. P)" |
115 |
115 |
116 lemma split_rsp[quot_respect]: |
|
117 "((R1 ===> R2 ===> op =) ===> (prod_rel R1 R2) ===> op =) split split" |
|
118 by auto |
|
119 |
|
120 lemma rvar_rsp[quot_respect]: "(op = ===> alpha_obj) rVar rVar" |
116 lemma rvar_rsp[quot_respect]: "(op = ===> alpha_obj) rVar rVar" |
121 by (simp add: a1) |
117 by (simp add: a1) |
122 |
118 |
123 lemma robj_rsp[quot_respect]: "(list_rel (prod_rel op = alpha_method) ===> alpha_obj) rObj rObj" |
119 lemma robj_rsp[quot_respect]: "(list_rel (prod_rel op = alpha_method) ===> alpha_obj) rObj rObj" |
124 sorry |
120 sorry |
125 lemma rinv_rsp[quot_respect]: "(alpha_obj ===> op = ===> alpha_obj) rInv rInv" |
121 lemma rinv_rsp[quot_respect]: "(alpha_obj ===> op = ===> alpha_obj) rInv rInv" |
126 sorry |
122 sorry |
148 apply (lifting tolift) |
144 apply (lifting tolift) |
149 apply (regularize) |
145 apply (regularize) |
150 apply (simp) |
146 apply (simp) |
151 prefer 2 |
147 prefer 2 |
152 apply cleaning |
148 apply cleaning |
153 apply simp |
149 apply (subst ex_prs) |
|
150 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) |
|
151 apply (rule refl) |
154 sorry |
152 sorry |
155 |
153 |
156 lemma tolift': |
154 lemma tolift': |
157 "\<forall> fvar. |
155 "\<forall> fvar. |
158 \<forall> fobj\<in>Respects (op = ===> list_rel (prod_rel (op =) alpha_method) ===> op =). |
156 \<forall> fobj\<in>Respects (op = ===> list_rel (prod_rel (op =) alpha_method) ===> op =). |