18 definition esl :: "'a esl \<Rightarrow> 'b esl \<Rightarrow> ('a * 'b ) esl" where |
18 definition esl :: "'a esl \<Rightarrow> 'b esl \<Rightarrow> ('a * 'b ) esl" where |
19 "esl == %(A,rA,fA) (B,rB,fB). (A \<times> B, le rA rB, sup fA fB)" |
19 "esl == %(A,rA,fA) (B,rB,fB). (A \<times> B, le rA rB, sup fA fB)" |
20 |
20 |
21 abbreviation |
21 abbreviation |
22 lesubprod_sntax :: "'a * 'b \<Rightarrow> 'a ord \<Rightarrow> 'b ord \<Rightarrow> 'a * 'b \<Rightarrow> bool" |
22 lesubprod_sntax :: "'a * 'b \<Rightarrow> 'a ord \<Rightarrow> 'b ord \<Rightarrow> 'a * 'b \<Rightarrow> bool" |
23 ("(_ /<='(_,_') _)" [50, 0, 0, 51] 50) |
23 (\<open>(_ /<='(_,_') _)\<close> [50, 0, 0, 51] 50) |
24 where "p <=(rA,rB) q == p <=_(le rA rB) q" |
24 where "p <=(rA,rB) q == p <=_(le rA rB) q" |
25 |
25 |
26 lemma unfold_lesub_prod: |
26 lemma unfold_lesub_prod: |
27 "p <=(rA,rB) q == le rA rB p q" |
27 "p <=(rA,rB) q == le rA rB p q" |
28 by (simp add: lesub_def) |
28 by (simp add: lesub_def) |