1.1 --- a/src/Tools/isac/ProgLang/ListC.thy Mon Jul 25 08:32:32 2011 +0200
1.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Tue Jul 26 13:27:59 2011 +0200
1.3 @@ -33,35 +33,36 @@
1.4 where "a -- b == foldl del a b"
1.5
1.6 consts NTH :: "[real, 'a list] => 'a"
1.7 -axioms
1.8 +
1.9 +axiomatization where
1.10 (*** more than one non-variable in pattern in "nth_ 1 [x] = x"--*)
1.11 - NTH_NIL: "NTH 1 (x#xs) = x"
1.12 + NTH_NIL: "NTH 1 (x#xs) = x" and
1.13 (* NTH_CONS: "NTH n (x#xs) = NTH (n+ -1) xs" *)
1.14
1.15 (*rewriter does not reach base case ...... ;
1.16 the condition involves another rule set (erls, eval_binop in Atools):*)
1.17 - NTH_CONS: "1 < n ==> NTH n (x#xs) = NTH (n+ - 1) xs"
1.18 + NTH_CONS: "1 < n ==> NTH n (x#xs) = NTH (n+ - 1) xs" and
1.19
1.20 (*primrec from Isabelle/src/HOL/List.thy -- def.twice not allowed*)
1.21 (*primrec*)
1.22 - hd_thm: "hd(x#xs) = x"
1.23 + hd_thm: "hd(x#xs) = x" and
1.24 (*primrec*)
1.25 - tl_Nil: "tl([]) = []"
1.26 - tl_Cons: "tl(x#xs) = xs"
1.27 + tl_Nil: "tl([]) = []" and
1.28 + tl_Cons: "tl(x#xs) = xs" and
1.29 (*primrec*)
1.30 - null_Nil: "null([]) = True"
1.31 - null_Cons: "null(x#xs) = False"
1.32 + null_Nil: "null([]) = True" and
1.33 + null_Cons: "null(x#xs) = False" and
1.34 (*primrec*)
1.35 - LAST: "last(x#xs) = (if xs=[] then x else last xs)"
1.36 + LAST: "last(x#xs) = (if xs=[] then x else last xs)" and
1.37 (*primrec*)
1.38 - butlast_Nil: "butlast [] = []"
1.39 - butlast_Cons: "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)"
1.40 + butlast_Nil: "butlast [] = []" and
1.41 + butlast_Cons: "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)" and
1.42 (*primrec
1.43 mem_Nil: "x mem [] = False"
1.44 mem_Cons: "x mem (y#ys) = (if y=x then True else x mem ys)"
1.45 *)
1.46 - mem_Nil: "x : set [] = False"
1.47 - mem_Cons: "x : set (y#ys) = (if y=x then True else x : set ys)"
1.48 + mem_Nil: "x : set [] = False" and
1.49 + mem_Cons: "x : set (y#ys) = (if y=x then True else x : set ys)" and
1.50 (*primrec-------already named---
1.51 "set [] = {}"
1.52 "set (x#xs) = insert x (set xs)"
1.53 @@ -70,27 +71,27 @@
1.54 list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)"
1.55 ----------------*)
1.56 (*primrec*)
1.57 - map_Nil: "map f [] = []"
1.58 - map_Cons: "map f (x#xs) = f(x)#map f xs"
1.59 + map_Nil: "map f [] = []" and
1.60 + map_Cons: "map f (x#xs) = f(x)#map f xs" and
1.61 (*primrec*)
1.62 - append_Nil: "[] @ys = ys"
1.63 - append_Cons: "(x#xs)@ys = x#(xs@ys)"
1.64 + append_Nil: "[] @ys = ys" and
1.65 + append_Cons: "(x#xs)@ys = x#(xs@ys)" and
1.66 (*primrec*)
1.67 - rev_Nil: "rev([]) = []"
1.68 - rev_Cons: "rev(x#xs) = rev(xs) @ [x]"
1.69 + rev_Nil: "rev([]) = []" and
1.70 + rev_Cons: "rev(x#xs) = rev(xs) @ [x]" and
1.71 (*primrec*)
1.72 - filter_Nil: "filter P [] = []"
1.73 - filter_Cons: "filter P (x#xs) =(if P x then x#filter P xs else filter P xs)"
1.74 + filter_Nil: "filter P [] = []" and
1.75 + filter_Cons: "filter P (x#xs) =(if P x then x#filter P xs else filter P xs)" and
1.76 (*primrec-------already named---
1.77 foldl_Nil "foldl f a [] = a"
1.78 foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs"
1.79 ----------------*)
1.80 (*primrec*)
1.81 - foldr_Nil: "foldr f [] a = a"
1.82 - foldr_Cons: "foldr f (x#xs) a = f x (foldr f xs a)"
1.83 + foldr_Nil: "foldr f [] a = a" and
1.84 + foldr_Cons: "foldr f (x#xs) a = f x (foldr f xs a)" and
1.85 (*primrec*)
1.86 - concat_Nil: "concat([]) = []"
1.87 - concat_Cons: "concat(x#xs) = x @ concat(xs)"
1.88 + concat_Nil: "concat([]) = []" and
1.89 + concat_Cons: "concat(x#xs) = x @ concat(xs)" and
1.90 (*primrec-------already named---
1.91 drop_Nil "drop n [] = []"
1.92 drop_Cons "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
1.93 @@ -111,16 +112,16 @@
1.94 | Suc j => x # xs[j:=v])"
1.95 ----------------*)
1.96 (*primrec*)
1.97 - takeWhile_Nil: "takeWhile P [] = []"
1.98 + takeWhile_Nil: "takeWhile P [] = []" and
1.99 takeWhile_Cons:
1.100 - "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])"
1.101 + "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])" and
1.102 (*primrec*)
1.103 - dropWhile_Nil: "dropWhile P [] = []"
1.104 + dropWhile_Nil: "dropWhile P [] = []" and
1.105 dropWhile_Cons:
1.106 - "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"
1.107 + "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)" and
1.108 (*primrec*)
1.109 - zip_Nil: "zip xs [] = []"
1.110 - zip_Cons: "zip xs (y#ys) =(case xs of [] => [] | z#zs =>(z,y)#zip zs ys)"
1.111 + zip_Nil: "zip xs [] = []" and
1.112 + zip_Cons: "zip xs (y#ys) =(case xs of [] => [] | z#zs =>(z,y)#zip zs ys)" and
1.113 (* Warning: simpset does not contain this definition but separate theorems
1.114 for xs=[] / xs=z#zs *)
1.115 (*primrec
1.116 @@ -128,12 +129,12 @@
1.117 upt_Suc "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])"
1.118 *)
1.119 (*primrec*)
1.120 - distinct_Nil: "distinct [] = True"
1.121 - distinct_Cons: "distinct (x#xs) = (x ~: set xs & distinct xs)"
1.122 + distinct_Nil: "distinct [] = True" and
1.123 + distinct_Cons: "distinct (x#xs) = (x ~: set xs & distinct xs)" and
1.124 (*primrec*)
1.125 - remdups_Nil: "remdups [] = []"
1.126 - remdups_Cons: "remdups (x#xs) =
1.127 - (if x : set xs then remdups xs else x # remdups xs)"
1.128 + remdups_Nil: "remdups [] = []" and
1.129 + remdups_Cons: "remdups (x#xs) =
1.130 + (if x : set xs then remdups xs else x # remdups xs)"
1.131 (*primrec-------already named---
1.132 replicate_0 "replicate 0 x = []"
1.133 replicate_Suc "replicate (Suc n) x = x # replicate n x"