src/HOL/Library/ListVector.thy
changeset 27109 779e73b02cca
parent 26166 dbeab703a28d
child 27368 9f90ac19e32b
     1.1 --- a/src/HOL/Library/ListVector.thy	Tue Jun 10 15:30:59 2008 +0200
     1.2 +++ b/src/HOL/Library/ListVector.thy	Tue Jun 10 15:31:01 2008 +0200
     1.3 @@ -29,19 +29,39 @@
     1.4  "zipwith0 f (x#xs) [] = f x 0 # zipwith0 f xs []" |
     1.5  "zipwith0 f [] (y#ys) = f 0 y # zipwith0 f [] ys"
     1.6  
     1.7 -instance list :: ("{zero,plus}")plus
     1.8 -list_add_def : "op + \<equiv> zipwith0 (op +)" ..
     1.9 +instantiation list :: ("{zero, plus}") plus
    1.10 +begin
    1.11 +
    1.12 +definition
    1.13 +  list_add_def: "op + = zipwith0 (op +)"
    1.14 +
    1.15 +instance ..
    1.16 +
    1.17 +end
    1.18 +
    1.19 +instantiation list :: ("{zero, uminus}") uminus
    1.20 +begin
    1.21  
    1.22 -instance list :: ("{zero,uminus}")uminus
    1.23 -list_uminus_def: "uminus \<equiv> map uminus" ..
    1.24 +definition
    1.25 +  list_uminus_def: "uminus = map uminus"
    1.26 +
    1.27 +instance ..
    1.28 +
    1.29 +end
    1.30  
    1.31 -instance list :: ("{zero,minus}")minus
    1.32 -list_diff_def: "op - \<equiv> zipwith0 (op -)" ..
    1.33 +instantiation list :: ("{zero,minus}") minus
    1.34 +begin
    1.35 +
    1.36 +definition
    1.37 +  list_diff_def: "op - = zipwith0 (op -)"
    1.38 +
    1.39 +instance ..
    1.40 +
    1.41 +end
    1.42  
    1.43  lemma zipwith0_Nil[simp]: "zipwith0 f [] ys = map (f 0) ys"
    1.44  by(induct ys) simp_all
    1.45  
    1.46 -
    1.47  lemma list_add_Nil[simp]: "[] + xs = (xs::'a::monoid_add list)"
    1.48  by (induct xs) (auto simp:list_add_def)
    1.49