172 fun eval_root_free (thmid:string) _ (t as (Const (op0, t0) $ arg)) thy = |
172 fun eval_root_free (thmid:string) _ (t as (Const (op0, t0) $ arg)) thy = |
173 if strip_thy op0 <> "is'_root'_free" |
173 if strip_thy op0 <> "is'_root'_free" |
174 then error ("eval_root_free: wrong " ^ op0) |
174 then error ("eval_root_free: wrong " ^ op0) |
175 else if TermC.const_in (strip_thy op0) arg |
175 else if TermC.const_in (strip_thy op0) arg |
176 then SOME (TermC.mk_thmid thmid "" (term_to_string''' thy arg)"", |
176 then SOME (TermC.mk_thmid thmid "" (term_to_string''' thy arg)"", |
177 TermC.Trueprop $ (TermC.mk_equality (t, @{term False}))) |
177 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))) |
178 else SOME (TermC.mk_thmid thmid "" (term_to_string''' thy arg)"", |
178 else SOME (TermC.mk_thmid thmid "" (term_to_string''' thy arg)"", |
179 TermC.Trueprop $ (TermC.mk_equality (t, @{term True}))) |
179 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))) |
180 | eval_root_free _ _ _ _ = NONE; |
180 | eval_root_free _ _ _ _ = NONE; |
181 |
181 |
182 (*does a term contain a root ?*) |
182 (*does a term contain a root ?*) |
183 fun eval_contains_root (thmid:string) _ |
183 fun eval_contains_root (thmid:string) _ |
184 (t as (Const("Test.contains'_root",t0) $ arg)) thy = |
184 (t as (Const("Test.contains'_root",t0) $ arg)) thy = |
185 if member op = (ids_of arg) "sqrt" |
185 if member op = (ids_of arg) "sqrt" |
186 then SOME (TermC.mk_thmid thmid "" (term_to_string''' thy arg)"", |
186 then SOME (TermC.mk_thmid thmid "" (term_to_string''' thy arg)"", |
187 TermC.Trueprop $ (TermC.mk_equality (t, @{term True}))) |
187 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))) |
188 else SOME (TermC.mk_thmid thmid "" (term_to_string''' thy arg)"", |
188 else SOME (TermC.mk_thmid thmid "" (term_to_string''' thy arg)"", |
189 TermC.Trueprop $ (TermC.mk_equality (t, @{term False}))) |
189 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))) |
190 | eval_contains_root _ _ _ _ = NONE; |
190 | eval_contains_root _ _ _ _ = NONE; |
191 |
191 |
192 (*dummy precondition for root-met of x+1=2*) |
192 (*dummy precondition for root-met of x+1=2*) |
193 fun eval_precond_rootmet (thmid:string) _ (t as (Const ("Test.precond'_rootmet", _) $ arg)) thy = |
193 fun eval_precond_rootmet (thmid:string) _ (t as (Const ("Test.precond'_rootmet", _) $ arg)) thy = |
194 SOME (TermC.mk_thmid thmid "" (term_to_string''' thy arg)"", |
194 SOME (TermC.mk_thmid thmid "" (term_to_string''' thy arg)"", |
195 TermC.Trueprop $ (TermC.mk_equality (t, @{term True}))) |
195 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))) |
196 | eval_precond_rootmet _ _ _ _ = NONE; |
196 | eval_precond_rootmet _ _ _ _ = NONE; |
197 |
197 |
198 (*dummy precondition for root-pbl of x+1=2*) |
198 (*dummy precondition for root-pbl of x+1=2*) |
199 fun eval_precond_rootpbl (thmid:string) _ (t as (Const ("Test.precond'_rootpbl", _) $ arg)) thy = |
199 fun eval_precond_rootpbl (thmid:string) _ (t as (Const ("Test.precond'_rootpbl", _) $ arg)) thy = |
200 SOME (TermC.mk_thmid thmid "" (term_to_string''' thy arg) "", |
200 SOME (TermC.mk_thmid thmid "" (term_to_string''' thy arg) "", |
201 TermC.Trueprop $ (TermC.mk_equality (t, @{term True}))) |
201 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))) |
202 | eval_precond_rootpbl _ _ _ _ = NONE; |
202 | eval_precond_rootpbl _ _ _ _ = NONE; |
203 *} |
203 *} |
204 setup {* KEStore_Elems.add_calcs |
204 setup {* KEStore_Elems.add_calcs |
205 [("is_root_free", ("Test.is'_root'_free", eval_root_free"#is_root_free_e")), |
205 [("is_root_free", ("Test.is'_root'_free", eval_root_free"#is_root_free_e")), |
206 ("contains_root", ("Test.contains'_root", eval_contains_root"#contains_root_")), |
206 ("contains_root", ("Test.contains'_root", eval_contains_root"#contains_root_")), |
624 (*| atom (_ (_,"?DUMMY" )) = true ..ML-error *) |
624 (*| atom (_ (_,"?DUMMY" )) = true ..ML-error *) |
625 | atom((Const ("Bin.integ_of_bin",_)) $ _) = true |
625 | atom((Const ("Bin.integ_of_bin",_)) $ _) = true |
626 | atom _ = false; |
626 | atom _ = false; |
627 |
627 |
628 fun varids (Const (s,Type (_,[]))) = [strip_thy s] |
628 fun varids (Const (s,Type (_,[]))) = [strip_thy s] |
629 | varids (Free (s,Type (_,[]))) = if TermC.is_no s then [] |
629 | varids (Free (s,Type (_,[]))) = if TermC.is_num' s then [] |
630 else [strip_thy s] |
630 else [strip_thy s] |
631 | varids (Var((s,_),Type (_,[]))) = [strip_thy s] |
631 | varids (Var((s,_),Type (_,[]))) = [strip_thy s] |
632 (*| varids (_ (s,"?DUMMY" )) = ..ML-error *) |
632 (*| varids (_ (s,"?DUMMY" )) = ..ML-error *) |
633 | varids((Const ("Bin.integ_of_bin",_)) $ _)= [](*8.01: superfluous?*) |
633 | varids((Const ("Bin.integ_of_bin",_)) $ _)= [](*8.01: superfluous?*) |
634 | varids (Abs(a,T,t)) = union op = [a] (varids t) |
634 | varids (Abs(a,T,t)) = union op = [a] (varids t) |
1055 | dest_hd' (Var v) = (v, 2) |
1055 | dest_hd' (Var v) = (v, 2) |
1056 | dest_hd' (Bound i) = ((("", i), dummyT), 3) |
1056 | dest_hd' (Bound i) = ((("", i), dummyT), 3) |
1057 | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4); |
1057 | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4); |
1058 (* RL *) |
1058 (* RL *) |
1059 fun get_order_pow (t $ (Free(order,_))) = |
1059 fun get_order_pow (t $ (Free(order,_))) = |
1060 (case TermC.int_of_str (order) of |
1060 (case TermC.int_of_str_opt (order) of |
1061 SOME d => d |
1061 SOME d => d |
1062 | NONE => 0) |
1062 | NONE => 0) |
1063 | get_order_pow _ = 0; |
1063 | get_order_pow _ = 0; |
1064 |
1064 |
1065 fun size_of_term' (Const(str,_) $ t) = |
1065 fun size_of_term' (Const(str,_) $ t) = |