1.1 --- a/src/Tools/isac/Knowledge/InsSort.thy Thu Aug 25 08:19:58 2016 +0200
1.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy Thu Aug 25 14:57:58 2016 +0200
1.3 @@ -43,15 +43,22 @@
1.4 Rls {
1.5 id = "ins_sort", preconds = [], rew_ord = ("tless_true", tless_true), erls = e_rls,
1.6 srls = e_rls, calc = [], rules = [
1.7 - Thm ("foldl_Nil",(*num_str*) @{thm foldl_Nil}),
1.8 - Thm ("foldr_Cons", @{thm foldr_Cons}),
1.9 - Thm ("ins_Nil", @{thm ins_Nil}),
1.10 - Thm ("ins_Cons", @{thm ins_Cons}),
1.11 - Thm ("sort_Cons", @{thm sort_Cons}),
1.12 + Thm ("foldr_Nil",(*num_str*) @{thm foldr_Nil} (* foldr ?f [] = id *)),
1.13 + Thm ("foldr_Cons", @{thm foldr_Cons} (* foldr ?f (?x # ?xs) = ?f ?x \<circ> foldr ?f ?xs *)),
1.14 +
1.15 + Thm ("ins_Nil", @{thm ins_Nil} (* ins ?i [] = [?i] *)),
1.16 + Thm ("ins_Cons", @{thm ins_Cons} (* ins ?i (?x # ?xs) = (if ?i < ?x then ?i # ?x # ?xs else ?x # ins ?i ?xs) *)),
1.17 + Thm ("sort_Cons", @{thm sort_Cons} (* InsSort.sort ?xs = foldr ins ?xs [] *)),
1.18 +
1.19 + Thm ("o_id", @{thm o_id} (* ?f \<circ> id = ?f *)),
1.20 + Thm ("o_assoc", @{thm o_assoc} (* ?f \<circ> (?g \<circ> ?h) = ?f \<circ> ?g \<circ> ?h *)),
1.21 + Thm ("o_apply", @{thm o_apply} (* (?f \<circ> ?g) ?x = ?f (?g ?x) *)),
1.22 + Thm ("id_apply", @{thm id_apply} (* id ?x = ?x *)),
1.23
1.24 Calc ("Orderings.ord_class.less", eval_equ "#less_"),
1.25 - Thm ("if_True", @{thm if_True}),
1.26 - Thm ("if_False", @{thm if_False})],
1.27 + 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.28 + Thm ("if_True", @{thm if_True} (* *)),
1.29 + Thm ("if_False", @{thm if_False} (* *))],
1.30 errpatts = [], scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")};
1.31 *}
1.32 setup {* KEStore_Elems.add_rlss [("ins_sort", (Context.theory_name @{theory}, ins_sort))] *}
2.1 --- a/test/Tools/isac/Knowledge/inssort.sml Thu Aug 25 08:19:58 2016 +0200
2.2 +++ b/test/Tools/isac/Knowledge/inssort.sml Thu Aug 25 14:57:58 2016 +0200
2.3 @@ -1,18 +1,21 @@
2.4 -(* use"test-inssort.sml";
2.5 - W.N.17.6.00
2.6 +(* Title: tests for ListC
2.7 + Author: Walther Neuper 17.6.00
2.8 + (c) copyright due to lincense terms.
2.9 *)
2.10 -"--------------------------------------------------------";
2.11 -"--------------------------------------------------------";
2.12 -"table of contents --------------------------------------";
2.13 -"--------------------------------------------------------";
2.14 -"----------- inssort in SML -----------------------------";
2.15 -"--------------------------------------------------------";
2.16 -"--------------------------------------------------------";
2.17 +"-----------------------------------------------------------------------------";
2.18 +"-----------------------------------------------------------------------------";
2.19 +"table of contents -----------------------------------------------------------";
2.20 +"-----------------------------------------------------------------------------";
2.21 +"----------- inssort in SML --------------------------------------------------";
2.22 +"----------- insertion sort by rewrite stepwise ------------------------------";
2.23 +"----------- insertion sort with ruleset -------------------------------------";
2.24 +"-----------------------------------------------------------------------------";
2.25 +"-----------------------------------------------------------------------------";
2.26
2.27
2.28 -"----------- inssort in SML -----------------------------";
2.29 -"----------- inssort in SML -----------------------------";
2.30 -"----------- inssort in SML -----------------------------";
2.31 +"----------- inssort in SML --------------------------------------------------";
2.32 +"----------- inssort in SML --------------------------------------------------";
2.33 +"----------- inssort in SML --------------------------------------------------";
2.34 fun foldr _ [] a = a
2.35 | foldr f (x :: xs) a = foldr f xs (f a x);
2.36 (*val foldr = fn : ('a -> 'b -> 'a) -> 'b list -> 'a -> 'a*)
2.37 @@ -22,92 +25,72 @@
2.38 fun sort xs = foldr ins xs [];
2.39 (*val sort = fn : int list -> int list*)
2.40
2.41 +"----------- insertion sort by rewrite stepwise ------------------------------";
2.42 +"----------- insertion sort by rewrite stepwise ------------------------------";
2.43 +"----------- insertion sort by rewrite stepwise ------------------------------";
2.44 +val ctxt = Proof_Context.init_global @{theory};
2.45 +val SOME t = parseNEW ctxt "sort [1, 3, 2]";
2.46 +
2.47 +val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm sort_Cons} t;
2.48 +term2str t' (*"foldr ins [1, 3, 2] []"*);
2.49 +
2.50 +val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm foldr_Cons} t';
2.51 +term2str t' (*"(ins 1 o foldr ins [3, 2]) []"*);
2.52 +
2.53 +val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm foldr_Cons} t';
2.54 +term2str t' (*"(ins 1 o (ins 3 o foldr ins [2])) []"*);
2.55 +
2.56 +val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm foldr_Cons} t';
2.57 +term2str t' (*"(ins 1 o (ins 3 o (ins 2 o foldr ins []))) []"*);
2.58 +
2.59 +val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm foldr_Nil} t';
2.60 +term2str t' (*"(ins 1 o (ins 3 o (ins 2 o id))) []"*);
2.61 +
2.62 +val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm o_id} t';
2.63 +term2str t' (*"(ins 1 o (ins 3 o ins 2)) []"*);
2.64 +
2.65 +val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm o_assoc} t';
2.66 +term2str t' (*"(ins 1 o ins 3 o ins 2) []" = "((ins 1 o ins 3) o ins 2) []"*);
2.67 +
2.68 +val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm o_apply} t';
2.69 +term2str t' (*"(ins 1 o ins 3) (ins 2 [])"*);
2.70 +
2.71 +val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm o_apply} t';
2.72 +term2str t' (*"ins 1 (ins 3 (ins 2 []))"*);
2.73 +
2.74 +val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm ins_Nil} t';
2.75 +term2str t' (*"ins 1 (ins 3 [2])"*);
2.76 +
2.77 +val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm ins_Cons} t';
2.78 +term2str t' (*"ins 1 (if 3 < 2 then [3, 2] else 2 # ins 3 [])"*);
2.79 +
2.80 +val SOME (t', _) = calculate_ @{theory} ("Orderings.ord_class.less", eval_equ "#less_") t';
2.81 +term2str t' (*"ins 1 (if False then [3, 2] else 2 # ins 3 [])"*);
2.82 +
2.83 +val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm if_False} t';
2.84 +term2str t' (*"ins 1 (2 # ins 3 [])"*);
2.85 +
2.86 +val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm ins_Nil} t';
2.87 +term2str t' (*"ins 1 [2, 3]"*);
2.88 +
2.89 +val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm ins_Cons} t';
2.90 +term2str t' (*"if 1 < 2 then [1, 2, 3] else 2 # ins 1 [3]"*);
2.91 +
2.92 +val SOME (t', _) = calculate_ @{theory} ("Orderings.ord_class.less", eval_equ "#less_") t';
2.93 +term2str t' (*"if True then [1, 2, 3] else 2 # ins 1 [3]"*);
2.94 +
2.95 +val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm if_True} t';
2.96 +if term2str t' = "[1, 2, 3]" then () else error "CHANGED RESULT FOR sort by rewrite stepwise";
2.97 +
2.98 +"----------- insertion sort with ruleset -------------------------------------";
2.99 +"----------- insertion sort with ruleset -------------------------------------";
2.100 +"----------- insertion sort with ruleset -------------------------------------";
2.101 +if term2str t = "InsSort.sort [1, 3, 2]" then () else error "CHANGED START FOR sort with ruleset";
2.102 +val SOME (t', _) = rewrite_set_ @{theory} false ins_sort t;
2.103 +if term2str t' = "[1, 2, 3]" then () else error "CHANGED RESULT FOR sort with ruleset";
2.104 +
2.105 +
2.106 (*========== inhibit exn =======================================================
2.107 -
2.108 -(* insertion sort, would need lists different from script-lists WN.11.00
2.109 -WN.7.6.03: -"- started with someList :: 'a list => unl, fun dest_list *)
2.110 -
2.111 -"--------------- sort [1,4,3,2] by rewrite_set ----------------";
2.112 -val thy' = "InsSort";
2.113 -val ct = "sort [1,4,3,2]";
2.114 -"--- 1 ---";
2.115 -val rls = "ins_sort";
2.116 -val (ct,_) = the (rewrite_set thy' "eval_rls" false rls ct);
2.117 -if ct="[1, 2, 3, 4]" then "sort [1,4,3,2] OK"
2.118 -else error "sort [1,4,3,2] didn't work";
2.119 -
2.120 -
2.121 -"---------------- sort [1,3,2] by rewrite stepwise ----------------";
2.122 -val thy' = "InsSort";
2.123 -val ct = "sort [1,3,2]";
2.124 -"--- 1 ---";
2.125 -val thm = ("sort_def","");
2.126 -val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
2.127 -(*val ct = "foldr ins [#1::real, #3::real, #2::real] []"*)
2.128 -"--- 2 ---";
2.129 -val thm = ("foldr_rec","");
2.130 -val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
2.131 -(*val ct = "foldr ins [#3, #2] (ins [] #1)"*)
2.132 -"--- 3 ---";
2.133 -val thm = ("ins_base","");
2.134 -val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
2.135 -(*val ct = "foldr ins [#3, #2] [#1]"*)
2.136 -"--- 4 ---";
2.137 -val thm = ("foldr_rec","");
2.138 -val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
2.139 -(*val ct = "foldr ins [#2] (ins [#1] #3)"*)
2.140 -"--- 5 ---";
2.141 -val thm = ("ins_rec","");
2.142 -val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
2.143 -(*val ct = "foldr ins [#2] (if #1 < #3 then #1 # ins [] #3 else [#3, #1])"*)
2.144 -"--- 6 ---";
2.145 -val op_ = "le";
2.146 -val (ct,_) = the (calculate thy' op_ ct);
2.147 -(*val ct = "foldr ins [#2] (if True then #1 # ins [] #3 else [#3, #1])"*)
2.148 -"--- 7 ---";
2.149 -val thm = ("if_True","");
2.150 -val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
2.151 -(*val ct = "foldr ins [#2] (#1 # ins [] #3)"*)
2.152 -"--- 8 ---";
2.153 -val thm = ("ins_base","");
2.154 -val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
2.155 -(*val ct = "foldr ins [#2] [#1, #3]"*)
2.156 -"--- 9 ---";
2.157 -val thm = ("foldr_rec","");
2.158 -val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
2.159 -(*val ct = "foldr ins [] (ins [#1, #3] #2)"*)
2.160 -"--- 10 ---";
2.161 -val thm = ("ins_rec","");
2.162 -val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
2.163 -(*val ct = "foldr ins [] (if #1 < #2 then #1 # ins [#3] #2 else [#2, #1, #3])"*)
2.164 -"--- 11 ---";
2.165 -val op_ = "le";
2.166 -val (ct,_) = the (calculate thy' op_ ct);
2.167 -(*val ct = "foldr ins [] (if True then #1 # ins [#3] #2 else [#2, #1, #3])"*)
2.168 -"--- 12 ---";
2.169 -val thm = ("if_True","");
2.170 -val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
2.171 -(*"foldr ins [] (#1 # ins [#3] #2)"*)
2.172 -"--- 13 ---";
2.173 -val thm = ("ins_rec","");
2.174 -val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
2.175 -(*"foldr ins [] (#1 # (if #3 < #2 then #3 # ins [] #2 else [#2, #3]))"*)
2.176 -"--- 14 ---";
2.177 -val op_ = "le";
2.178 -val (ct,_) = the (calculate thy' op_ ct);
2.179 -(*val ct = "foldr ins [] (#1 # (if False then #3 # ins [] #2 else [#2, #3]))"*)
2.180 -"--- 15 ---";
2.181 -val thm = ("if_False","");
2.182 -val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
2.183 -(*val ct = "foldr ins [] [#1, #2, #3]"*)
2.184 -"--- 16 ---";
2.185 -val thm = ("foldr_base","");
2.186 -val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
2.187 -(*val ct = "[#1, #2, #3]"*)
2.188 -if ct="[1, 2, 3]" then "sort [1,3,2] OK"
2.189 -else error "sort [1,3,2] didn't work";
2.190 -
2.191 -
2.192 "---------------- sort [1,3,2] from script ----------------";
2.193 val fmz = ["unsorted [1,3,2]", "sorted S"];
2.194 val (dI',pI',mI') =
3.1 --- a/test/Tools/isac/Test_Isac.thy Thu Aug 25 08:19:58 2016 +0200
3.2 +++ b/test/Tools/isac/Test_Isac.thy Thu Aug 25 14:57:58 2016 +0200
3.3 @@ -149,6 +149,7 @@
3.4 ML_file "Knowledge/algein.sml"
3.5 ML_file "Knowledge/diophanteq.sml"
3.6 ML_file "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"
3.7 + ML_file "Knowledge/inssort.sml"
3.8 ML_file "Knowledge/isac.sml"
3.9 ML_file "Knowledge/build_thydata.sml"
3.10 ML {*"%%%%%%%%%%%%%%%%% end Knowledge %%%%%%%%%%%%%%%%%%%%%%%%";*}