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

equal deleted inserted replaced

-:4dd533681fef
+:ea7e6679080e
 section \<open>rulesets\<close>
 ML \<open>
 val testerls =
 Rule_Def.Repeat {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI),
-erls = Rule_Set.e_rls, srls = Rule_Set.Empty,
+erls = Rule_Set.empty, srls = Rule_Set.Empty,
 calc = [], errpatts = [],
 rules = [Rule.Thm ("refl",TermC.num_str @{thm refl}),
 	       Rule.Thm ("order_refl",TermC.num_str @{thm order_refl}),
 	       Rule.Thm ("radd_left_cancel_le",TermC.num_str @{thm radd_left_cancel_le}),
 	       Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
 (*.for evaluation of conditions in rewrite rules.*)
 (*FIXXXXXXME 10.8.02: handle like _simplify*)
 val tval_rls =
 Rule_Def.Repeat{id = "tval_rls", preconds = [],
 rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}),
-erls=testerls,srls = Rule_Set.e_rls,
+erls=testerls,srls = Rule_Set.empty,
 calc=[], errpatts = [],
 rules = [Rule.Thm ("refl",TermC.num_str @{thm refl}),
 	       Rule.Thm ("order_refl",TermC.num_str @{thm order_refl}),
 	       Rule.Thm ("radd_left_cancel_le",TermC.num_str @{thm radd_left_cancel_le}),
 	       Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
 ML \<open>
 (*make () dissappear*)
 val rearrange_assoc =
 Rule_Def.Repeat{id = "rearrange_assoc", preconds = [],
 rew_ord = ("e_rew_ord",Rule.e_rew_ord),
-erls = Rule_Set.e_rls, srls = Rule_Set.e_rls, calc = [], errpatts = [],
+erls = Rule_Set.empty, srls = Rule_Set.empty, calc = [], errpatts = [],
 rules =
 [Rule.Thm ("sym_add_assoc",TermC.num_str (@{thm add.assoc} RS @{thm sym})),
 Rule.Thm ("sym_rmult_assoc",TermC.num_str (@{thm rmult_assoc} RS @{thm sym}))],
 scr = Rule.EmptyScr
 };
 val ac_plus_times =
 Rule_Def.Repeat{id = "ac_plus_times", preconds = [], rew_ord = ("term_order",term_order),
-erls = Rule_Set.e_rls, srls = Rule_Set.e_rls, calc = [], errpatts = [],
+erls = Rule_Set.empty, srls = Rule_Set.empty, calc = [], errpatts = [],
 rules =
 [Rule.Thm ("radd_commute",TermC.num_str @{thm radd_commute}),
 Rule.Thm ("radd_left_commute",TermC.num_str @{thm radd_left_commute}),
 Rule.Thm ("add_assoc",TermC.num_str @{thm add.assoc}),
 Rule.Thm ("rmult_commute",TermC.num_str @{thm rmult_commute}),
 };
 (*todo: replace by Rewrite("rnorm_equation_add",TermC.num_str @{thm rnorm_equation_add)*)
 val norm_equation =
 Rule_Def.Repeat{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",Rule.e_rew_ord),
-erls = tval_rls, srls = Rule_Set.e_rls, calc = [], errpatts = [],
+erls = tval_rls, srls = Rule_Set.empty, calc = [], errpatts = [],
 rules = [Rule.Thm ("rnorm_equation_add",TermC.num_str @{thm rnorm_equation_add})
 	       ],
 scr = Rule.EmptyScr
 };
 \<close>
 ML \<open>
 (* expects * distributed over + *)
 val Test_simplify =
 Rule_Def.Repeat{id = "Test_simplify", preconds = [],
 rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}),
-erls = tval_rls, srls = Rule_Set.e_rls,
+erls = tval_rls, srls = Rule_Set.empty,
 calc=[(*since 040209 filled by prep_rls'*)], errpatts = [],
 rules = [
 	       Rule.Thm ("real_diff_minus",TermC.num_str @{thm real_diff_minus}),
 	       Rule.Thm ("radd_mult_distrib2",TermC.num_str @{thm radd_mult_distrib2}),
 	       Rule.Thm ("rdistr_right_assoc",TermC.num_str @{thm rdistr_right_assoc}),
 \<close>
 ML \<open>
 (*isolate the root in a root-equation*)
 val isolate_root =
 Rule_Def.Repeat{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",Rule.e_rew_ord),
-erls=tval_rls,srls = Rule_Set.e_rls, calc=[], errpatts = [],
+erls=tval_rls,srls = Rule_Set.empty, calc=[], errpatts = [],
 rules = [Rule.Thm ("rroot_to_lhs",TermC.num_str @{thm rroot_to_lhs}),
 	       Rule.Thm ("rroot_to_lhs_mult",TermC.num_str @{thm rroot_to_lhs_mult}),
 	       Rule.Thm ("rroot_to_lhs_add_mult",TermC.num_str @{thm rroot_to_lhs_add_mult}),
 	       Rule.Thm ("risolate_root_add",TermC.num_str @{thm risolate_root_add}),
 	       Rule.Thm ("risolate_root_mult",TermC.num_str @{thm risolate_root_mult}),
 };
 (*isolate the bound variable in an equation; 'bdv' is a meta-constant*)
 val isolate_bdv =
 Rule_Def.Repeat{id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",Rule.e_rew_ord),
-	erls=tval_rls,srls = Rule_Set.e_rls, calc= [], errpatts = [],
+	erls=tval_rls,srls = Rule_Set.empty, calc= [], errpatts = [],
 	rules =
 	[Rule.Thm ("risolate_bdv_add",TermC.num_str @{thm risolate_bdv_add}),
 	 Rule.Thm ("risolate_bdv_mult_add",TermC.num_str @{thm risolate_bdv_mult_add}),
 	 Rule.Thm ("risolate_bdv_mult",TermC.num_str @{thm risolate_bdv_mult}),
 	 Rule.Thm ("mult_square",TermC.num_str @{thm mult_square}),
 [("Test_simplify", (Context.theory_name @{theory}, prep_rls' Test_simplify)),
 ("tval_rls", (Context.theory_name @{theory}, prep_rls' tval_rls)),
 ("isolate_root", (Context.theory_name @{theory}, prep_rls' isolate_root)),
 ("isolate_bdv", (Context.theory_name @{theory}, prep_rls' isolate_bdv)),
 ("matches", (Context.theory_name @{theory}, prep_rls'
-(Rule_Set.append_rls "matches" testerls [Rule.Num_Calc ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_")])))]
+(Rule_Set.append_rules "matches" testerls [Rule.Num_Calc ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_")])))]
 \<close>
 subsection \<open>problems\<close>
 (** problem types **)
 setup \<open>KEStore_Elems.add_pbts
-[(Specify.prep_pbt thy "pbl_test" [] Celem.e_pblID (["test"], [], Rule_Set.e_rls, NONE, [])),
+[(Specify.prep_pbt thy "pbl_test" [] Celem.e_pblID (["test"], [], Rule_Set.empty, NONE, [])),
 (Specify.prep_pbt thy "pbl_test_equ" [] Celem.e_pblID
 (["equation","test"],
 [("#Given" ,["equality e_e","solveFor v_v"]),
 ("#Where" ,["matches (?a = ?b) e_e"]),
 ("#Find"  ,["solutions v_v'i'"])],
 (Specify.prep_pbt thy "pbl_test_uni_poly" [] Celem.e_pblID
 (["polynomial","univariate","equation","test"],
 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
 ("#Where" ,["HOL.False"]),
 ("#Find"  ,["solutions v_v'i'"])],
-Rule_Set.e_rls, SOME "solve (e_e::bool, v_v)", [])),
+Rule_Set.empty, SOME "solve (e_e::bool, v_v)", [])),
 (Specify.prep_pbt thy "pbl_test_uni_poly_deg2" [] Celem.e_pblID
 (["degree_two","polynomial","univariate","equation","test"],
 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
 ("#Find"  ,["solutions v_v'i'"])],
-Rule_Set.e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", [])),
+Rule_Set.empty, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", [])),
 (Specify.prep_pbt thy "pbl_test_uni_poly_deg2_pq" [] Celem.e_pblID
 (["pq_formula","degree_two","polynomial","univariate","equation","test"],
 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
 ("#Find"  ,["solutions v_v'i'"])],
-Rule_Set.e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", [])),
+Rule_Set.empty, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", [])),
 (Specify.prep_pbt thy "pbl_test_uni_poly_deg2_abc" [] Celem.e_pblID
 (["abc_formula","degree_two","polynomial","univariate","equation","test"],
 [("#Given" ,["equality (a_a * x ^^^2 + b_b * x + c_c = 0)","solveFor v_v"]),
 ("#Find"  ,["solutions v_v'i'"])],
-Rule_Set.e_rls, SOME "solve (a_a * x ^^^2 + b_b * x + c_c = 0, v_v)", [])),
+Rule_Set.empty, SOME "solve (a_a * x ^^^2 + b_b * x + c_c = 0, v_v)", [])),
 (Specify.prep_pbt thy "pbl_test_uni_root" [] Celem.e_pblID
 (["squareroot","univariate","equation","test"],
 [("#Given" ,["equality e_e","solveFor v_v"]),
 ("#Where" ,["precond_rootpbl v_v"]),
 ("#Find"  ,["solutions v_v'i'"])],
-Rule_Set.append_rls "contains_root" Rule_Set.e_rls [Rule.Num_Calc ("Test.contains'_root",
+Rule_Set.append_rules "contains_root" Rule_Set.empty [Rule.Num_Calc ("Test.contains'_root",
 eval_contains_root "#contains_root_")],
 SOME "solve (e_e::bool, v_v)", [["Test","square_equation"]])),
 (Specify.prep_pbt thy "pbl_test_uni_norm" [] Celem.e_pblID
 (["normalise","univariate","equation","test"],
 [("#Given" ,["equality e_e","solveFor v_v"]),
 ("#Where" ,[]),
 ("#Find"  ,["solutions v_v'i'"])],
-Rule_Set.e_rls, SOME "solve (e_e::bool, v_v)", [["Test","norm_univar_equation"]])),
+Rule_Set.empty, SOME "solve (e_e::bool, v_v)", [["Test","norm_univar_equation"]])),
 (Specify.prep_pbt thy "pbl_test_uni_roottest" [] Celem.e_pblID
 (["sqroot-test","univariate","equation","test"],
 [("#Given" ,["equality e_e","solveFor v_v"]),
 ("#Where" ,["precond_rootpbl v_v"]),
 ("#Find"  ,["solutions v_v'i'"])],
-Rule_Set.e_rls, SOME "solve (e_e::bool, v_v)", [])),
+Rule_Set.empty, SOME "solve (e_e::bool, v_v)", [])),
 (Specify.prep_pbt thy "pbl_test_intsimp" [] Celem.e_pblID
 (["inttype","test"],
 [("#Given" ,["intTestGiven t_t"]),
 ("#Where" ,[]),
 ("#Find"  ,["intTestFind s_s"])],
-Rule_Set.e_rls, NONE, [["Test","intsimp"]]))]\<close>
+Rule_Set.empty, NONE, [["Test","intsimp"]]))]\<close>
 section \<open>methods\<close>
 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_Set.e_rls, prls=Rule_Set.e_rls,
+{rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
-crls=Atools_erls, errpats = [], nrls = Rule_Set.e_rls}, @{thm refl})]
+crls=Atools_erls, errpats = [], nrls = Rule_Set.empty}, @{thm refl})]
 \<close>
 partial_function (tailrec) solve_linear :: "bool \<Rightarrow> real \<Rightarrow> bool list"
 where
 "solve_linear e_e v_v = (
 [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_Set.e_rls,
+{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty,
 prls = assoc_rls' @{theory} "matches", calc = [], crls = tval_rls, errpats = [],
 nrls = Test_simplify},
 @{thm solve_linear.simps})]
 \<close>
 subsection \<open>root equation\<close>
 (["Test","sqrt-equ-test"],
 [("#Given" ,["equality e_e","solveFor v_v"]),
 ("#Where" ,["contains_root (e_e::bool)"]),
 ("#Find"  ,["solutions v_v'i'"])],
 {rew_ord'="e_rew_ord",rls'=tval_rls,
-srls = Rule_Set.append_rls "srls_contains_root" Rule_Set.e_rls
+srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
 [Rule.Num_Calc ("Test.contains'_root", eval_contains_root "")],
-prls = Rule_Set.append_rls "prls_contains_root" Rule_Set.e_rls
+prls = Rule_Set.append_rules "prls_contains_root" Rule_Set.empty
 [Rule.Num_Calc ("Test.contains'_root", eval_contains_root "")],
-calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.e_rls (*,asm_rls=[],
+calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty (*,asm_rls=[],
 asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
 @{thm solve_root_equ.simps})]
 \<close>
 partial_function (tailrec) minisubpbl :: "bool \<Rightarrow> real \<Rightarrow> bool list"
 (*tests subproblem fixed linear*)
 (["Test","squ-equ-test-subpbl1"],
 [("#Given" ,["equality e_e","solveFor v_v"]),
 ("#Where" ,["precond_rootmet v_v"]),
 ("#Find"  ,["solutions v_v'i'"])],
-{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.e_rls,
+{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty,
-prls = Rule_Set.append_rls "prls_met_test_squ_sub" Rule_Set.e_rls
+prls = Rule_Set.append_rules "prls_met_test_squ_sub" Rule_Set.empty
 [Rule.Num_Calc ("Test.precond'_rootmet", eval_precond_rootmet "")],
 calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify},
 @{thm minisubpbl.simps})]
 \<close>
 (*root-equation1:*)
 (["Test","square_equation1"],
 [("#Given" ,["equality e_e","solveFor v_v"]),
 ("#Find"  ,["solutions v_v'i'"])],
 {rew_ord'="e_rew_ord",rls'=tval_rls,
-srls = Rule_Set.append_rls "srls_contains_root" Rule_Set.e_rls
+srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
-[Rule.Num_Calc ("Test.contains'_root", eval_contains_root"")], prls=Rule_Set.e_rls, calc=[], crls=tval_rls,
+[Rule.Num_Calc ("Test.contains'_root", eval_contains_root"")], prls=Rule_Set.empty, calc=[], crls=tval_rls,
-errpats = [], nrls = Rule_Set.e_rls(*,asm_rls=[], asm_thm=[("square_equation_left",""),
+errpats = [], nrls = Rule_Set.empty(*,asm_rls=[], asm_thm=[("square_equation_left",""),
 ("square_equation_right","")]*)},
 @{thm solve_root_equ2.simps})]
 \<close>
 partial_function (tailrec) solve_root_equ3 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
 (*root-equation2*)
 (["Test","square_equation2"],
 [("#Given" ,["equality e_e","solveFor v_v"]),
 ("#Find"  ,["solutions v_v'i'"])],
 {rew_ord'="e_rew_ord",rls'=tval_rls,
-srls = Rule_Set.append_rls "srls_contains_root" Rule_Set.e_rls
+srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
 [Rule.Num_Calc ("Test.contains'_root", eval_contains_root"")],
-prls=Rule_Set.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.e_rls(*,asm_rls=[],
+prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty(*,asm_rls=[],
 asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
 @{thm solve_root_equ3.simps})]
 \<close>
 partial_function (tailrec) solve_root_equ4 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
 (*root-equation*)
 (["Test","square_equation"],
 [("#Given" ,["equality e_e","solveFor v_v"]),
 ("#Find"  ,["solutions v_v'i'"])],
 {rew_ord'="e_rew_ord",rls'=tval_rls,
-srls = Rule_Set.append_rls "srls_contains_root" Rule_Set.e_rls
+srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
 [Rule.Num_Calc ("Test.contains'_root", eval_contains_root"")],
-prls=Rule_Set.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.e_rls (*,asm_rls=[],
+prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty (*,asm_rls=[],
 asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
 @{thm solve_root_equ4.simps})]
 \<close>
 partial_function (tailrec) solve_plain_square :: "bool \<Rightarrow> real \<Rightarrow> bool list"
 ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^
 "(matches (     ?b*v_v ^^^2 = 0) e_e) |" ^
 "(matches (?a +    v_v ^^^2 = 0) e_e) |" ^
 "(matches (        v_v ^^^2 = 0) e_e)"]),
 ("#Find"  ,["solutions v_v'i'"])],
-{rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=Rule_Set.e_rls,
+{rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=Rule_Set.empty,
-prls = assoc_rls' @{theory} "matches", crls=tval_rls, errpats = [], nrls = Rule_Set.e_rls(*,
+prls = assoc_rls' @{theory} "matches", crls=tval_rls, errpats = [], nrls = Rule_Set.empty(*,
 asm_rls=[],asm_thm=[]*)},
 @{thm solve_plain_square.simps})]
 \<close>
 subsection \<open>polynomial equation\<close>
 [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_Set.e_rls,prls=Rule_Set.e_rls, calc=[], crls=tval_rls,
+{rew_ord'="e_rew_ord",rls'=tval_rls,srls = Rule_Set.empty,prls=Rule_Set.empty, calc=[], crls=tval_rls,
-errpats = [], nrls = Rule_Set.e_rls},
+errpats = [], nrls = Rule_Set.empty},
 @{thm norm_univariate_equ.simps})]
 \<close>
 subsection \<open>diophantine equation\<close>
 partial_function (tailrec) test_simplify :: "int \<Rightarrow> int"
 [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_Set.e_rls,  prls = Rule_Set.e_rls, calc = [],
+{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty,  prls = Rule_Set.empty, calc = [],
 crls = tval_rls, errpats = [], nrls = Test_simplify},
 @{thm test_simplify.simps})]
 \<close>
 end

changeset 59852	ea7e6679080e
parent 59851	4dd533681fef
child 59857	cbb3fae0381d