|
1 signature ASYMPTOTIC_BASIS = sig |
|
2 |
|
3 type basis_info = {wf_thm : thm, head : term} |
|
4 type basis_ln_info = {ln_thm : thm, trimmed_thm : thm} |
|
5 datatype basis' = SSng of basis_info | SCons of (basis_info * basis_ln_info * basis') |
|
6 datatype basis = SEmpty | SNE of basis' |
|
7 type lifting = thm |
|
8 |
|
9 exception BASIS of string * basis |
|
10 |
|
11 val basis_size' : basis' -> int |
|
12 val basis_size : basis -> int |
|
13 val tl_basis' : basis' -> basis |
|
14 val tl_basis : basis -> basis |
|
15 val get_basis_wf_thm' : basis' -> thm |
|
16 val get_basis_wf_thm : basis -> thm |
|
17 val get_ln_info : basis -> basis_ln_info option |
|
18 val get_basis_head' : basis' -> term |
|
19 val get_basis_head : basis -> term |
|
20 val split_basis' : basis' -> basis_info * basis_ln_info option * basis |
|
21 val split_basis : basis -> (basis_info * basis_ln_info option * basis) option |
|
22 val get_basis_list' : basis' -> term list |
|
23 val get_basis_list : basis -> term list |
|
24 val get_basis_term : basis -> term |
|
25 val extract_basis_list : thm -> term list |
|
26 |
|
27 val basis_eq' : basis' -> basis' -> bool |
|
28 val basis_eq : basis -> basis -> bool |
|
29 |
|
30 val mk_expansion_level_eq_thm' : basis' -> thm |
|
31 val mk_expansion_level_eq_thm : basis -> thm |
|
32 |
|
33 val check_basis' : basis' -> basis' |
|
34 val check_basis : basis -> basis |
|
35 |
|
36 val combine_lifts : lifting -> lifting -> lifting |
|
37 val mk_lifting : term list -> basis -> lifting |
|
38 val lift_expands_to_thm : lifting -> thm -> thm |
|
39 val lift_trimmed_thm : lifting -> thm -> thm |
|
40 val lift_trimmed_pos_thm : lifting -> thm -> thm |
|
41 val lift : basis -> thm -> thm |
|
42 |
|
43 val lift_modification' : basis' -> basis' -> basis' |
|
44 val lift_modification : basis -> basis -> basis |
|
45 |
|
46 val insert_ln' : basis' -> basis' |
|
47 val insert_ln : basis -> basis |
|
48 |
|
49 val default_basis : basis |
|
50 |
|
51 end |
|
52 |
|
53 structure Asymptotic_Basis : ASYMPTOTIC_BASIS = struct |
|
54 |
|
55 type lifting = thm |
|
56 |
|
57 val concl_of' = Thm.concl_of #> HOLogic.dest_Trueprop |
|
58 val dest_fun = dest_comb #> fst |
|
59 val dest_arg = dest_comb #> snd |
|
60 |
|
61 type basis_info = {wf_thm : thm, head : term} |
|
62 type basis_ln_info = {ln_thm : thm, trimmed_thm : thm} |
|
63 |
|
64 datatype basis' = SSng of basis_info | SCons of (basis_info * basis_ln_info * basis') |
|
65 datatype basis = SEmpty | SNE of basis' |
|
66 |
|
67 val basis_size' = |
|
68 let |
|
69 fun go acc (SSng _) = acc |
|
70 | go acc (SCons (_, _, tl)) = go (acc + 1) tl |
|
71 in |
|
72 go 1 |
|
73 end |
|
74 |
|
75 fun basis_size SEmpty = 0 |
|
76 | basis_size (SNE b) = basis_size' b |
|
77 |
|
78 fun tl_basis' (SSng _) = SEmpty |
|
79 | tl_basis' (SCons (_, _, tl)) = SNE tl |
|
80 |
|
81 fun tl_basis SEmpty = error "tl_basis" |
|
82 | tl_basis (SNE basis) = tl_basis' basis |
|
83 |
|
84 fun get_basis_wf_thm' (SSng i) = #wf_thm i |
|
85 | get_basis_wf_thm' (SCons (i, _, _)) = #wf_thm i |
|
86 |
|
87 fun get_basis_wf_thm SEmpty = @{thm basis_wf_Nil} |
|
88 | get_basis_wf_thm (SNE basis) = get_basis_wf_thm' basis |
|
89 |
|
90 fun get_ln_info (SNE (SCons (_, info, _))) = SOME info |
|
91 | get_ln_info _ = NONE |
|
92 |
|
93 fun get_basis_head' (SSng i) = #head i |
|
94 | get_basis_head' (SCons (i, _, _)) = #head i |
|
95 |
|
96 fun get_basis_head SEmpty = error "get_basis_head" |
|
97 | get_basis_head (SNE basis') = get_basis_head' basis' |
|
98 |
|
99 fun split_basis' (SSng i) = (i, NONE, SEmpty) |
|
100 | split_basis' (SCons (i, ln_thm, tl)) = (i, SOME ln_thm, SNE tl) |
|
101 |
|
102 fun split_basis SEmpty = NONE |
|
103 | split_basis (SNE basis) = SOME (split_basis' basis) |
|
104 |
|
105 fun get_basis_list' (SSng i) = [#head i] |
|
106 | get_basis_list' (SCons (i, _, tl)) = #head i :: get_basis_list' tl |
|
107 |
|
108 fun get_basis_list SEmpty = [] |
|
109 | get_basis_list (SNE basis) = get_basis_list' basis |
|
110 |
|
111 val get_basis_term = HOLogic.mk_list @{typ "real => real"} o get_basis_list |
|
112 |
|
113 fun extract_basis_list thm = |
|
114 let |
|
115 val basis = |
|
116 case HOLogic.dest_Trueprop (Thm.concl_of thm) of |
|
117 Const (@{const_name "is_expansion"}, _) $ _ $ basis => basis |
|
118 | Const (@{const_name "expands_to"}, _) $ _ $ _ $ basis => basis |
|
119 | Const (@{const_name "basis_wf"}, _) $ basis => basis |
|
120 | _ => raise THM ("get_basis", 1, [thm]) |
|
121 in |
|
122 HOLogic.dest_list basis |> map Envir.eta_contract |
|
123 end |
|
124 |
|
125 fun basis_eq' (SSng i) (SSng i') = #head i = #head i' |
|
126 | basis_eq' (SCons (i,_,tl)) (SCons (i',_,tl')) = #head i aconv #head i' andalso basis_eq' tl tl' |
|
127 | basis_eq' _ _ = false |
|
128 |
|
129 fun basis_eq SEmpty SEmpty = true |
|
130 | basis_eq (SNE x) (SNE y) = basis_eq' x y |
|
131 | basis_eq _ _ = false |
|
132 |
|
133 fun mk_expansion_level_eq_thm' (SSng _) = @{thm expansion_level_eq_Cons[OF expansion_level_eq_Nil]} |
|
134 | mk_expansion_level_eq_thm' (SCons (_, _, tl)) = |
|
135 mk_expansion_level_eq_thm' tl RS @{thm expansion_level_eq_Cons} |
|
136 |
|
137 fun mk_expansion_level_eq_thm SEmpty = @{thm expansion_level_eq_Nil} |
|
138 | mk_expansion_level_eq_thm (SNE basis) = mk_expansion_level_eq_thm' basis |
|
139 |
|
140 fun dest_wf_thm_head thm = thm |> concl_of' |> dest_arg |> dest_fun |> dest_arg |
|
141 |
|
142 fun abconv (t, t') = Envir.beta_eta_contract t aconv Envir.beta_eta_contract t' |
|
143 |
|
144 exception BASIS of (string * basis) |
|
145 |
|
146 fun check_basis' (basis as (SSng {head, wf_thm})) = |
|
147 if abconv (dest_wf_thm_head wf_thm, head) then basis |
|
148 else raise BASIS ("Head mismatch", SNE basis) |
|
149 | check_basis' (basis' as (SCons ({head, wf_thm}, {ln_thm, trimmed_thm}, basis))) = |
|
150 case strip_comb (concl_of' ln_thm) of |
|
151 (_, [ln_fun, ln_exp, ln_basis]) => |
|
152 let |
|
153 val _ = if abconv (dest_wf_thm_head wf_thm, head) then () else |
|
154 raise BASIS ("Head mismatch", SNE basis') |
|
155 val _ = if eq_list abconv (HOLogic.dest_list ln_basis, get_basis_list' basis) |
|
156 then () else raise BASIS ("Incorrect basis in ln_thm", SNE basis') |
|
157 val _ = if abconv (ln_fun, @{term "\<lambda>(f::real\<Rightarrow>real) x. ln (f x)"} $ head) then () else |
|
158 raise BASIS ("Wrong function in ln_expansion", SNE basis') |
|
159 val _ = if abconv (ln_exp, trimmed_thm |> concl_of' |> dest_arg) then () else |
|
160 raise BASIS ("Wrong expansion in trimmed_thm", SNE basis') |
|
161 val _ = check_basis' basis |
|
162 in |
|
163 basis' |
|
164 end |
|
165 | _ => raise BASIS ("Malformed ln_thm", SNE basis') |
|
166 |
|
167 fun check_basis SEmpty = SEmpty |
|
168 | check_basis (SNE basis) = SNE (check_basis' basis) |
|
169 |
|
170 fun combine_lifts thm1 thm2 = @{thm is_lifting_trans} OF [thm1, thm2] |
|
171 |
|
172 fun mk_lifting bs basis = |
|
173 let |
|
174 fun mk_lifting_aux [] basis = |
|
175 (case split_basis basis of |
|
176 NONE => @{thm is_lifting_id} |
|
177 | SOME (_, _, basis') => |
|
178 combine_lifts (mk_lifting_aux [] basis') |
|
179 (get_basis_wf_thm basis RS @{thm is_lifting_lift})) |
|
180 | mk_lifting_aux (b :: bs) basis = |
|
181 (case split_basis basis of |
|
182 NONE => raise Match |
|
183 | SOME ({head = b', ...}, _, basis') => |
|
184 if b aconv b' then |
|
185 if eq_list (op aconv) (get_basis_list basis', bs) then |
|
186 @{thm is_lifting_id} |
|
187 else |
|
188 @{thm is_lifting_map} OF |
|
189 [mk_lifting_aux bs basis', mk_expansion_level_eq_thm basis'] |
|
190 else |
|
191 combine_lifts (mk_lifting_aux (b :: bs) basis') |
|
192 (get_basis_wf_thm basis RS @{thm is_lifting_lift})) |
|
193 val bs' = get_basis_list basis |
|
194 fun err () = raise TERM ("mk_lifting", map (HOLogic.mk_list @{typ "real => real"}) [bs, bs']) |
|
195 in |
|
196 if subset (op aconv) (bs, bs') then |
|
197 mk_lifting_aux bs basis handle Match => err () |
|
198 else |
|
199 err () |
|
200 end |
|
201 |
|
202 fun lift_expands_to_thm lifting thm = @{thm expands_to_lift} OF [lifting, thm] |
|
203 fun lift_trimmed_thm lifting thm = @{thm trimmed_lifting} OF [lifting, thm] |
|
204 fun lift_trimmed_pos_thm lifting thm = @{thm trimmed_pos_lifting} OF [lifting, thm] |
|
205 fun apply_lifting lifting thm = @{thm expands_to_lift} OF [lifting, thm] |
|
206 fun lift basis thm = apply_lifting (mk_lifting (extract_basis_list thm) basis) thm |
|
207 |
|
208 fun lift_modification' (SSng s) _ = raise BASIS ("lift_modification", SNE (SSng s)) |
|
209 | lift_modification' (SCons ({wf_thm, head}, {ln_thm, trimmed_thm}, _)) new_tail = |
|
210 let |
|
211 val wf_thm' = @{thm basis_wf_lift_modification} OF [wf_thm, get_basis_wf_thm' new_tail] |
|
212 val lifting = mk_lifting (extract_basis_list ln_thm) (SNE new_tail) |
|
213 val ln_thm' = apply_lifting lifting ln_thm |
|
214 val trimmed_thm' = lift_trimmed_pos_thm lifting trimmed_thm |
|
215 in |
|
216 SCons ({wf_thm = wf_thm', head = head}, |
|
217 {ln_thm = ln_thm', trimmed_thm = trimmed_thm'}, new_tail) |
|
218 end |
|
219 |
|
220 fun lift_modification (SNE basis) (SNE new_tail) = SNE (lift_modification' basis new_tail) |
|
221 | lift_modification _ _ = raise BASIS ("lift_modification", SEmpty) |
|
222 |
|
223 fun insert_ln' (SSng {wf_thm, head}) = |
|
224 let |
|
225 val head' = Envir.eta_contract |
|
226 (Abs ("x", @{typ real}, @{term "ln :: real \<Rightarrow> real"} $ (betapply (head, Bound 0)))) |
|
227 val info1 = {wf_thm = wf_thm RS @{thm basis_wf_insert_ln(2)}, head = head} |
|
228 val info2 = {wf_thm = wf_thm RS @{thm basis_wf_insert_ln(1)}, head = head'} |
|
229 val ln_thm = wf_thm RS @{thm expands_to_insert_ln} |
|
230 val trimmed_thm = wf_thm RS @{thm trimmed_pos_insert_ln} |
|
231 in |
|
232 SCons (info1, {ln_thm = ln_thm, trimmed_thm = trimmed_thm}, SSng info2) |
|
233 end |
|
234 | insert_ln' (basis as (SCons (_, _, tail))) = lift_modification' basis (insert_ln' tail) |
|
235 |
|
236 fun insert_ln SEmpty = raise BASIS ("Empty basis", SEmpty) |
|
237 | insert_ln (SNE basis) = check_basis (SNE (insert_ln' basis)) |
|
238 |
|
239 val default_basis = |
|
240 SNE (SSng {head = @{term "\<lambda>x::real. x"}, wf_thm = @{thm default_basis_wf}}) |
|
241 |
|
242 end |