1.1 --- a/src/Tools/isac/ProgLang/ListC.thy Fri Oct 18 14:36:51 2013 +0200
1.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Mon Oct 21 09:03:50 2013 +0200
1.3 @@ -11,130 +11,82 @@
1.4 ML_file "~~/src/Tools/isac/ProgLang/calculate.sml"
1.5 ML_file "~~/src/Tools/isac/ProgLang/rewrite.sml"
1.6
1.7 -text {* 'nat' in List.thy replaced by 'real' *}
1.8 +text {*
1.9 + This file gives names to equations of function definitions,
1.10 + which are required for Lucas-Interpretation (by Isac's rewriter) of
1.11 + Isac's programming language. This language preceeded the function package
1.12 + in 2002. For naming "axiomatization" is used for reasons of uniformity
1.13 + with the other replacements for "axioms".
1.14 + Another reminiscence from Isabelle2002 are Isac-specific numerals,
1.15 + introduced in order to have floating point numerals at a time,
1.16 + when Isabelle did not consider that requirement. For the sake of uniformity
1.17 + 'nat' from List.thy is replaced by 'real'.
1.18 +
1.19 + TODO: shift name-declarations to HOL/List.thy, adopt new names from there
1.20 + and remove this ListC.thy.
1.21 + Note: *one* "axiomatization" over all equations caused strange "'a list list"
1.22 + types.
1.23 +*}
1.24
1.25 primrec LENGTH :: "'a list => real"
1.26 where
1.27 - LENGTH_NIL: "LENGTH [] = 0" (*length: 'a list => nat*)
1.28 -| LENGTH_CONS: "LENGTH (x#xs) = 1 + LENGTH xs"
1.29 +LENGTH_NIL: "LENGTH [] = 0" |
1.30 +LENGTH_CONS: "LENGTH (x#xs) = 1 + LENGTH xs"
1.31
1.32 -primrec del :: "['a list, 'a] => 'a list"
1.33 -where
1.34 - del_base: "del [] x = []"
1.35 -| del_rec: "del (y#ys) x = (if x = y then ys else y#(del ys x))"
1.36 +consts NTH :: "[real, 'a list] => 'a"
1.37 +axiomatization where
1.38 +NTH_NIL: "NTH 1 (x # xs) = x" and
1.39 +NTH_CONS: (*NO primrec, fun ..*)"1 < n ==> NTH n (x # xs) = NTH (n + -1) xs"
1.40
1.41 -definition
1.42 - list_diff :: "['a list, 'a list] => 'a list" (* as -- bs *)
1.43 - ("(_ --/ _)" [66, 66] 65)
1.44 - where "a -- b == foldl del a b"
1.45 -
1.46 -consts NTH :: "[real, 'a list] => 'a"
1.47 +axiomatization where
1.48 +hd_thm: "hd (x # xs) = x"
1.49
1.50 -axioms(*axiomatization where*)
1.51 - (*** more than one non-variable in pattern in "nth_ 1 [x] = x"--*)
1.52 - NTH_NIL: "NTH 1 (x#xs) = x" (*and*)
1.53 -(* NTH_CONS: "NTH n (x#xs) = NTH (n+ -1) xs" *)
1.54 +axiomatization where
1.55 +tl_Nil: "tl [] = []" and
1.56 +tl_Cons: "tl (x # xs) = xs"
1.57
1.58 -(*rewriter does not reach base case ...... ;
1.59 - the condition involves another rule set (erls, eval_binop in Atools):*)
1.60 - NTH_CONS: "1 < n ==> NTH n (x#xs) = NTH (n+ - 1) xs" (*and*)
1.61 +axiomatization where
1.62 +LAST: "last (x # xs) = (if xs = [] then x else last xs)"
1.63
1.64 -(*primrec from Isabelle/src/HOL/List.thy -- def.twice not allowed*)
1.65 -(*primrec*)
1.66 - hd_thm: "hd(x#xs) = x" (*and*)
1.67 -(*primrec*)
1.68 - tl_Nil: "tl([]) = []" (*and*)
1.69 - tl_Cons: "tl(x#xs) = xs" (*and*)
1.70 -(*primrec*)
1.71 - null_Nil: "null([]) = True" (*and*)
1.72 - null_Cons: "null(x#xs) = False" (*and*)
1.73 -(*primrec*)
1.74 - LAST: "last(x#xs) = (if xs=[] then x else last xs)" (*and*)
1.75 -(*primrec*)
1.76 - butlast_Nil: "butlast [] = []" (*and*)
1.77 - butlast_Cons: "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)" (*and*)
1.78 -(*primrec
1.79 - mem_Nil: "x mem [] = False"
1.80 - mem_Cons: "x mem (y#ys) = (if y=x then True else x mem ys)"
1.81 -*)
1.82 - mem_Nil: "x : set [] = False" (*and*)
1.83 - mem_Cons: "x : set (y#ys) = (if y=x then True else x : set ys)" (*and*)
1.84 -(*primrec-------already named---
1.85 - "set [] = {}"
1.86 - "set (x#xs) = insert x (set xs)"
1.87 - primrec
1.88 - list_all_Nil "list_all P [] = True"
1.89 - list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)"
1.90 -----------------*)
1.91 -(*primrec*)
1.92 - map_Nil: "map f [] = []" (*and*)
1.93 - map_Cons: "map f (x#xs) = f(x)#map f xs" (*and*)
1.94 -(*primrec*)
1.95 - append_Nil: "[] @ys = ys" (*and*)
1.96 - append_Cons: "(x#xs)@ys = x#(xs@ys)" (*and*)
1.97 -(*primrec*)
1.98 - rev_Nil: "rev([]) = []" (*and*)
1.99 - rev_Cons: "rev(x#xs) = rev(xs) @ [x]" (*and*)
1.100 -(*primrec*)
1.101 - filter_Nil: "filter P [] = []" (*and*)
1.102 - filter_Cons: "filter P (x#xs) =(if P x then x#filter P xs else filter P xs)" (*and*)
1.103 -(*primrec-------already named---
1.104 - foldl_Nil "foldl f a [] = a"
1.105 - foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs"
1.106 -----------------*)
1.107 -(*primrec*)
1.108 - foldr_Nil: "foldr f [] a = a" (*and*)
1.109 - foldr_Cons: "foldr f (x#xs) a = f x (foldr f xs a)" (*and*)
1.110 -(*primrec*)
1.111 - concat_Nil: "concat([]) = []" (*and*)
1.112 - concat_Cons: "concat(x#xs) = x @ concat(xs)" (*and*)
1.113 -(*primrec-------already named---
1.114 - drop_Nil "drop n [] = []"
1.115 - drop_Cons "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
1.116 - (* Warning: simpset does not contain this definition but separate theorems
1.117 - for n=0 / n=Suc k*)
1.118 -(*primrec*)
1.119 - take_Nil "take n [] = []"
1.120 - take_Cons "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"
1.121 - (* Warning: simpset does not contain this definition but separate theorems
1.122 - for n=0 / n=Suc k*)
1.123 -(*primrec*)
1.124 - nth_Cons "(x#xs)!n = (case n of 0 => x | (Suc k) => xs!k)"
1.125 - (* Warning: simpset does not contain this definition but separate theorems
1.126 - for n=0 / n=Suc k*)
1.127 -(*primrec*)
1.128 - " [][i:=v] = []"
1.129 - "(x#xs)[i:=v] = (case i of 0 => v # xs
1.130 - | Suc j => x # xs[j:=v])"
1.131 -----------------*)
1.132 -(*primrec*)
1.133 - takeWhile_Nil: "takeWhile P [] = []" (*and*)
1.134 - takeWhile_Cons:
1.135 - "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])" (*and*)
1.136 -(*primrec*)
1.137 - dropWhile_Nil: "dropWhile P [] = []" (*and*)
1.138 - dropWhile_Cons:
1.139 - "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)" (*and*)
1.140 -(*primrec*)
1.141 - zip_Nil: "zip xs [] = []" (*and*)
1.142 - zip_Cons: "zip xs (y#ys) =(case xs of [] => [] | z#zs =>(z,y)#zip zs ys)" (*and*)
1.143 - (* Warning: simpset does not contain this definition but separate theorems
1.144 - for xs=[] / xs=z#zs *)
1.145 -(*primrec
1.146 - upt_0 "[i..0(] = []"
1.147 - upt_Suc "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])"
1.148 -*)
1.149 -(*primrec*)
1.150 - distinct_Nil: "distinct [] = True" (*and*)
1.151 - distinct_Cons: "distinct (x#xs) = (x ~: set xs & distinct xs)" (*and*)
1.152 -(*primrec*)
1.153 - remdups_Nil: "remdups [] = []" (*and*)
1.154 - remdups_Cons: "remdups (x#xs) =
1.155 - (if x : set xs then remdups xs else x # remdups xs)"
1.156 -(*primrec-------already named---
1.157 - replicate_0 "replicate 0 x = []"
1.158 - replicate_Suc "replicate (Suc n) x = x # replicate n x"
1.159 -----------------*)
1.160 +axiomatization where
1.161 +butlast_Nil: "butlast [] = []" and
1.162 +butlast_Cons: "butlast (x # xs) = (if xs = [] then [] else x # butlast xs)"
1.163 +
1.164 +axiomatization where
1.165 +map_Nil:"map f [] = []" and
1.166 +map_Cons: "map f (x # xs) = f x # map f xs"
1.167 +
1.168 +axiomatization where
1.169 +rev_Nil: "rev [] = []" and
1.170 +rev_Cons: "rev (x # xs) = rev xs @ [x]"
1.171 +
1.172 +axiomatization where
1.173 +filter_Nil: "filter P [] = []" and
1.174 +filter_Cons: "filter P (x # xs) = (if P x then x # filter P xs else filter P xs)"
1.175 +
1.176 +axiomatization where
1.177 +concat_Nil: "concat [] = []" and
1.178 +concat_Cons: "concat (x # xs) = x @ concat xs"
1.179 +
1.180 +axiomatization where
1.181 +takeWhile_Nil: "takeWhile P [] = []" and
1.182 +takeWhile_Cons: "takeWhile P (x # xs) = (if P x then x # takeWhile P xs else [])"
1.183 +
1.184 +axiomatization where
1.185 +dropWhile_Nil: "dropWhile P [] = []" and
1.186 +dropWhile_Cons: "dropWhile P (x # xs) = (if P x then dropWhile P xs else x#xs)"
1.187 +
1.188 +axiomatization where
1.189 +zip_Nil: "zip xs [] = []" and
1.190 +zip_Cons: "zip xs (y # ys) = (case xs of [] => [] | z # zs => (z,y) # zip zs ys)"
1.191 +
1.192 +axiomatization where
1.193 +distinct_Nil: "distinct [] = True" and
1.194 +distinct_Cons: "distinct (x # xs) = (x ~: set xs & distinct xs)"
1.195 +
1.196 +axiomatization where
1.197 +remdups_Nil: "remdups [] = []" and
1.198 +remdups_Cons: "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"
1.199
1.200 (** Lexicographic orderings on lists ...!!!**)
1.201
1.202 @@ -150,12 +102,12 @@
1.203 Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
1.204 Thm ("append_Cons",num_str @{thm append_Cons}),
1.205 Thm ("append_Nil",num_str @{thm append_Nil}),
1.206 - Thm ("butlast_Cons",num_str @{thm butlast_Cons}),
1.207 - Thm ("butlast_Nil",num_str @{thm butlast_Nil}),
1.208 +(* Thm ("butlast_Cons",num_str @{thm butlast_Cons}),
1.209 + Thm ("butlast_Nil",num_str @{thm butlast_Nil}),*)
1.210 Thm ("concat_Cons",num_str @{thm concat_Cons}),
1.211 Thm ("concat_Nil",num_str @{thm concat_Nil}),
1.212 - Thm ("del_base",num_str @{thm del_base}),
1.213 - Thm ("del_rec",num_str @{thm del_rec}),
1.214 +(* Thm ("del_base",num_str @{thm del_base}),
1.215 + Thm ("del_rec",num_str @{thm del_rec}), *)
1.216
1.217 Thm ("distinct_Cons",num_str @{thm distinct_Cons}),
1.218 Thm ("distinct_Nil",num_str @{thm distinct_Nil}),
1.219 @@ -169,13 +121,13 @@
1.220 Thm ("LAST",num_str @{thm LAST}),
1.221 Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
1.222 Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
1.223 - Thm ("list_diff_def",num_str @{thm list_diff_def}),
1.224 +(* Thm ("list_diff_def",num_str @{thm list_diff_def}),*)
1.225 Thm ("map_Cons",num_str @{thm map_Cons}),
1.226 Thm ("map_Nil",num_str @{thm map_Cons}),
1.227 - Thm ("mem_Cons",num_str @{thm mem_Cons}),
1.228 - Thm ("mem_Nil",num_str @{thm mem_Nil}),
1.229 - Thm ("null_Cons",num_str @{thm null_Cons}),
1.230 - Thm ("null_Nil",num_str @{thm null_Nil}),
1.231 +(* Thm ("mem_Cons",num_str @{thm mem_Cons}),
1.232 + Thm ("mem_Nil",num_str @{thm mem_Nil}), *)
1.233 +(* Thm ("null_Cons",num_str @{thm null_Cons}),
1.234 + Thm ("null_Nil",num_str @{thm null_Nil}),*)
1.235 Thm ("remdups_Cons",num_str @{thm remdups_Cons}),
1.236 Thm ("remdups_Nil",num_str @{thm remdups_Nil}),
1.237 Thm ("rev_Cons",num_str @{thm rev_Cons}),