1.1 --- a/src/Tools/isac/Knowledge/InsSort.thy Thu Mar 15 10:17:44 2018 +0100
1.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy Thu Mar 15 12:42:04 2018 +0100
1.3 @@ -44,67 +44,67 @@
1.4 subsection {* rulesets *}
1.5 ML {*
1.6 val ins_sort =
1.7 - Rls {
1.8 - id = "ins_sort", preconds = [], rew_ord = ("tless_true", tless_true), erls = e_rls,
1.9 - srls = e_rls, calc = [], rules = [
1.10 - Thm ("xfoldr_Nil",(*num_str*) @{thm xfoldr_Nil} (* foldr ?f [] = id *)),
1.11 - Thm ("xfoldr_Cons", @{thm xfoldr_Cons} (* foldr ?f (?x # ?xs) = ?f ?x \<circ> foldr ?f ?xs *)),
1.12 + Celem.Rls {
1.13 + id = "ins_sort", preconds = [], rew_ord = ("tless_true", tless_true), erls = Celem.e_rls,
1.14 + srls = Celem.e_rls, calc = [], rules = [
1.15 + Celem.Thm ("xfoldr_Nil",(*num_str*) @{thm xfoldr_Nil} (* foldr ?f [] = id *)),
1.16 + Celem.Thm ("xfoldr_Cons", @{thm xfoldr_Cons} (* foldr ?f (?x # ?xs) = ?f ?x \<circ> foldr ?f ?xs *)),
1.17
1.18 - Thm ("ins_Nil", @{thm ins_Nil} (* ins ?i [] = [?i] *)),
1.19 - Thm ("ins_Cons", @{thm ins_Cons} (* ins ?i (?x # ?xs) = (if ?i < ?x then ?i # ?x # ?xs else ?x # ins ?i ?xs) *)),
1.20 - Thm ("sort_deff", @{thm sort_deff} (* InsSort.sort ?xs = foldr ins ?xs [] *)),
1.21 + Celem.Thm ("ins_Nil", @{thm ins_Nil} (* ins ?i [] = [?i] *)),
1.22 + Celem.Thm ("ins_Cons", @{thm ins_Cons} (* ins ?i (?x # ?xs) = (if ?i < ?x then ?i # ?x # ?xs else ?x # ins ?i ?xs) *)),
1.23 + Celem.Thm ("sort_deff", @{thm sort_deff} (* InsSort.sort ?xs = foldr ins ?xs [] *)),
1.24
1.25 - Thm ("o_id", @{thm o_id} (* ?f \<circ> id = ?f *)),
1.26 - Thm ("o_assoc", @{thm o_assoc} (* ?f \<circ> (?g \<circ> ?h) = ?f \<circ> ?g \<circ> ?h *)),
1.27 - Thm ("o_apply", @{thm o_apply} (* (?f \<circ> ?g) ?x = ?f (?g ?x) *)),
1.28 - Thm ("id_apply", @{thm id_apply} (* id ?x = ?x *)),
1.29 + Celem.Thm ("o_id", @{thm o_id} (* ?f \<circ> id = ?f *)),
1.30 + Celem.Thm ("o_assoc", @{thm o_assoc} (* ?f \<circ> (?g \<circ> ?h) = ?f \<circ> ?g \<circ> ?h *)),
1.31 + Celem.Thm ("o_apply", @{thm o_apply} (* (?f \<circ> ?g) ?x = ?f (?g ?x) *)),
1.32 + Celem.Thm ("id_apply", @{thm id_apply} (* id ?x = ?x *)),
1.33
1.34 - Calc ("Orderings.ord_class.less", eval_equ "#less_"),
1.35 - 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 - Thm ("if_True", @{thm if_True} (* "(if True then x else y) = x" *)),
1.37 - Thm ("if_False", @{thm if_False} (* "(if False then x else y) = y" *))],
1.38 - errpatts = [], scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")};
1.39 + Celem.Calc ("Orderings.ord_class.less", eval_equ "#less_"),
1.40 + 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.41 + Celem.Thm ("if_True", @{thm if_True} (* "(if True then x else y) = x" *)),
1.42 + Celem.Thm ("if_False", @{thm if_False} (* "(if False then x else y) = y" *))],
1.43 + errpatts = [], scr = Celem.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" [] e_pblID
1.50 - (["Programming"], [], e_rls, NONE, [])),
1.51 - (Specify.prep_pbt @{theory} "pbl_Prog_sort" [] e_pblID
1.52 - (["SORT","Programming"], [], e_rls, NONE, [])),
1.53 - (Specify.prep_pbt @{theory} "pbl_Prog_sort_ins" [] e_pblID
1.54 + [(Specify.prep_pbt @{theory} "pbl_Programming" [] Celem.e_pblID
1.55 + (["Programming"], [], Celem.e_rls, NONE, [])),
1.56 + (Specify.prep_pbt @{theory} "pbl_Prog_sort" [] Celem.e_pblID
1.57 + (["SORT","Programming"], [], Celem.e_rls, NONE, [])),
1.58 + (Specify.prep_pbt @{theory} "pbl_Prog_sort_ins" [] Celem.e_pblID
1.59 (["insertion","SORT","Programming"],
1.60 [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])],
1.61 - e_rls,
1.62 + Celem.e_rls,
1.63 SOME "Sort u_u", [["Programming","SORT","insertion_steps"]]))] *}
1.64
1.65 subsection {* methods *}
1.66 (* TODO: implementation needs extra object-level lists ?!?*)
1.67 setup {* KEStore_Elems.add_mets
1.68 - [ Specify.prep_met @{theory} "met_Programming" [] e_metID
1.69 + [ Specify.prep_met @{theory} "met_Programming" [] Celem.e_metID
1.70 (["Programming"], [],
1.71 - {rew_ord'="tless_true",rls' = e_rls, calc = [], srls = e_rls, prls = e_rls,
1.72 - crls = e_rls, errpats = [], nrls = e_rls}, "empty_script"),
1.73 - Specify.prep_met @{theory} "met_Prog_sort" [] e_metID
1.74 + {rew_ord'="tless_true",rls' = Celem.e_rls, calc = [], srls = Celem.e_rls, prls = Celem.e_rls,
1.75 + crls = Celem.e_rls, errpats = [], nrls = Celem.e_rls}, "empty_script"),
1.76 + Specify.prep_met @{theory} "met_Prog_sort" [] Celem.e_metID
1.77 (["Programming","SORT"], [],
1.78 - {rew_ord'="tless_true",rls' = e_rls, calc = [], srls = e_rls, prls = e_rls,
1.79 - crls = e_rls, errpats = [], nrls = e_rls},
1.80 + {rew_ord'="tless_true",rls' = Celem.e_rls, calc = [], srls = Celem.e_rls, prls = Celem.e_rls,
1.81 + crls = Celem.e_rls, errpats = [], nrls = Celem.e_rls},
1.82 "empty_script"),
1.83 - Specify.prep_met @{theory} "met_Prog_sort_ins" [] e_metID
1.84 + Specify.prep_met @{theory} "met_Prog_sort_ins" [] Celem.e_metID
1.85 (["Programming","SORT","insertion"],
1.86 [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])],
1.87 - {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = e_rls, prls = e_rls,
1.88 + {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Celem.e_rls, prls = Celem.e_rls,
1.89 crls = Atools_crls, errpats = [], nrls = norm_Rational},
1.90 "Script Sortprog (unso :: int xlist) = " ^
1.91 " (let uns = Take (sort unso) " ^
1.92 " in " ^
1.93 " (Rewrite_Set ins_sort False) uns" ^
1.94 " )"),
1.95 - Specify.prep_met @{theory} "met_Prog_sort_ins_steps" [] e_metID
1.96 + Specify.prep_met @{theory} "met_Prog_sort_ins_steps" [] Celem.e_metID
1.97 (["Programming","SORT","insertion_steps"],
1.98 [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])],
1.99 - {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = e_rls, prls = e_rls,
1.100 + {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Celem.e_rls, prls = Celem.e_rls,
1.101 crls = Atools_crls, errpats = [], nrls = norm_Rational},
1.102 "Script Sortprog (unso :: int xlist) = " ^
1.103 " (let uns = Take (sort unso) " ^