1.1 --- a/src/Tools/isac/Knowledge/Atools.thy Tue Jul 26 13:30:37 2011 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Atools.thy Tue Jul 26 15:25:28 2011 +0200
1.3 @@ -52,17 +52,19 @@
1.4 radd_left_cancel_le:"((k::real) + m <= k + n) = (m <= n)" and
1.5 not_true: "(~ True) = False" and
1.6 not_false: "(~ False) = True"
1.7 -axiomatization where
1.8 +axiomatization where (*..if replaced by "and" we get error:
1.9 +Type unification failed: No type arity bool :: zero ...*)
1.10 and_true: "(a & True) = a" and
1.11 and_false: "(a & False) = False" and
1.12 or_true: "(a | True) = True" and
1.13 or_false: "(a | False) = a" and
1.14 and_commute: "(a & b) = (b & a)" and
1.15 - or_commute: "(a | b) = (b | a)"
1.16 + or_commute: "(a | b) = (b | a)"
1.17
1.18 (*.should be in Rational.thy, but:
1.19 needed for asms in e.g. d2_pqformula1 in PolyEq.ML, RootEq.ML.*)
1.20 -axiomatization where
1.21 + axiomatization where (*..if replaced by "and" we get error:
1.22 +Type unification failed: No type arity bool :: zero ...*)
1.23 rat_leq1: "[| b ~= 0; d ~= 0 |] ==>
1.24 ((a / b) <= (c / d)) = ((a*d) <= (b*c))"(*Isa?*) and
1.25 rat_leq2: "d ~= 0 ==>
2.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Tue Jul 26 13:30:37 2011 +0200
2.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Tue Jul 26 15:25:28 2011 +0200
2.3 @@ -47,7 +47,7 @@
2.4 separate_bdvs_mult:
2.5 "[| [] from [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a; Not (a=!=0) |]
2.6 ==>(a * b = c) = (b = c / a)"
2.7 -axiomatization where (*..if replaced by "and" we get an error in
2.8 +axiomatization where (*..if replaced by "and" we get an error in
2.9 --- rewrite in [EqSystem,normalize,2x2] --- step "--- 3---";*)
2.10 order_system_NxN: "[a,b] = [b,a]"
2.11 (*requires rew_ord for termination, eg. ord_simplify_Integral;
3.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Tue Jul 26 13:30:37 2011 +0200
3.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Tue Jul 26 15:25:28 2011 +0200
3.3 @@ -169,10 +169,24 @@
3.4 "[|(c<0);Not(bdv occurs_in c)|] ==> (bdv^^^2=c) = False" and
3.5 d2_sqrt_equation2: "(bdv^^^2=0) = (bdv=0)" and
3.6 d2_sqrt_equation3: "(b*bdv^^^2=0) = (bdv=0)"
3.7 - axiomatization where
3.8 +axiomatization where (*..if replaced by "and" we get errors:
3.9 + exception PTREE "nth _ []" raised
3.10 + (line 783 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml"):
3.11 + 'fun nth _ [] = raise PTREE "nth _ []"'
3.12 +and
3.13 + exception Bind raised
3.14 + (line 1097 of "/usr/local/isabisac/test/Tools/isac/Frontend/interface.sml"):
3.15 + 'val (Form f, tac, asms) = pt_extract (pt, p);' *)
3.16 d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))" and
3.17 - d2_reduce_equation2: "(bdv*(a + bdv)=0) = ((bdv=0)|(a+ bdv=0))"
3.18 - axiomatization where
3.19 + d2_reduce_equation2: "(bdv*(a + bdv)=0) = ((bdv=0)|(a+ bdv=0))"
3.20 +axiomatization where (*..if replaced by "and" we get errors:
3.21 + exception PTREE "nth _ []" raised
3.22 + (line 783 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml"):
3.23 + 'fun nth _ [] = raise PTREE "nth _ []"'
3.24 +and
3.25 + exception Bind raised
3.26 + (line 1097 of "/usr/local/isabisac/test/Tools/isac/Frontend/interface.sml"):
3.27 + 'val (Form f, tac, asms) = pt_extract (pt, p);' *)
3.28 d2_pqformula1: "[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+ bdv^^^2=0) =
3.29 ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 4*q)/2)
3.30 | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 4*q)/2))" and
3.31 @@ -184,184 +198,184 @@
3.32 d2_pqformula3: "[|0<=1 - 4*q|] ==> (q+ bdv+ bdv^^^2=0) =
3.33 ((bdv= (-1)*(1/2) + sqrt(1 - 4*q)/2)
3.34 | (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))" and
3.35 - d2_pqformula3_neg: "[|1 - 4*q<0|] ==> (q+ bdv+ bdv^^^2=0) = False"
3.36 - axioms
3.37 + d2_pqformula3_neg: "[|1 - 4*q<0|] ==> (q+ bdv+ bdv^^^2=0) = False" and
3.38 d2_pqformula4: "[|0<=1 - 4*q|] ==> (q+ bdv+1*bdv^^^2=0) =
3.39 ((bdv= (-1)*(1/2) + sqrt(1 - 4*q)/2)
3.40 - | (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))"
3.41 - d2_pqformula4_neg: "[|1 - 4*q<0|] ==> (q+ bdv+1*bdv^^^2=0) = False"
3.42 + | (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))" and
3.43 + d2_pqformula4_neg: "[|1 - 4*q<0|] ==> (q+ bdv+1*bdv^^^2=0) = False" and
3.44 d2_pqformula5: "[|0<=p^^^2 - 0|] ==> ( p*bdv+ bdv^^^2=0) =
3.45 ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 0)/2)
3.46 - | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))"
3.47 - (* d2_pqformula5_neg not need p^2 never less zero in R *)
3.48 + | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))" and
3.49 + (* d2_pqformula5_neg not need p^2 never less zero in R *)
3.50 d2_pqformula6: "[|0<=p^^^2 - 0|] ==> ( p*bdv+1*bdv^^^2=0) =
3.51 ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 0)/2)
3.52 - | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))"
3.53 + | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))" and
3.54 (* d2_pqformula6_neg not need p^2 never less zero in R *)
3.55 - d2_pqformula7: "[|0<=1 - 0|] ==> ( bdv+ bdv^^^2=0) =
3.56 + d2_pqformula7: "[|0<=1 - 0|] ==> ( bdv+ bdv^^^2=0) =
3.57 ((bdv= (-1)*(1/2) + sqrt(1 - 0)/2)
3.58 - | (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))"
3.59 + | (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))" and
3.60 (* d2_pqformula7_neg not need, because 1<0 ==> False*)
3.61 d2_pqformula8: "[|0<=1 - 0|] ==> ( bdv+1*bdv^^^2=0) =
3.62 ((bdv= (-1)*(1/2) + sqrt(1 - 0)/2)
3.63 - | (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))"
3.64 + | (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))" and
3.65 (* d2_pqformula8_neg not need, because 1<0 ==> False*)
3.66 d2_pqformula9: "[|Not(bdv occurs_in q); 0<= (-1)*4*q|] ==>
3.67 (q+ 1*bdv^^^2=0) = ((bdv= 0 + sqrt(0 - 4*q)/2)
3.68 - | (bdv= 0 - sqrt(0 - 4*q)/2))"
3.69 + | (bdv= 0 - sqrt(0 - 4*q)/2))" and
3.70 d2_pqformula9_neg:
3.71 - "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+ 1*bdv^^^2=0) = False"
3.72 + "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+ 1*bdv^^^2=0) = False" and
3.73 d2_pqformula10:
3.74 "[|Not(bdv occurs_in q); 0<= (-1)*4*q|] ==> (q+ bdv^^^2=0) =
3.75 ((bdv= 0 + sqrt(0 - 4*q)/2)
3.76 - | (bdv= 0 - sqrt(0 - 4*q)/2))"
3.77 + | (bdv= 0 - sqrt(0 - 4*q)/2))" and
3.78 d2_pqformula10_neg:
3.79 - "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+ bdv^^^2=0) = False"
3.80 + "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+ bdv^^^2=0) = False" and
3.81 d2_abcformula1:
3.82 "[|0<=b^^^2 - 4*a*c|] ==> (c + b*bdv+a*bdv^^^2=0) =
3.83 ((bdv=( -b + sqrt(b^^^2 - 4*a*c))/(2*a))
3.84 - | (bdv=( -b - sqrt(b^^^2 - 4*a*c))/(2*a)))"
3.85 + | (bdv=( -b - sqrt(b^^^2 - 4*a*c))/(2*a)))" and
3.86 d2_abcformula1_neg:
3.87 - "[|b^^^2 - 4*a*c<0|] ==> (c + b*bdv+a*bdv^^^2=0) = False"
3.88 + "[|b^^^2 - 4*a*c<0|] ==> (c + b*bdv+a*bdv^^^2=0) = False" and
3.89 d2_abcformula2:
3.90 "[|0<=1 - 4*a*c|] ==> (c+ bdv+a*bdv^^^2=0) =
3.91 ((bdv=( -1 + sqrt(1 - 4*a*c))/(2*a))
3.92 - | (bdv=( -1 - sqrt(1 - 4*a*c))/(2*a)))"
3.93 + | (bdv=( -1 - sqrt(1 - 4*a*c))/(2*a)))" and
3.94 d2_abcformula2_neg:
3.95 - "[|1 - 4*a*c<0|] ==> (c+ bdv+a*bdv^^^2=0) = False"
3.96 + "[|1 - 4*a*c<0|] ==> (c+ bdv+a*bdv^^^2=0) = False" and
3.97 d2_abcformula3:
3.98 "[|0<=b^^^2 - 4*1*c|] ==> (c + b*bdv+ bdv^^^2=0) =
3.99 ((bdv=( -b + sqrt(b^^^2 - 4*1*c))/(2*1))
3.100 - | (bdv=( -b - sqrt(b^^^2 - 4*1*c))/(2*1)))"
3.101 + | (bdv=( -b - sqrt(b^^^2 - 4*1*c))/(2*1)))" and
3.102 d2_abcformula3_neg:
3.103 - "[|b^^^2 - 4*1*c<0|] ==> (c + b*bdv+ bdv^^^2=0) = False"
3.104 + "[|b^^^2 - 4*1*c<0|] ==> (c + b*bdv+ bdv^^^2=0) = False" and
3.105 d2_abcformula4:
3.106 "[|0<=1 - 4*1*c|] ==> (c + bdv+ bdv^^^2=0) =
3.107 ((bdv=( -1 + sqrt(1 - 4*1*c))/(2*1))
3.108 - | (bdv=( -1 - sqrt(1 - 4*1*c))/(2*1)))"
3.109 + | (bdv=( -1 - sqrt(1 - 4*1*c))/(2*1)))" and
3.110 d2_abcformula4_neg:
3.111 - "[|1 - 4*1*c<0|] ==> (c + bdv+ bdv^^^2=0) = False"
3.112 + "[|1 - 4*1*c<0|] ==> (c + bdv+ bdv^^^2=0) = False" and
3.113 d2_abcformula5:
3.114 "[|Not(bdv occurs_in c); 0<=0 - 4*a*c|] ==> (c + a*bdv^^^2=0) =
3.115 ((bdv=( 0 + sqrt(0 - 4*a*c))/(2*a))
3.116 - | (bdv=( 0 - sqrt(0 - 4*a*c))/(2*a)))"
3.117 + | (bdv=( 0 - sqrt(0 - 4*a*c))/(2*a)))" and
3.118 d2_abcformula5_neg:
3.119 - "[|Not(bdv occurs_in c); 0 - 4*a*c<0|] ==> (c + a*bdv^^^2=0) = False"
3.120 + "[|Not(bdv occurs_in c); 0 - 4*a*c<0|] ==> (c + a*bdv^^^2=0) = False" and
3.121 d2_abcformula6:
3.122 "[|Not(bdv occurs_in c); 0<=0 - 4*1*c|] ==> (c+ bdv^^^2=0) =
3.123 ((bdv=( 0 + sqrt(0 - 4*1*c))/(2*1))
3.124 - | (bdv=( 0 - sqrt(0 - 4*1*c))/(2*1)))"
3.125 + | (bdv=( 0 - sqrt(0 - 4*1*c))/(2*1)))" and
3.126 d2_abcformula6_neg:
3.127 - "[|Not(bdv occurs_in c); 0 - 4*1*c<0|] ==> (c+ bdv^^^2=0) = False"
3.128 + "[|Not(bdv occurs_in c); 0 - 4*1*c<0|] ==> (c+ bdv^^^2=0) = False" and
3.129 d2_abcformula7:
3.130 "[|0<=b^^^2 - 0|] ==> ( b*bdv+a*bdv^^^2=0) =
3.131 ((bdv=( -b + sqrt(b^^^2 - 0))/(2*a))
3.132 - | (bdv=( -b - sqrt(b^^^2 - 0))/(2*a)))"
3.133 + | (bdv=( -b - sqrt(b^^^2 - 0))/(2*a)))" and
3.134 (* d2_abcformula7_neg not need b^2 never less zero in R *)
3.135 d2_abcformula8:
3.136 "[|0<=b^^^2 - 0|] ==> ( b*bdv+ bdv^^^2=0) =
3.137 ((bdv=( -b + sqrt(b^^^2 - 0))/(2*1))
3.138 - | (bdv=( -b - sqrt(b^^^2 - 0))/(2*1)))"
3.139 + | (bdv=( -b - sqrt(b^^^2 - 0))/(2*1)))" and
3.140 (* d2_abcformula8_neg not need b^2 never less zero in R *)
3.141 d2_abcformula9:
3.142 "[|0<=1 - 0|] ==> ( bdv+a*bdv^^^2=0) =
3.143 ((bdv=( -1 + sqrt(1 - 0))/(2*a))
3.144 - | (bdv=( -1 - sqrt(1 - 0))/(2*a)))"
3.145 + | (bdv=( -1 - sqrt(1 - 0))/(2*a)))" and
3.146 (* d2_abcformula9_neg not need, because 1<0 ==> False*)
3.147 d2_abcformula10:
3.148 "[|0<=1 - 0|] ==> ( bdv+ bdv^^^2=0) =
3.149 ((bdv=( -1 + sqrt(1 - 0))/(2*1))
3.150 - | (bdv=( -1 - sqrt(1 - 0))/(2*1)))"
3.151 + | (bdv=( -1 - sqrt(1 - 0))/(2*1)))" and
3.152 (* d2_abcformula10_neg not need, because 1<0 ==> False*)
3.153
3.154 +
3.155 (* ---- degree 3 ----*)
3.156 d3_reduce_equation1:
3.157 - "(a*bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + b*bdv + c*bdv^^^2=0))"
3.158 + "(a*bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + b*bdv + c*bdv^^^2=0))" and
3.159 d3_reduce_equation2:
3.160 - "( bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + b*bdv + c*bdv^^^2=0))"
3.161 + "( bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + b*bdv + c*bdv^^^2=0))" and
3.162 d3_reduce_equation3:
3.163 - "(a*bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + bdv + c*bdv^^^2=0))"
3.164 + "(a*bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + bdv + c*bdv^^^2=0))" and
3.165 d3_reduce_equation4:
3.166 - "( bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + bdv + c*bdv^^^2=0))"
3.167 + "( bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + bdv + c*bdv^^^2=0))" and
3.168 d3_reduce_equation5:
3.169 - "(a*bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (a + b*bdv + bdv^^^2=0))"
3.170 + "(a*bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (a + b*bdv + bdv^^^2=0))" and
3.171 d3_reduce_equation6:
3.172 - "( bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + b*bdv + bdv^^^2=0))"
3.173 + "( bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + b*bdv + bdv^^^2=0))" and
3.174 d3_reduce_equation7:
3.175 - "(a*bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0))"
3.176 + "(a*bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0))" and
3.177 d3_reduce_equation8:
3.178 - "( bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0))"
3.179 + "( bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0))" and
3.180 d3_reduce_equation9:
3.181 - "(a*bdv + c*bdv^^^3=0) = (bdv=0 | (a + c*bdv^^^2=0))"
3.182 + "(a*bdv + c*bdv^^^3=0) = (bdv=0 | (a + c*bdv^^^2=0))" and
3.183 d3_reduce_equation10:
3.184 - "( bdv + c*bdv^^^3=0) = (bdv=0 | (1 + c*bdv^^^2=0))"
3.185 + "( bdv + c*bdv^^^3=0) = (bdv=0 | (1 + c*bdv^^^2=0))" and
3.186 d3_reduce_equation11:
3.187 - "(a*bdv + bdv^^^3=0) = (bdv=0 | (a + bdv^^^2=0))"
3.188 + "(a*bdv + bdv^^^3=0) = (bdv=0 | (a + bdv^^^2=0))" and
3.189 d3_reduce_equation12:
3.190 - "( bdv + bdv^^^3=0) = (bdv=0 | (1 + bdv^^^2=0))"
3.191 + "( bdv + bdv^^^3=0) = (bdv=0 | (1 + bdv^^^2=0))" and
3.192 d3_reduce_equation13:
3.193 - "( b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( b*bdv + c*bdv^^^2=0))"
3.194 + "( b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( b*bdv + c*bdv^^^2=0))" and
3.195 d3_reduce_equation14:
3.196 - "( bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( bdv + c*bdv^^^2=0))"
3.197 + "( bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( bdv + c*bdv^^^2=0))" and
3.198 d3_reduce_equation15:
3.199 - "( b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( b*bdv + bdv^^^2=0))"
3.200 + "( b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( b*bdv + bdv^^^2=0))" and
3.201 d3_reduce_equation16:
3.202 - "( bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( bdv + bdv^^^2=0))"
3.203 + "( bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( bdv + bdv^^^2=0))" and
3.204 d3_isolate_add1:
3.205 - "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^3=0) = (b*bdv^^^3= (-1)*a)"
3.206 + "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^3=0) = (b*bdv^^^3= (-1)*a)" and
3.207 d3_isolate_add2:
3.208 - "[|Not(bdv occurs_in a)|] ==> (a + bdv^^^3=0) = ( bdv^^^3= (-1)*a)"
3.209 + "[|Not(bdv occurs_in a)|] ==> (a + bdv^^^3=0) = ( bdv^^^3= (-1)*a)" and
3.210 d3_isolate_div:
3.211 - "[|Not(b=0);Not(bdv occurs_in a)|] ==> (b*bdv^^^3=c) = (bdv^^^3=c/b)"
3.212 + "[|Not(b=0);Not(bdv occurs_in a)|] ==> (b*bdv^^^3=c) = (bdv^^^3=c/b)" and
3.213 d3_root_equation2:
3.214 - "(bdv^^^3=0) = (bdv=0)"
3.215 + "(bdv^^^3=0) = (bdv=0)" and
3.216 d3_root_equation1:
3.217 - "(bdv^^^3=c) = (bdv = nroot 3 c)"
3.218 + "(bdv^^^3=c) = (bdv = nroot 3 c)" and
3.219
3.220 (* ---- degree 4 ----*)
3.221 (* RL03.FIXME es wir nicht getestet ob u>0 *)
3.222 d4_sub_u1:
3.223 "(c+b*bdv^^^2+a*bdv^^^4=0) =
3.224 - ((a*u^^^2+b*u+c=0) & (bdv^^^2=u))"
3.225 + ((a*u^^^2+b*u+c=0) & (bdv^^^2=u))" and
3.226
3.227 (* ---- 7.3.02 von Termorder ---- *)
3.228
3.229 - bdv_collect_1: "l * bdv + m * bdv = (l + m) * bdv"
3.230 - bdv_collect_2: "bdv + m * bdv = (1 + m) * bdv"
3.231 - bdv_collect_3: "l * bdv + bdv = (l + 1) * bdv"
3.232 + bdv_collect_1: "l * bdv + m * bdv = (l + m) * bdv" and
3.233 + bdv_collect_2: "bdv + m * bdv = (1 + m) * bdv" and
3.234 + bdv_collect_3: "l * bdv + bdv = (l + 1) * bdv" and
3.235
3.236 (* bdv_collect_assoc0_1 "l * bdv + m * bdv + k = (l + m) * bdv + k"
3.237 bdv_collect_assoc0_2 "bdv + m * bdv + k = (1 + m) * bdv + k"
3.238 bdv_collect_assoc0_3 "l * bdv + bdv + k = (l + 1) * bdv + k"
3.239 *)
3.240 - bdv_collect_assoc1_1: "l * bdv + (m * bdv + k) = (l + m) * bdv + k"
3.241 - bdv_collect_assoc1_2: "bdv + (m * bdv + k) = (1 + m) * bdv + k"
3.242 - bdv_collect_assoc1_3: "l * bdv + (bdv + k) = (l + 1) * bdv + k"
3.243 + bdv_collect_assoc1_1: "l * bdv + (m * bdv + k) = (l + m) * bdv + k" and
3.244 + bdv_collect_assoc1_2: "bdv + (m * bdv + k) = (1 + m) * bdv + k" and
3.245 + bdv_collect_assoc1_3: "l * bdv + (bdv + k) = (l + 1) * bdv + k" and
3.246
3.247 - bdv_collect_assoc2_1: "k + l * bdv + m * bdv = k + (l + m) * bdv"
3.248 - bdv_collect_assoc2_2: "k + bdv + m * bdv = k + (1 + m) * bdv"
3.249 - bdv_collect_assoc2_3: "k + l * bdv + bdv = k + (l + 1) * bdv"
3.250 + bdv_collect_assoc2_1: "k + l * bdv + m * bdv = k + (l + m) * bdv" and
3.251 + bdv_collect_assoc2_2: "k + bdv + m * bdv = k + (1 + m) * bdv" and
3.252 + bdv_collect_assoc2_3: "k + l * bdv + bdv = k + (l + 1) * bdv" and
3.253
3.254
3.255 - bdv_n_collect_1: "l * bdv^^^n + m * bdv^^^n = (l + m) * bdv^^^n"
3.256 - bdv_n_collect_2: " bdv^^^n + m * bdv^^^n = (1 + m) * bdv^^^n"
3.257 - bdv_n_collect_3: "l * bdv^^^n + bdv^^^n = (l + 1) * bdv^^^n" (*order!*)
3.258 + bdv_n_collect_1: "l * bdv^^^n + m * bdv^^^n = (l + m) * bdv^^^n" and
3.259 + bdv_n_collect_2: " bdv^^^n + m * bdv^^^n = (1 + m) * bdv^^^n" and
3.260 + bdv_n_collect_3: "l * bdv^^^n + bdv^^^n = (l + 1) * bdv^^^n" (*order!*) and
3.261
3.262 bdv_n_collect_assoc1_1:
3.263 - "l * bdv^^^n + (m * bdv^^^n + k) = (l + m) * bdv^^^n + k"
3.264 - bdv_n_collect_assoc1_2: "bdv^^^n + (m * bdv^^^n + k) = (1 + m) * bdv^^^n + k"
3.265 - bdv_n_collect_assoc1_3: "l * bdv^^^n + (bdv^^^n + k) = (l + 1) * bdv^^^n + k"
3.266 + "l * bdv^^^n + (m * bdv^^^n + k) = (l + m) * bdv^^^n + k" and
3.267 + bdv_n_collect_assoc1_2: "bdv^^^n + (m * bdv^^^n + k) = (1 + m) * bdv^^^n + k" and
3.268 + bdv_n_collect_assoc1_3: "l * bdv^^^n + (bdv^^^n + k) = (l + 1) * bdv^^^n + k" and
3.269
3.270 - bdv_n_collect_assoc2_1: "k + l * bdv^^^n + m * bdv^^^n = k +(l + m) * bdv^^^n"
3.271 - bdv_n_collect_assoc2_2: "k + bdv^^^n + m * bdv^^^n = k + (1 + m) * bdv^^^n"
3.272 - bdv_n_collect_assoc2_3: "k + l * bdv^^^n + bdv^^^n = k + (l + 1) * bdv^^^n"
3.273 + bdv_n_collect_assoc2_1: "k + l * bdv^^^n + m * bdv^^^n = k +(l + m) * bdv^^^n" and
3.274 + bdv_n_collect_assoc2_2: "k + bdv^^^n + m * bdv^^^n = k + (1 + m) * bdv^^^n" and
3.275 + bdv_n_collect_assoc2_3: "k + l * bdv^^^n + bdv^^^n = k + (l + 1) * bdv^^^n" and
3.276
3.277 (*WN.14.3.03*)
3.278 - real_minus_div: "- (a / b) = (-1 * a) / b"
3.279 + real_minus_div: "- (a / b) = (-1 * a) / b" and
3.280
3.281 - separate_bdv: "(a * bdv) / b = (a / b) * (bdv::real)"
3.282 - separate_bdv_n: "(a * bdv ^^^ n) / b = (a / b) * bdv ^^^ n"
3.283 - separate_1_bdv: "bdv / b = (1 / b) * (bdv::real)"
3.284 + separate_bdv: "(a * bdv) / b = (a / b) * (bdv::real)" and
3.285 + separate_bdv_n: "(a * bdv ^^^ n) / b = (a / b) * bdv ^^^ n" and
3.286 + separate_1_bdv: "bdv / b = (1 / b) * (bdv::real)" and
3.287 separate_1_bdv_n: "bdv ^^^ n / b = (1 / b) * bdv ^^^ n"
3.288
3.289 ML {*
4.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Tue Jul 26 13:30:37 2011 +0200
4.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Tue Jul 26 15:25:28 2011 +0200
4.3 @@ -455,25 +455,25 @@
4.4 *)
4.5
4.6
4.7 -(*=== inhibit exn 110722=============================================================
4.8
4.9 "--------------------- 30.4.03: maximum .. rewrite_set_ list_rls ---------";
4.10 "--------------------- 30.4.03: maximum .. rewrite_set_ list_rls ---------";
4.11 "--------------------- 30.4.03: maximum .. rewrite_set_ list_rls ---------";
4.12 str2term
4.13 - "Script Maximum_value(f_ix::bool list)(m_::real) (r_s::bool list)\
4.14 - \ (v_v::real) (itv_v::real set) (err_::bool) = \
4.15 - \ (let e_e = (hd o (filterVar m_)) r_s; \
4.16 - \ t_ = (if 1 < length_ r_s \
4.17 - \ then (SubProblem (Reals_,[make,function],[no_met])\
4.18 - \ [REAL m_, REAL v_v, BOOL_LIST r_s])\
4.19 + "Script Maximum_value(f_ix::bool list)(m_m::real) (r_s::bool list)\
4.20 + \ (v_v::real) (itv_v::real set) (err_r::bool) = \
4.21 + \ (let e_e = (hd o (filterVar m_m)) r_s; \
4.22 + \ t_t = (if 1 < length_h r_s \
4.23 + \ then (SubProblem (Reals_s,[make,function],[no_met])\
4.24 + \ [REAL m_m, REAL v_v, BOOL_LIST r_s])\
4.25 \ else (hd r_s)); \
4.26 - \ (mx_::real) = SubProblem (Reals_,[on_interval,max_of,function], \
4.27 + \ (mx_x::real) = SubProblem (Reals_s,[on_interval,max_of,function], \
4.28 \ [Isac,maximum_on_interval])\
4.29 - \ [BOOL t_, REAL v_v, REAL_SET itv_]\
4.30 - \ in ((SubProblem (Reals_,[find_values,tool],[Isac,find_values]) \
4.31 - \ [REAL mx_, REAL (Rhs t_), REAL v_v, REAL m_, \
4.32 + \ [BOOL t_t, REAL v_v, REAL_SET itv_v]\
4.33 + \ in ((SubProblem (Reals_s,[find_values,tool],[Isac,find_values]) \
4.34 + \ [REAL mx_x, REAL (Rhs t_t), REAL v_v, REAL m_m, \
4.35 \ BOOL_LIST (dropWhile (ident e_e) r_s)])::bool list))";
4.36 +(*=== inhibit exn 110722=============================================================
4.37
4.38 val f_ix = (str2term "f_ix::bool list",
4.39 str2term "[r=Arbfix]");
4.40 @@ -768,3 +768,4 @@
4.41
4.42 ===== inhibit exn 110722===========================================================*)
4.43
4.44 +
5.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Tue Jul 26 13:30:37 2011 +0200
5.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Tue Jul 26 15:25:28 2011 +0200
5.3 @@ -17,7 +17,6 @@
5.4 "----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
5.5 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
5.6 "----------- rewrite in [EqSystem,normalize,4x4] -----------------";
5.7 -"----------- script [EqSystem,normalize,2x2] ---------------------";
5.8 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
5.9 "----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
5.10 "----------- refine [linear,system]-------------------------------";
5.11 @@ -281,238 +280,6 @@
5.12 \ c + (c_2 + (c_3 + c_4)) = 0]"
5.13 then () else error "eqsystem.sml rewrite in 4x4 order_system";
5.14
5.15 -(*=== inhibit exn 110722=============================================================
5.16 -
5.17 -"----------- script [EqSystem,normalize,2x2] ---------------------";
5.18 -"----------- script [EqSystem,normalize,2x2] ---------------------";
5.19 -"----------- script [EqSystem,normalize,2x2] ---------------------";
5.20 -val str =
5.21 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
5.22 -\ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.23 -\ simplify_System_parenthesized False) es_ \
5.24 -\ in ([]))";
5.25 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.26 -val str =
5.27 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
5.28 -\ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.29 -\ simplify_System_parenthesized False) es_ \
5.30 -\ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
5.31 -\ []))";
5.32 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.33 -val str =
5.34 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
5.35 -\ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.36 -\ simplify_System_parenthesized False) es_ \
5.37 -\ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
5.38 -\ [BOOL_LIST es__, REAL_LIST v_s]))"
5.39 -;
5.40 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.41 -val str =
5.42 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
5.43 -\ (let es__ = Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.44 -\ simplify_System_parenthesized False) es_ \
5.45 -\ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
5.46 -\ [BOOL_LIST es__, REAL_LIST v_s]))"
5.47 -;
5.48 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.49 -val str =
5.50 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
5.51 -\ (let es__ = (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.52 -\ simplify_System_parenthesized False)) es_ \
5.53 -\ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
5.54 -\ [BOOL_LIST es__, REAL_LIST v_s]))"
5.55 -;
5.56 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.57 -val str =
5.58 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
5.59 -\ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.60 -\ simplify_System_parenthesized False)) @@\
5.61 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.62 -\ simplify_System_parenthesized False))) es_\
5.63 -\ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
5.64 -\ [BOOL_LIST es__, REAL_LIST v_s]))"
5.65 -;
5.66 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.67 -val str =
5.68 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
5.69 -\ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.70 -\ simplify_System_parenthesized False)) @@\
5.71 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.72 -\ simplify_System_parenthesized False)) @@\
5.73 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.74 -\ simplify_System_parenthesized False))) es_\
5.75 -\ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
5.76 -\ [BOOL_LIST es__, REAL_LIST v_s]))"
5.77 -;
5.78 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.79 -val str =
5.80 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
5.81 -\ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.82 -\ simplify_System_parenthesized False)) @@\
5.83 -\ (Try (Rewrite_Set_Inst [] isolate_bdvs False)) @@\
5.84 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.85 -\ simplify_System_parenthesized False)) @@\
5.86 -\ (Try (Rewrite_Set order_system False))) es_\
5.87 -\ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
5.88 -\ [BOOL_LIST es__, REAL_LIST v_s]))"
5.89 -;
5.90 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.91 -val str =
5.92 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
5.93 -\ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.94 -\ simplify_System_parenthesized False)) @@\
5.95 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s)]\
5.96 -\ isolate_bdvs False)) @@\
5.97 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.98 -\ simplify_System_parenthesized False)) @@\
5.99 -\ (Try (Rewrite_Set order_system False))) es_\
5.100 -\ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
5.101 -\ [BOOL_LIST es__, REAL_LIST v_s]))"
5.102 -;
5.103 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.104 -val str =
5.105 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
5.106 -\ (let es__ = ((Try (Rewrite_Set simplify_System_parenthesized False)) @@\
5.107 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.108 -\ isolate_bdvs False)) @@\
5.109 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.110 -\ simplify_System_parenthesized False)) @@\
5.111 -\ (Try (Rewrite_Set order_system False))) es_\
5.112 -\ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
5.113 -\ [BOOL_LIST es__, REAL_LIST v_s]))"
5.114 -;
5.115 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.116 -
5.117 -"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
5.118 -"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
5.119 -"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
5.120 -val str =
5.121 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
5.122 -\ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.123 -\ simplify_System_parenthesized False) es_ \
5.124 -\ in ([]))";
5.125 -
5.126 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.127 -val str =
5.128 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
5.129 -\ (let e1__ = Take (hd es_) \
5.130 -\ in ([]))";
5.131 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.132 -val str =
5.133 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
5.134 -\ (let e1__ = Take (hd es_); \
5.135 -\ e1__ = Take (hd es_) \
5.136 -\ in ([]))";
5.137 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.138 -val str =
5.139 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
5.140 -\ (let e1__ = Take (hd es_); \
5.141 -\ e1__ = (Take (hd es_))\
5.142 -\ in ([]))";
5.143 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.144 -val str =
5.145 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
5.146 -\ (let e1__ = Take (hd es_); \
5.147 -\ e1__ = ((Rewrite_Set order_system False)) e1__\
5.148 -\ in ([]))";
5.149 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.150 -val str =
5.151 -"(Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.152 -\ isolate_bdvs False) (e1__::bool)";
5.153 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.154 -val str =
5.155 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
5.156 -\ (let e1__ = Take (hd es_); \
5.157 -\ e1__ = ((Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.158 -\ isolate_bdvs False)) e1__\
5.159 -\ in ([]))";
5.160 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.161 -val str =
5.162 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
5.163 -\ (let e1__ = Take (hd es_); \
5.164 -\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.165 -\ isolate_bdvs False)) @@\
5.166 -\ (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.167 -\ simplify_System False)) e1__\
5.168 -\ in ([]))";
5.169 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.170 -val str =
5.171 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
5.172 -\ (let e1__ = Take (hd es_); \
5.173 -\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.174 -\ isolate_bdvs False)) @@\
5.175 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.176 -\ simplify_System False))) e1__\
5.177 -\ in ([]))";
5.178 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.179 -val str =
5.180 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
5.181 -\ (let e1__ = Take (hd es_); \
5.182 -\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.183 -\ isolate_bdvs False)) @@ \
5.184 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.185 -\ simplify_System False))) e1__; \
5.186 -\ e2__ = Take (hd (tl es_)) \
5.187 -\ in ([]))";
5.188 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.189 -val str =
5.190 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
5.191 -\ (let e1__ = Take (hd es_); \
5.192 -\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.193 -\ isolate_bdvs False)) @@ \
5.194 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.195 -\ simplify_System False))) e1__; \
5.196 -\ e2__ = Take (hd (tl es_)); \
5.197 -\ e2__ = Substitute [e1__] e2__ \
5.198 -\ in ([]))";
5.199 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.200 -val str =
5.201 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
5.202 -\ (let e1__ = Take (hd es_); \
5.203 -\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.204 -\ isolate_bdvs False)) @@ \
5.205 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.206 -\ simplify_System False))) e1__; \
5.207 -\ e2__ = Take (hd (tl es_)); \
5.208 -\ e2__ = ((Substitute [e1__])) e2__ \
5.209 -\ in ([]))";
5.210 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.211 -val str =
5.212 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
5.213 -\ (let e1__ = Take (hd es_); \
5.214 -\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.215 -\ isolate_bdvs False)) @@ \
5.216 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.217 -\ simplify_System False))) e1__; \
5.218 -\ e2__ = Take (hd (tl es_)); \
5.219 -\ e2__ = ((Substitute [e1__]) @@ \
5.220 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.221 -\ isolate_bdvs False)) @@ \
5.222 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.223 -\ simplify_System False))) e2__ \
5.224 -\ in [e1__, e2__])"
5.225 -;
5.226 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.227 -val str =
5.228 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
5.229 -\ (let e1__ = Take (hd es_); \
5.230 -\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.231 -\ isolate_bdvs False)) @@ \
5.232 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.233 -\ simplify_System False))) e1__; \
5.234 -\ e2__ = Take (hd (tl es_)); \
5.235 -\ e2__ = ((Substitute [e1__]) @@ \
5.236 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.237 -\ simplify_System_parenthesized False)) @@ \
5.238 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.239 -\ isolate_bdvs False)) @@ \
5.240 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.241 -\ simplify_System False)) @@ \
5.242 -\ (Try (Rewrite_Set order_system False))) e2__ \
5.243 -\ in [e1__, e2__])"
5.244 -;
5.245 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.246 -=== inhibit exn 110722=============================================================*)
5.247
5.248 val str =
5.249 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
6.1 --- a/test/Tools/isac/Test_Some.thy Tue Jul 26 13:30:37 2011 +0200
6.2 +++ b/test/Tools/isac/Test_Some.thy Tue Jul 26 15:25:28 2011 +0200
6.3 @@ -7,26 +7,10 @@
6.4
6.5 ML{* writeln "**** run the test ***************************************" *}
6.6
6.7 -use"../../../test/Tools/isac/Interpret/ctree.sml"
6.8 +use"../../../test/Tools/isac/Knowledge/diffapp.sml"
6.9
6.10 ML {*
6.11
6.12 -
6.13 -
6.14 -
6.15 -
6.16 -
6.17 -
6.18 -
6.19 -
6.20 -
6.21 -
6.22 -
6.23 -
6.24 -
6.25 -
6.26 -
6.27 -
6.28 *}
6.29 ML{*
6.30 *}