Up to index of Isabelle/HOL/HOL-Complex/CSP
theory Infra_HOL (*-------------------------------------------*
| CSP-Prover on Isabelle2005 |
| January 2006 |
| |
| Yoshinao Isobe (AIST JAPAN) |
*-------------------------------------------*)
theory Infra_HOL
imports Infra_common
begin
(*--------------------------*
| exchange order in ALL |
*--------------------------*)
lemma exchange_forall_orderE:
"[| ALL x y. P x y ; ALL y x. P x y ==> R |] ==> R"
by (simp)
lemma exchange_forall_order3E:
"[| ALL x y z. P x y z ; ALL y z x. P x y z ==> R |] ==> R"
by (simp)
lemma exchange_ALL_BALL:
"(ALL x:X. ALL y. P x y) = (ALL y. ALL x:X. P x y)"
apply (auto)
done
lemma ALL_BALL_fun:
"(ALL y. ALL x:X. P x y) = (ALL f. ALL x:X. P x (f x))"
apply (auto)
done
lemma ALL_BALL_funE:
"[| ALL y. ALL x:X. P x y ; (ALL f. ALL x:X. P x (f x)) ==> S |] ==> S"
apply (auto)
done
(*-------------------------------*
| distribution of ALL on conj |
*-------------------------------*)
lemma dist_ALL_conjI:
"ALL x. (P x & Q x) ==> (ALL x. P x) & (ALL x. Q x)"
by (simp)
lemma dist_ALL_conjE:
"[| ALL x. (P x & Q x) ; [| ALL x. P x ; ALL x. Q x |] ==> R |] ==> R"
by (simp)
lemma dist_ALL_conj: "(ALL x. P x & Q x) = ((ALL x. P x) & (ALL x. Q x)) "
by (auto)
lemma dist_ALL_conj2I:
"ALL x y. (P x y & Q x y) ==> (ALL x y. P x y) & (ALL x y. Q x y)"
by (simp)
lemma dist_ALL_conj2E:
"[| ALL x y. (P x y & Q x y) ; [| ALL x y. P x y ; ALL x y. Q x y |] ==> R |] ==> R"
by (simp)
lemma dist_ALL_conj2: "(ALL x y. P x y & Q x y) = ((ALL x y. P x y) & (ALL x y. Q x y)) "
by (auto)
(* BALL *)
lemma dist_BALL_conjI:
"ALL x:X. (P x & Q x) ==> (ALL x:X. P x) & (ALL x:X. Q x)"
by (simp)
lemma dist_BALL_conjE:
"[| ALL x:X. (P x & Q x) ;
[| ALL x:X. P x ; ALL x:X. Q x |] ==> S
|] ==> S"
by (simp)
lemma dist_BALL_conj2I:
"ALL x:X. ALL y:(Y x). (P x y & Q x y) ==>
(ALL x:X. ALL y:(Y x). P x y) &
(ALL x:X. ALL y:(Y x). Q x y)"
by (simp)
lemma dist_BALL_conj2E:
"[| ALL x:X. ALL y:(Y x). (P x y & Q x y) ;
[| ALL x:X. ALL y:(Y x). P x y ;
ALL x:X. ALL y:(Y x). Q x y |] ==> S
|] ==> S"
by (simp)
lemma dist_ALL_imply_conjE:
"(ALL x. (b x) --> (P x & Q x))
= ((ALL x. (b x) --> P x) & (ALL x. (b x) --> Q x))"
apply (auto)
done
(*****************************************************
ALL EX --> EX ALL
*****************************************************)
(*** ALL ***)
lemma choice_ALL_EX_only_if:
"ALL P. (ALL x. EX y. P x y) --> (EX f. ALL x. P x (f x))"
apply (intro allI impI)
apply (rule_tac x="(%x. SOME y. P x y)" in exI)
apply (rule allI)
apply (drule_tac x="x" in spec)
apply (erule exE)
apply (rule someI2)
apply (simp)
apply (simp)
done
lemma choice_ALL_EX:
"(ALL x. EX y. P x y) = (EX f. ALL x. P x (f x))"
apply (rule)
apply (simp add: choice_ALL_EX_only_if)
apply (elim exE)
apply (rule allI)
apply (drule_tac x="x" in spec)
apply (rule_tac x="f x" in exI)
apply (simp)
done
(*** imply ***)
lemma choice_ALL_imply_EX_only_if:
"ALL b P. (ALL x. (b x) --> (EX y. P x y)) --> (EX f. ALL x. (b x) --> P x (f x))"
apply (intro allI impI)
apply (rule_tac x="(%x. if (b x) then (SOME y. P x y) else (SOME y. True))" in exI)
apply (rule allI)
apply (drule_tac x="x" in spec)
apply (intro impI)
apply (simp)
apply (erule exE)
apply (rule someI2)
apply (simp)
apply (simp)
done
lemma choice_ALL_imply_EX:
"(ALL x. (b x) --> (EX y. P x y)) = (EX f. ALL x. (b x) --> P x (f x))"
apply (rule)
apply (simp add: choice_ALL_imply_EX_only_if)
apply (elim exE)
apply (rule allI)
apply (drule_tac x="x" in spec)
apply (intro impI)
apply (rule_tac x="f x" in exI)
apply (simp)
done
(*** BALL ***)
lemma choice_BALL_EX:
"(ALL x:X. EX y. P x y) = (EX f. ALL x:X. P x (f x))"
apply (simp add: Ball_def)
apply (simp add: choice_ALL_imply_EX)
done
(*****************************************************
EX!
*****************************************************)
lemma ex1_implies_exE:
"[| EX! x. P x ; EX x. P x ==> S |] ==> S"
by (auto)
(*** 1 ***)
lemma EX1_1I:
"((EX X1. P X1 & (ALL Y1. P Y1 --> (Y1 = X1))))
==> (EX! X1. P X1)"
apply (simp add: Ex1_def)
done
(*** 2 ***)
lemma EX1_2I:
"(EX X1 X2. P X1 X2 & (ALL Y1 Y2. P Y1 Y2 --> ((Y1 = X1) & (Y2 = X2))))
==> (EX! X1 X2. P X1 X2)"
apply (simp add: Ex1_def)
apply (auto)
done
(*** 3 ***)
lemma EX1_3I:
"(EX X1 X2 X3. P X1 X2 X3 &
(ALL Y1 Y2 Y3. P Y1 Y2 Y3 --> ((Y1 = X1) & (Y2 = X2) & (Y3 = X3))))
==> (EX! X1 X2 X3. P X1 X2 X3)"
apply (rule EX1_2I)
apply (elim conjE exE)
apply (rule_tac x="X1" in exI)
apply (rule_tac x="X2" in exI)
apply (rule conjI)
apply (rule EX1_1I)
apply (rule_tac x="X3" in exI)
apply (rule conjI)
apply (assumption)
apply (intro allI impI)
apply (drule_tac x="X1" in spec)
apply (drule_tac x="X2" in spec)
apply (drule_tac x="Y1" in spec)
apply (simp)
apply (intro allI impI)
apply (erule ex1E)
apply (drule_tac x="Y1" in spec)
apply (drule_tac x="Y2" in spec)
apply (drule_tac x="X3a" in spec)
apply (drule_tac x="X3a" in spec)
apply (simp)
done
(*** 4 ***)
lemma EX1_4I:
"(EX X1 X2 X3 X4. P X1 X2 X3 X4 &
(ALL Y1 Y2 Y3 Y4. P Y1 Y2 Y3 Y4
--> ((Y1 = X1) & (Y2 = X2) & (Y3 = X3) & (Y4 = X4))))
==> (EX! X1 X2 X3 X4. P X1 X2 X3 X4)"
apply (rule EX1_3I)
apply (elim conjE exE)
apply (rule_tac x="X1" in exI)
apply (rule_tac x="X2" in exI)
apply (rule_tac x="X3" in exI)
apply (rule conjI)
apply (rule EX1_1I)
apply (rule_tac x="X4" in exI)
apply (rule conjI)
apply (assumption)
apply (intro allI impI)
apply (drule_tac x="X1" in spec)
apply (drule_tac x="X2" in spec)
apply (drule_tac x="X3" in spec)
apply (drule_tac x="Y1" in spec)
apply (simp)
apply (intro allI impI)
apply (erule ex1E)
apply (drule_tac x="Y1" in spec)
apply (drule_tac x="Y2" in spec)
apply (drule_tac x="Y3" in spec)
apply (drule_tac x="X4a" in spec)
apply (drule_tac x="X4a" in spec)
apply (simp)
done
(*** 5 ***)
lemma EX1_5I:
"(EX X1 X2 X3 X4 X5. P X1 X2 X3 X4 X5 &
(ALL Y1 Y2 Y3 Y4 Y5. P Y1 Y2 Y3 Y4 Y5
--> ((Y1 = X1) & (Y2 = X2) & (Y3 = X3) & (Y4 = X4) & (Y5 = X5))))
==> (EX! X1 X2 X3 X4 X5. P X1 X2 X3 X4 X5)"
apply (rule EX1_4I)
apply (elim conjE exE)
apply (rule_tac x="X1" in exI)
apply (rule_tac x="X2" in exI)
apply (rule_tac x="X3" in exI)
apply (rule_tac x="X4" in exI)
apply (rule conjI)
apply (rule EX1_1I)
apply (rule_tac x="X5" in exI)
apply (rule conjI)
apply (assumption)
apply (intro allI impI)
apply (drule_tac x="X1" in spec)
apply (drule_tac x="X2" in spec)
apply (drule_tac x="X3" in spec)
apply (drule_tac x="X4" in spec)
apply (drule_tac x="Y1" in spec)
apply (simp)
apply (intro allI impI)
apply (erule ex1E)
apply (drule_tac x="Y1" in spec)
apply (drule_tac x="Y2" in spec)
apply (drule_tac x="Y3" in spec)
apply (drule_tac x="Y4" in spec)
apply (drule_tac x="X5a" in spec)
apply (drule_tac x="X5a" in spec)
apply (simp)
done
(*** 6 ***)
lemma EX1_6I:
"(EX X1 X2 X3 X4 X5 X6. P X1 X2 X3 X4 X5 X6 &
(ALL Y1 Y2 Y3 Y4 Y5 Y6. P Y1 Y2 Y3 Y4 Y5 Y6
--> ((Y1 = X1) & (Y2 = X2) & (Y3 = X3) &
(Y4 = X4) & (Y5 = X5) & (Y6 = X6))))
==> (EX! X1 X2 X3 X4 X5 X6. P X1 X2 X3 X4 X5 X6)"
apply (rule EX1_5I)
apply (elim conjE exE)
apply (rule_tac x="X1" in exI)
apply (rule_tac x="X2" in exI)
apply (rule_tac x="X3" in exI)
apply (rule_tac x="X4" in exI)
apply (rule_tac x="X5" in exI)
apply (rule conjI)
apply (rule EX1_1I)
apply (rule_tac x="X6" in exI)
apply (rule conjI)
apply (assumption)
apply (intro allI impI)
apply (drule_tac x="X1" in spec)
apply (drule_tac x="X2" in spec)
apply (drule_tac x="X3" in spec)
apply (drule_tac x="X4" in spec)
apply (drule_tac x="X5" in spec)
apply (drule_tac x="Y1" in spec)
apply (simp)
apply (intro allI impI)
apply (erule ex1E)
apply (drule_tac x="Y1" in spec)
apply (drule_tac x="Y2" in spec)
apply (drule_tac x="Y3" in spec)
apply (drule_tac x="Y4" in spec)
apply (drule_tac x="Y5" in spec)
apply (drule_tac x="X6a" in spec)
apply (drule_tac x="X6a" in spec)
apply (simp)
done
end
lemma exchange_forall_orderE:
[| ∀x y. P x y; ∀y x. P x y ==> R |] ==> R
lemma exchange_forall_order3E:
[| ∀x y z. P x y z; ∀y z x. P x y z ==> R |] ==> R
lemma exchange_ALL_BALL:
(∀x∈X. ∀y. P x y) = (∀y. ∀x∈X. P x y)
lemma ALL_BALL_fun:
(∀y. ∀x∈X. P x y) = (∀f. ∀x∈X. P x (f x))
lemma ALL_BALL_funE:
[| ∀y. ∀x∈X. P x y; ∀f. ∀x∈X. P x (f x) ==> S |] ==> S
lemma dist_ALL_conjI:
∀x. P x ∧ Q x ==> (∀x. P x) ∧ (∀x. Q x)
lemma dist_ALL_conjE:
[| ∀x. P x ∧ Q x; [| ∀x. P x; ∀x. Q x |] ==> R |] ==> R
lemma dist_ALL_conj:
(∀x. P x ∧ Q x) = ((∀x. P x) ∧ (∀x. Q x))
lemma dist_ALL_conj2I:
∀x y. P x y ∧ Q x y ==> (∀x y. P x y) ∧ (∀x y. Q x y)
lemma dist_ALL_conj2E:
[| ∀x y. P x y ∧ Q x y; [| ∀x y. P x y; ∀x y. Q x y |] ==> R |] ==> R
lemma dist_ALL_conj2:
(∀x y. P x y ∧ Q x y) = ((∀x y. P x y) ∧ (∀x y. Q x y))
lemma dist_BALL_conjI:
∀x∈X. P x ∧ Q x ==> (∀x∈X. P x) ∧ (∀x∈X. Q x)
lemma dist_BALL_conjE:
[| ∀x∈X. P x ∧ Q x; [| ∀x∈X. P x; ∀x∈X. Q x |] ==> S |] ==> S
lemma dist_BALL_conj2I:
∀x∈X. ∀y∈Y x. P x y ∧ Q x y ==> (∀x∈X. ∀y∈Y x. P x y) ∧ (∀x∈X. ∀y∈Y x. Q x y)
lemma dist_BALL_conj2E:
[| ∀x∈X. ∀y∈Y x. P x y ∧ Q x y;
[| ∀x∈X. ∀y∈Y x. P x y; ∀x∈X. ∀y∈Y x. Q x y |] ==> S |]
==> S
lemma dist_ALL_imply_conjE:
(∀x. b x --> P x ∧ Q x) = ((∀x. b x --> P x) ∧ (∀x. b x --> Q x))
lemma choice_ALL_EX_only_if:
∀P. (∀x. ∃y. P x y) --> (∃f. ∀x. P x (f x))
lemma choice_ALL_EX:
(∀x. ∃y. P x y) = (∃f. ∀x. P x (f x))
lemma choice_ALL_imply_EX_only_if:
∀b P. (∀x. b x --> (∃y. P x y)) --> (∃f. ∀x. b x --> P x (f x))
lemma choice_ALL_imply_EX:
(∀x. b x --> (∃y. P x y)) = (∃f. ∀x. b x --> P x (f x))
lemma choice_BALL_EX:
(∀x∈X. ∃y. P x y) = (∃f. ∀x∈X. P x (f x))
lemma ex1_implies_exE:
[| ∃!x. P x; ∃x. P x ==> S |] ==> S
lemma EX1_1I:
∃X1. P X1 ∧ (∀Y1. P Y1 --> Y1 = X1) ==> ∃!X1. P X1
lemma EX1_2I:
∃X1 X2. P X1 X2 ∧ (∀Y1 Y2. P Y1 Y2 --> Y1 = X1 ∧ Y2 = X2) ==> ∃!X1 X2. P X1 X2
lemma EX1_3I:
∃X1 X2 X3. P X1 X2 X3 ∧ (∀Y1 Y2 Y3. P Y1 Y2 Y3 --> Y1 = X1 ∧ Y2 = X2 ∧ Y3 = X3)
==> ∃!X1 X2 X3. P X1 X2 X3
lemma EX1_4I:
∃X1 X2 X3 X4.
P X1 X2 X3 X4 ∧
(∀Y1 Y2 Y3 Y4. P Y1 Y2 Y3 Y4 --> Y1 = X1 ∧ Y2 = X2 ∧ Y3 = X3 ∧ Y4 = X4)
==> ∃!X1 X2 X3 X4. P X1 X2 X3 X4
lemma EX1_5I:
∃X1 X2 X3 X4 X5.
P X1 X2 X3 X4 X5 ∧
(∀Y1 Y2 Y3 Y4 Y5.
P Y1 Y2 Y3 Y4 Y5 --> Y1 = X1 ∧ Y2 = X2 ∧ Y3 = X3 ∧ Y4 = X4 ∧ Y5 = X5)
==> ∃!X1 X2 X3 X4 X5. P X1 X2 X3 X4 X5
lemma EX1_6I:
∃X1 X2 X3 X4 X5 X6.
P X1 X2 X3 X4 X5 X6 ∧
(∀Y1 Y2 Y3 Y4 Y5 Y6.
P Y1 Y2 Y3 Y4 Y5 Y6 -->
Y1 = X1 ∧ Y2 = X2 ∧ Y3 = X3 ∧ Y4 = X4 ∧ Y5 = X5 ∧ Y6 = X6)
==> ∃!X1 X2 X3 X4 X5 X6. P X1 X2 X3 X4 X5 X6