blob: fced534de28989df5767307d2ab4ddc7579f38b8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
|
chapter \<open>Generated by Lem from show.lem.\<close>
theory "Lem_show"
imports
Main
"Lem_string"
"Lem_maybe"
"Lem_num"
"Lem_basic_classes"
begin
(*open import String Maybe Num Basic_classes*)
(*open import {hol} `lemTheory`*)
record 'a Show_class=
show_method::" 'a \<Rightarrow> string "
definition instance_Show_Show_string_dict :: "(string)Show_class " where
" instance_Show_Show_string_dict = ((|
show_method = (\<lambda> s. ([(char_of_nat 34)]) @ (s @ ([(char_of_nat 34)])))|) )"
(*val stringFromMaybe : forall 'a. ('a -> string) -> maybe 'a -> string*)
fun stringFromMaybe :: "('a \<Rightarrow> string)\<Rightarrow> 'a option \<Rightarrow> string " where
" stringFromMaybe showX (Some x) = ( (''Just ('') @ (showX x @ ('')'')))"
|" stringFromMaybe showX None = ( (''Nothing''))"
definition instance_Show_Show_Maybe_maybe_dict :: " 'a Show_class \<Rightarrow>('a option)Show_class " where
" instance_Show_Show_Maybe_maybe_dict dict_Show_Show_a = ((|
show_method = (\<lambda> x_opt. stringFromMaybe
(show_method dict_Show_Show_a) x_opt)|) )"
(*val stringFromListAux : forall 'a. ('a -> string) -> list 'a -> string*)
function (sequential,domintros) stringFromListAux :: "('a \<Rightarrow> string)\<Rightarrow> 'a list \<Rightarrow> string " where
" stringFromListAux showX ([]) = ( (''''))"
|" stringFromListAux showX (x # xs') = (
(case xs' of
[] => showX x
| _ => showX x @ ((''; '') @ stringFromListAux showX xs')
))"
by pat_completeness auto
(*val stringFromList : forall 'a. ('a -> string) -> list 'a -> string*)
definition stringFromList :: "('a \<Rightarrow> string)\<Rightarrow> 'a list \<Rightarrow> string " where
" stringFromList showX xs = (
(''['') @ (stringFromListAux showX xs @ ('']'')))"
definition instance_Show_Show_list_dict :: " 'a Show_class \<Rightarrow>('a list)Show_class " where
" instance_Show_Show_list_dict dict_Show_Show_a = ((|
show_method = (\<lambda> xs. stringFromList
(show_method dict_Show_Show_a) xs)|) )"
(*val stringFromPair : forall 'a 'b. ('a -> string) -> ('b -> string) -> ('a * 'b) -> string*)
fun stringFromPair :: "('a \<Rightarrow> string)\<Rightarrow>('b \<Rightarrow> string)\<Rightarrow> 'a*'b \<Rightarrow> string " where
" stringFromPair showX showY (x,y) = (
(''('') @ (showX x @ (('', '') @ (showY y @ ('')'')))))"
definition instance_Show_Show_tup2_dict :: " 'a Show_class \<Rightarrow> 'b Show_class \<Rightarrow>('a*'b)Show_class " where
" instance_Show_Show_tup2_dict dict_Show_Show_a dict_Show_Show_b = ((|
show_method = (stringFromPair
(show_method dict_Show_Show_a) (show_method dict_Show_Show_b))|) )"
definition instance_Show_Show_bool_dict :: "(bool)Show_class " where
" instance_Show_Show_bool_dict = ((|
show_method = (\<lambda> b. if b then (''true'') else (''false''))|) )"
end
|
