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