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]: "((R1 ===> R2 ===> op =) ===> (prod_rel R1 R2) ===> op =) split split" |
116 lemma split_rsp[quot_respect]: |
|
117 "((R1 ===> R2 ===> op =) ===> (prod_rel R1 R2) ===> op =) split split" |
117 by auto |
118 by auto |
118 |
119 |
119 lemma rvar_rsp[quot_respect]: "(op = ===> alpha_obj) rVar rVar" |
120 lemma rvar_rsp[quot_respect]: "(op = ===> alpha_obj) rVar rVar" |
120 by (simp add: a1) |
121 by (simp add: a1) |
121 |
122 |
127 sorry |
128 sorry |
128 lemma rsig_rsp[quot_respect]: "(op = ===> alpha_obj ===> alpha_method) rSig rSig" |
129 lemma rsig_rsp[quot_respect]: "(op = ===> alpha_obj ===> alpha_method) rSig rSig" |
129 sorry |
130 sorry |
130 lemma operm_rsp[quot_respect]: "(op = ===> alpha_obj ===> alpha_obj) op \<bullet> op \<bullet>" |
131 lemma operm_rsp[quot_respect]: "(op = ===> alpha_obj ===> alpha_obj) op \<bullet> op \<bullet>" |
131 sorry |
132 sorry |
|
133 |
|
134 |
132 |
135 |
133 lemma liftd: " |
136 lemma liftd: " |
134 \<exists>\<exists>(hom_o, (hom_d, (hom_e, hom_m))). |
137 \<exists>\<exists>(hom_o, (hom_d, (hom_e, hom_m))). |
135 ( |
138 ( |
136 (\<forall>x. hom_o (Var x) = fvar x) \<and> |
139 (\<forall>x. hom_o (Var x) = fvar x) \<and> |