Theory Infra_set

           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2004         |
            |               November 2004               |
            |                   June 2005  (modified)   |
            |                   July 2005  (modified)   |
            |                                           |
            |        CSP-Prover on Isabelle2005         |
            |                October 2005  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory Infra_set
imports Infra_list
begin

(*****************************************************
               Small lemmas for Set
 *****************************************************)

lemma notin_subset: "[| S <= T ; a ~: T |] ==> a ~: S"
by (auto)

lemma notin_set_butlast: "a ~: set s ==> a ~: set (butlast s)"
apply (rule notin_subset[of _ "set s"])
by (simp_all add: butlast_subseteq)

lemma in_set_butlast: "a : set (butlast s) ==> a : set s"
apply (erule contrapos_pp)
by (simp add: notin_set_butlast)

lemma in_image_set: "x : f ` X = (EX y. x = f y & y:X)"
by (auto)

lemma inj_image_diff_dist: "inj f ==> f ` (A - B) = f ` A - f ` B"
by (auto simp add: inj_on_def)

lemma inj_image_Int_dist: "inj f ==> f ` (A Int B) = f ` A Int f ` B"
by (auto simp add: inj_on_def)

lemma subsetE: "[| A <= B ; [| ALL x:A. x:B |] ==> R |] ==> R"
by (auto)

lemma Un_sym: "X Un Y = Y Un X"
by (auto)

lemma Int_subset_eq:"A <= B ==> A Int B = A"
by (auto)

lemma Int_insert_eq: "A Int insert x A = A"
by (auto)

lemma in_Union_EX: "x : Union Xs = (EX X. x:X & X:Xs)"
by (auto)

lemma subset_or_not_subset:
 "ALL A B. ((A::'a set) <= B) | (B <= A) | (EX a b. a : A & a ~: B & b ~: A & b : B)"
by (auto)

lemma not_subset_iff:
  "(~ (A::'a set) < B) = ((B <= A) | (EX a b. a : A & a ~: B & b ~: A & b : B))"
by (auto)

lemma Union_snd_Un: 
  "Union (snd ` f ` (I1 Un I2))=
   Union (snd ` f ` I1) Un Union (snd ` f ` I2)"
by (auto)

lemma Union_snd_set_Un: 
  "Union (snd ` (set s Un set t)) = Union (snd ` set s) Un Union (snd ` set t)"
by (auto)

lemma neq_Set_EX1: "EX a:A. a~:B ==> A ~= B"
by (auto)

lemma neq_Set_EX2: "EX a:A. a~:B ==> B ~= A"
by (auto)

(*****************************
          finite set
 *****************************)

lemma Union_index_fun:
   "ALL i:I1. PXf2 (f i) = PXf1 i
    ==> Union (snd ` PXf2 ` f ` I1) = Union (snd ` PXf1 ` I1)"
apply (rule)
apply (rule, simp)
apply (rule, simp)
done

lemma finite_pair_set1:
   "[| finite F1 ;ALL j:F1. finite (F2 j) |]
       ==> finite {(i, j)|i j. j : F1 & i : F2 j}"
(*
apply (induct set: Finites)     Isabelle 2005
*)
apply (induct set: finite)     (* Isabelle 2007 *)
apply (simp_all)
apply (subgoal_tac 
   "{(i, j). (j = x | j : F) & i : F2 j}
  = (%i. (i, x)) ` (F2 x) Un {(i, j). j : F & i : F2 j}")
apply (simp)
by (auto)

lemmas finite_pair_set2 = finite_pair_set1[simplified]

lemmas finite_pair_set = finite_pair_set1 finite_pair_set2

(* finite set --> EX max *)

lemma nonempty_finite_set_exists_max_fun_subset:
  "[| finite I ; I ~= {} |]
    ==> EX J. J <= I & J ~= {} & (ALL j:J. ALL i:I. ~((f::'a => 'b::order) j < f i))"
(*
apply (induct set: Finites)     Isabelle 2005
*)
apply (induct set: finite)     (* Isabelle 2007 *)
apply (simp_all)

(* {} *)
 apply (case_tac "F = {}")
 apply (simp_all)

(* {x} *)
 apply (rule_tac x="{x}" in exI)
 apply (simp)

(* step case *)
 apply (elim conjE exE)
 apply (case_tac "EX j:J. (f j < f x)")
 apply (rule_tac x="(J - {j. f j < f x}) Un {x}" in exI)
 apply (simp)
 apply (rule conjI)
 apply (fast)
 apply (intro ballI)
 apply (elim bexE)
 apply (drule_tac x="j" in bspec, simp)
 apply (drule_tac x="i" in bspec, simp)
 apply (case_tac "~ f x < f i", simp)
 apply (simp)
 apply (rotate_tac -2)
 apply (erule contrapos_np)
 apply (force)

 apply (rule_tac x="J" in exI)
 apply (fast)
done

lemma nonempty_finite_set_exists_max_fun:
  "[| finite I ; I ~= {} |]
    ==> EX j:I. ALL i:I. ~((f::'a => 'b::order) j < f i)"
apply (insert nonempty_finite_set_exists_max_fun_subset[of I f])
apply (simp)
apply (elim conjE exE)
apply (subgoal_tac "EX j. j:J")
apply (elim exE)
apply (rule_tac x="j" in bexI)
apply (auto)
done

(* finite set --> EX min *)

lemma nonempty_finite_set_exists_min_fun_subset:
  "[| finite I ; I ~= {} |]
    ==> EX J. J <= I & J ~= {} & (ALL j:J. ALL i:I. ~((f::'a => 'b::order) i < f j))"
(*
apply (induct set: Finites)     Isabelle 2005
*)
apply (induct set: finite)     (* Isabelle 2007 *)
apply (simp_all)

(* {} *)
 apply (case_tac "F = {}")
 apply (simp_all)

(* {x} *)
 apply (rule_tac x="{x}" in exI)
 apply (simp)

(* step case *)
 apply (elim conjE exE)
 apply (case_tac "EX j:J. (f x < f j)")
 apply (rule_tac x="(J - {j. f x < f j}) Un {x}" in exI)
 apply (simp)
 apply (rule conjI)
 apply (fast)
 apply (intro ballI)
 apply (elim bexE)
 apply (drule_tac x="j" in bspec, simp)
 apply (drule_tac x="i" in bspec, simp)
 apply (case_tac "~ f i < f x", simp)
 apply (simp)
 apply (rotate_tac -2)
 apply (erule contrapos_np)
 apply (force)

 apply (rule_tac x="J" in exI)
 apply (fast)
done

lemma nonempty_finite_set_exists_min_fun:
  "[| finite I ; I ~= {} |]
    ==> EX j:I. ALL i:I. ~((f::'a => 'b::order) i < f j)"
apply (insert nonempty_finite_set_exists_min_fun_subset[of I f])
apply (simp)
apply (elim conjE exE)
apply (subgoal_tac "EX j. j:J")
apply (elim exE)
apply (rule_tac x="j" in bexI)
apply (auto)
done

(*** cardinality of the set of a list ***)

lemma card_set_eq_length:
  "(card (set s) = length s) =
   (ALL i. i < length s --> (ALL j. j < length s & s!i = s!j --> i = j))"
apply (induct_tac s)
apply (auto)

apply (insert nat_zero_or_Suc)
apply (rotate_tac -1)
apply (frule_tac x="i" in spec)
apply (drule_tac x="j" in spec)
apply (elim disjE exE)
apply (simp_all)
apply (simp add: card_insert_if)
apply (simp add: card_insert_if)
apply (force)

apply (simp add: card_insert)
apply (subgoal_tac "set list - {a} = set list")
apply (simp)
apply (case_tac "a ~: set list")
apply (simp)
apply (simp)
apply (simp add: in_set_conv_nth)
apply (elim conjE exE)
apply (rotate_tac 2)
apply (drule_tac x="0" in spec)
apply (simp)
apply (rotate_tac -1)
apply (drule_tac x="Suc i" in spec)
apply (simp)

apply (case_tac "a ~: set list")
apply (simp)
apply (simp add: card_insert_if)
apply (subgoal_tac "card (set list) <= (length list)")
apply (simp)
apply (simp (no_asm_use) add: card_length)

apply (drule_tac x="Suc i" in spec)
apply (simp)
apply (rotate_tac -1)
apply (drule_tac x="Suc j" in spec)
apply (simp)
done

(*****************************************************
   Small lemmas for isListOf (Finite Set <--> List)
 *****************************************************)

consts
  isListOf :: "'a list => 'a set => bool"       ("_ isListOf _" [55,55] 55)

defs
  isListOf_def : 
    "s isListOf X  == 
     X = set s & (card (set s) = length s)"

lemma isListOf_EX: "(finite X) ==> EX s. s isListOf X"
apply (simp add: isListOf_def)
apply (rule finite_induct[of _ "(%X. EX s. X = set s & card (set s) = length s)"])
                        (* for Isabelle 2008 *)
apply (simp_all)

apply (elim conjE exE)
apply (simp)
apply (rule_tac x="x # s" in exI)
apply (simp)
done

(* finite_list: "finite A ==> EX l. set l = A" *)
(* finite_set : "finite (set xs)" *)

lemma isListOf_set_eq:
  "x isListOf X ==> set x = X"
by (simp add: isListOf_def)

lemma set_SOME_isListOf: "(finite S) ==> set (SOME t. t isListOf S) = S"
apply (insert isListOf_EX[of S])
apply (simp)
apply (erule exE)
apply (rule someI2)
apply (simp)
apply (simp add: isListOf_set_eq)
done

lemma isListOf_nonemptyset:
  "[| X ~= {} ; x isListOf X |] ==> x ~= []"
by (simp add: isListOf_def)

lemma isListOf_index_to_nth:
  "Is isListOf I ==> ALL i:I. EX n. n<length Is & i = Is ! n"
apply (rule ballI)
apply (simp add: isListOf_def)
apply (elim conjE)
apply (simp add: set_nth)
done

lemma isListOf_nth_in_index:
  "[| Is isListOf I ; n<length Is |] ==> Is ! n : I"
by (simp add: isListOf_def)

lemma isListOf_index_to_nthE:
  "[| Is isListOf I ; 
   [| Is isListOf I ; ALL i:I. EX n. n<length Is & i = Is ! n |] ==> R |]
   ==> R"
by (simp add: isListOf_index_to_nth)

lemma isListOf_nth_in_indexE:
  "[| Is isListOf I ; [| Is isListOf I ; ALL n. n<length Is --> Is ! n : I |] ==> R |]
   ==> R"
by (simp add: isListOf_def)

lemma isListOf_THE_nth:
  "[| Is isListOf I ; n < length Is|]
   ==> (THE m. Is ! m = Is ! n & m < length Is) = n"
apply (rule the_equality)
apply (simp)
apply (simp add: isListOf_def)
apply (simp add: card_set_eq_length)
done

(*** nil ***)

lemma isListOf_emptyset_to_nil[simp]: "(Is isListOf {}) = (Is = [])"
apply (auto simp add: isListOf_def)
done

lemma isListOf_nil_to_emptyset[simp]: "([] isListOf X) = (X = {})"
by (simp add: isListOf_def)

(*** one ***)

lemma isListOf_oneset_to_onelist_ALL: "ALL t a. t isListOf {a} --> t = [a]"
apply (rule allI)
apply (induct_tac t)
apply (simp add: isListOf_def)

apply (intro allI impI)
apply (insert list_nil_or_unnil)
apply (drule_tac x="list" in spec)
apply (elim exE disjE)
apply (simp add: isListOf_def)

apply (simp add: isListOf_def)
apply (elim conjE)
apply (simp)
apply (simp add: card_insert)
apply (subgoal_tac "set s - {aa} = {}")
apply (simp_all)
done

lemma isListOf_oneset_to_onelist[simp]: "(t isListOf {a}) = (t = [a])"
apply (auto simp add: isListOf_oneset_to_onelist_ALL)
apply (simp add: isListOf_def)
done

lemma isListOf_onelist_to_oneset[simp]: "([a] isListOf X) = (X = {a})"
apply (simp add: isListOf_def)
done

end