Theory ExtMain

Up to index of Isabelle/HOL/PI

theory ExtMain = Main
files [ExtMain.ML]:
(* 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