1.1 --- a/src/Tools/isac/Knowledge/Test.thy Mon Sep 06 15:09:37 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Test.thy Mon Sep 06 15:53:18 2010 +0200
1.3 @@ -203,7 +203,7 @@
1.4 ]);
1.5
1.6 (** term order **)
1.7 -fun term_order (_:subst) tu = (term_ordI [] tu = LESS);
1.8 +fun Term_Ord.term_order (_:subst) tu = (term_ordI [] tu = LESS);
1.9
1.10 (** rule sets GOON **)
1.11
1.12 @@ -272,7 +272,7 @@
1.13
1.14 Calc ("op +",eval_binop "#add_"),
1.15 Calc ("op *",eval_binop "#mult_"),
1.16 - Calc ("Root.sqrt",eval_sqrt "#sqrt_"),
1.17 + Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
1.18 Calc ("Atools.pow" ,eval_binop "#power_"),
1.19
1.20 Calc ("op <",eval_equ "#less_"),
1.21 @@ -491,7 +491,7 @@
1.22 ("leq" ,("op <=" ,eval_equ "#less_equal_")),
1.23 ("ident" ,("Atools.ident",eval_ident "#ident_")),
1.24 (*von hier (ehem.SqRoot*)
1.25 - ("sqrt" ,("Root.sqrt" ,eval_sqrt "#sqrt_")),
1.26 + ("sqrt" ,("NthRoot.sqrt" ,eval_sqrt "#sqrt_")),
1.27 ("Test.is_root_free",("is'_root'_free", eval_root_free"#is_root_free_e")),
1.28 ("Test.contains_root",("contains'_root",
1.29 eval_contains_root"#contains_root_"))
1.30 @@ -594,7 +594,7 @@
1.31 prls=assoc_rls "matches",
1.32 calc=[],
1.33 crls=tval_rls, nrls=Test_simplify},
1.34 - "Script Solve_linear (e_e::bool) (v_::real)= " ^
1.35 + "Script Solve_linear (e_e::bool) (v_v::real)= " ^
1.36 "(let e_e =" ^
1.37 " Repeat" ^
1.38 " (((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@" ^
1.39 @@ -887,7 +887,7 @@
1.40 crls=tval_rls, nrls=e_rls(*,asm_rls=[],
1.41 asm_thm=[("square_equation_left",""),
1.42 ("square_equation_right","")]*)},
1.43 - "Script Solve_root_equation (e_e::bool) (v_::real) = " ^
1.44 + "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.45 "(let e_e = " ^
1.46 " ((While (contains_root e_e) Do" ^
1.47 " ((Rewrite square_equation_left True) @@" ^
1.48 @@ -917,7 +917,7 @@
1.49 crls=tval_rls, nrls=e_rls(*,asm_rls=[],
1.50 asm_thm=[("square_equation_left",""),
1.51 ("square_equation_right","")]*)},
1.52 - "Script Solve_root_equation (e_e::bool) (v_::real) = " ^
1.53 + "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.54 "(let e_e = " ^
1.55 " ((While (contains_root e_e) Do" ^
1.56 " ((Rewrite square_equation_left True) @@" ^
1.57 @@ -932,7 +932,7 @@
1.58 " e_;" ^
1.59 " (L_::bool list) = Tac subproblem_equation_dummy; " ^
1.60 " L_ = Tac solve_equation_dummy " ^
1.61 - " in Check_elementwise L_ {(v_::real). Assumptions})"
1.62 + " in Check_elementwise L_ {(v_v::real). Assumptions})"
1.63 ));
1.64
1.65 store_met
1.66 @@ -944,12 +944,12 @@
1.67 ],
1.68 {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
1.69 crls=tval_rls, nrls=Test_simplify},
1.70 - "Script Solve_root_equation (e_e::bool) (v_::real) = " ^
1.71 + "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.72 " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@ " ^
1.73 " (Try (Rewrite_Set Test_simplify False))) e_; " ^
1.74 "(L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test]," ^
1.75 " [Test,solve_linear]) [bool_ e_e, real_ v_])" ^
1.76 - "in Check_elementwise L_ {(v_::real). Assumptions})"
1.77 + "in Check_elementwise L_ {(v_v::real). Assumptions})"
1.78 ));
1.79
1.80 store_met
1.81 @@ -963,11 +963,11 @@
1.82 crls=tval_rls, nrls=e_rls(*,
1.83 asm_rls=[],asm_thm=[("square_equation_left",""),
1.84 ("square_equation_right","")]*)},
1.85 - "Script Solve_root_equation (e_e::bool) (v_::real) = " ^
1.86 + "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.87 " (let e_e = Try (Rewrite_Set norm_equation False) e_; " ^
1.88 "(L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test]," ^
1.89 " [Test,solve_by_pq_formula]) [bool_ e_e, real_ v_])" ^
1.90 - "in Check_elementwise L_ {(v_::real). Assumptions})"
1.91 + "in Check_elementwise L_ {(v_v::real). Assumptions})"
1.92 ));
1.93
1.94 store_met
1.95 @@ -984,7 +984,7 @@
1.96 crls=tval_rls, nrls=e_rls(*,asm_rls=[],
1.97 asm_thm=[("square_equation_left",""),
1.98 ("square_equation_right","")]*)},
1.99 - "Script Solve_root_equation (e_e::bool) (v_::real) = " ^
1.100 + "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.101 "(let e_e = " ^
1.102 " ((While (contains_root e_e) Do" ^
1.103 " ((Rewrite square_equation_left True) @@" ^
1.104 @@ -998,7 +998,7 @@
1.105 " (L_::bool list) = " ^
1.106 " (SubProblem (Test_,[linear,univariate,equation,test]," ^
1.107 " [Test,solve_linear]) [bool_ e_e, real_ v_])" ^
1.108 - "in Check_elementwise L_ {(v_::real). Assumptions})"
1.109 + "in Check_elementwise L_ {(v_v::real). Assumptions})"
1.110 ));
1.111
1.112 store_met
1.113 @@ -1015,7 +1015,7 @@
1.114 crls=tval_rls, nrls=e_rls(*,asm_rls=[],
1.115 asm_thm=[("square_equation_left",""),
1.116 ("square_equation_right","")]*)},
1.117 - "Script Solve_root_equation (e_e::bool) (v_::real) = " ^
1.118 + "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.119 "(let e_e = " ^
1.120 " ((While (contains_root e_e) Do" ^
1.121 " ((Rewrite square_equation_left True) @@" ^
1.122 @@ -1028,7 +1028,7 @@
1.123 " e_;" ^
1.124 " (L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test]," ^
1.125 " [Test,solve_linear]) [bool_ e_e, real_ v_])" ^
1.126 - " in Check_elementwise L_ {(v_::real). Assumptions})"
1.127 + " in Check_elementwise L_ {(v_v::real). Assumptions})"
1.128 ));
1.129
1.130 store_met
1.131 @@ -1045,7 +1045,7 @@
1.132 crls=tval_rls, nrls=e_rls(*,asm_rls=[],
1.133 asm_thm=[("square_equation_left",""),
1.134 ("square_equation_right","")]*)},
1.135 - "Script Solve_root_equation (e_e::bool) (v_::real) = " ^
1.136 + "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.137 "(let e_e = " ^
1.138 " ((While (contains_root e_e) Do" ^
1.139 " (((Rewrite square_equation_left True) Or " ^
1.140 @@ -1059,7 +1059,7 @@
1.141 " e_;" ^
1.142 " (L_::bool list) = (SubProblem (Test_,[plain_square,univariate,equation,test]," ^
1.143 " [Test,solve_plain_square]) [bool_ e_e, real_ v_])" ^
1.144 - " in Check_elementwise L_ {(v_::real). Assumptions})"
1.145 + " in Check_elementwise L_ {(v_v::real). Assumptions})"
1.146 ));
1.147
1.148 store_met
1.149 @@ -1076,7 +1076,7 @@
1.150 crls=tval_rls, nrls=e_rls(*,asm_rls=[],
1.151 asm_thm=[("square_equation_left",""),
1.152 ("square_equation_right","")]*)},
1.153 - "Script Solve_root_equation (e_e::bool) (v_::real) = " ^
1.154 + "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.155 "(let e_e = " ^
1.156 " ((While (contains_root e_e) Do" ^
1.157 " (((Rewrite square_equation_left True) Or" ^
1.158 @@ -1090,7 +1090,7 @@
1.159 " e_;" ^
1.160 " (L_::bool list) = (SubProblem (Test_,[univariate,equation,test]," ^
1.161 " [no_met]) [bool_ e_e, real_ v_])" ^
1.162 - " in Check_elementwise L_ {(v_::real). Assumptions})"
1.163 + " in Check_elementwise L_ {(v_v::real). Assumptions})"
1.164 ) ); (*#######*)
1.165
1.166 store_met
1.167 @@ -1108,7 +1108,7 @@
1.168 prls = assoc_rls "matches",
1.169 crls=tval_rls, nrls=e_rls(*,
1.170 asm_rls=[],asm_thm=[]*)},
1.171 - "Script Solve_plain_square (e_e::bool) (v_::real) = " ^
1.172 + "Script Solve_plain_square (e_e::bool) (v_v::real) = " ^
1.173 " (let e_e = ((Try (Rewrite_Set isolate_bdv False)) @@ " ^
1.174 " (Try (Rewrite_Set Test_simplify False)) @@ " ^
1.175 " ((Rewrite square_equality_0 False) Or " ^
1.176 @@ -1127,7 +1127,7 @@
1.177 {rew_ord'="e_rew_ord",rls'=tval_rls,srls = e_rls,prls=e_rls,
1.178 calc=[],
1.179 crls=tval_rls, nrls=e_rls(*,asm_rls=[],asm_thm=[]*)},
1.180 - "Script Norm_univar_equation (e_e::bool) (v_::real) = " ^
1.181 + "Script Norm_univar_equation (e_e::bool) (v_v::real) = " ^
1.182 " (let e_e = ((Try (Rewrite rnorm_equation_add False)) @@ " ^
1.183 " (Try (Rewrite_Set Test_simplify False))) e_e " ^
1.184 " in (SubProblem (Test_,[univariate,equation,test], " ^
1.185 @@ -1171,9 +1171,9 @@
1.186 | size_of_term' (f$t) = size_of_term' f + size_of_term' t
1.187 | size_of_term' _ = 1;
1.188
1.189 -fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
1.190 - (case term_ord' pr thy (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
1.191 - | term_ord' pr thy (t, u) =
1.192 +fun Term_Ord.term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
1.193 + (case Term_Ord.term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
1.194 + | Term_Ord.term_ord' pr thy (t, u) =
1.195 (if pr then
1.196 let
1.197 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
1.198 @@ -1200,7 +1200,7 @@
1.199 end
1.200 | ord => ord)
1.201 and hd_ord (f, g) = (* ~ term.ML *)
1.202 - prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd' f, dest_hd' g)
1.203 + prod_ord (prod_ord indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
1.204 and terms_ord str pr (ts, us) =
1.205 list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us);
1.206 in
1.207 @@ -1271,7 +1271,7 @@
1.208 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1.209 Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}),
1.210 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
1.211 - Thm ("left_diff_distrib2",num_str @{thm left_diff_distrib2}),
1.212 + Thm ("right_diff_distrib",num_str @{thm right_diff_distrib}),
1.213 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
1.214 Thm ("mult_1_left",num_str @{thm mult_1_left}),
1.215 (*"1 * z = z"*)
1.216 @@ -1401,7 +1401,7 @@
1.217 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1.218 Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}}),
1.219 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
1.220 - Thm ("left_diff_distrib2",num_str @{thm left_diff_distrib}2}),
1.221 + Thm ("right_diff_distrib",num_str @{thm right_diff_distrib}),
1.222 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
1.223 *)
1.224