1.1 --- a/src/Tools/isac/Knowledge/InsSort.thy Fri Aug 26 12:02:43 2016 +0200
1.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy Fri Aug 26 12:25:03 2016 +0200
1.3 @@ -7,24 +7,24 @@
1.4 sorted :: "'a list => unl"
1.5
1.6 (* subproblem and script-name *)
1.7 - Ins'_sort :: "['a list,
1.8 - 'a list] => 'a list"
1.9 + Ins'_sort :: "['a xlist,
1.10 + 'a xlist] => 'a xlist"
1.11 ("((Script Ins'_sort (_ =))//
1.12 (_))" 9)
1.13 - Sort :: "['a list,
1.14 - 'a list] => 'a list"
1.15 + Sort :: "['a xlist,
1.16 + 'a xlist] => 'a xlist"
1.17 ("((Script Sort (_ =))//
1.18 (_))" 9)
1.19
1.20 subsection {* functions *}
1.21 -primrec ins :: "int \<Rightarrow> int list \<Rightarrow> int list"
1.22 +primrec ins :: "int \<Rightarrow> int xlist \<Rightarrow> int xlist"
1.23 where
1.24 -ins_Nil: "ins i [] = [i]" |
1.25 -ins_Cons: "ins i (x # xs) = (if i < x then (i # x # xs) else x # (ins i xs))"
1.26 +ins_Nil: "ins i [|| ||] = [||i||]" |
1.27 +ins_Cons: "ins i (x @# xs) = (if i < x then (i @# x @# xs) else x @# (ins i xs))"
1.28
1.29 -fun sort :: "int list \<Rightarrow> int list"
1.30 +fun sort :: "int xlist \<Rightarrow> int xlist"
1.31 where
1.32 -sort_deff: "sort xs = foldr ins xs []"
1.33 +sort_deff: "sort xs = xfoldr ins xs [|| ||]"
1.34 print_theorems
1.35 thm sort_def (* InsSort.sort \<equiv> sort_sumC *)
1.36 thm sort_deff (* InsSort.sort ?xs = foldr ins ?xs [] *)
1.37 @@ -35,8 +35,8 @@
1.38 @{thm ins.simps(2)};
1.39 *}
1.40
1.41 -value "sort [2,3,1]"
1.42 -lemma test: "sort [2,3,1] = [1,2,3]"
1.43 +value "sort [||2,3,1||]"
1.44 +lemma test: "sort [||2,3,1||] = [||1,2,3||]"
1.45 by simp
1.46
1.47 subsection {* eval functions *}
1.48 @@ -46,8 +46,8 @@
1.49 Rls {
1.50 id = "ins_sort", preconds = [], rew_ord = ("tless_true", tless_true), erls = e_rls,
1.51 srls = e_rls, calc = [], rules = [
1.52 - Thm ("foldr_Nil",(*num_str*) @{thm foldr_Nil} (* foldr ?f [] = id *)),
1.53 - Thm ("foldr_Cons", @{thm foldr_Cons} (* foldr ?f (?x # ?xs) = ?f ?x \<circ> foldr ?f ?xs *)),
1.54 + Thm ("xfoldr_Nil",(*num_str*) @{thm xfoldr_Nil} (* foldr ?f [] = id *)),
1.55 + Thm ("xfoldr_Cons", @{thm xfoldr_Cons} (* foldr ?f (?x # ?xs) = ?f ?x \<circ> foldr ?f ?xs *)),
1.56
1.57 Thm ("ins_Nil", @{thm ins_Nil} (* ins ?i [] = [?i] *)),
1.58 Thm ("ins_Cons", @{thm ins_Cons} (* ins ?i (?x # ?xs) = (if ?i < ?x then ?i # ?x # ?xs else ?x # ins ?i ?xs) *)),
1.59 @@ -96,7 +96,7 @@
1.60 (["Programming","sort"], [],
1.61 {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = e_rls, prls = e_rls,
1.62 crls = Atools_crls, errpats = [], nrls = norm_Rational},
1.63 - "Script Sort (u_u::'a list) = (Rewrite_Set ins_sort False) u_u")
1.64 + "Script Sort (u_u::'a xlist) = (Rewrite_Set ins_sort False) u_u")
1.65 ]
1.66 *}
1.67 end
2.1 --- a/src/Tools/isac/ProgLang/ListC.thy Fri Aug 26 12:02:43 2016 +0200
2.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Fri Aug 26 12:25:03 2016 +0200
2.3 @@ -11,23 +11,60 @@
2.4 ML_file "~~/src/Tools/isac/ProgLang/calculate.sml"
2.5 ML_file "~~/src/Tools/isac/ProgLang/rewrite.sml"
2.6
2.7 -text {*
2.8 - This file gives names to equations of function definitions,
2.9 - which are required for Lucas-Interpretation (by Isac's rewriter) of
2.10 - Isac's programming language. This language preceeded the function package
2.11 +subsection {* Notes on Isac's programming language *}
2.12 +text {*
2.13 + Isac's programming language combines tacticals (TRY, etc) and
2.14 + tactics (Rewrite, etc) with list processing.
2.15 +
2.16 + In order to distinguish list expressions of the meta (programming)
2.17 + language from the object language in Lucas-Interpretation, a
2.18 + new 'type xlist' is introduced.
2.19 + TODO: Switch the role of 'xlist' and 'list' (the former only used
2.20 + by InsSort.thy)
2.21 +
2.22 + Isac's programming language preceeded the function package
2.23 in 2002. For naming "axiomatization" is used for reasons of uniformity
2.24 with the other replacements for "axioms".
2.25 Another reminiscence from Isabelle2002 are Isac-specific numerals,
2.26 introduced in order to have floating point numerals at a time,
2.27 when Isabelle did not consider that requirement. For the sake of uniformity
2.28 - 'nat' from List.thy is replaced by 'real'.
2.29 + 'nat' from List.thy is replaced by 'real' by 'fun parse',
2.30 + however, 'fun parseNEW' has started to replace this fix (after finishing
2.31 + this fix, there will be a 'rename all parseNEW --> parse).
2.32
2.33 - TODO: shift name-declarations to HOL/List.thy, adopt new names from there
2.34 - and remove this ListC.thy.
2.35 Note: *one* "axiomatization" over all equations caused strange "'a list list"
2.36 types.
2.37 *}
2.38
2.39 +subsection {* Type 'xlist' for Lucas-Interpretation *}
2.40 +(*TODO: ask for shorter deliminters in xlist *)
2.41 +datatype 'a xlist =
2.42 + XNil ("[|| ||]")
2.43 + | XCons 'a "'a xlist" (infixr "@#" 65)
2.44 +
2.45 +syntax
2.46 + -- {* list Enumeration *}
2.47 + "_xlist" :: "args => 'a xlist" ("[||(_)||]")
2.48 +
2.49 +translations
2.50 + "[||x, xs||]" == "x@#[||xs||]"
2.51 + "[||x||]" == "x@#[|| ||]"
2.52 +
2.53 +term "[|| ||]"
2.54 +term "[||1,2,3||]"
2.55 +
2.56 +subsection {* Functions for 'xlist' *}
2.57 +(* TODO:
2.58 +(1) revise, if definition of identifiers like LENGTH_NIL are still required.
2.59 +(2) switch the role of 'xlist' and 'list' in the functions below, in particular for
2.60 + 'foldr', 'foldr_Nil', 'foldr_Cons' and 'xfoldr', 'xfoldr_Nil', 'xfoldr_Cons'.
2.61 + For transition phase just outcomment InsSort.thy and inssort.sml.
2.62 +*)
2.63 +
2.64 +primrec xfoldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a xlist \<Rightarrow> 'b \<Rightarrow> 'b" where
2.65 +xfoldr_Nil: "xfoldr f [|| ||] = id" |
2.66 +xfoldr_Cons: "xfoldr f (x @# xs) = f x \<circ> xfoldr f xs"
2.67 +
2.68 primrec LENGTH :: "'a list => real"
2.69 where
2.70 LENGTH_NIL: "LENGTH [] = 0" |
3.1 --- a/test/Tools/isac/Knowledge/inssort.sml Fri Aug 26 12:02:43 2016 +0200
3.2 +++ b/test/Tools/isac/Knowledge/inssort.sml Fri Aug 26 12:25:03 2016 +0200
3.3 @@ -29,21 +29,21 @@
3.4 "----------- insertion sort by rewrite stepwise ------------------------------";
3.5 "----------- insertion sort by rewrite stepwise ------------------------------";
3.6 val ctxt = Proof_Context.init_global @{theory};
3.7 -val SOME t = parseNEW ctxt "sort [1, 3, 2]";
3.8 +val SOME t = parseNEW ctxt "sort [||1, 3, 2||]";
3.9
3.10 val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm sort_deff} t;
3.11 term2str t' (*"foldr ins [1, 3, 2] []"*);
3.12
3.13 -val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm foldr_Cons} t';
3.14 +val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm xfoldr_Cons} t';
3.15 term2str t' (*"(ins 1 o foldr ins [3, 2]) []"*);
3.16
3.17 -val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm foldr_Cons} t';
3.18 +val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm xfoldr_Cons} t';
3.19 term2str t' (*"(ins 1 o (ins 3 o foldr ins [2])) []"*);
3.20
3.21 -val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm foldr_Cons} t';
3.22 +val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm xfoldr_Cons} t';
3.23 term2str t' (*"(ins 1 o (ins 3 o (ins 2 o foldr ins []))) []"*);
3.24
3.25 -val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm foldr_Nil} t';
3.26 +val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm xfoldr_Nil} t';
3.27 term2str t' (*"(ins 1 o (ins 3 o (ins 2 o id))) []"*);
3.28
3.29 val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm o_id} t';
3.30 @@ -80,14 +80,14 @@
3.31 term2str t' (*"if True then [1, 2, 3] else 2 # ins 1 [3]"*);
3.32
3.33 val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm if_True} t';
3.34 -if term2str t' = "[1, 2, 3]" then () else error "CHANGED RESULT FOR sort by rewrite stepwise";
3.35 +if term2str t' = "[||1, 2, 3||]" then () else error "CHANGED RESULT FOR sort by rewrite stepwise";
3.36
3.37 "----------- insertion sort with ruleset -------------------------------------";
3.38 "----------- insertion sort with ruleset -------------------------------------";
3.39 "----------- insertion sort with ruleset -------------------------------------";
3.40 -if term2str t = "InsSort.sort [1, 3, 2]" then () else error "CHANGED START FOR sort with ruleset";
3.41 +if term2str t = "InsSort.sort [||1, 3, 2||]" then () else error "CHANGED START FOR sort with ruleset";
3.42 val SOME (t', _) = rewrite_set_ @{theory} false ins_sort t;
3.43 -if term2str t' = "[1, 2, 3]" then () else error "CHANGED RESULT FOR sort with ruleset";
3.44 +if term2str t' = "[||1, 2, 3||]" then () else error "CHANGED RESULT FOR sort with ruleset";
3.45
3.46
3.47 (*========== inhibit exn =======================================================
4.1 --- a/test/Tools/isac/ProgLang/listC.sml Fri Aug 26 12:02:43 2016 +0200
4.2 +++ b/test/Tools/isac/ProgLang/listC.sml Fri Aug 26 12:25:03 2016 +0200
4.3 @@ -7,12 +7,34 @@
4.4 "-----------------------------------------------------------------------------";
4.5 "table of contents -----------------------------------------------------------";
4.6 "-----------------------------------------------------------------------------";
4.7 +"----------- check 'type xlist' [||1, 2, 3||] --------------------------------";
4.8 "--------------------- NTH ---------------------------------------------------";
4.9 "--------------------- LENGTH ------------------------------------------------";
4.10 "--------------------- tl ----------------------------------------------------";
4.11 "-----------------------------------------------------------------------------";
4.12 "-----------------------------------------------------------------------------";
4.13
4.14 +"----------- check 'type xlist' [||1, 2, 3||] --------------------------------";
4.15 +"----------- check 'type xlist' [||1, 2, 3||] --------------------------------";
4.16 +"----------- check 'type xlist' [||1, 2, 3||] --------------------------------";
4.17 +(* ML representation *)
4.18 +val t1 = @{term "[|| ||]"};
4.19 +val t2 = @{term "[||1,2,3||]"};
4.20 +
4.21 +(* pretty printing *)
4.22 +if Print_Mode.setmp []
4.23 + (Syntax.string_of_term (Config.put show_markup false (Proof_Context.init_global @{theory}))) t1
4.24 + = "[|| ||]"
4.25 +then () else error "CHANGED pretty printing of '[|| ||]'";
4.26 +
4.27 +if Print_Mode.setmp []
4.28 + (Syntax.string_of_term (Config.put show_markup false (Proof_Context.init_global @{theory}))) t2
4.29 + = "[||1::'a, 2::'a, 3::'a||]"
4.30 +then () else error "CHANGED pretty printing of '[||1,2,3||]'"
4.31 +
4.32 +(* parsing *)
4.33 +Syntax.read_term_global @{theory} "[|| ||]";
4.34 +Syntax.read_term_global @{theory} "[||1,2,3||]";
4.35
4.36 "--------------------- NTH ---------------------------------------------------";
4.37 "--------------------- NTH ---------------------------------------------------";