wneuper/isa: comparison src/Tools/isac/Knowledge/Test.thy

equal deleted inserted replaced

-:dbe1a10234df
+:4035ec339062
 subsection \<open>differentiate\<close>
 setup \<open>KEStore_Elems.add_mets
 [Specify.prep_met @{theory "Diff"} "met_test" [] Celem.e_metID
 (["Test"], [],
 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
-crls=Atools_erls, errpats = [], nrls = Rule.e_rls}, "empty_script")]
+crls=Atools_erls, errpats = [], nrls = Rule.e_rls}, @{thm refl})]
 \<close>
-(*ok
 partial_function (tailrec) solve_linear :: "bool \<Rightarrow> real \<Rightarrow> bool list"
 where
 "solve_linear e_e v_v =
 (let e_e =
 Repeat
 (((Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'' False) @@
 (Rewrite_Set ''Test_simplify'' False))) e_e
 in [e_e])"
-*)
 setup \<open>KEStore_Elems.add_mets
 [Specify.prep_met thy "met_test_solvelin" [] Celem.e_metID
 (["Test","solve_linear"],
 [("#Given" ,["equality e_e","solveFor v_v"]),
 ("#Where" ,["matches (?a = ?b) e_e"]),
 ("#Find"  ,["solutions v_v'i'"])],
 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule.e_rls,
 prls = assoc_rls' @{theory} "matches", calc = [], crls = tval_rls, errpats = [],
 nrls = Test_simplify},
-"Script Solve_linear (e_e::bool) (v_v::real)=                     " ^
+@{thm solve_linear.simps}
+	    (*"Script Solve_linear (e_e::bool) (v_v::real)=                     " ^
 "(let e_e =                                                       " ^
 "  Repeat                                                         " ^
 "    (((Rewrite_Set_Inst [(''bdv'',v_v::real)] ''isolate_bdv'' False) @@  " ^
 "      (Rewrite_Set ''Test_simplify'' False))) e_e" ^
-" in [e_e::bool])")]
+" in [e_e::bool])"*))]
 \<close>
 subsection \<open>root equation\<close>
-(*ok
 partial_function (tailrec) solve_root_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
 where
 "solve_root_equ e_e v_v =
 (let e_e =
 ((While (contains_root e_e) Do
 (Try (Rewrite_Set ''norm_equation'' False)) @@
 (Try (Rewrite_Set ''Test_simplify'' False)) @@
 (Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'' False) @@
 (Try (Rewrite_Set ''Test_simplify'' False))) e_e
 in [e_e])"
-*)
 setup \<open>KEStore_Elems.add_mets
 [Specify.prep_met thy  "met_test_sqrt" [] Celem.e_metID
 (*root-equation, version for tests before 8.01.01*)
 (["Test","sqrt-equ-test"],
 [("#Given" ,["equality e_e","solveFor v_v"]),
 [Rule.Calc ("Test.contains'_root",eval_contains_root "")],
 prls = Rule.append_rls "prls_contains_root" Rule.e_rls
 [Rule.Calc ("Test.contains'_root",eval_contains_root "")],
 calc=[], crls=tval_rls, errpats = [], nrls = Rule.e_rls (*,asm_rls=[],
 asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
-"Script Solve_root_equation (e_e::bool) (v_v::real) =  " ^
+@{thm solve_root_equ.simps}
+	    (*"Script Solve_root_equation (e_e::bool) (v_v::real) =  " ^
 "(let e_e = " ^
 "   ((While (contains_root e_e) Do" ^
 "      ((Rewrite ''square_equation_left'' True) @@" ^
 "       (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^
 "       (Try (Rewrite_Set ''rearrange_assoc'' False)) @@" ^
 "    (Try (Rewrite_Set ''norm_equation'' False)) @@" ^
 "    (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^
 "    (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''isolate_bdv'' False) @@" ^
 "    (Try (Rewrite_Set ''Test_simplify'' False)))" ^
 "   e_e" ^
-" in [e_e::bool])")]
+" in [e_e::bool])"*))]
 \<close>
 (* UNUSED?
 partial_function (tailrec) solve_root_equ2 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
 where "solve_root_equ e_e v_v =
 (let e_e =
 "  L_L = Tac solve_equation_dummy                             " ^
 "  in Check_elementwise L_L {(v_v::real). Assumptions})")]
 \<close>
 *)
-(*ok
+partial_function (tailrec) minisubpbl ::
-partial_function (tailrec) solve_root_equation ::
 "bool \<Rightarrow> real \<Rightarrow> bool list"
 where "minisubpbl e_e v_v =
 (let e_e = ((Try (Rewrite_Set ''norm_equation'' False)) @@
 (Try (Rewrite_Set ''Test_simplify'' False))) e_e;
 (L_L::bool list) =
 SubProblem (''TestX'', [''LINEAR'', ''univariate'', ''equation'', ''test''],
 [''Test'', ''solve_linear'']) [BOOL e_e, REAL v_v]
 in Check_elementwise L_L {(v_v::real). Assumptions})"
-*)
 setup \<open>KEStore_Elems.add_mets
 [Specify.prep_met thy "met_test_squ_sub" [] Celem.e_metID
 (*tests subproblem fixed linear*)
 (["Test","squ-equ-test-subpbl1"],
 [("#Given" ,["equality e_e","solveFor v_v"]),
 ("#Find"  ,["solutions v_v'i'"])],
 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule.e_rls,
 prls = Rule.append_rls "prls_met_test_squ_sub" Rule.e_rls
 [Rule.Calc ("Test.precond'_rootmet", eval_precond_rootmet "")],
 calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify},
-"Script Solve_root_equation (e_e::bool) (v_v::real) =                  " ^
+@{thm minisubpbl.simps}
+	    (*"Script Solve_root_equation (e_e::bool) (v_v::real) =                  " ^
 " (let e_e = ((Try (Rewrite_Set ''norm_equation'' False)) @@               " ^
 "             (Try (Rewrite_Set ''Test_simplify'' False))) e_e;            " ^
 "     (L_L::bool list) =                                               " ^
 "            (SubProblem (''Test'',                                    " ^
 "                [''LINEAR'', ''univariate'', ''equation'', ''test''], " ^
 "                [''Test'', ''solve_linear''])                         " ^
 "              [BOOL e_e, REAL v_v])                                   " ^
-"  in Check_elementwise L_L {(v_v::real). Assumptions})                ")]
+"  in Check_elementwise L_L {(v_v::real). Assumptions})                "*))]
 \<close>
-(*ok
 partial_function (tailrec) solve_root_equ2 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
-where "solve_root_equ e_e v_v =
+where "solve_root_equ2 e_e v_v =
 (let e_e =
 ((While (contains_root e_e) Do
 ((Rewrite ''square_equation_left'' True) @@
 (Try (Rewrite_Set ''Test_simplify'' False)) @@
 (Try (Rewrite_Set ''rearrange_assoc'' False)) @@
 (Try (Rewrite_Set ''norm_equation'' False)) @@
 (Try (Rewrite_Set ''Test_simplify'' False))) e_e;
 L_L = SubProblem (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''],
 [''Test'', ''solve_linear'']) [BOOL e_e, REAL v_v]
 in Check_elementwise L_L {(v_v::real). Assumptions})                                       "
-*)
 setup \<open>KEStore_Elems.add_mets
 [Specify.prep_met thy  "met_test_eq1" [] Celem.e_metID
 (*root-equation1:*)
 (["Test","square_equation1"],
 [("#Given" ,["equality e_e","solveFor v_v"]),
 {rew_ord'="e_rew_ord",rls'=tval_rls,
 srls = Rule.append_rls "srls_contains_root" Rule.e_rls
 [Rule.Calc ("Test.contains'_root",eval_contains_root"")], prls=Rule.e_rls, calc=[], crls=tval_rls,
 errpats = [], nrls = Rule.e_rls(*,asm_rls=[], asm_thm=[("square_equation_left",""),
 ("square_equation_right","")]*)},
-"Script Solve_root_equation (e_e::bool) (v_v::real) =  " ^
+@{thm solve_root_equ2.simps}
+	    (*"Script Solve_root_equation (e_e::bool) (v_v::real) =  " ^
 "(let e_e = " ^
 "   ((While (contains_root e_e) Do" ^
 "      ((Rewrite ''square_equation_left'' True) @@" ^
 "       (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^
 "       (Try (Rewrite_Set ''rearrange_assoc'' False)) @@" ^
 "    (Try (Rewrite_Set ''norm_equation'' False)) @@" ^
 "    (Try (Rewrite_Set ''Test_simplify'' False)))" ^
 "   e_e;" ^
 "  (L_L::bool list) = (SubProblem (''Test'',[''LINEAR'',''univariate'',''equation'',''test'']," ^
 "                    [''Test'',''solve_linear'']) [BOOL e_e, REAL v_v])" ^
-"  in Check_elementwise L_L {(v_v::real). Assumptions})")]
+"  in Check_elementwise L_L {(v_v::real). Assumptions})"*))]
 \<close>
-(*ok
 partial_function (tailrec) solve_root_equ3 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
 where
-"solve_root_equ e_e v_v =
+"solve_root_equ3 e_e v_v =
 (let e_e =
 ((While (contains_root e_e) Do
 (((Rewrite ''square_equation_left'' True) Or
 (Rewrite ''square_equation_right'' True)) @@
 (Try (Rewrite_Set ''Test_simplify'' False)) @@
 (Try (Rewrite_Set ''norm_equation'' False)) @@
 (Try (Rewrite_Set ''Test_simplify'' False))) e_e;
 L_L = SubProblem (''Test'', [''plain_square'', ''univariate'', ''equation'', ''test''],
 [''Test'', ''solve_plain_square'']) [BOOL e_e, REAL v_v]
 in Check_elementwise L_L {(v_v::real). Assumptions})"
-*)
 setup \<open>KEStore_Elems.add_mets
 [Specify.prep_met thy "met_test_squ2" [] Celem.e_metID
 (*root-equation2*)
 (["Test","square_equation2"],
 [("#Given" ,["equality e_e","solveFor v_v"]),
 {rew_ord'="e_rew_ord",rls'=tval_rls,
 srls = Rule.append_rls "srls_contains_root" Rule.e_rls
 [Rule.Calc ("Test.contains'_root",eval_contains_root"")],
 prls=Rule.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Rule.e_rls(*,asm_rls=[],
 asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
-"Script Solve_root_equation (e_e::bool) (v_v::real)  =  " ^
+@{thm solve_root_equ3.simps}
+	    (*"Script Solve_root_equation (e_e::bool) (v_v::real)  =  " ^
 "(let e_e = " ^
 "   ((While (contains_root e_e) Do" ^
 "      (((Rewrite ''square_equation_left'' True) Or " ^
 "        (Rewrite ''square_equation_right'' True)) @@" ^
 "       (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^
 "    (Try (Rewrite_Set ''norm_equation'' False)) @@" ^
 "    (Try (Rewrite_Set ''Test_simplify'' False)))" ^
 "   e_e;" ^
 "  (L_L::bool list) = (SubProblem (''Test'',[''plain_square'',''univariate'',''equation'',''test'']," ^
 "                    [''Test'',''solve_plain_square'']) [BOOL e_e, REAL v_v])" ^
-"  in Check_elementwise L_L {(v_v::real). Assumptions})")]
+"  in Check_elementwise L_L {(v_v::real). Assumptions})"*))]
 \<close>
-(*ok
 partial_function (tailrec) solve_root_equ4 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
 where
-"solve_root_equ e_e v_v =
+"solve_root_equ4 e_e v_v =
 (let e_e =
 ((While (contains_root e_e) Do
 (((Rewrite ''square_equation_left'' True) Or
 (Rewrite ''square_equation_right'' True)) @@
 (Try (Rewrite_Set ''Test_simplify'' False)) @@
 (Try (Rewrite_Set ''norm_equation'' False)) @@
 (Try (Rewrite_Set ''Test_simplify'' False))) e_e;
 L_L = SubProblem (''Test'', [''univariate'', ''equation'', ''test''],
 [''no_met'']) [BOOL e_e, REAL v_v]
 in Check_elementwise L_L {(v_v::real). Assumptions})"
-*)
 setup \<open>KEStore_Elems.add_mets
 [Specify.prep_met thy "met_test_squeq" [] Celem.e_metID
 (*root-equation*)
 (["Test","square_equation"],
 [("#Given" ,["equality e_e","solveFor v_v"]),
 {rew_ord'="e_rew_ord",rls'=tval_rls,
 srls = Rule.append_rls "srls_contains_root" Rule.e_rls
 [Rule.Calc ("Test.contains'_root",eval_contains_root"")],
 prls=Rule.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Rule.e_rls (*,asm_rls=[],
 asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
-"Script Solve_root_equation (e_e::bool) (v_v::real) =  " ^
+@{thm solve_root_equ4.simps}
+	    (*"Script Solve_root_equation (e_e::bool) (v_v::real) =  " ^
 "(let e_e = " ^
 "   ((While (contains_root e_e) Do" ^
 "      (((Rewrite ''square_equation_left'' True) Or" ^
 "        (Rewrite ''square_equation_right'' True)) @@" ^
 "       (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^
 "    (Try (Rewrite_Set ''norm_equation'' False)) @@" ^
 "    (Try (Rewrite_Set ''Test_simplify'' False)))" ^
 "   e_e;" ^
 "  (L_L::bool list) = (SubProblem (''Test'',[''univariate'',''equation'',''test'']," ^
 "                    [''no_met'']) [BOOL e_e, REAL v_v])" ^
-"  in Check_elementwise L_L {(v_v::real). Assumptions})")]
+"  in Check_elementwise L_L {(v_v::real). Assumptions})"*))]
 \<close>
-(*ok
 partial_function (tailrec) solve_plain_square :: "bool \<Rightarrow> real \<Rightarrow> bool list"
 where
 "solve_plain_square e_e v_v =
 (let e_e = ((Try (Rewrite_Set ''isolate_bdv'' False)) @@
 (Try (Rewrite_Set ''Test_simplify'' False))    @@
 ((Rewrite ''square_equality_0'' False) Or
 (Rewrite ''square_equality'' True)) @@
 (Try (Rewrite_Set ''tval_rls'' False))) e_e
 in Or_to_List e_e)"
-*)
 setup \<open>KEStore_Elems.add_mets
 [Specify.prep_met thy "met_test_eq_plain" [] Celem.e_metID
 (*solve_plain_square*)
 (["Test","solve_plain_square"],
 [("#Given",["equality e_e","solveFor v_v"]),
 "(matches (        v_v ^^^2 = 0) e_e)"]),
 ("#Find"  ,["solutions v_v'i'"])],
 {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=Rule.e_rls,
 prls = assoc_rls' @{theory} "matches", crls=tval_rls, errpats = [], nrls = Rule.e_rls(*,
 asm_rls=[],asm_thm=[]*)},
-"Script Solve_plain_square (e_e::bool) (v_v::real) =           " ^
+@{thm solve_plain_square.simps}
+	    (*"Script Solve_plain_square (e_e::bool) (v_v::real) =           " ^
 " (let e_e = ((Try (Rewrite_Set ''isolate_bdv'' False)) @@         " ^
 "            (Try (Rewrite_Set ''Test_simplify'' False)) @@     " ^
 "            ((Rewrite ''square_equality_0'' False) Or        " ^
 "             (Rewrite ''square_equality'' True)) @@            " ^
 "            (Try (Rewrite_Set ''tval_rls'' False))) e_e             " ^
-"  in ((Or_to_List e_e)::bool list))")]
+"  in ((Or_to_List e_e)::bool list))"*))]
 \<close>
 subsection \<open>polynomial equation\<close>
-(*ok
 partial_function (tailrec) norm_univariate_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
 where
 "norm_univariate_equ e_e v_v =
 (let e_e = ((Try (Rewrite ''rnorm_equation_add'' False)) @@
 (Try (Rewrite_Set ''Test_simplify'' False))) e_e
 in SubProblem (''Test'', [''univariate'', ''equation'', ''test''],
 [''no_met'']) [BOOL e_e, REAL v_v])"
-*)
 setup \<open>KEStore_Elems.add_mets
 [Specify.prep_met thy "met_test_norm_univ" [] Celem.e_metID
 (["Test","norm_univar_equation"],
 [("#Given",["equality e_e","solveFor v_v"]),
 ("#Where" ,[]),
 ("#Find"  ,["solutions v_v'i'"])],
 {rew_ord'="e_rew_ord",rls'=tval_rls,srls = Rule.e_rls,prls=Rule.e_rls, calc=[], crls=tval_rls,
 errpats = [], nrls = Rule.e_rls},
-"Script Norm_univar_equation (e_e::bool) (v_v::real) =      " ^
+@{thm norm_univariate_equ.simps}
+	    (*"Script Norm_univar_equation (e_e::bool) (v_v::real) =      " ^
 " (let e_e = ((Try (Rewrite ''rnorm_equation_add'' False)) @@   " ^
 "            (Try (Rewrite_Set ''Test_simplify'' False))) e_e   " ^
 "  in (SubProblem (''Test'',[''univariate'',''equation'',''test''],         " ^
-"                    [''no_met'']) [BOOL e_e, REAL v_v]))")]
+"                    [''no_met'']) [BOOL e_e, REAL v_v]))"*))]
 \<close>
 subsection \<open>diophantine equation\<close>
-(*ok
 partial_function (tailrec) test_simplify :: "int \<Rightarrow> int"
 where
 "test_simplify t_t =
 (Repeat
 ((Try (Calculate ''PLUS'')) @@
 (Try (Calculate ''TIMES''))) t_t)"
-*)
 setup \<open>KEStore_Elems.add_mets
 [Specify.prep_met thy "met_test_intsimp" [] Celem.e_metID
 (["Test","intsimp"],
 [("#Given" ,["intTestGiven t_t"]),
 ("#Where" ,[]),
 ("#Find"  ,["intTestFind s_s"])],
 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule.e_rls,  prls = Rule.e_rls, calc = [],
 crls = tval_rls, errpats = [], nrls = Test_simplify},
-"Script STest_simplify (t_t::int) =                  " ^
+@{thm test_simplify.simps}
+	    (*"Script STest_simplify (t_t::int) =                  " ^
 "(Repeat                                                          " ^
 "    ((Try (Calculate ''PLUS'')) @@  " ^
-"     (Try (Calculate ''TIMES''))) t_t::int)")]
+"     (Try (Calculate ''TIMES''))) t_t::int)"*))]
 \<close>
 end

changeset 59545	4035ec339062
parent 59505	a1f223658994
child 59546	1ada701c4811