Up to index of Isabelle/HOL/PI

(* Title: ExtMain.thy Author: Christine Roeckl ExtMain extends Main.thy from Isabelle/HOL with additional results, especially about sets and lists. *) ExtMain = Main

**theorem** *all_conjE:*

[| ALL x. Pa x & Pb x; [| ALL x. Pa x; ALL x. Pb x |] ==> P |] ==> P

**theorem** *inst_fun_eq:*

f = g ==> f x = g x

**theorem** *inst_fun_eq_all:*

f = g ==> ALL x. f x = g x

**theorem** *max_le1:*

max i j <= k ==> i <= k

**theorem** *max_le2:*

max i j <= k ==> j <= k

**theorem** *insert_elem:*

a : A ==> insert a A = A

**theorem** *Inter_insert:*

Inter (insert A AA) = A Int Inter AA

**theorem** *Inter_insert_finite:*

finite A ==> finite (Inter (insert A AA))

**theorem** *Inter_finite_elem:*

[| finite A; A : AA |] ==> finite (Inter AA)

**theorem** *eq_Inter_mono:*

A = B ==> Inter A = Inter B

**theorem** *insert_swap:*

insert a (insert b A) = insert b (insert a A)

**theorem** *subset_insert_mono:*

A <= B ==> insert a A <= insert a B

**theorem** *subset_insert_mono1:*

A <= insert a B ==> insert a A <= insert a B

**theorem** *insert_elem:*

a : A ==> insert a A = A

**theorem** *Un_subset_conj:*

A Un B <= C ==> A <= C & B <= C

**theorem** *set_elem_dist:*

[| a : A; b ~: A |] ==> a ~= b

**theorem** *rtranclD:*

(a, b) : R^* ==> a = b | a ~= b & (a, b) : R^+

**theorem** *set_list_transform:*

finite A ==> EX xs. set xs = A & length xs = card A & nodups xs

**theorem** *nodups_tl:*

[| nodups xs; xs ~= [] |] ==> nodups (tl xs)

**theorem** *lemma:*

nodups (xs @ ys) --> nodups xs

**theorem** *nodups_app1:*

nodups (xs @ ys) ==> nodups xs

**theorem** *lemma:*

nodups (xs @ ys) --> nodups ys

**theorem** *nodups_app2:*

nodups (xs @ ys) ==> nodups ys

**theorem** *lemma:*

nodups (xs @ ys) & x ~: set xs & x ~: set ys --> nodups (xs @ x # ys)

**theorem** *nodups_insert:*

[| nodups (xs @ ys); x ~: set xs; x ~: set ys |] ==> nodups (xs @ x # ys)

**theorem** *lemma:*

nodups (xs @ x # ys) --> nodups (xs @ ys)

**theorem** *nodups_rem:*

nodups (xs @ x # ys) ==> nodups (xs @ ys)

**theorem** *nodups_cons:*

[| nodups xs; x ~: set xs |] ==> nodups (x # xs)

**theorem** *lemma:*

nodups (xs @ ys) --> nodups (ys @ xs)

**theorem** *nodups_swap_app:*

nodups (xs @ ys) ==> nodups (ys @ xs)

**theorem** *lemma:*

nodups (xs @ x # ys) --> x ~: set xs

**theorem** *nodups_set1:*

nodups (xs @ x # ys) ==> x ~: set xs

**theorem** *lemma:*

nodups (xs @ x # ys) --> x ~: set ys

**theorem** *nodups_set2:*

nodups (xs @ x # ys) ==> x ~: set ys

**theorem** *nodups_rearrange:*

nodups (x # xs @ y # ys) ==> nodups (x # y # xs @ ys)

**theorem** *nodups_hd_tl2:*

[| ys ~= []; nodups (x # xs @ ys) |] ==> nodups (x # hd ys # xs @ tl ys)

**theorem** *nodups_cons_app1:*

nodups (x # xs @ ys) ==> nodups xs

**theorem** *nodups_cons_app2:*

nodups (x # xs @ ys) ==> nodups ys

**theorem** *lemma:*

Suc n <= length xs --> xs ~= [] & n <= length (tl xs)

**theorem** *Suc_le_lengthD:*

Suc n <= length xs ==> xs ~= [] & n <= length (tl xs)

**theorem** *Int_empty_ineq_hd:*

[| set ys Int insert a A = {}; ys ~= [] |] ==> a ~= hd ys

**theorem** *Int_empty_Int_tl_empty:*

[| set ys Int insert a A = {}; ys ~= []; nodups ys |] ==> set (tl ys) Int insert (hd ys) A = {}

**theorem** *Int_empty_sort:*

[| set ys Int insert a A = {}; ys ~= []; nodups ys |] ==> set (tl ys) Int insert a (insert (hd ys) A) = {}

**theorem** *Int_empty_not_cont_hd:*

[| set ys Int insert a A = {}; ys ~= []; nodups ys |] ==> hd ys ~: A

**theorem** *Int_empty_not_cont_hd_ins:*

[| set ys Int insert a A = {}; ys ~= []; nodups ys |] ==> hd ys ~: insert a A

**theorem** *lemma:*

a ~: set (map fst xs) & x : set xs --> a ~= fst x

**theorem** *not_in_not_fst:*

a ~: set (map fst xs) ==> ALL x:set xs. a ~= fst x

**theorem** *Int_empty_ineq_mem:*

[| set ys Int insert a A = {}; ys ~= []; nodups ys; b : A |] ==> hd ys ~= b