(* Title: HOL/Algebra/Congruence.thy
Author: Clemens Ballarin, started 3 January 2008
Copyright: Clemens Ballarin
*)
theory Congruence
imports
Main
"HOL-Library.FuncSet"
begin
section \Objects\
subsection \Structure with Carrier Set.\
record 'a partial_object =
carrier :: "'a set"
lemma funcset_carrier:
"\ f \ carrier X \ carrier Y; x \ carrier X \ \ f x \ carrier Y"
by (fact funcset_mem)
lemma funcset_carrier':
"\ f \ carrier A \ carrier A; x \ carrier A \ \ f x \ carrier A"
by (fact funcset_mem)
subsection \Structure with Carrier and Equivalence Relation \eq\\
record 'a eq_object = "'a partial_object" +
eq :: "'a \ 'a \ bool" (infixl ".=\" 50)
definition
elem :: "_ \ 'a \ 'a set \ bool" (infixl ".\\" 50)
where "x .\\<^bsub>S\<^esub> A \ (\y \ A. x .=\<^bsub>S\<^esub> y)"
definition
set_eq :: "_ \ 'a set \ 'a set \ bool" (infixl "{.=}\" 50)
where "A {.=}\<^bsub>S\<^esub> B \ ((\x \ A. x .\\<^bsub>S\<^esub> B) \ (\x \ B. x .\\<^bsub>S\<^esub> A))"
definition
eq_class_of :: "_ \ 'a \ 'a set" ("class'_of\")
where "class_of\<^bsub>S\<^esub> x = {y \ carrier S. x .=\<^bsub>S\<^esub> y}"
definition
eq_closure_of :: "_ \ 'a set \ 'a set" ("closure'_of\")
where "closure_of\<^bsub>S\<^esub> A = {y \ carrier S. y .\\<^bsub>S\<^esub> A}"
definition
eq_is_closed :: "_ \ 'a set \ bool" ("is'_closed\")
where "is_closed\<^bsub>S\<^esub> A \ A \ carrier S \ closure_of\<^bsub>S\<^esub> A = A"
abbreviation
not_eq :: "_ \ 'a \ 'a \ bool" (infixl ".\\" 50)
where "x .\\<^bsub>S\<^esub> y == ~(x .=\<^bsub>S\<^esub> y)"
abbreviation
not_elem :: "_ \ 'a \ 'a set \ bool" (infixl ".\\" 50)
where "x .\\<^bsub>S\<^esub> A == ~(x .\\<^bsub>S\<^esub> A)"
abbreviation
set_not_eq :: "_ \ 'a set \ 'a set \ bool" (infixl "{.\}\" 50)
where "A {.\}\<^bsub>S\<^esub> B == ~(A {.=}\<^bsub>S\<^esub> B)"
locale equivalence =
fixes S (structure)
assumes refl [simp, intro]: "x \ carrier S \ x .= x"
and sym [sym]: "\ x .= y; x \ carrier S; y \ carrier S \ \ y .= x"
and trans [trans]:
"\ x .= y; y .= z; x \ carrier S; y \ carrier S; z \ carrier S \ \ x .= z"
(* Lemmas by Stephan Hohe *)
lemma elemI:
fixes R (structure)
assumes "a' \ A" and "a .= a'"
shows "a .\ A"
unfolding elem_def
using assms
by fast
lemma (in equivalence) elem_exact:
assumes "a \ carrier S" and "a \ A"
shows "a .\ A"
using assms
by (fast intro: elemI)
lemma elemE:
fixes S (structure)
assumes "a .\ A"
and "\a'. \a' \ A; a .= a'\ \ P"
shows "P"
using assms
unfolding elem_def
by fast
lemma (in equivalence) elem_cong_l [trans]:
assumes cong: "a' .= a"
and a: "a .\ A"
and carr: "a \ carrier S" "a' \ carrier S"
and Acarr: "A \ carrier S"
shows "a' .\ A"
using a
apply (elim elemE, intro elemI)
proof assumption
fix b
assume bA: "b \ A"
note [simp] = carr bA[THEN subsetD[OF Acarr]]
note cong
also assume "a .= b"
finally show "a' .= b" by simp
qed
lemma (in equivalence) elem_subsetD:
assumes "A \ B"
and aA: "a .\ A"
shows "a .\ B"
using assms
by (fast intro: elemI elim: elemE dest: subsetD)
lemma (in equivalence) mem_imp_elem [simp, intro]:
"[| x \ A; x \ carrier S |] ==> x .\ A"
unfolding elem_def by blast
lemma set_eqI:
fixes R (structure)
assumes ltr: "\a. a \ A \ a .\ B"
and rtl: "\b. b \ B \ b .\ A"
shows "A {.=} B"
unfolding set_eq_def
by (fast intro: ltr rtl)
lemma set_eqI2:
fixes R (structure)
assumes ltr: "\a b. a \ A \ \b\B. a .= b"
and rtl: "\b. b \ B \ \a\A. b .= a"
shows "A {.=} B"
by (intro set_eqI, unfold elem_def) (fast intro: ltr rtl)+
lemma set_eqD1:
fixes R (structure)
assumes AA': "A {.=} A'"
and "a \ A"
shows "\a'\A'. a .= a'"
using assms
unfolding set_eq_def elem_def
by fast
lemma set_eqD2:
fixes R (structure)
assumes AA': "A {.=} A'"
and "a' \ A'"
shows "\a\A. a' .= a"
using assms
unfolding set_eq_def elem_def
by fast
lemma set_eqE:
fixes R (structure)
assumes AB: "A {.=} B"
and r: "\\a\A. a .\ B; \b\B. b .\ A\ \ P"
shows "P"
using AB
unfolding set_eq_def
by (blast dest: r)
lemma set_eqE2:
fixes R (structure)
assumes AB: "A {.=} B"
and r: "\\a\A. (\b\B. a .= b); \b\B. (\a\A. b .= a)\ \ P"
shows "P"
using AB
unfolding set_eq_def elem_def
by (blast dest: r)
lemma set_eqE':
fixes R (structure)
assumes AB: "A {.=} B"
and aA: "a \ A" and bB: "b \ B"
and r: "\a' b'. \a' \ A; b .= a'; b' \ B; a .= b'\ \ P"
shows "P"
proof -
from AB aA
have "\b'\B. a .= b'" by (rule set_eqD1)
from this obtain b'
where b': "b' \ B" "a .= b'" by auto
from AB bB
have "\a'\A. b .= a'" by (rule set_eqD2)
from this obtain a'
where a': "a' \ A" "b .= a'" by auto
from a' b'
show "P" by (rule r)
qed
lemma (in equivalence) eq_elem_cong_r [trans]:
assumes a: "a .\ A"
and cong: "A {.=} A'"
and carr: "a \ carrier S"
and Carr: "A \ carrier S" "A' \ carrier S"
shows "a .\ A'"
using a cong
proof (elim elemE set_eqE)
fix b
assume bA: "b \ A"
and inA': "\b\A. b .\ A'"
note [simp] = carr Carr Carr[THEN subsetD] bA
assume "a .= b"
also from bA inA'
have "b .\ A'" by fast
finally
show "a .\ A'" by simp
qed
lemma (in equivalence) set_eq_sym [sym]:
assumes "A {.=} B"
and "A \ carrier S" "B \ carrier S"
shows "B {.=} A"
using assms
unfolding set_eq_def elem_def
by fast
(* FIXME: the following two required in Isabelle 2008, not Isabelle 2007 *)
(* alternatively, could declare lemmas [trans] = ssubst [where 'a = "'a set"] *)
lemma (in equivalence) equal_set_eq_trans [trans]:
assumes AB: "A = B" and BC: "B {.=} C"
shows "A {.=} C"
using AB BC by simp
lemma (in equivalence) set_eq_equal_trans [trans]:
assumes AB: "A {.=} B" and BC: "B = C"
shows "A {.=} C"
using AB BC by simp
lemma (in equivalence) set_eq_trans [trans]:
assumes AB: "A {.=} B" and BC: "B {.=} C"
and carr: "A \ carrier S" "B \ carrier S" "C \ carrier S"
shows "A {.=} C"
proof (intro set_eqI)
fix a
assume aA: "a \ A"
with carr have "a \ carrier S" by fast
note [simp] = carr this
from aA
have "a .\ A" by (simp add: elem_exact)
also note AB
also note BC
finally
show "a .\ C" by simp
next
fix c
assume cC: "c \ C"
with carr have "c \ carrier S" by fast
note [simp] = carr this
from cC
have "c .\ C" by (simp add: elem_exact)
also note BC[symmetric]
also note AB[symmetric]
finally
show "c .\ A" by simp
qed
(* FIXME: generalise for insert *)
(*
lemma (in equivalence) set_eq_insert:
assumes x: "x .= x'"
and carr: "x \ carrier S" "x' \ carrier S" "A \ carrier S"
shows "insert x A {.=} insert x' A"
unfolding set_eq_def elem_def
apply rule
apply rule
apply (case_tac "xa = x")
using x apply fast
apply (subgoal_tac "xa \ A") prefer 2 apply fast
apply (rule_tac x=xa in bexI)
using carr apply (rule_tac refl) apply auto [1]
apply safe
*)
lemma (in equivalence) set_eq_pairI:
assumes xx': "x .= x'"
and carr: "x \ carrier S" "x' \ carrier S" "y \ carrier S"
shows "{x, y} {.=} {x', y}"
unfolding set_eq_def elem_def
proof safe
have "x' \ {x', y}" by fast
with xx' show "\b\{x', y}. x .= b" by fast
next
have "y \ {x', y}" by fast
with carr show "\b\{x', y}. y .= b" by fast
next
have "x \ {x, y}" by fast
with xx'[symmetric] carr
show "\a\{x, y}. x' .= a" by fast
next
have "y \ {x, y}" by fast
with carr show "\a\{x, y}. y .= a" by fast
qed
lemma (in equivalence) is_closedI:
assumes closed: "!!x y. [| x .= y; x \ A; y \ carrier S |] ==> y \ A"
and S: "A \ carrier S"
shows "is_closed A"
unfolding eq_is_closed_def eq_closure_of_def elem_def
using S
by (blast dest: closed sym)
lemma (in equivalence) closure_of_eq:
"[| x .= x'; A \ carrier S; x \ closure_of A; x \ carrier S; x' \ carrier S |] ==> x' \ closure_of A"
unfolding eq_closure_of_def elem_def
by (blast intro: trans sym)
lemma (in equivalence) is_closed_eq [dest]:
"[| x .= x'; x \ A; is_closed A; x \ carrier S; x' \ carrier S |] ==> x' \ A"
unfolding eq_is_closed_def
using closure_of_eq [where A = A]
by simp
lemma (in equivalence) is_closed_eq_rev [dest]:
"[| x .= x'; x' \ A; is_closed A; x \ carrier S; x' \ carrier S |] ==> x \ A"
by (drule sym) (simp_all add: is_closed_eq)
lemma closure_of_closed [simp, intro]:
fixes S (structure)
shows "closure_of A \ carrier S"
unfolding eq_closure_of_def
by fast
lemma closure_of_memI:
fixes S (structure)
assumes "a .\ A"
and "a \ carrier S"
shows "a \ closure_of A"
unfolding eq_closure_of_def
using assms
by fast
lemma closure_ofI2:
fixes S (structure)
assumes "a .= a'"
and "a' \ A"
and "a \ carrier S"
shows "a \ closure_of A"
unfolding eq_closure_of_def elem_def
using assms
by fast
lemma closure_of_memE:
fixes S (structure)
assumes p: "a \ closure_of A"
and r: "\a \ carrier S; a .\ A\ \ P"
shows "P"
proof -
from p
have acarr: "a \ carrier S"
and "a .\ A"
by (simp add: eq_closure_of_def)+
thus "P" by (rule r)
qed
lemma closure_ofE2:
fixes S (structure)
assumes p: "a \ closure_of A"
and r: "\a'. \a \ carrier S; a' \ A; a .= a'\ \