1.1 --- a/src/Tools/isac/BaseDefinitions/rewrite-order.sml Tue Apr 27 18:14:02 2021 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/rewrite-order.sml Tue Apr 27 19:52:29 2021 +0200
1.3 @@ -47,7 +47,7 @@
1.4 fun assoc' ([], key) = raise ERROR ("ME_Isa: \"" ^ key ^ "\" not known")
1.5 | assoc' ((keyi, xi) :: pairs, key) =
1.6 if key = keyi then SOME xi else assoc' (pairs, key);
1.7 -fun assoc_rew_ord ro = ((the o assoc') (! rew_ord',ro))
1.8 - handle _ => raise ERROR ("ME_Isa: rew_ord '" ^ ro ^ "' not in system");
1.9 +fun assoc_rew_ord ro = ((the o assoc') (! rew_ord', ro))
1.10 + handle ERROR _ => raise ERROR ("ME_Isa: rew_ord '" ^ ro ^ "' not in system");
1.11
1.12 end
1.13 \ No newline at end of file
2.1 --- a/src/Tools/isac/BaseDefinitions/theoryC.sml Tue Apr 27 18:14:02 2021 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/theoryC.sml Tue Apr 27 19:52:29 2021 +0200
2.3 @@ -48,7 +48,7 @@
2.4 fun get_theory thy =
2.5 if thy = "empty_thy_id"
2.6 then (get_thy "Base_Tools") (*lower bound of Knowledge*)
2.7 - else (get_thy thy) handle _ => raise ERROR ("ME_Isa: thy \"" ^ thy ^ "\" not in system");
2.8 + else (get_thy thy) handle ERROR _ => raise ERROR ("ME_Isa: thy \"" ^ thy ^ "\" not in system");
2.9
2.10 fun id_to_ctxt thy' = Proof_Context.init_global (get_theory thy');
2.11 fun to_ctxt thy = Proof_Context.init_global thy;
3.1 --- a/src/Tools/isac/BridgeLibisabelle/present-tool.sml Tue Apr 27 18:14:02 2021 +0200
3.2 +++ b/src/Tools/isac/BridgeLibisabelle/present-tool.sml Tue Apr 27 19:52:29 2021 +0200
3.3 @@ -75,9 +75,9 @@
3.4 (* make a guh from a reference to an element in the kestore;
3.5 EXCEPT theory hierarchy ... compare 'fun keref2xml' *)
3.6 fun pblID2guh pblID = (((#guh o Problem.from_store) pblID)
3.7 - handle _ => raise ERROR ("Ptool.pblID2guh: not for \"" ^ strs2str' pblID ^ "\""));
3.8 + handle ERROR _ => raise ERROR ("Ptool.pblID2guh: not for \"" ^ strs2str' pblID ^ "\""));
3.9 fun metID2guh metID = (((#guh o MethodC.from_store) metID)
3.10 - handle _ => raise ERROR ("metID2guh: no 'Met_' for \"" ^ strs2str' metID ^ "\""));
3.11 + handle ERROR _ => raise ERROR ("metID2guh: no 'Met_' for \"" ^ strs2str' metID ^ "\""));
3.12 fun kestoreID2guh Pbl_ kestoreID = pblID2guh kestoreID
3.13 | kestoreID2guh Met_ kestoreID = metID2guh kestoreID
3.14 | kestoreID2guh ketyp kestoreID =
4.1 --- a/src/Tools/isac/Interpret/Interpret.thy Tue Apr 27 18:14:02 2021 +0200
4.2 +++ b/src/Tools/isac/Interpret/Interpret.thy Tue Apr 27 19:52:29 2021 +0200
4.3 @@ -8,7 +8,6 @@
4.4 theory Interpret
4.5 imports Specify.Specify
4.6 begin
4.7 -(* removed all warnings here, only "handle _" remains *)
4.8 ML_file istate.sml
4.9 ML_file "sub-problem.sml"
4.10 ML_file "thy-read.sml"
5.1 --- a/src/Tools/isac/Interpret/derive.sml Tue Apr 27 18:14:02 2021 +0200
5.2 +++ b/src/Tools/isac/Interpret/derive.sml Tue Apr 27 19:52:29 2021 +0200
5.3 @@ -94,7 +94,7 @@
5.4 val _ = msg_5 t'
5.5 val r' = Rule.Thm (thmid, tm)
5.6 in rew_once (lim - 1) (rts @ [(t, r', (t', a'))]) t' Appl rrs' end)
5.7 - handle _ => raise ERROR "derive_norm, Eval: no rewrite")
5.8 + handle NO_REWRITE => raise ERROR "derive_norm, Eval: no rewrite")
5.9 | Rule.Rls_ rls =>
5.10 (case Rewrite.rewrite_set_ thy true rls t of
5.11 NONE => rew_once lim rts t apno rs'
6.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Tue Apr 27 18:14:02 2021 +0200
6.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Tue Apr 27 19:52:29 2021 +0200
6.3 @@ -56,15 +56,15 @@
6.4 in mk_prod TermC.empty (map fac_from_sol ts) end;
6.5
6.6 (*("factors_from_solution", ("Partial_Fractions.factors_from_solution",
6.7 - eval_factors_from_solution ""))*)
6.8 + eval_factors_from_solution ""))
6.9 + this code is limited (max 3 solutions) AND has too little checks *)
6.10 fun eval_factors_from_solution (thmid:string) _
6.11 - (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol) thy =
6.12 - ((let val prod = factors_from_solution sol
6.13 - in SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy prod) "",
6.14 - HOLogic.Trueprop $ (TermC.mk_equality (t, prod)))
6.15 - end)
6.16 - handle _ => NONE)
6.17 - | eval_factors_from_solution _ _ _ _ = NONE;
6.18 + (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol) thy =
6.19 + let val prod = factors_from_solution sol
6.20 + in SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy prod) "",
6.21 + HOLogic.Trueprop $ (TermC.mk_equality (t, prod)))
6.22 + end
6.23 + | eval_factors_from_solution _ _ _ _ = NONE;
6.24 \<close>
6.25
6.26 subsection \<open>'ansatz' for partial fractions\<close>
7.1 --- a/src/Tools/isac/Knowledge/Rational-WN.sml Tue Apr 27 18:14:02 2021 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,257 +0,0 @@
7.4 -(*Stefan K.*)
7.5 -
7.6 -(*protokoll 14.3.02 --------------------------------------------------
7.7 -val ct = parse thy "(a + #1)//(#2*a^^^#2 - #2)";
7.8 -val t = (Thm.term_of o the) ct;
7.9 -atomt t;
7.10 -val ct = parse thy "not (#1+a)"; (*HOL.thy ?*)
7.11 -val t = (Thm.term_of o the) ct;
7.12 -atomt t;
7.13 -val ct = parse thy "x"; (*momentan ist alles 'real'*)
7.14 -val t = (Thm.term_of o the) ct;
7.15 -atomty t;
7.16 -val ct = parse thy "(x::int)"; (* !!! *)
7.17 -val t = (Thm.term_of o the) ct;
7.18 -atomty t;
7.19 -
7.20 -val ct = parse thy "(x::int)*(y::real)"; (*momentan ist alles 'real'*)
7.21 -
7.22 -val Const ("RatArith.cancel",_) $ zaehler $ nenner = t;
7.23 ----------------------------------------------------------------------*)
7.24 -
7.25 -
7.26 -(*diese vvv funktionen kommen nach src/Isa99/termC.sml -------------*)
7.27 -fun UnparseC.term t =
7.28 - let fun ato (Const(a,T)) n =
7.29 - "\n"^indent n^"Const ( "^a^")"
7.30 - | ato (Free (a,T)) n =
7.31 - "\n"^indent n^"Free ( "^a^", "^")"
7.32 - | ato (Var ((a,ix),T)) n =
7.33 - "\n"^indent n^"Var (("^a^", "^string_of_int ix^"), "^")"
7.34 - | ato (Bound ix) n =
7.35 - "\n"^indent n^"Bound "^string_of_int ix
7.36 - | ato (Abs(a,T,body)) n =
7.37 - "\n"^indent n^"Abs( "^a^",.."^ato body (n+1)
7.38 - | ato (f$t') n = ato f n^ato t' (n+1)
7.39 - in "\n-------------"^ato t 0^"\n" end;
7.40 -fun free2int (t as Free (s, _)) = (((the o int_of_str) s)
7.41 - handle _ => raise ERROR ("free2int: "^UnparseC.term t))
7.42 - | free2int t = raise ERROR ("free2int: "^UnparseC.term t);
7.43 -(*diese ^^^ funktionen kommen nach src/Isa99/termC.sml -------------*)
7.44 -
7.45 -
7.46 -(* remark on exceptions: 'error' is implemented by Isabelle
7.47 - as the typical system error *)
7.48 -
7.49 -
7.50 -type poly = int list;
7.51 -
7.52 -(* transform a Isabelle-term t into internal polynomial format
7.53 - preconditions for t:
7.54 - a-b -> a+(-b)
7.55 - x^1 -> x
7.56 - term ordered ascending
7.57 - parentheses right side (caused by 'ordered rewriting')
7.58 - variable as power (not as product) *)
7.59 -
7.60 -fun mono (Const ("RatArith.pow",_) $ t1 $ t2) v g =
7.61 - if t1 = v then ((replicate ((free2int t2) - g) 0) @ [1]) : poly
7.62 - else raise ERROR ("term2poly.1 "^UnparseC.term t1)
7.63 - | mono (t as Const ("Groups.times_class.times",_) $ t1 $
7.64 - (Const ("RatArith.pow",_) $ t2 $ t3)) v g =
7.65 - if t2 = v then (replicate ((free2int t3) - g) 0) @ [free2int t1]
7.66 - else raise ERROR ("term2poly.2 "^UnparseC.term t)
7.67 - | mono t _ _ = raise ERROR ("term2poly.3 "^UnparseC.term t);
7.68 -
7.69 -fun poly (Const ("Groups.plus_class.plus",_) $ t1 $ t2) v g =
7.70 - let val l = mono t1 v g
7.71 - in (l @ (poly t2 v ((length l) + g))) end
7.72 - | poly t v g = mono t v g;
7.73 -
7.74 -fun term2poly (t as Free (s, _)) v =
7.75 - if t = v then SOME ([0,1] : poly) else (SOME [(the o int_of_str) s]
7.76 - handle _ => NONE)
7.77 - | term2poly (Const ("Groups.times_class.times",_) $ (Free (s1,_)) $ (t as Free (s2,_))) v =
7.78 - if t = v then SOME [0, (the o int_of_str) s1] else NONE
7.79 - | term2poly (Const ("Groups.plus_class.plus",_) $ (Free (s1,_)) $ t) v =
7.80 - SOME ([(the o int_of_str) s1] @ (poly t v 1))
7.81 - | term2poly t v =
7.82 - SOME (poly t v 0) handle _ => NONE;
7.83 -
7.84 -(*tests*)
7.85 -val v = (Thm.term_of o the o (parse thy)) "x::real";
7.86 -val t = (Thm.term_of o the o (parse thy)) "#-1::real";
7.87 -term2poly t v;
7.88 -val t = (Thm.term_of o the o (parse thy)) "x::real";
7.89 -term2poly t v;
7.90 -val t = (Thm.term_of o the o (parse thy)) "#1 * x::real"; (*FIXME: drop it*)
7.91 -term2poly t v;
7.92 -val t = (Thm.term_of o the o (parse thy)) "x \<up> #1"; (*FIXME: drop it*)
7.93 -term2poly t v;
7.94 -val t = (Thm.term_of o the o (parse thy)) "x \<up> #3";
7.95 -term2poly t v;
7.96 -val t = (Thm.term_of o the o (parse thy)) "#3 * x \<up> #3";
7.97 -term2poly t v;
7.98 -val t = (Thm.term_of o the o (parse thy)) "#-1 + #3 * x \<up> #3";
7.99 -term2poly t v;
7.100 -val t = (Thm.term_of o the o (parse thy)) "#-1 + (#3 * x \<up> #3 + #5 * x \<up> #5)";
7.101 -term2poly t v;
7.102 -val t = (Thm.term_of o the o (parse thy))
7.103 - "#-1 + (#3 * x \<up> #3 + (#5 * x \<up> #5 + #7 * x \<up> #7))";
7.104 -term2poly t v;
7.105 -val t = (Thm.term_of o the o (parse thy))
7.106 - "#3 * x \<up> #3 + (#5 * x \<up> #5 + #7 * x \<up> #7)";
7.107 -term2poly t v;
7.108 -
7.109 -
7.110 -fun is_polynomial_in t v =
7.111 - case term2poly t v of SOME _ => true | NONE => false;
7.112 -
7.113 -(* transform the internal polynomial p into an Isabelle term t
7.114 - where t meets the preconditions of term2poly
7.115 -val mk_mono =
7.116 - fn : typ -> of the coefficients
7.117 - typ -> of the unknown
7.118 - typ -> of the monomial and polynomial
7.119 - typ -> of the exponent of the unknown
7.120 - int -> the coefficient <> 0
7.121 - string -> the unknown
7.122 - int -> the degree, i.e. the value of the exponent
7.123 - term
7.124 -remark: all the typs above are "RealDef.real" due to the typs of * + ^
7.125 -which may change in the future
7.126 -*)
7.127 -fun mk_mono cT vT pT eT c v g =
7.128 - case g of
7.129 - 0 => Free (str_of_int c, cT) (*will cause problems with diff.typs*)
7.130 - | 1 => if c = 1 then Free (v, vT)
7.131 - else Const ("Groups.times_class.times", [cT, vT]--->pT) $
7.132 - Free (str_of_int c, cT) $ Free (v, vT)
7.133 - | n => if c = 1 then (Const ("RatArith.pow", [vT, eT]--->pT) $
7.134 - Free (v, vT) $ Free (str_of_int g, eT))
7.135 - else Const ("Groups.times_class.times", [cT, vT]--->pT) $
7.136 - Free (str_of_int c, cT) $
7.137 - (Const ("RatArith.pow", [vT, eT]--->pT) $
7.138 - Free (v, vT) $ Free (str_of_int g, eT));
7.139 -(*tests*)
7.140 -val cT = HOLogic.realT; val vT = HOLogic.realT; val pT = HOLogic.realT;
7.141 -val eT = HOLogic.realT;
7.142 -val t = mk_mono cT vT pT eT ~5 "x" 5;
7.143 -(Thm.global_cterm_of thy) t;
7.144 -val t = mk_mono cT vT pT eT ~1 "x" 0;
7.145 -(Thm.global_cterm_of thy) t;
7.146 -val t = mk_mono cT vT pT eT 1 "x" 1;
7.147 -(Thm.global_cterm_of thy) t;
7.148 -
7.149 -
7.150 -fun mk_sum pT t1 t2 = Const ("Groups.plus_class.plus", [pT, pT]--->pT) $ t1 $ t2;
7.151 -
7.152 -
7.153 -fun poly2term cT vT pT eT ([p]:poly) v = mk_mono cT vT pT eT p v 0
7.154 - | poly2term cT vT pT eT (p:poly) v =
7.155 - let
7.156 - fun mk_poly cT vT pT eT [] t v g = t
7.157 - | mk_poly cT vT pT eT [p] t v g =
7.158 - if p = 0 then t
7.159 - else mk_sum pT (mk_mono cT vT pT eT p v g) t
7.160 - | mk_poly cT vT pT eT (p::ps) t v g =
7.161 - if p = 0 then mk_poly cT vT pT eT ps t v (g-1)
7.162 - else mk_poly cT vT pT eT ps
7.163 - (mk_sum pT (mk_mono cT vT pT eT p v g) t) v (g-1)
7.164 - val (p'::ps') = rev p
7.165 - val g = (length p) - 1
7.166 - in mk_poly cT vT pT eT ps' (mk_mono cT vT pT eT p' v g) v (g-1) end;
7.167 -
7.168 -(*tests*)
7.169 -val t = poly2term cT vT pT eT [~1] "x";
7.170 -(Thm.global_cterm_of thy) t;
7.171 -val t = poly2term cT vT pT eT [0,1] "x";
7.172 -(Thm.global_cterm_of thy) t;
7.173 -val t = poly2term cT vT pT eT [0,0,0,1] "x";
7.174 -(Thm.global_cterm_of thy) t;
7.175 -val t = poly2term cT vT pT eT [0,0,0,3] "x";
7.176 -(Thm.global_cterm_of thy) t;
7.177 -val t = poly2term cT vT pT eT [~1,0,0,3] "x";
7.178 -(Thm.global_cterm_of thy) t;
7.179 -val t = poly2term cT vT pT eT [~1,0,0,3,0,5] "x";
7.180 -(Thm.global_cterm_of thy) t;
7.181 -val t = poly2term cT vT pT eT [~1,0,0,3,0,5,0,7] "x";
7.182 -(Thm.global_cterm_of thy) t;
7.183 -val t = poly2term cT vT pT eT [0,0,0,3,0,5,0,7] "x";
7.184 -(Thm.global_cterm_of thy) t;
7.185 -
7.186 -"***************************************************************************";
7.187 -"* reverse-rewriting 12.8.02 *";
7.188 -"***************************************************************************";
7.189 -fun rewrite_set_' thy rls put_asm ruless ct =
7.190 - case ruless of
7.191 - Rule_Set.Rrls _ => raise ERROR "rewrite_set_' not for Rule_Set.Rrls"
7.192 - | Rule_Def.Repeat _ =>
7.193 - let
7.194 - datatype switch = Appl | Noap;
7.195 - fun rew_once ruls asm ct Noap [] = (ct,asm)
7.196 - | rew_once ruls asm ct Appl [] = rew_once ruls asm ct Noap ruls
7.197 - | rew_once ruls asm ct apno (rul::thms) =
7.198 - case rul of
7.199 - Rule.Thm (thmid, thm) =>
7.200 - (case rewrite_ thy ((snd o #rew_ord o Rule_Set.rep) ruless)
7.201 - rls put_asm (Rule.thm rul) ct of
7.202 - NONE => rew_once ruls asm ct apno thms
7.203 - | SOME (ct',asm') =>
7.204 - rew_once ruls (asm union asm') ct' Appl (rul::thms))
7.205 - | Rule.Eval (cc as (op_,_)) =>
7.206 - (case adhoc_thm thy cc ct of
7.207 - NONE => rew_once ruls asm ct apno thms
7.208 - | SOME (thmid, thm') =>
7.209 - let
7.210 - val pairopt =
7.211 - rewrite_ thy ((snd o #rew_ord o Rule_Set.rep) ruless)
7.212 - rls put_asm thm' ct;
7.213 - val _ = if pairopt <> NONE then ()
7.214 - else raise ERROR("rewrite_set_, rewrite_ \""^
7.215 - (ThmC.string_of_thm thm')^"\" \""^
7.216 - (Syntax.string_of_term (ThyC.to_ctxt thy) ct)^"\" = NONE")
7.217 - in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end);
7.218 - val ruls = (#rules o Rule_Set.rep) ruless;
7.219 - val (ct',asm') = rew_once ruls [] ct Noap ruls;
7.220 - in if ct = ct' then NONE else SOME (ct',asm') end;
7.221 -
7.222 -(*
7.223 -fun reverse_rewrite t1 t2 rls =
7.224 -*)
7.225 -fun rewrite_set_' thy rls put_asm ruless ct =
7.226 - case ruless of
7.227 - Rule_Set.Rrls _ => raise ERROR "rewrite_set_' not for Rule_Set.Rrls"
7.228 - | Rule_Def.Repeat _ =>
7.229 - let
7.230 - datatype switch = Appl | Noap;
7.231 - fun rew_once ruls asm ct Noap [] = (ct,asm)
7.232 - | rew_once ruls asm ct Appl [] = rew_once ruls asm ct Noap ruls
7.233 - | rew_once ruls asm ct apno (rul::thms) =
7.234 - case rul of
7.235 - Rule.Thm (thmid, thm) =>
7.236 - (case rewrite_ thy ((snd o #rew_ord o Rule_Set.rep) ruless)
7.237 - rls put_asm (Rule.thm rul) ct of
7.238 - NONE => rew_once ruls asm ct apno thms
7.239 - | SOME (ct',asm') =>
7.240 - rew_once ruls (asm union asm') ct' Appl (rul::thms))
7.241 - | Rule.Eval (cc as (op_,_)) =>
7.242 - (case adhoc_thm thy cc ct of
7.243 - NONE => rew_once ruls asm ct apno thms
7.244 - | SOME (thmid, thm') =>
7.245 - let
7.246 - val pairopt =
7.247 - rewrite_ thy ((snd o #rew_ord o Rule_Set.rep) ruless)
7.248 - rls put_asm thm' ct;
7.249 - val _ = if pairopt <> NONE then ()
7.250 - else raise ERROR("rewrite_set_, rewrite_ \""^
7.251 - (ThmC.string_of_thm thm')^"\" \""^
7.252 - (Syntax.string_of_term (ThyC.to_ctxt thy) ct)^"\" = NONE")
7.253 - in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end);
7.254 - val ruls = (#rules o Rule_Set.rep) ruless;
7.255 - val (ct',asm') = rew_once ruls [] ct Noap ruls;
7.256 - in if ct = ct' then NONE else SOME (ct',asm') end;
7.257 -
7.258 - realpow_two;
7.259 - real_mult_div_cancel1;
7.260 -