1.1 --- a/src/Tools/isac/Scripts/ListG.thy Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,204 +0,0 @@
1.4 -(* use_thy_only"../Scripts/ListG";
1.5 - use_thy_only"Scripts/ListG";
1.6 - use_thy"Scripts/ListG";
1.7 -
1.8 - use_thy_only"ListG";
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 ListG imports Complex_Main
1.17 -uses ("library.sml")("calcelems.sml")
1.18 -("Scripts/term_G.sml")("Scripts/calculate.sml")
1.19 -("Scripts/rewrite.sml")
1.20 -begin
1.21 -use "library.sml" (*indent,...*)
1.22 -use "calcelems.sml" (*str_of_type, Thm,...*)
1.23 -use "Scripts/term_G.sml" (*num_str,...*)
1.24 -use "Scripts/calculate.sml" (*???*)
1.25 -use "Scripts/rewrite.sml" (*?*** At command "end" (line 205../ListG.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 ListG.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