Quelle  Relations.thy

section‹Predicates and relations›

theory Relations
imports Var
begin
default_sort type

text ‹Unifying Theories of Programming (UTP) is a semantic framework based on
  alphabetized relational calculus. An alphabetized predicate is a pair (alphabet, predicate)
  the free variables appearing in the predicate are all in the alphabet.›

text ‹An alphabetized relation is an alphabetized predicate where the alphabet is
  of input (undecorated) and output (dashed) variables. In this case the
  describes a relation between input and output variables.›

subsection‹Definitions›

text ‹In this section, the definitions of predicates, relations and
  operators are given.›

type_synonym 'α "alphabet"  = "'α"
type_synonym 'α predicate = "'α alphabet ==> bool"

definition  true::"'α predicate"
where "true ≡ λA. True"

definition  false::"'α predicate"
where "false ≡ λA. False"

definition  not::"'α predicate ==> 'α predicate" (‹¬ _› [40] 40)
where "¬ P ≡ λA. ¬ (P A)"

definition  conj::"'α predicate ==> 'α predicate ==> 'α predicate" (infixr ‹∧› 35)
where "P ∧ Q ≡ λA. P A ∧ Q A"

definition disj::"'α predicate ==> 'α predicate ==> 'α predicate" (infixr ‹∨› 30)
where "P ∨ Q ≡ λA. P A ∨ Q A"

definition impl::"'α predicate ==> 'α predicate ==> 'α predicate" (infixr ‹⟶› 25)
where "P ⟶ Q ≡ λA. P A ⟶ Q A"

definition iff::"'α predicate ==> 'α predicate ==> 'α predicate" (infixr ‹⟷› 25)
where "P ⟷ Q ≡ λA. P A ⟷ Q A"

definition ex::"['β ==>'α predicate] ==> 'α predicate" (binder ‹\∃› 10)
where "\<exists>x. P x ≡ λA. ∃ x. (P x) A"

definition all::"['β ==>'α predicate] ==> 'α predicate" (binder ‹\∀› 10)
where "\<forall>x. P x ≡ λ A. ∀x. (P x) A"

type_synonym 'α condition = "('α × 'α) ==> bool"
type_synonym 'α relation  = "('α × 'α) ==> bool"

definition cond::"'α relation ==> 'α condition ==> 'α relation ==> 'α relation" 
                                                          (‹(3_ ◃ _ ▹ / _)› [14,0,15] 14)
where " (P ◃ b ▹ Q) ≡ (b ∧ P) ∨ ((¬ b) ∧ Q)"

definition comp::"(('α × 'β) ==> bool) ==> (('β × 'γ) ==> bool) ==> ('α × 'γ) ==> bool" 
                                                                          (infixr ‹;;› 25)
where "P ;; Q ≡ λr. r : ({p. P p} O {q. Q q})"

definition Assign::"('a, 'b) var ==> 'a ==> 'b relation" 
  where "Assign x a ≡ λ(A, A'). A' = (assign x a) A"

syntax
  "_assignment" :: "id ==> 'a ==> 'b relation"  (‹_ :== _›)
translations
  "y :== vv"   => "CONST Assign (VAR y) vv"

abbreviation (input) closure::"'α predicate ==> bool" (‹[_]›)
where "[ P ] ≡ ∀ A. P A"

abbreviation (input) ndet::"'α relation ==> 'α relation ==> 'α relation" (‹(_ ⊓ _)›)
where "P ⊓ Q ≡ P ∨ Q"

abbreviation (input) join::"'α relation ==> 'α relation ==> 'α relation" (‹(_ ⊔ _)›)
where "P ⊔ Q ≡ P ∧ Q"

abbreviation (input) ndetS::"'α relation set ==> 'α relation" (‹(⊓ _)›)
where "⊓ S ≡ λA. A ∈ ∪{{p. P p} | P. P ∈ S}"

abbreviation (input) conjS::"'α relation set ==> 'α relation" (‹(⊔ _)›)
where "⊔ S ≡ λA. A ∈ ∩{{p. P p} | P. P ∈ S}"

abbreviation (input) skip_r::"'α relation" (‹Πr›)
where "Πr ≡ λ (A, A') . A = A'"

abbreviation (input) Bot::"'α relation"
where "Bot ≡ true"

abbreviation (input) Top::"'α relation"
where "Top ≡ false"


lemmas utp_defs = true_def false_def conj_def disj_def not_def impl_def iff_def
                  ex_def all_def cond_def comp_def Assign_def


subsection ‹Proofs›


text ‹All useful proved lemmas over predicates and relations are presented here.
 , we introduce the most important lemmas that will be used by automatic tools to simplify
 . In the second part, other lemmas are proved using these basic ones.›


subsubsection ‹Setup of automated tools›

lemma true_intro: "true x" by (simp add: utp_defs)
lemma false_elim: "false x ==> C" by (simp add: utp_defs)
lemma true_elim: "true x ==> C ==> C" by (simp add: utp_defs)

lemma not_intro: "(P x ==> false x) ==> (¬ P) x" by (auto simp add: utp_defs)
lemma not_elim: "(¬ P) x ==> P x ==> C" by (auto simp add: utp_defs)
lemma not_dest: "(¬ P) x ==> ¬ P x" by (auto simp add: utp_defs)

lemma conj_intro: "P x ==> Q x ==> (P ∧ Q) x" by (auto simp add: utp_defs)
lemma conj_elim: "(P ∧ Q) x ==> (P x ==> Q x ==> C) ==> C" by (auto simp add: utp_defs)

lemma disj_introC: "(¬ Q x ==> P x) ==> (P ∨ Q) x" by (auto simp add: utp_defs)
lemma disj_elim: "(P ∨ Q) x ==> (P x ==> C) ==> (Q x ==> C) ==> C" by (auto simp add: utp_defs)

lemma impl_intro: "(P x ==> Q x) ==> (P ⟶ Q) x" by (auto simp add: utp_defs)
lemma impl_elimC: "(P ⟶ Q) x ==> (¬ P x ==> R) ==> (Q x ==> R) ==> R " by (auto simp add: utp_defs)

lemma iff_intro: "(P x ==> Q x) ==> (Q x ==> P x) ==> (P ⟷ Q) x" by (auto simp add: utp_defs)
lemma iff_elimC: 
"(P ⟷ Q) x ==> (P x ==> Q x ==> R) ==> (¬ P x ==> ¬ Q x ==> R) ==> R" by (auto simp add: utp_defs)

lemma all_intro: "(∧a. P a x) ==> (\<forall>a. P a) x" by (auto simp add: utp_defs)
lemma all_elim: "(\<forall>a. P a) x ==> (P a x ==> R) ==> R" by (auto simp add: utp_defs)

lemma ex_intro: "P a x ==> (\<exists>a. P a) x" by (auto simp add: utp_defs)
lemma ex_elim: "(\<exists>a. P a) x ==> (∧a. P a x ==> Q) ==> Q" by (auto simp add: utp_defs)

lemma comp_intro: "P (a, b) ==> Q (b, c) ==> (P ;; Q) (a, c)"
  by (auto simp add: comp_def)

lemma comp_elim: 
"(P ;; Q) ac ==> (∧a b c. ac = (a, c) ==> P (a, b) ==> Q (b, c) ==> C) ==> C"
  by (auto simp add: comp_def)

declare not_def [simp]

declare iff_intro [intro!]
  and not_intro [intro!]
  and impl_intro [intro!]
  and disj_introC [intro!]
  and conj_intro [intro!]
  and true_intro [intro!]
  and comp_intro [intro]

declare not_dest [dest!]
  and iff_elimC [elim!]
  and false_elim [elim!]
  and impl_elimC [elim!]
  and disj_elim [elim!]
  and conj_elim [elim!]
  and comp_elim [elim!]
  and true_elim [elim!]

declare all_intro [intro!] and ex_intro [intro]
declare ex_elim [elim!] and all_elim [elim]

lemmas relation_rules = iff_intro not_intro impl_intro disj_introC conj_intro true_intro
                        comp_intro not_dest iff_elimC false_elim impl_elimC all_elim
                        disj_elim conj_elim comp_elim all_intro ex_intro ex_elim 
                        


lemma split_cond: 
"A ((P ◃ b ▹ Q) x) = ((b x ⟶ A (P x)) ∧ (¬ b x ⟶ A (Q x)))"
  by (cases "b x") (auto simp add: utp_defs)

lemma split_cond_asm: 
"A ((P ◃ b ▹ Q) x) = (¬ ((b x ∧ ¬ A (P x)) ∨ (¬ b x ∧ ¬ A (Q x))))"
  by (cases "b x") (auto simp add: utp_defs)

lemmas cond_splits = split_cond split_cond_asm


subsubsection ‹Misc lemmas›

lemma cond_idem:"(P ◃ b ▹ P) = P"
  by (rule ext) (auto split: cond_splits)

lemma cond_symm:"(P ◃ b ▹ Q) = (Q ◃ ¬ b ▹ P)"
  by (rule ext) (auto split: cond_splits)

lemma cond_assoc: "((P ◃ b ▹ Q) ◃ c ▹ R) = (P ◃ b ∧ c ▹ (Q ◃ c ▹ R))"
  by (rule ext) (auto split: cond_splits)

lemma cond_distr: "(P ◃ b ▹ (Q ◃ c ▹ R)) = ((P ◃ b ▹ Q) ◃ c ▹ (P ◃ b ▹ R))"
  by (rule ext) (auto split: cond_splits)

lemma cond_unit_T:"(P ◃ true ▹ Q) = P"
  by (rule ext) (auto split: cond_splits)

lemma cond_unit_F:"(P ◃ false ▹ Q) = Q"
  by (rule ext) (auto split: cond_splits)

lemma cond_L6: "(P ◃ b ▹ (Q ◃ b ▹ R)) = (P ◃ b ▹ R)"
  by (rule ext) (auto split: cond_splits)

lemma cond_L7: "(P ◃ b ▹ (P ◃ c ▹ Q)) = (P ◃ b ∨ c ▹ Q)"
  by (rule ext) (auto split: cond_splits)

lemma cond_and_distr: "((P ∧ Q) ◃ b ▹ (R ∧ S)) = ((P ◃ b ▹ R) ∧ (Q ◃ b ▹ S))"
  by (rule ext) (auto split: cond_splits)

lemma cond_or_distr: "((P ∨ Q) ◃ b ▹ (R ∨ S)) = ((P ◃ b ▹ R) ∨ (Q ◃ b ▹ S))"
  by (rule ext) (auto split: cond_splits)

lemma cond_imp_distr: 
"((P ⟶ Q) ◃ b ▹ (R ⟶ S)) = ((P ◃ b ▹ R) ⟶ (Q ◃ b ▹ S))"
  by (rule ext) (auto split: cond_splits)

lemma cond_eq_distr: 
"((P ⟷ Q) ◃ b ▹ (R ⟷ S)) = ((P ◃ b ▹ R) ⟷ (Q ◃ b ▹ S))"
  by (rule ext) (auto split: cond_splits)

lemma comp_assoc: "(P ;; (Q ;; R)) = ((P ;; Q) ;; R)"
  by (rule ext) blast

lemma conj_comp: 
"(∧ a b c. P (a, b) = P (a, c)) ==> (P ∧ (Q ;; R)) = ((P ∧ Q) ;; R)"
  by (rule ext) blast

lemma comp_cond_left_distr:
  assumes "∧x y z. b (x, y) = b (x, z)"
  shows "((P ◃ b ▹ Q) ;; R) = ((P ;; R) ◃ b ▹ (Q ;; R))"
  using assms by (auto simp: fun_eq_iff utp_defs)

lemma ndet_symm: "(P::'a relation) ⊓ Q = Q ⊓ P"
  by (rule ext) blast

lemma ndet_assoc: "P ⊓ (Q ⊓ R) = (P ⊓ Q) ⊓ R"
  by (rule ext) blast

lemma ndet_idemp: "P ⊓ P = P"
  by (rule ext) blast

lemma ndet_distr: "P ⊓ (Q ⊓ R) = (P ⊓ Q) ⊓ (P ⊓ R)"
  by (rule ext) blast

lemma cond_ndet_distr: "(P ◃ b ▹ (Q ⊓ R)) = ((P ◃ b ▹ Q) ⊓ (P ◃ b ▹ R))"
  by (rule ext) (auto split: cond_splits)

lemma ndet_cond_distr: "(P ⊓ (Q ◃ b ▹ R)) = ((P ⊓ Q) ◃ b ▹ (P ⊓ R))"
  by (rule ext) (auto split: cond_splits)

lemma comp_ndet_l_distr: "((P ⊓ Q) ;; R) = ((P ;; R) ⊓ (Q ;; R))"
  by (auto simp: fun_eq_iff utp_defs)

lemma comp_ndet_r_distr: "(P ;; (Q ⊓ R)) = ((P ;; Q) ⊓ (P ;; R))"
  by (auto simp: fun_eq_iff utp_defs)

lemma l2_5_1_A: "∀X ∈ S. [X ⟶ (⊓ S)]"
  by blast

lemma l2_5_1_B: "(∀ X ∈ S. [X ⟶ P]) ⟶ [(⊓ S) ⟶ P]"
  by blast

lemma l2_5_1: "[(⊓ S) ⟶ P] ⟷ (∀ X ∈ S. [X ⟶ P])"
  by blast

lemma empty_disj: "⊓ {} = Top"
  by (rule ext) blast

lemma l2_5_1_2: "[P ⟶ (⊔ S)] ⟷ (∀ X ∈ S. [P ⟶ X])"
  by blast

lemma empty_conj: "⊔ {} = Bot"
  by (rule ext) blast

lemma l2_5_2: "((⊔ S) ⊓ Q) = (⊔{P ⊓ Q | P. P∈S})"
  by (rule ext) blast

lemma l2_5_3: "((⊓ S) ⊔ Q) = (⊓{P ⊔ Q | P. P ∈ S})"
  by (rule ext) blast

lemma l2_5_4: "((⊓ S) ;; Q) = (⊓{P ;; Q | P. P ∈ S})"
  by (rule ext) blast

lemma l2_5_5: "(Q ;; (⊓ S)) = (⊓{Q ;; P | P. P ∈ S})"
  by (rule ext) blast

lemma all_idem :"(\<forall>b. \<forall>a. P a) = (\<forall>a. P a)"
  by (simp add: all_def)

lemma comp_unit_R [simp]: "(P ;; Πr) = P"
  by (auto simp: fun_eq_iff utp_defs)

lemma comp_unit_L [simp]: "(Πr ;; P) = P"
  by (auto simp: fun_eq_iff utp_defs)

lemmas comp_unit_simps = comp_unit_R comp_unit_L

lemma not_cond: "(¬(P ◃ b ▹ Q)) = ((¬ P) ◃ b ▹ (¬ Q))"
  by (rule ext) (auto split: cond_splits)

lemma cond_conj_not_distr: 
"((P ◃ b ▹ Q) ∧ ¬(R ◃ b ▹ S)) = ((P ∧ ¬R) ◃ b ▹ (Q ∧ ¬S))"
  by (rule ext) (auto split: cond_splits)

lemma imp_cond_distr: "(R ⟶ (P ◃ b ▹ Q)) = ((R ⟶ P) ◃ b ▹ (R ⟶ Q))"
  by (rule ext) (auto split: cond_splits)

lemma cond_imp_dist: "((P ◃ b ▹ Q) ⟶ R) = ((P ⟶ R) ◃ b ▹ (Q ⟶ R))"
  by (rule ext) (auto split: cond_splits)

lemma cond_conj_distr: "((P ◃ b ▹ Q) ∧ R) = ((P ∧ R) ◃ b ▹ (Q ∧ R))"
  by (rule ext) (auto split: cond_splits)

lemma cond_disj_distr: "((P ◃ b ▹ Q) ∨ R) = ((P ∨ R) ◃ b ▹ (Q ∨ R))"
  by (rule ext) (auto split: cond_splits)

lemma cond_know_b: "(b ∧ (P ◃ b ▹ Q)) = (b ∧ P)"
  by (rule ext) (auto split: cond_splits)

lemma cond_know_nb: "((¬ (b)) ∧ (P ◃ b ▹ Q)) = ((¬ (b)) ∧ Q)"
  by (rule ext) (auto split: cond_splits)

lemma cond_ass_if: "(P ◃ b ▹ Q) = (((b) ∧ P ◃ b ▹ Q))"
  by (rule ext) (auto split: cond_splits)

lemma cond_ass_else: "(P ◃ b ▹ Q) = (P ◃ b ▹ ((¬b) ∧ Q))"
  by (rule ext) (auto split: cond_splits)

lemma not_true_eq_false: "(¬ true) = false"
  by (rule ext) blast

lemma not_false_eq_true: "(¬ false) = true"
  by (rule ext) blast

lemma conj_idem: "((P::'α predicate) ∧ P) = P"
  by (rule ext) blast

lemma disj_idem: "((P::'α predicate) ∨ P) = P"
  by (rule ext) blast

lemma conj_comm: "((P::'α predicate) ∧ Q) = (Q ∧ P)"
  by (rule ext) blast

lemma disj_comm: "((P::'α predicate) ∨ Q) = (Q ∨ P)"
  by (rule ext) blast

lemma conj_subst: "P = R ==> ((P::'α predicate) ∧ Q) = (R ∧ Q)"
  by (rule ext) blast

lemma disj_subst: "P = R ==> ((P::'α predicate) ∨ Q) = (R ∨ Q)"
  by (rule ext) blast

lemma conj_assoc:"(((P::'α predicate) ∧ Q) ∧ S) = (P ∧ (Q ∧ S))"
  by (rule ext) blast

lemma disj_assoc:"(((P::'α predicate) ∨ Q) ∨ S) = (P ∨ (Q ∨ S))"
  by (rule ext) blast

lemma conj_disj_abs:"((P::'α predicate) ∧ (P ∨ Q)) = P"
  by (rule ext) blast

lemma disj_conj_abs:"((P::'α predicate) ∨ (P ∧ Q)) = P"
  by (rule ext) blast

lemma conj_disj_distr:"((P::'α predicate) ∧ (Q ∨ R)) = ((P ∧ Q) ∨ (P ∧ R))"
  by (rule ext) blast

lemma disj_conj_dsitr:"((P::'α predicate) ∨ (Q ∧ R)) = ((P ∨ Q) ∧ (P ∨ R))"
  by (rule ext) blast

lemma true_conj_id:"(P ∧ true) = P"
  by (rule ext) blast

lemma true_dsij_zero:"(P ∨ true) = true"
  by (rule ext) blast

lemma true_conj_zero:"(P ∧ false) = false"
  by (rule ext) blast

lemma true_dsij_id:"(P ∨ false) = P"
  by (rule ext) blast

lemma imp_vacuous: "(false ⟶ u) = true"
  by (rule ext) blast

lemma p_and_not_p: "(P ∧ ¬ P) = false"
  by (rule ext) blast

lemma conj_disj_not_abs: "((P::'α predicate) ∧ ((¬P) ∨ Q)) = (P ∧ Q)"
  by (rule ext) blast

lemma p_or_not_p: "(P ∨ ¬ P) = true"
  by (rule ext) blast

lemma double_negation: "(¬ ¬ (P::'α predicate)) = P"
  by (rule ext) blast

lemma not_conj_deMorgans: "(¬ ((P::'α predicate) ∧ Q)) = ((¬ P) ∨ (¬ Q))"
  by (rule ext) blast

lemma not_disj_deMorgans: "(¬ ((P::'α predicate) ∨ Q)) = ((¬ P) ∧ (¬ Q))"
  by (rule ext) blast

lemma p_imp_p: "(P ⟶ P) = true"
  by (rule ext) blast

lemma imp_imp: "((P::'α predicate) ⟶ (Q ⟶ R)) = ((P ∧ Q) ⟶ R)"
  by (rule ext) blast

lemma imp_trans: "((P ⟶ Q) ∧ (Q ⟶ R) ⟶ P ⟶ R) = true"
  by (rule ext) blast

lemma p_equiv_p: "(P ⟷ P) = true"
  by (rule ext) blast

lemma equiv_eq: "((((P::'α predicate) ∧ Q) ∨ (¬P ∧ ¬Q)) = true) ⟷ (P = Q)"
  by (auto simp add: fun_eq_iff utp_defs)

lemma equiv_eq1: "(((P::'α predicate) ⟷ Q) = true) ⟷ (P = Q)"
  by (auto simp add: fun_eq_iff utp_defs)

lemma cond_subst: "b = c ==> (P ◃ b ▹ Q) = (P ◃ c ▹ Q)"
  by simp

lemma ex_disj_distr: "((\<exists>x. P x) ∨ (\<exists>x. Q x)) = (\<exists>x. (P x ∨ Q x))"
  by (rule ext) blast

lemma all_disj_distr: "((\<forall>x. P x) ∨ (\<forall>x. Q)) = (\<forall>x. (P x ∨ Q))"
  by (rule ext) blast

lemma all_conj_distr: "((\<forall>x. P x) ∧ (\<forall>x. Q x)) = (\<forall>x. (P x ∧ Q x))"
  by (rule ext) blast

lemma all_triv: "(\<forall>x. P) = P"
  by (rule ext) blast

lemma closure_true: "[true]"
  by blast

lemma closure_p_eq_true: "[P] ⟷ (P = true)"
  by (simp add: fun_eq_iff utp_defs)

lemma closure_equiv_eq: "[P ⟷ Q] ⟷ (P = Q)"
  by (simp add: fun_eq_iff utp_defs)

lemma closure_conj_distr: "([P] ∧ [Q]) = [P ∧ Q]"
  by blast

lemma closure_imp_distr: "[P ⟶ Q] ⟶ [P] ⟶ [Q]"
  by blast

lemma true_iff[simp]: "(P ⟷ true) = P"
  by blast

lemma true_imp[simp]: "(true ⟶ P) = P"
  by blast

end