1.1 --- a/src/Tools/isac/Knowledge/InsSort.thy	Sat Jun 12 18:33:15 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy	Tue Jun 15 22:24:20 2021 +0200
     1.3 @@ -84,17 +84,14 @@
     1.4  
     1.5  section \<open>methods\<close>
     1.6  (* TODO: implementation needs extra object-level lists ?!?*)
     1.7 -setup \<open>KEStore_Elems.add_mets
     1.8 -  [ MethodC.prep_input @{theory} "met_Programming" [] MethodC.id_empty
     1.9 -      (["Programming"], [],
    1.10 -        {rew_ord'="tless_true",rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
    1.11 -          crls = Rule_Set.empty, errpats = [], nrls = Rule_Set.empty}, @{thm refl}),
    1.12 -    MethodC.prep_input @{theory} "met_Prog_sort" [] MethodC.id_empty
    1.13 -      (["Programming", "SORT"], [],
    1.14 -        {rew_ord'="tless_true",rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
    1.15 -          crls = Rule_Set.empty, errpats = [], nrls = Rule_Set.empty},
    1.16 -        @{thm refl})]
    1.17 -\<close>
    1.18 +
    1.19 +method met_Programming : "Programming" =
    1.20 +  \<open>{rew_ord'="tless_true",rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
    1.21 +    crls = Rule_Set.empty, errpats = [], nrls = Rule_Set.empty}\<close>
    1.22 +
    1.23 +method met_Prog_sort : "Programming/SORT" =
    1.24 +  \<open>{rew_ord'="tless_true",rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
    1.25 +    crls = Rule_Set.empty, errpats = [], nrls = Rule_Set.empty}\<close>
    1.26  
    1.27  partial_function (tailrec) sort_program :: "int xlist => int xlist"
    1.28    where
    1.29 @@ -103,14 +100,13 @@
    1.30      uns = Take (sort unso)
    1.31    in
    1.32      (Rewrite_Set ''ins_sort'') uns)"
    1.33 -setup \<open>KEStore_Elems.add_mets
    1.34 -   [MethodC.prep_input @{theory} "met_Prog_sort_ins" [] MethodC.id_empty
    1.35 -      (["Programming", "SORT", "insertion"], 
    1.36 -      [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])],
    1.37 -        {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
    1.38 -          crls = Atools_crls, errpats = [], nrls = norm_Rational},
    1.39 -        @{thm sort_program.simps})]
    1.40 -\<close>
    1.41 +
    1.42 +method met_Prog_sort_ins : "Programming/SORT/insertion" =
    1.43 +  \<open>{rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
    1.44 +    crls = Atools_crls, errpats = [], nrls = norm_Rational}\<close>
    1.45 +  Program: sort_program.simps
    1.46 +  Given: "unsorted u_u"
    1.47 +  Find: "sorted s_s"
    1.48  
    1.49  partial_function (tailrec) sort_program2 :: "int xlist => int xlist"
    1.50    where 
    1.51 @@ -133,14 +129,13 @@
    1.52        (Repeat (Rewrite ''if_True'')) Or
    1.53        (Repeat (Rewrite ''if_False'')))
    1.54      ) uns)"
    1.55 -setup \<open>KEStore_Elems.add_mets
    1.56 -   [MethodC.prep_input @{theory} "met_Prog_sort_ins_steps" [] MethodC.id_empty
    1.57 -      (["Programming", "SORT", "insertion_steps"], 
    1.58 -      [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])],
    1.59 -        {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
    1.60 -          crls = Atools_crls, errpats = [], nrls = norm_Rational},
    1.61 -        @{thm sort_program2.simps})]
    1.62 -\<close>
    1.63 +
    1.64 +method met_Prog_sort_ins_steps : "Programming/SORT/insertion_steps" =
    1.65 +  \<open>{rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
    1.66 +    crls = Atools_crls, errpats = [], nrls = norm_Rational}\<close>
    1.67 +  Program: sort_program2.simps
    1.68 +  Given: "unsorted u_u"
    1.69 +  Find: "sorted s_s"
    1.70  
    1.71  subsection \<open>CAS-commands\<close>
    1.72  ML \<open>