equal
deleted
inserted
replaced
29 "csplit = (\<Lambda> f p. f\<cdot>(fst p)\<cdot>(snd p))" |
29 "csplit = (\<Lambda> f p. f\<cdot>(fst p)\<cdot>(snd p))" |
30 |
30 |
31 translations |
31 translations |
32 "\<Lambda>(CONST Pair x y). t" == "CONST csplit\<cdot>(\<Lambda> x y. t)" |
32 "\<Lambda>(CONST Pair x y). t" == "CONST csplit\<cdot>(\<Lambda> x y. t)" |
33 |
33 |
|
34 abbreviation |
|
35 cfst :: "'a \<times> 'b \<rightarrow> 'a" where |
|
36 "cfst \<equiv> Abs_cfun fst" |
|
37 |
|
38 abbreviation |
|
39 csnd :: "'a \<times> 'b \<rightarrow> 'b" where |
|
40 "csnd \<equiv> Abs_cfun snd" |
34 |
41 |
35 subsection {* Convert all lemmas to the continuous versions *} |
42 subsection {* Convert all lemmas to the continuous versions *} |
36 |
43 |
37 lemma csplit1 [simp]: "csplit\<cdot>f\<cdot>\<bottom> = f\<cdot>\<bottom>\<cdot>\<bottom>" |
44 lemma csplit1 [simp]: "csplit\<cdot>f\<cdot>\<bottom> = f\<cdot>\<bottom>\<cdot>\<bottom>" |
38 by (simp add: csplit_def) |
45 by (simp add: csplit_def) |