equal
deleted
inserted
replaced
32 |
32 |
33 setup {* |
33 setup {* |
34 Code.add_case @{thm If_case_cert} |
34 Code.add_case @{thm If_case_cert} |
35 *} |
35 *} |
36 |
36 |
37 code_const "HOL.equal \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool" |
37 code_printing |
38 (Haskell infix 4 "==") |
38 constant "HOL.equal :: bool \<Rightarrow> bool \<Rightarrow> bool" \<rightharpoonup> (Haskell) infix 4 "==" |
39 |
39 | class_instance "bool" :: "equal" \<rightharpoonup> (Haskell) - |
40 code_instance bool :: equal |
|
41 (Haskell -) |
|
42 |
40 |
43 |
41 |
44 subsection {* The @{text unit} type *} |
42 subsection {* The @{text unit} type *} |
45 |
43 |
46 typedef unit = "{True}" |
44 typedef unit = "{True}" |
93 end |
91 end |
94 |
92 |
95 lemma [code]: |
93 lemma [code]: |
96 "HOL.equal (u\<Colon>unit) v \<longleftrightarrow> True" unfolding equal unit_eq [of u] unit_eq [of v] by rule+ |
94 "HOL.equal (u\<Colon>unit) v \<longleftrightarrow> True" unfolding equal unit_eq [of u] unit_eq [of v] by rule+ |
97 |
95 |
98 code_type unit |
96 code_printing |
99 (SML "unit") |
97 type_constructor unit \<rightharpoonup> |
100 (OCaml "unit") |
98 (SML) "unit" |
101 (Haskell "()") |
99 and (OCaml) "unit" |
102 (Scala "Unit") |
100 and (Haskell) "()" |
103 |
101 and (Scala) "Unit" |
104 code_const Unity |
102 | constant Unity \<rightharpoonup> |
105 (SML "()") |
103 (SML) "()" |
106 (OCaml "()") |
104 and (OCaml) "()" |
107 (Haskell "()") |
105 and (Haskell) "()" |
108 (Scala "()") |
106 and (Scala) "()" |
109 |
107 | class_instance unit :: equal \<rightharpoonup> |
110 code_instance unit :: equal |
108 (Haskell) - |
111 (Haskell -) |
109 | constant "HOL.equal :: unit \<Rightarrow> unit \<Rightarrow> bool" \<rightharpoonup> |
112 |
110 (Haskell) infix 4 "==" |
113 code_const "HOL.equal \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool" |
|
114 (Haskell infix 4 "==") |
|
115 |
111 |
116 code_reserved SML |
112 code_reserved SML |
117 unit |
113 unit |
118 |
114 |
119 code_reserved OCaml |
115 code_reserved OCaml |
286 end |
282 end |
287 *} |
283 *} |
288 |
284 |
289 subsubsection {* Code generator setup *} |
285 subsubsection {* Code generator setup *} |
290 |
286 |
291 code_type prod |
287 code_printing |
292 (SML infix 2 "*") |
288 type_constructor prod \<rightharpoonup> |
293 (OCaml infix 2 "*") |
289 (SML) infix 2 "*" |
294 (Haskell "!((_),/ (_))") |
290 and (OCaml) infix 2 "*" |
295 (Scala "((_),/ (_))") |
291 and (Haskell) "!((_),/ (_))" |
296 |
292 and (Scala) "((_),/ (_))" |
297 code_const Pair |
293 | constant Pair \<rightharpoonup> |
298 (SML "!((_),/ (_))") |
294 (SML) "!((_),/ (_))" |
299 (OCaml "!((_),/ (_))") |
295 and (OCaml) "!((_),/ (_))" |
300 (Haskell "!((_),/ (_))") |
296 and (Haskell) "!((_),/ (_))" |
301 (Scala "!((_),/ (_))") |
297 and (Scala) "!((_),/ (_))" |
302 |
298 | class_instance prod :: equal \<rightharpoonup> |
303 code_instance prod :: equal |
299 (Haskell) - |
304 (Haskell -) |
300 | constant "HOL.equal :: 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" \<rightharpoonup> |
305 |
301 (Haskell) infix 4 "==" |
306 code_const "HOL.equal \<Colon> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" |
|
307 (Haskell infix 4 "==") |
|
308 |
302 |
309 |
303 |
310 subsubsection {* Fundamental operations and properties *} |
304 subsubsection {* Fundamental operations and properties *} |
311 |
305 |
312 lemma Pair_inject: |
306 lemma Pair_inject: |
328 unfolding fst_def by simp |
322 unfolding fst_def by simp |
329 |
323 |
330 lemma snd_conv [simp, code]: "snd (a, b) = b" |
324 lemma snd_conv [simp, code]: "snd (a, b) = b" |
331 unfolding snd_def by simp |
325 unfolding snd_def by simp |
332 |
326 |
333 code_const fst and snd |
327 code_printing |
334 (Haskell "fst" and "snd") |
328 constant fst \<rightharpoonup> (Haskell) "fst" |
|
329 | constant snd \<rightharpoonup> (Haskell) "snd" |
335 |
330 |
336 lemma prod_case_unfold [nitpick_unfold]: "prod_case = (%c p. c (fst p) (snd p))" |
331 lemma prod_case_unfold [nitpick_unfold]: "prod_case = (%c p. c (fst p) (snd p))" |
337 by (simp add: fun_eq_iff split: prod.split) |
332 by (simp add: fun_eq_iff split: prod.split) |
338 |
333 |
339 lemma fst_eqD: "fst (x, y) = a ==> x = a" |
334 lemma fst_eqD: "fst (x, y) = a ==> x = a" |
762 by (simp add: fun_eq_iff scomp_unfold fcomp_def) |
757 by (simp add: fun_eq_iff scomp_unfold fcomp_def) |
763 |
758 |
764 lemma fcomp_scomp: "(f \<circ>> g) \<circ>\<rightarrow> h = f \<circ>> (g \<circ>\<rightarrow> h)" |
759 lemma fcomp_scomp: "(f \<circ>> g) \<circ>\<rightarrow> h = f \<circ>> (g \<circ>\<rightarrow> h)" |
765 by (simp add: fun_eq_iff scomp_unfold) |
760 by (simp add: fun_eq_iff scomp_unfold) |
766 |
761 |
767 code_const scomp |
762 code_printing |
768 (Eval infixl 3 "#->") |
763 constant scomp \<rightharpoonup> (Eval) infixl 3 "#->" |
769 |
764 |
770 no_notation fcomp (infixl "\<circ>>" 60) |
765 no_notation fcomp (infixl "\<circ>>" 60) |
771 no_notation scomp (infixl "\<circ>\<rightarrow>" 60) |
766 no_notation scomp (infixl "\<circ>\<rightarrow>" 60) |
772 |
767 |
773 text {* |
768 text {* |