1.1 --- a/src/Tools/isac/Knowledge/InsSort.thy Sun Mar 25 13:59:57 2018 +0200
1.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy Mon Mar 26 07:28:39 2018 +0200
1.3 @@ -44,39 +44,39 @@
1.4 subsection {* rulesets *}
1.5 ML {*
1.6 val ins_sort =
1.7 - Celem.Rls {
1.8 - id = "ins_sort", preconds = [], rew_ord = ("tless_true", tless_true), erls = Celem.e_rls,
1.9 - srls = Celem.e_rls, calc = [], rules = [
1.10 - Celem.Thm ("xfoldr_Nil",(*num_str*) @{thm xfoldr_Nil} (* foldr ?f [] = id *)),
1.11 - Celem.Thm ("xfoldr_Cons", @{thm xfoldr_Cons} (* foldr ?f (?x # ?xs) = ?f ?x \<circ> foldr ?f ?xs *)),
1.12 + Rule.Rls {
1.13 + id = "ins_sort", preconds = [], rew_ord = ("tless_true", tless_true), erls = Rule.e_rls,
1.14 + srls = Rule.e_rls, calc = [], rules = [
1.15 + Rule.Thm ("xfoldr_Nil",(*num_str*) @{thm xfoldr_Nil} (* foldr ?f [] = id *)),
1.16 + Rule.Thm ("xfoldr_Cons", @{thm xfoldr_Cons} (* foldr ?f (?x # ?xs) = ?f ?x \<circ> foldr ?f ?xs *)),
1.17
1.18 - Celem.Thm ("ins_Nil", @{thm ins_Nil} (* ins ?i [] = [?i] *)),
1.19 - Celem.Thm ("ins_Cons", @{thm ins_Cons} (* ins ?i (?x # ?xs) = (if ?i < ?x then ?i # ?x # ?xs else ?x # ins ?i ?xs) *)),
1.20 - Celem.Thm ("sort_deff", @{thm sort_deff} (* InsSort.sort ?xs = foldr ins ?xs [] *)),
1.21 + Rule.Thm ("ins_Nil", @{thm ins_Nil} (* ins ?i [] = [?i] *)),
1.22 + Rule.Thm ("ins_Cons", @{thm ins_Cons} (* ins ?i (?x # ?xs) = (if ?i < ?x then ?i # ?x # ?xs else ?x # ins ?i ?xs) *)),
1.23 + Rule.Thm ("sort_deff", @{thm sort_deff} (* InsSort.sort ?xs = foldr ins ?xs [] *)),
1.24
1.25 - Celem.Thm ("o_id", @{thm o_id} (* ?f \<circ> id = ?f *)),
1.26 - Celem.Thm ("o_assoc", @{thm o_assoc} (* ?f \<circ> (?g \<circ> ?h) = ?f \<circ> ?g \<circ> ?h *)),
1.27 - Celem.Thm ("o_apply", @{thm o_apply} (* (?f \<circ> ?g) ?x = ?f (?g ?x) *)),
1.28 - Celem.Thm ("id_apply", @{thm id_apply} (* id ?x = ?x *)),
1.29 + Rule.Thm ("o_id", @{thm o_id} (* ?f \<circ> id = ?f *)),
1.30 + Rule.Thm ("o_assoc", @{thm o_assoc} (* ?f \<circ> (?g \<circ> ?h) = ?f \<circ> ?g \<circ> ?h *)),
1.31 + Rule.Thm ("o_apply", @{thm o_apply} (* (?f \<circ> ?g) ?x = ?f (?g ?x) *)),
1.32 + Rule.Thm ("id_apply", @{thm id_apply} (* id ?x = ?x *)),
1.33
1.34 - Celem.Calc ("Orderings.ord_class.less", eval_equ "#less_"),
1.35 - Celem.Thm ("If_def", @{thm If_def} (* if ?P then ?x else ?y \<equiv> THE z. (?P = True \<longrightarrow> z = ?x) \<and> (?P = False \<longrightarrow> z = ?y) *)),
1.36 - Celem.Thm ("if_True", @{thm if_True} (* "(if True then x else y) = x" *)),
1.37 - Celem.Thm ("if_False", @{thm if_False} (* "(if False then x else y) = y" *))],
1.38 - errpatts = [], scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")};
1.39 + Rule.Calc ("Orderings.ord_class.less", eval_equ "#less_"),
1.40 + Rule.Thm ("If_def", @{thm If_def} (* if ?P then ?x else ?y \<equiv> THE z. (?P = True \<longrightarrow> z = ?x) \<and> (?P = False \<longrightarrow> z = ?y) *)),
1.41 + Rule.Thm ("if_True", @{thm if_True} (* "(if True then x else y) = x" *)),
1.42 + Rule.Thm ("if_False", @{thm if_False} (* "(if False then x else y) = y" *))],
1.43 + errpatts = [], scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")};
1.44 *}
1.45 setup {* KEStore_Elems.add_rlss [("ins_sort", (Context.theory_name @{theory}, ins_sort))] *}
1.46
1.47 subsection {* problems *}
1.48 setup {* KEStore_Elems.add_pbts
1.49 [(Specify.prep_pbt @{theory} "pbl_Programming" [] Celem.e_pblID
1.50 - (["Programming"], [], Celem.e_rls, NONE, [])),
1.51 + (["Programming"], [], Rule.e_rls, NONE, [])),
1.52 (Specify.prep_pbt @{theory} "pbl_Prog_sort" [] Celem.e_pblID
1.53 - (["SORT","Programming"], [], Celem.e_rls, NONE, [])),
1.54 + (["SORT","Programming"], [], Rule.e_rls, NONE, [])),
1.55 (Specify.prep_pbt @{theory} "pbl_Prog_sort_ins" [] Celem.e_pblID
1.56 (["insertion","SORT","Programming"],
1.57 [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])],
1.58 - Celem.e_rls,
1.59 + Rule.e_rls,
1.60 SOME "Sort u_u", [["Programming","SORT","insertion_steps"]]))] *}
1.61
1.62 subsection {* methods *}
1.63 @@ -84,17 +84,17 @@
1.64 setup {* KEStore_Elems.add_mets
1.65 [ Specify.prep_met @{theory} "met_Programming" [] Celem.e_metID
1.66 (["Programming"], [],
1.67 - {rew_ord'="tless_true",rls' = Celem.e_rls, calc = [], srls = Celem.e_rls, prls = Celem.e_rls,
1.68 - crls = Celem.e_rls, errpats = [], nrls = Celem.e_rls}, "empty_script"),
1.69 + {rew_ord'="tless_true",rls' = Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls,
1.70 + crls = Rule.e_rls, errpats = [], nrls = Rule.e_rls}, "empty_script"),
1.71 Specify.prep_met @{theory} "met_Prog_sort" [] Celem.e_metID
1.72 (["Programming","SORT"], [],
1.73 - {rew_ord'="tless_true",rls' = Celem.e_rls, calc = [], srls = Celem.e_rls, prls = Celem.e_rls,
1.74 - crls = Celem.e_rls, errpats = [], nrls = Celem.e_rls},
1.75 + {rew_ord'="tless_true",rls' = Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls,
1.76 + crls = Rule.e_rls, errpats = [], nrls = Rule.e_rls},
1.77 "empty_script"),
1.78 Specify.prep_met @{theory} "met_Prog_sort_ins" [] Celem.e_metID
1.79 (["Programming","SORT","insertion"],
1.80 [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])],
1.81 - {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Celem.e_rls, prls = Celem.e_rls,
1.82 + {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls,
1.83 crls = Atools_crls, errpats = [], nrls = norm_Rational},
1.84 "Script Sortprog (unso :: int xlist) = " ^
1.85 " (let uns = Take (sort unso) " ^
1.86 @@ -104,7 +104,7 @@
1.87 Specify.prep_met @{theory} "met_Prog_sort_ins_steps" [] Celem.e_metID
1.88 (["Programming","SORT","insertion_steps"],
1.89 [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])],
1.90 - {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Celem.e_rls, prls = Celem.e_rls,
1.91 + {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls,
1.92 crls = Atools_crls, errpats = [], nrls = norm_Rational},
1.93 "Script Sortprog (unso :: int xlist) = " ^
1.94 " (let uns = Take (sort unso) " ^