89 instantiation "fun" :: ("{equal, exhaustive}", exhaustive) exhaustive |
89 instantiation "fun" :: ("{equal, exhaustive}", exhaustive) exhaustive |
90 begin |
90 begin |
91 |
91 |
92 fun exhaustive_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option" |
92 fun exhaustive_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option" |
93 where |
93 where |
94 "exhaustive_fun' f i d = (if i > 1 then |
94 "exhaustive_fun' f i d = (exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d) |
95 exhaustive (%(a, at). exhaustive (%(b, bt). |
95 orelse (if i > 1 then |
96 exhaustive_fun' (%(g, gt). f (g(a := b), |
96 exhaustive_fun' (%(g, gt). exhaustive (%(a, at). exhaustive (%(b, bt). |
97 (%_. let T1 = (Typerep.typerep (TYPE('a))); |
97 f (g(a := b), |
98 T2 = (Typerep.typerep (TYPE('b))) |
98 (%_. let A = (Typerep.typerep (TYPE('a))); |
99 in |
99 B = (Typerep.typerep (TYPE('b))); |
100 Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App |
100 fun = (%T U. Typerep.Typerep (STR ''fun'') [T, U]) |
101 (Code_Evaluation.Const (STR ''Fun.fun_upd'') |
101 in |
102 (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2], |
102 Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App |
103 Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]])) |
103 (Code_Evaluation.Const (STR ''Fun.fun_upd'') (fun (fun A B) (fun A (fun B (fun A B))))) |
104 (gt ())) (at ())) (bt ())))) (i - 1) d) d) d |
104 (gt ())) (at ())) (bt ())))) d) d) (i - 1) d else None)" |
105 else (if i > 0 then |
|
106 exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d else None))" |
|
107 |
105 |
108 definition exhaustive_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option" |
106 definition exhaustive_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option" |
109 where |
107 where |
110 "exhaustive_fun f d = exhaustive_fun' f d d" |
108 "exhaustive_fun f d = exhaustive_fun' f d d" |
111 |
109 |