equal
deleted
inserted
replaced
15 |
15 |
16 subsection {* exhaustive generator type classes *} |
16 subsection {* exhaustive generator type classes *} |
17 |
17 |
18 class exhaustive = term_of + |
18 class exhaustive = term_of + |
19 fixes exhaustive :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option" |
19 fixes exhaustive :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option" |
|
20 |
|
21 class full_exhaustive = term_of + |
20 fixes full_exhaustive :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option" |
22 fixes full_exhaustive :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option" |
21 |
23 |
22 instantiation code_numeral :: exhaustive |
24 instantiation code_numeral :: full_exhaustive |
23 begin |
25 begin |
24 |
26 |
25 function full_exhaustive_code_numeral' :: "(code_numeral * (unit => term) => term list option) => code_numeral => code_numeral => term list option" |
27 function full_exhaustive_code_numeral' :: "(code_numeral * (unit => term) => term list option) => code_numeral => code_numeral => term list option" |
26 where "full_exhaustive_code_numeral' f d i = |
28 where "full_exhaustive_code_numeral' f d i = |
27 (if d < i then None |
29 (if d < i then None |
31 termination |
33 termination |
32 by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto |
34 by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto |
33 |
35 |
34 definition "full_exhaustive f d = full_exhaustive_code_numeral' f d 0" |
36 definition "full_exhaustive f d = full_exhaustive_code_numeral' f d 0" |
35 |
37 |
|
38 instance .. |
|
39 |
|
40 end |
|
41 |
|
42 instantiation code_numeral :: exhaustive |
|
43 begin |
|
44 |
36 function exhaustive_code_numeral' :: "(code_numeral => term list option) => code_numeral => code_numeral => term list option" |
45 function exhaustive_code_numeral' :: "(code_numeral => term list option) => code_numeral => code_numeral => term list option" |
37 where "exhaustive_code_numeral' f d i = |
46 where "exhaustive_code_numeral' f d i = |
38 (if d < i then None |
47 (if d < i then None |
39 else (f i orelse exhaustive_code_numeral' f d (i + 1)))" |
48 else (f i orelse exhaustive_code_numeral' f d (i + 1)))" |
40 by pat_completeness auto |
49 by pat_completeness auto |
42 termination |
51 termination |
43 by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto |
52 by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto |
44 |
53 |
45 definition "exhaustive f d = exhaustive_code_numeral' f d 0" |
54 definition "exhaustive f d = exhaustive_code_numeral' f d 0" |
46 |
55 |
47 |
|
48 instance .. |
56 instance .. |
49 |
57 |
50 end |
58 end |
51 |
59 |
52 instantiation nat :: exhaustive |
60 instantiation nat :: exhaustive |
53 begin |
61 begin |
54 |
62 |
55 definition "exhaustive f d = exhaustive (%x. f (Code_Numeral.nat_of x)) d" |
63 definition "exhaustive f d = exhaustive (%x. f (Code_Numeral.nat_of x)) d" |
|
64 |
|
65 instance .. |
|
66 |
|
67 end |
|
68 |
|
69 instantiation nat :: full_exhaustive |
|
70 begin |
56 |
71 |
57 definition "full_exhaustive f d = full_exhaustive (%(x, xt). f (Code_Numeral.nat_of x, %_. Code_Evaluation.term_of (Code_Numeral.nat_of x))) d" |
72 definition "full_exhaustive f d = full_exhaustive (%(x, xt). f (Code_Numeral.nat_of x, %_. Code_Evaluation.term_of (Code_Numeral.nat_of x))) d" |
58 |
73 |
59 instance .. |
74 instance .. |
60 |
75 |
70 termination |
85 termination |
71 by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto |
86 by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto |
72 |
87 |
73 definition "exhaustive f d = exhaustive' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))" |
88 definition "exhaustive f d = exhaustive' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))" |
74 |
89 |
|
90 instance .. |
|
91 |
|
92 end |
|
93 |
|
94 instantiation int :: full_exhaustive |
|
95 begin |
|
96 |
75 function full_exhaustive' :: "(int * (unit => term) => term list option) => int => int => term list option" |
97 function full_exhaustive' :: "(int * (unit => term) => term list option) => int => int => term list option" |
76 where "full_exhaustive' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => full_exhaustive' f d (i + 1)))" |
98 where "full_exhaustive' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => full_exhaustive' f d (i + 1)))" |
77 by pat_completeness auto |
99 by pat_completeness auto |
78 |
100 |
79 termination |
101 termination |
88 instantiation prod :: (exhaustive, exhaustive) exhaustive |
110 instantiation prod :: (exhaustive, exhaustive) exhaustive |
89 begin |
111 begin |
90 |
112 |
91 definition |
113 definition |
92 "exhaustive f d = exhaustive (%x. exhaustive (%y. f ((x, y))) d) d" |
114 "exhaustive f d = exhaustive (%x. exhaustive (%y. f ((x, y))) d) d" |
|
115 |
|
116 instance .. |
|
117 |
|
118 end |
|
119 |
|
120 instantiation prod :: (full_exhaustive, full_exhaustive) full_exhaustive |
|
121 begin |
93 |
122 |
94 definition |
123 definition |
95 "full_exhaustive f d = full_exhaustive (%(x, t1). full_exhaustive (%(y, t2). f ((x, y), |
124 "full_exhaustive f d = full_exhaustive (%(x, t1). full_exhaustive (%(y, t2). f ((x, y), |
96 %u. let T1 = (Typerep.typerep (TYPE('a))); |
125 %u. let T1 = (Typerep.typerep (TYPE('a))); |
97 T2 = (Typerep.typerep (TYPE('b))) |
126 T2 = (Typerep.typerep (TYPE('b))) |
116 |
145 |
117 definition exhaustive_fun :: "(('a => 'b) => term list option) => code_numeral => term list option" |
146 definition exhaustive_fun :: "(('a => 'b) => term list option) => code_numeral => term list option" |
118 where |
147 where |
119 "exhaustive_fun f d = exhaustive_fun' f d d" |
148 "exhaustive_fun f d = exhaustive_fun' f d d" |
120 |
149 |
|
150 instance .. |
|
151 |
|
152 end |
|
153 |
|
154 instantiation "fun" :: ("{equal, full_exhaustive}", full_exhaustive) full_exhaustive |
|
155 begin |
121 |
156 |
122 fun full_exhaustive_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option" |
157 fun full_exhaustive_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option" |
123 where |
158 where |
124 "full_exhaustive_fun' f i d = (full_exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d) |
159 "full_exhaustive_fun' f i d = (full_exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d) |
125 orelse (if i > 1 then |
160 orelse (if i > 1 then |