68630
|
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 |
|
69597
|
111 |
val get_basis_term = HOLogic.mk_list \<^typ>\<open>real => real\<close> o get_basis_list
|
68630
|
112 |
|
|
113 |
fun extract_basis_list thm =
|
|
114 |
let
|
|
115 |
val basis =
|
|
116 |
case HOLogic.dest_Trueprop (Thm.concl_of thm) of
|
69597
|
117 |
Const (\<^const_name>\<open>is_expansion\<close>, _) $ _ $ basis => basis
|
|
118 |
| Const (\<^const_name>\<open>expands_to\<close>, _) $ _ $ _ $ basis => basis
|
|
119 |
| Const (\<^const_name>\<open>basis_wf\<close>, _) $ basis => basis
|
68630
|
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')
|
69597
|
157 |
val _ = if abconv (ln_fun, \<^term>\<open>\<lambda>(f::real\<Rightarrow>real) x. ln (f x)\<close> $ head) then () else
|
68630
|
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
|
69597
|
194 |
fun err () = raise TERM ("mk_lifting", map (HOLogic.mk_list \<^typ>\<open>real => real\<close>) [bs, bs'])
|
68630
|
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
|
69597
|
226 |
(Abs ("x", \<^typ>\<open>real\<close>, \<^term>\<open>ln :: real \<Rightarrow> real\<close> $ (betapply (head, Bound 0))))
|
68630
|
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 =
|
69597
|
240 |
SNE (SSng {head = \<^term>\<open>\<lambda>x::real. x\<close>, wf_thm = @{thm default_basis_wf}})
|
68630
|
241 |
|
|
242 |
end |