1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Sun Sep 22 14:47:35 2019 +0200
1.3 @@ -0,0 +1,183 @@
1.4 +(* Title: functions on lists for Programs
1.5 + Author: Walther Neuper 0108
1.6 + (c) due to copyright terms
1.7 +*)
1.8 +
1.9 +theory ListC imports "~~/src/Tools/isac/CalcElements/CalcElements"
1.10 +
1.11 +begin
1.12 +
1.13 +text \<open>Abstract:
1.14 + There are examples in the Knowledge, which demonstrate list processing, e.g. InsSort.thy.
1.15 +
1.16 + Lists in example calculations must have a different type for list processing in Isac programs.
1.17 + Presently the lists in examples have a new type xlist with the unfamiliar list
1.18 + notation "{||a, b, c||}". One could expect math-authors to use such unfamiliar notation
1.19 + and expose students to familiar notation in calculations, and not vice versa as done presently.
1.20 +
1.21 + Thus this theory resides in ProgLang so far.
1.22 +\<close>
1.23 +
1.24 +subsection \<open>General constants\<close>
1.25 +consts
1.26 + EmptyList :: "bool list"
1.27 + UniversalList :: "bool list"
1.28 +
1.29 +ML \<open>
1.30 +\<close> ML \<open>
1.31 +val UniversalList = (Thm.term_of o the o (TermC.parse @{theory})) "UniversalList";
1.32 +val EmptyList = (Thm.term_of o the o (TermC.parse @{theory})) "[]::bool list";
1.33 +\<close> ML \<open>
1.34 +\<close>
1.35 +
1.36 +subsection \<open>Type 'xlist' for Lucas-Interpretation | for InsSort.thy\<close>
1.37 +(* cp fom ~~/src/HOL/List.thy
1.38 + TODO: ask for shorter deliminters in xlist *)
1.39 +datatype 'a xlist =
1.40 + XNil ("{|| ||}")
1.41 + | XCons (xhd: 'a) (xtl: "'a xlist") (infixr "@#" 65)
1.42 +
1.43 +syntax
1.44 + \<comment> \<open>list Enumeration\<close>
1.45 + "_xlist" :: "args => 'a xlist" ("{|| (_) ||}")
1.46 +
1.47 +translations
1.48 + "{||x, xs||}" == "x@#{||xs||}"
1.49 + "{||x||}" == "x@#{|| ||}"
1.50 +
1.51 +term "{|| ||}"
1.52 +term "{||1,2,3||}"
1.53 +
1.54 +subsection \<open>Functions for 'xlist'\<close>
1.55 +(* TODO:
1.56 +(1) revise, if definition of identifiers like LENGTH_NIL are still required.
1.57 +(2) switch the role of 'xlist' and 'list' in the functions below, in particular for
1.58 + 'foldr', 'foldr_Nil', 'foldr_Cons' and 'xfoldr', 'xfoldr_Nil', 'xfoldr_Cons'.
1.59 + For transition phase just outcomment InsSort.thy and inssort.sml.
1.60 +*)
1.61 +
1.62 +primrec xfoldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a xlist \<Rightarrow> 'b \<Rightarrow> 'b" where
1.63 +xfoldr_Nil: "xfoldr f {|| ||} = id" |
1.64 +xfoldr_Cons: "xfoldr f (x @# xs) = f x \<circ> xfoldr f xs"
1.65 +
1.66 +primrec LENGTH :: "'a list => real"
1.67 +where
1.68 +LENGTH_NIL: "LENGTH [] = 0" |
1.69 +LENGTH_CONS: "LENGTH (x#xs) = 1 + LENGTH xs"
1.70 +
1.71 +subsection \<open>Functions for 'list'\<close>
1.72 +
1.73 +consts NTH :: "[real, 'a list] => 'a"
1.74 +axiomatization where
1.75 +NTH_NIL: "NTH 1 (x # xs) = x" and
1.76 +NTH_CONS: (*NO primrec, fun ..*)"1 < n ==> NTH n (x # xs) = NTH (n + -1) xs"
1.77 +
1.78 +(* redefine together with identifiers (still) required for KEStore ..*)
1.79 +axiomatization where
1.80 +hd_thm: "hd (x # xs) = x"
1.81 +
1.82 +axiomatization where
1.83 +tl_Nil: "tl [] = []" and
1.84 +tl_Cons: "tl (x # xs) = xs"
1.85 +
1.86 +axiomatization where
1.87 +LAST: "last (x # xs) = (if xs = [] then x else last xs)"
1.88 +
1.89 +axiomatization where
1.90 +butlast_Nil: "butlast [] = []" and
1.91 +butlast_Cons: "butlast (x # xs) = (if xs = [] then [] else x # butlast xs)"
1.92 +
1.93 +axiomatization where
1.94 +map_Nil:"map f [] = []" and
1.95 +map_Cons: "map f (x # xs) = f x # map f xs"
1.96 +
1.97 +axiomatization where
1.98 +rev_Nil: "rev [] = []" and
1.99 +rev_Cons: "rev (x # xs) = rev xs @ [x]"
1.100 +
1.101 +axiomatization where
1.102 +filter_Nil: "filter P [] = []" and
1.103 +filter_Cons: "filter P (x # xs) = (if P x then x # filter P xs else filter P xs)"
1.104 +
1.105 +axiomatization where
1.106 +concat_Nil: "concat [] = []" and
1.107 +concat_Cons: "concat (x # xs) = x @ concat xs"
1.108 +
1.109 +axiomatization where
1.110 +takeWhile_Nil: "takeWhile P [] = []" and
1.111 +takeWhile_Cons: "takeWhile P (x # xs) = (if P x then x # takeWhile P xs else [])"
1.112 +
1.113 +axiomatization where
1.114 +dropWhile_Nil: "dropWhile P [] = []" and
1.115 +dropWhile_Cons: "dropWhile P (x # xs) = (if P x then dropWhile P xs else x#xs)"
1.116 +
1.117 +axiomatization where
1.118 +zip_Nil: "zip xs [] = []" and
1.119 +zip_Cons: "zip xs (y # ys) = (case xs of [] => [] | z # zs => (z,y) # zip zs ys)"
1.120 +
1.121 +axiomatization where
1.122 +distinct_Nil: "distinct [] = True" and
1.123 +distinct_Cons: "distinct (x # xs) = (x ~: set xs & distinct xs)"
1.124 +
1.125 +axiomatization where
1.126 +remdups_Nil: "remdups [] = []" and
1.127 +remdups_Cons: "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"
1.128 +
1.129 +consts lastI :: "'a list \<Rightarrow> 'a"
1.130 +axiomatization where
1.131 +last_thmI: "lastI (x#xs) = (if xs = [] then x else lastI xs)"
1.132 +
1.133 +subsection \<open>rule set for evaluating Porg_Expr, will be extended in several thys\<close>
1.134 +ML \<open>
1.135 +\<close> ML \<open>
1.136 +val list_rls =
1.137 + Rule.Rls {id = "list_rls", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
1.138 + erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [],
1.139 + rules = [Rule.Thm ("refl", TermC.num_str @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*)
1.140 + Rule.Thm ("o_apply", TermC.num_str @{thm o_apply}),
1.141 +
1.142 + Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),(*erls for cond. in Atools.ML*)
1.143 + Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
1.144 + Rule.Thm ("append_Cons",TermC.num_str @{thm append_Cons}),
1.145 + Rule.Thm ("append_Nil",TermC.num_str @{thm append_Nil}),
1.146 +(* Thm ("butlast_Cons",num_str @{thm butlast_Cons}),
1.147 + Thm ("butlast_Nil",num_str @{thm butlast_Nil}),*)
1.148 + Rule.Thm ("concat_Cons",TermC.num_str @{thm concat_Cons}),
1.149 + Rule.Thm ("concat_Nil",TermC.num_str @{thm concat_Nil}),
1.150 +(* Rule.Thm ("del_base",num_str @{thm del_base}),
1.151 + Rule.Thm ("del_rec",num_str @{thm del_rec}), *)
1.152 +
1.153 + Rule.Thm ("distinct_Cons",TermC.num_str @{thm distinct_Cons}),
1.154 + Rule.Thm ("distinct_Nil",TermC.num_str @{thm distinct_Nil}),
1.155 + Rule.Thm ("dropWhile_Cons",TermC.num_str @{thm dropWhile_Cons}),
1.156 + Rule.Thm ("dropWhile_Nil",TermC.num_str @{thm dropWhile_Nil}),
1.157 + Rule.Thm ("filter_Cons",TermC.num_str @{thm filter_Cons}),
1.158 + Rule.Thm ("filter_Nil",TermC.num_str @{thm filter_Nil}),
1.159 + Rule.Thm ("foldr_Cons",TermC.num_str @{thm foldr_Cons}),
1.160 + Rule.Thm ("foldr_Nil",TermC.num_str @{thm foldr_Nil}),
1.161 + Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
1.162 + Rule.Thm ("LAST",TermC.num_str @{thm LAST}),
1.163 + Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
1.164 + Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
1.165 +(* Rule.Thm ("list_diff_def",num_str @{thm list_diff_def}),*)
1.166 + Rule.Thm ("map_Cons",TermC.num_str @{thm map_Cons}),
1.167 + Rule.Thm ("map_Nil",TermC.num_str @{thm map_Cons}),
1.168 +(* Rule.Thm ("mem_Cons",TermC.num_str @{thm mem_Cons}),
1.169 + Rule.Thm ("mem_Nil",TermC.num_str @{thm mem_Nil}), *)
1.170 +(* Rule.Thm ("null_Cons",TermC.num_str @{thm null_Cons}),
1.171 + Rule.Thm ("null_Nil",TermC.num_str @{thm null_Nil}),*)
1.172 + Rule.Thm ("remdups_Cons",TermC.num_str @{thm remdups_Cons}),
1.173 + Rule.Thm ("remdups_Nil",TermC.num_str @{thm remdups_Nil}),
1.174 + Rule.Thm ("rev_Cons",TermC.num_str @{thm rev_Cons}),
1.175 + Rule.Thm ("rev_Nil",TermC.num_str @{thm rev_Nil}),
1.176 + Rule.Thm ("take_Nil",TermC.num_str @{thm take_Nil}),
1.177 + Rule.Thm ("take_Cons",TermC.num_str @{thm take_Cons}),
1.178 + Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.179 + Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil}),
1.180 + Rule.Thm ("zip_Cons",TermC.num_str @{thm zip_Cons}),
1.181 + Rule.Thm ("zip_Nil",TermC.num_str @{thm zip_Nil})],
1.182 + scr = Rule.EmptyScr}: Rule.rls;
1.183 +\<close>
1.184 +setup \<open>KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))]\<close>
1.185 +
1.186 +end