Basic.thy

Back to the index of JVM0_ASCII

Basic = Main

Theorems proved in Basic.ML:

Suc_imp_0_less

n = Suc m ==> 0 < n

zip_append

[| length a = length c; length b = length d |] ==> zip (a @ b) (c @ d) = zip a c @ zip b d

length_lupdate

! i. length (xs[i := x]) = length xs

zip_rev

length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)

in_set_replicate

x : set (replicate n v) ==> x = v

in_set_list_update_disj

x : set (xs[i := v]) ==> x = v | x : set xs

zip_list_update

length xs = length ys ==> zip (xs[i := x]) (ys[i := y]) = zip xs ys[i := (x, y)]

nth_Cons

(x # xs) ! i = nat_case x (op ! xs) i

nth_in_set_list

i < length xs ==> xs ! i : set xs

all_nth_imp_set_list

! i. i < length xs --> P (xs ! i) ==> Ball (set xs) P

set_list_all_nth_conv

Ball (set xs) P = (! i. i < length xs --> P (xs ! i))