Theory Infra_type

           (*-------------------------------------------*
            |        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_type = Infra_common: 

(*****************************************************
              Infinite Sequence type
 *****************************************************)

types 'a infinite_seq = "nat => 'a"           (* synonym *)

(********************************************************** 
                      set or nat
 **********************************************************)

datatype
  'a selector
   = sel_set "'a set"
   | sel_nat "nat"

lemma inj_sel_set[simp]: "inj sel_set"
by (simp add: inj_on_def)

lemma inj_sel_nat[simp]: "inj sel_nat"
by (simp add: inj_on_def)

lemma tri_compo_is:
  "ALL x. ( (EX b. x = sel_set b)
          | (EX c. x = sel_nat c) )"
apply (intro allI)
apply (induct_tac x)
by (auto)

lemma P_image_sel_set:
  "[| ALL x:X. P x ; y : (sel_set ` X) |] ==> P ((inv sel_set) y)"
by (auto)

lemma P_image_sel_nat:
  "[| ALL x:X. P x ; y : (sel_nat ` X) |] ==> P ((inv sel_nat) y)"
by (auto)

lemma P_inv_sel_set:
  "(ALL x. P (inv sel_set x)) = (ALL y. P y)"
apply (auto)
apply (drule_tac x="sel_set y" in spec)
by (simp)

lemma P_inv_sel_nat:
  "(ALL x. P (inv sel_nat x)) = (ALL y. P y)"
apply (auto)
apply (drule_tac x="sel_nat y" in spec)
by (simp)

lemma P_inv_sel_setI:
  "ALL x. P (inv sel_set x) ==> P y"
by (simp add: P_inv_sel_set)

lemma P_inv_sel_natI:
  "ALL x. P (inv sel_nat x) ==> P y"
by (simp add: P_inv_sel_nat)

end