1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Wed Aug 25 16:20:07 2010 +0200
1.3 @@ -0,0 +1,204 @@
1.4 +(* use_thy_only"../ProgLang/ListC";
1.5 + use_thy_only"ProgLang/ListC";
1.6 + use_thy"ProgLang/ListC";
1.7 +
1.8 + use_thy_only"ListC";
1.9 + W.N. 8.01
1.10 + attaches identifiers to definition of listfuns,
1.11 + for storing them in list_rls
1.12 +
1.13 +WN.29.4.03:
1.14 +*)
1.15 +
1.16 +theory ListC imports Complex_Main
1.17 +uses ("library.sml")("calcelems.sml")
1.18 +("ProgLang/term.sml")("ProgLang/calculate.sml")
1.19 +("ProgLang/rewrite.sml")
1.20 +begin
1.21 +use "library.sml" (*indent,...*)
1.22 +use "calcelems.sml" (*str_of_type, Thm,...*)
1.23 +use "ProgLang/term.sml" (*num_str,...*)
1.24 +use "ProgLang/calculate.sml" (*???*)
1.25 +use "ProgLang/rewrite.sml" (*?*** At command "end" (line 205../ListC.thy*)
1.26 +
1.27 +text {* 'nat' in List.thy replaced by 'real' *}
1.28 +
1.29 +primrec length_' :: "'a list => real"
1.30 +where
1.31 + LENGTH_NIL: "length_' [] = 0" (*length: 'a list => nat*)
1.32 +| LENGTH_CONS: "length_' (x#xs) = 1 + length_' xs"
1.33 +
1.34 +primrec del :: "['a list, 'a] => 'a list"
1.35 +where
1.36 + del_base: "del [] x = []"
1.37 +| del_rec: "del (y#ys) x = (if x = y then ys else y#(del ys x))"
1.38 +
1.39 +definition
1.40 + list_diff :: "['a list, 'a list] => 'a list" (* as -- bs *)
1.41 + ("(_ --/ _)" [66, 66] 65)
1.42 + where "a -- b == foldl del a b"
1.43 +
1.44 +consts nth_' :: "[real, 'a list] => 'a"
1.45 +axioms
1.46 + (*** more than one non-variable in pattern in "nth_ 1 [x] = x"--*)
1.47 + NTH_NIL: "nth_' 1 (x#xs) = x"
1.48 +(* NTH_CONS: "nth_' n (x#xs) = nth_' (n+ -1) xs" *)
1.49 +
1.50 +(*rewriter does not reach base case ...... ;
1.51 + the condition involves another rule set (erls, eval_binop in Atools):*)
1.52 + NTH_CONS: "1 < n ==> nth_' n (x#xs) = nth_' (n+ - 1) xs"
1.53 +
1.54 +(*primrec from Isabelle/src/HOL/List.thy -- def.twice not allowed*)
1.55 +(*primrec*)
1.56 + hd_thm: "hd(x#xs) = x"
1.57 +(*primrec*)
1.58 + tl_Nil: "tl([]) = []"
1.59 + tl_Cons: "tl(x#xs) = xs"
1.60 +(*primrec*)
1.61 + null_Nil: "null([]) = True"
1.62 + null_Cons: "null(x#xs) = False"
1.63 +(*primrec*)
1.64 + LAST: "last(x#xs) = (if xs=[] then x else last xs)"
1.65 +(*primrec*)
1.66 + butlast_Nil: "butlast [] = []"
1.67 + butlast_Cons: "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)"
1.68 +(*primrec*)
1.69 + mem_Nil: "x mem [] = False"
1.70 + mem_Cons: "x mem (y#ys) = (if y=x then True else x mem ys)"
1.71 +(*primrec-------already named---
1.72 + "set [] = {}"
1.73 + "set (x#xs) = insert x (set xs)"
1.74 + primrec
1.75 + list_all_Nil "list_all P [] = True"
1.76 + list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)"
1.77 +----------------*)
1.78 +(*primrec*)
1.79 + map_Nil: "map f [] = []"
1.80 + map_Cons: "map f (x#xs) = f(x)#map f xs"
1.81 +(*primrec*)
1.82 + append_Nil: "[] @ys = ys"
1.83 + append_Cons: "(x#xs)@ys = x#(xs@ys)"
1.84 +(*primrec*)
1.85 + rev_Nil: "rev([]) = []"
1.86 + rev_Cons: "rev(x#xs) = rev(xs) @ [x]"
1.87 +(*primrec*)
1.88 + filter_Nil: "filter P [] = []"
1.89 + filter_Cons: "filter P (x#xs) =(if P x then x#filter P xs else filter P xs)"
1.90 +(*primrec-------already named---
1.91 + foldl_Nil "foldl f a [] = a"
1.92 + foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs"
1.93 +----------------*)
1.94 +(*primrec*)
1.95 + foldr_Nil: "foldr f [] a = a"
1.96 + foldr_Cons: "foldr f (x#xs) a = f x (foldr f xs a)"
1.97 +(*primrec*)
1.98 + concat_Nil: "concat([]) = []"
1.99 + concat_Cons: "concat(x#xs) = x @ concat(xs)"
1.100 +(*primrec-------already named---
1.101 + drop_Nil "drop n [] = []"
1.102 + drop_Cons "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
1.103 + (* Warning: simpset does not contain this definition but separate theorems
1.104 + for n=0 / n=Suc k*)
1.105 +(*primrec*)
1.106 + take_Nil "take n [] = []"
1.107 + take_Cons "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"
1.108 + (* Warning: simpset does not contain this definition but separate theorems
1.109 + for n=0 / n=Suc k*)
1.110 +(*primrec*)
1.111 + nth_Cons "(x#xs)!n = (case n of 0 => x | (Suc k) => xs!k)"
1.112 + (* Warning: simpset does not contain this definition but separate theorems
1.113 + for n=0 / n=Suc k*)
1.114 +(*primrec*)
1.115 + " [][i:=v] = []"
1.116 + "(x#xs)[i:=v] = (case i of 0 => v # xs
1.117 + | Suc j => x # xs[j:=v])"
1.118 +----------------*)
1.119 +(*primrec*)
1.120 + takeWhile_Nil: "takeWhile P [] = []"
1.121 + takeWhile_Cons:
1.122 + "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])"
1.123 +(*primrec*)
1.124 + dropWhile_Nil: "dropWhile P [] = []"
1.125 + dropWhile_Cons:
1.126 + "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"
1.127 +(*primrec*)
1.128 + zip_Nil: "zip xs [] = []"
1.129 + zip_Cons: "zip xs (y#ys) =(case xs of [] => [] | z#zs =>(z,y)#zip zs ys)"
1.130 + (* Warning: simpset does not contain this definition but separate theorems
1.131 + for xs=[] / xs=z#zs *)
1.132 +(*primrec
1.133 + upt_0 "[i..0(] = []"
1.134 + upt_Suc "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])"
1.135 +*)
1.136 +(*primrec*)
1.137 + distinct_Nil: "distinct [] = True"
1.138 + distinct_Cons: "distinct (x#xs) = (x ~: set xs & distinct xs)"
1.139 +(*primrec*)
1.140 + remdups_Nil: "remdups [] = []"
1.141 + remdups_Cons: "remdups (x#xs) =
1.142 + (if x : set xs then remdups xs else x # remdups xs)"
1.143 +(*primrec-------already named---
1.144 + replicate_0 "replicate 0 x = []"
1.145 + replicate_Suc "replicate (Suc n) x = x # replicate n x"
1.146 +----------------*)
1.147 +
1.148 +(** Lexicographic orderings on lists ...!!!**)
1.149 +
1.150 +ML{* (*the former ListC.ML*)
1.151 +(** rule set for evaluating listexpr in scripts **)
1.152 +val list_rls =
1.153 + Rls{id="list_rls",preconds = [], rew_ord = ("dummy_ord",dummy_ord),
1.154 + erls = e_rls, srls = Erls, calc = [], (*asm_thm=[],*)
1.155 + rules = (*8.01: copied from*)
1.156 + [Thm ("refl", num_str refl), (*'a<>b -> FALSE' by fun eval_equal*)
1.157 + Thm ("o_apply", num_str @{thm o_apply}),
1.158 +
1.159 + Thm ("NTH_CONS",num_str @{thm NTH_CONS}),(*erls for cond. in Atools.ML*)
1.160 + Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
1.161 + Thm ("append_Cons",num_str @{thm append_Cons}),
1.162 + Thm ("append_Nil",num_str @{thm append_Nil}),
1.163 + Thm ("butlast_Cons",num_str @{thm butlast_Cons}),
1.164 + Thm ("butlast_Nil",num_str @{thm butlast_Nil}),
1.165 + Thm ("concat_Cons",num_str @{thm concat_Cons}),
1.166 + Thm ("concat_Nil",num_str @{thm concat_Nil}),
1.167 + Thm ("del_base",num_str @{thm del_base}),
1.168 + Thm ("del_rec",num_str @{thm del_rec}),
1.169 +
1.170 + Thm ("distinct_Cons",num_str @{thm distinct_Cons}),
1.171 + Thm ("distinct_Nil",num_str @{thm distinct_Nil}),
1.172 + Thm ("dropWhile_Cons",num_str @{thm dropWhile_Cons}),
1.173 + Thm ("dropWhile_Nil",num_str @{thm dropWhile_Nil}),
1.174 + Thm ("filter_Cons",num_str @{thm filter_Cons}),
1.175 + Thm ("filter_Nil",num_str @{thm filter_Nil}),
1.176 + Thm ("foldr_Cons",num_str @{thm foldr_Cons}),
1.177 + Thm ("foldr_Nil",num_str @{thm foldr_Nil}),
1.178 + Thm ("hd_thm",num_str @{thm hd_thm}),
1.179 + Thm ("LAST",num_str @{thm LAST}),
1.180 + Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
1.181 + Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
1.182 + Thm ("list_diff_def",num_str @{thm list_diff_def}),
1.183 + Thm ("map_Cons",num_str @{thm map_Cons}),
1.184 + Thm ("map_Nil",num_str @{thm map_Cons}),
1.185 + Thm ("mem_Cons",num_str @{thm mem_Cons}),
1.186 + Thm ("mem_Nil",num_str @{thm mem_Nil}),
1.187 + Thm ("null_Cons",num_str @{thm null_Cons}),
1.188 + Thm ("null_Nil",num_str @{thm null_Nil}),
1.189 + Thm ("remdups_Cons",num_str @{thm remdups_Cons}),
1.190 + Thm ("remdups_Nil",num_str @{thm remdups_Nil}),
1.191 + Thm ("rev_Cons",num_str @{thm rev_Cons}),
1.192 + Thm ("rev_Nil",num_str @{thm rev_Nil}),
1.193 + Thm ("take_Nil",num_str @{thm take_Nil}),
1.194 + Thm ("take_Cons",num_str @{thm take_Cons}),
1.195 + Thm ("tl_Cons",num_str @{thm tl_Cons}),
1.196 + Thm ("tl_Nil",num_str @{thm tl_Nil}),
1.197 + Thm ("zip_Cons",num_str @{thm zip_Cons}),
1.198 + Thm ("zip_Nil",num_str @{thm zip_Nil})
1.199 + ], scr = EmptyScr}:rls;
1.200 +*}
1.201 +
1.202 +ML{*
1.203 +ruleset' := overwritelthy @{theory} (!ruleset',
1.204 + [("list_rls",list_rls)
1.205 + ]);
1.206 +*}
1.207 +end