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