blob: 25ab25709f8e12799a6ab3fe0750259319414a70 (
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
|
chapter \<open>Generated by Lem from show_extra.lem.\<close>
theory "Lem_show_extra"
imports
Main
"Lem_string"
"Lem_maybe"
"Lem_num"
"Lem_basic_classes"
"Lem_set"
"Lem_relation"
"Lem_show"
"Lem_set_extra"
"Lem_string_extra"
begin
(*open import String Maybe Num Basic_classes Set Relation Show*)
(*import Set_extra String_extra*)
definition instance_Show_Show_nat_dict :: "(nat)Show_class " where
" instance_Show_Show_nat_dict = ((|
show_method = Lem_string_extra.stringFromNat |) )"
definition instance_Show_Show_Num_natural_dict :: "(nat)Show_class " where
" instance_Show_Show_Num_natural_dict = ((|
show_method = Lem_string_extra.stringFromNatural |) )"
definition instance_Show_Show_Num_int_dict :: "(int)Show_class " where
" instance_Show_Show_Num_int_dict = ((|
show_method = Lem_string_extra.stringFromInt |) )"
definition instance_Show_Show_Num_integer_dict :: "(int)Show_class " where
" instance_Show_Show_Num_integer_dict = ((|
show_method = Lem_string_extra.stringFromInteger |) )"
definition stringFromSet :: "('a \<Rightarrow> string)\<Rightarrow> 'a set \<Rightarrow> string " where
" stringFromSet showX xs = (
(''{'') @ (Lem_show.stringFromListAux showX (list_of_set xs) @ (''}'')))"
(* Abbreviates the representation if the relation is transitive. *)
definition stringFromRelation :: "('a*'a \<Rightarrow> string)\<Rightarrow>('a*'a)set \<Rightarrow> string " where
" stringFromRelation showX rel = (
if trans rel then
(let pruned_rel = (LemExtraDefs.without_trans_edges rel) in
if ((\<forall> e \<in> rel. (e \<in> pruned_rel))) then
(* The relations are the same (there are no transitive edges),
so we can just as well print the original one. *)
stringFromSet showX rel
else
(''trancl of '') @ stringFromSet showX pruned_rel)
else
stringFromSet showX rel )"
definition instance_Show_Show_set_dict :: " 'a Show_class \<Rightarrow>('a set)Show_class " where
" instance_Show_Show_set_dict dict_Show_Show_a = ((|
show_method = (\<lambda> xs. stringFromSet
(show_method dict_Show_Show_a) xs)|) )"
end
|
