equal
deleted
inserted
replaced
20 rep_datatype True False by (auto intro: bool_induct) |
20 rep_datatype True False by (auto intro: bool_induct) |
21 |
21 |
22 declare case_split [cases type: bool] |
22 declare case_split [cases type: bool] |
23 -- "prefer plain propositional version" |
23 -- "prefer plain propositional version" |
24 |
24 |
25 lemma [code func]: |
25 lemma |
26 shows "False = P \<longleftrightarrow> \<not> P" |
26 shows [code func]: "eq_class.eq False P \<longleftrightarrow> \<not> P" |
27 and "True = P \<longleftrightarrow> P" |
27 and [code func]: "eq_class.eq True P \<longleftrightarrow> P" |
28 and "P = False \<longleftrightarrow> \<not> P" |
28 and [code func]: "eq_class.eq P False \<longleftrightarrow> \<not> P" |
29 and "P = True \<longleftrightarrow> P" by simp_all |
29 and [code func]: "eq_class.eq P True \<longleftrightarrow> P" |
30 |
30 and [code nbe]: "eq_class.eq P P \<longleftrightarrow> True" |
31 code_const "op = \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool" |
31 by (simp_all add: eq) |
|
32 |
|
33 code_const "eq_class.eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool" |
32 (Haskell infixl 4 "==") |
34 (Haskell infixl 4 "==") |
33 |
35 |
34 code_instance bool :: eq |
36 code_instance bool :: eq |
35 (Haskell -) |
37 (Haskell -) |
36 |
38 |
86 text {* code generator setup *} |
88 text {* code generator setup *} |
87 |
89 |
88 instance unit :: eq .. |
90 instance unit :: eq .. |
89 |
91 |
90 lemma [code func]: |
92 lemma [code func]: |
91 "(u\<Colon>unit) = v \<longleftrightarrow> True" unfolding unit_eq [of u] unit_eq [of v] by rule+ |
93 "eq_class.eq (u\<Colon>unit) v \<longleftrightarrow> True" unfolding eq unit_eq [of u] unit_eq [of v] by rule+ |
92 |
94 |
93 code_type unit |
95 code_type unit |
94 (SML "unit") |
96 (SML "unit") |
95 (OCaml "unit") |
97 (OCaml "unit") |
96 (Haskell "()") |
98 (Haskell "()") |
97 |
99 |
98 code_instance unit :: eq |
100 code_instance unit :: eq |
99 (Haskell -) |
101 (Haskell -) |
100 |
102 |
101 code_const "op = \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool" |
103 code_const "eq_class.eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool" |
102 (Haskell infixl 4 "==") |
104 (Haskell infixl 4 "==") |
103 |
105 |
104 code_const Unity |
106 code_const Unity |
105 (SML "()") |
107 (SML "()") |
106 (OCaml "()") |
108 (OCaml "()") |
914 subsubsection {* Code generator setup *} |
916 subsubsection {* Code generator setup *} |
915 |
917 |
916 instance * :: (eq, eq) eq .. |
918 instance * :: (eq, eq) eq .. |
917 |
919 |
918 lemma [code func]: |
920 lemma [code func]: |
919 "(x1\<Colon>'a\<Colon>eq, y1\<Colon>'b\<Colon>eq) = (x2, y2) \<longleftrightarrow> x1 = x2 \<and> y1 = y2" by auto |
921 "eq_class.eq (x1\<Colon>'a\<Colon>eq, y1\<Colon>'b\<Colon>eq) (x2, y2) \<longleftrightarrow> x1 = x2 \<and> y1 = y2" by (simp add: eq) |
920 |
922 |
921 lemma split_case_cert: |
923 lemma split_case_cert: |
922 assumes "CASE \<equiv> split f" |
924 assumes "CASE \<equiv> split f" |
923 shows "CASE (a, b) \<equiv> f a b" |
925 shows "CASE (a, b) \<equiv> f a b" |
924 using assms by simp |
926 using assms by simp |
933 (Haskell "!((_),/ (_))") |
935 (Haskell "!((_),/ (_))") |
934 |
936 |
935 code_instance * :: eq |
937 code_instance * :: eq |
936 (Haskell -) |
938 (Haskell -) |
937 |
939 |
938 code_const "op = \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" |
940 code_const "eq_class.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" |
939 (Haskell infixl 4 "==") |
941 (Haskell infixl 4 "==") |
940 |
942 |
941 code_const Pair |
943 code_const Pair |
942 (SML "!((_),/ (_))") |
944 (SML "!((_),/ (_))") |
943 (OCaml "!((_),/ (_))") |
945 (OCaml "!((_),/ (_))") |