1signature ASYMPTOTIC_BASIS = sig
2
3type basis_info = {wf_thm : thm, head : term}
4type basis_ln_info = {ln_thm : thm, trimmed_thm : thm}
5datatype basis' = SSng of basis_info | SCons of (basis_info * basis_ln_info * basis')
6datatype basis = SEmpty | SNE of basis'
7type lifting = thm
8
9exception BASIS of string * basis
10
11val basis_size' : basis' -> int
12val basis_size : basis -> int
13val tl_basis' : basis' -> basis
14val tl_basis : basis -> basis
15val get_basis_wf_thm' : basis' -> thm
16val get_basis_wf_thm : basis -> thm
17val get_ln_info : basis -> basis_ln_info option
18val get_basis_head' : basis' -> term
19val get_basis_head : basis -> term
20val split_basis' : basis' -> basis_info * basis_ln_info option * basis
21val split_basis : basis -> (basis_info * basis_ln_info option * basis) option
22val get_basis_list' : basis' -> term list
23val get_basis_list : basis -> term list
24val get_basis_term : basis -> term
25val extract_basis_list : thm -> term list
26
27val basis_eq' : basis' -> basis' -> bool
28val basis_eq : basis -> basis -> bool
29
30val mk_expansion_level_eq_thm' : basis' -> thm
31val mk_expansion_level_eq_thm : basis -> thm
32
33val check_basis' : basis' -> basis'
34val check_basis : basis -> basis
35
36val combine_lifts : lifting -> lifting -> lifting
37val mk_lifting : term list -> basis -> lifting
38val lift_expands_to_thm : lifting -> thm -> thm
39val lift_trimmed_thm : lifting -> thm -> thm
40val lift_trimmed_pos_thm : lifting -> thm -> thm
41val lift : basis -> thm -> thm
42
43val lift_modification' : basis' -> basis' -> basis'
44val lift_modification : basis -> basis -> basis
45
46val insert_ln' : basis' -> basis'
47val insert_ln : basis -> basis
48
49val default_basis : basis
50
51end
52
53structure Asymptotic_Basis : ASYMPTOTIC_BASIS = struct
54
55type lifting = thm
56
57val concl_of' = Thm.concl_of #> HOLogic.dest_Trueprop
58val dest_fun = dest_comb #> fst
59val dest_arg = dest_comb #> snd
60
61type basis_info = {wf_thm : thm, head : term}
62type basis_ln_info = {ln_thm : thm, trimmed_thm : thm}
63
64datatype basis' = SSng of basis_info | SCons of (basis_info * basis_ln_info * basis')
65datatype basis = SEmpty | SNE of basis'
66
67val 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
75fun basis_size SEmpty = 0
76  | basis_size (SNE b) = basis_size' b
77
78fun tl_basis' (SSng _) = SEmpty
79  | tl_basis' (SCons (_, _, tl)) = SNE tl
80
81fun tl_basis SEmpty = error "tl_basis"
82  | tl_basis (SNE basis) = tl_basis' basis
83
84fun get_basis_wf_thm' (SSng i) = #wf_thm i
85  | get_basis_wf_thm' (SCons (i, _, _)) = #wf_thm i
86
87fun get_basis_wf_thm SEmpty = @{thm basis_wf_Nil}
88  | get_basis_wf_thm (SNE basis) = get_basis_wf_thm' basis
89
90fun get_ln_info (SNE (SCons (_, info, _))) = SOME info
91  | get_ln_info _ = NONE
92
93fun get_basis_head' (SSng i) = #head i
94  | get_basis_head' (SCons (i, _, _)) = #head i
95
96fun get_basis_head SEmpty = error "get_basis_head"
97  | get_basis_head (SNE basis') = get_basis_head' basis'
98
99fun split_basis' (SSng i) = (i, NONE, SEmpty)
100  | split_basis' (SCons (i, ln_thm, tl)) = (i, SOME ln_thm, SNE tl)
101
102fun split_basis SEmpty = NONE
103  | split_basis (SNE basis) = SOME (split_basis' basis)
104
105fun get_basis_list' (SSng i) = [#head i]
106  | get_basis_list' (SCons (i, _, tl)) = #head i :: get_basis_list' tl
107
108fun get_basis_list SEmpty = []
109  | get_basis_list (SNE basis) = get_basis_list' basis
110
111val get_basis_term = HOLogic.mk_list \<^typ>\<open>real => real\<close> o get_basis_list
112
113fun extract_basis_list thm =
114  let
115    val basis =
116      case HOLogic.dest_Trueprop (Thm.concl_of thm) of
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
120      | _ => raise THM ("get_basis", 1, [thm])
121  in
122    HOLogic.dest_list basis |> map Envir.eta_contract
123  end
124
125fun 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
129fun basis_eq SEmpty SEmpty = true
130  | basis_eq (SNE x) (SNE y) = basis_eq' x y
131  | basis_eq _ _ = false
132
133fun 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
137fun 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
140fun dest_wf_thm_head thm = thm |> concl_of' |> dest_arg |> dest_fun |> dest_arg
141
142fun abconv (t, t') = Envir.beta_eta_contract t aconv Envir.beta_eta_contract t'
143
144exception BASIS of (string * basis)
145
146fun 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>\<open>\<lambda>(f::real\<Rightarrow>real) x. ln (f x)\<close> $ 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
167fun check_basis SEmpty = SEmpty
168  | check_basis (SNE basis) = SNE (check_basis' basis)
169
170fun combine_lifts thm1 thm2 = @{thm is_lifting_trans} OF [thm1, thm2]
171
172fun 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>\<open>real => real\<close>) [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
202fun lift_expands_to_thm lifting thm = @{thm expands_to_lift} OF [lifting, thm]
203fun lift_trimmed_thm lifting thm = @{thm trimmed_lifting} OF [lifting, thm]
204fun lift_trimmed_pos_thm lifting thm = @{thm trimmed_pos_lifting} OF [lifting, thm]
205fun apply_lifting lifting thm = @{thm expands_to_lift} OF [lifting, thm]
206fun lift basis thm = apply_lifting (mk_lifting (extract_basis_list thm) basis) thm
207
208fun 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
220fun lift_modification (SNE basis) (SNE new_tail) = SNE (lift_modification' basis new_tail)
221  | lift_modification _ _ = raise BASIS ("lift_modification", SEmpty)
222
223fun insert_ln' (SSng {wf_thm, head}) = 
224      let
225        val head' = Envir.eta_contract
226          (Abs ("x", \<^typ>\<open>real\<close>, \<^term>\<open>ln :: real \<Rightarrow> real\<close> $ (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
236fun insert_ln SEmpty = raise BASIS ("Empty basis", SEmpty)
237  | insert_ln (SNE basis) = check_basis (SNE (insert_ln' basis))
238
239val default_basis = 
240  SNE (SSng {head = \<^term>\<open>\<lambda>x::real. x\<close>, wf_thm = @{thm default_basis_wf}})
241
242end