Theory FrecR
section‹Well-founded relation on names›
theory FrecR
imports
Transitive_Models.Discipline_Function
Edrel
begin
text‹\<^term>‹frecR› is the well-founded relation on names that allows
us to define forcing for atomic formulas.›
definition
ftype :: "i⇒i" where
"ftype ≡ fst"
definition
name1 :: "i⇒i" where
"name1(x) ≡ fst(snd(x))"
definition
name2 :: "i⇒i" where
"name2(x) ≡ fst(snd(snd(x)))"
definition
cond_of :: "i⇒i" where
"cond_of(x) ≡ snd(snd(snd((x))))"
lemma components_simp:
"ftype(⟨f,n1,n2,c⟩) = f"
"name1(⟨f,n1,n2,c⟩) = n1"
"name2(⟨f,n1,n2,c⟩) = n2"
"cond_of(⟨f,n1,n2,c⟩) = c"
unfolding ftype_def name1_def name2_def cond_of_def
by simp_all
definition eclose_n :: "[i⇒i,i] ⇒ i" where
"eclose_n(name,x) = eclose({name(x)})"
definition
ecloseN :: "i ⇒ i" where
"ecloseN(x) = eclose_n(name1,x) ∪ eclose_n(name2,x)"
lemma components_in_eclose :
"n1 ∈ ecloseN(⟨f,n1,n2,c⟩)"
"n2 ∈ ecloseN(⟨f,n1,n2,c⟩)"
unfolding ecloseN_def eclose_n_def
using components_simp arg_into_eclose by auto
lemmas names_simp = components_simp(2) components_simp(3)
lemma ecloseNI1 :
assumes "x ∈ eclose(n1) ∨ x∈eclose(n2)"
shows "x ∈ ecloseN(⟨f,n1,n2,c⟩)"
unfolding ecloseN_def eclose_n_def
using assms eclose_sing names_simp
by auto
lemmas ecloseNI = ecloseNI1
lemma ecloseN_mono :
assumes "u ∈ ecloseN(x)" "name1(x) ∈ ecloseN(y)" "name2(x) ∈ ecloseN(y)"
shows "u ∈ ecloseN(y)"
proof -
from ‹u∈_›
consider (a) "u∈eclose({name1(x)})" | (b) "u ∈ eclose({name2(x)})"
unfolding ecloseN_def eclose_n_def by auto
then
show ?thesis
proof cases
case a
with ‹name1(x) ∈ _›
show ?thesis
unfolding ecloseN_def eclose_n_def
using eclose_singE[OF a] mem_eclose_trans[of u "name1(x)" ] by auto
next
case b
with ‹name2(x) ∈ _›
show ?thesis
unfolding ecloseN_def eclose_n_def
using eclose_singE[OF b] mem_eclose_trans[of u "name2(x)"] by auto
qed
qed
definition
is_ftype :: "(i⇒o)⇒i⇒i⇒o" where
"is_ftype ≡ is_fst"
definition
ftype_fm :: "[i,i] ⇒ i" where
"ftype_fm ≡ fst_fm"
lemma is_ftype_iff_sats [iff_sats]:
assumes
"nth(a,env) = x" "nth(b,env) = y" "a∈nat" "b∈nat" "env ∈ list(A)"
shows
"is_ftype(##A,x,y) ⟷ sats(A,ftype_fm(a,b), env)"
unfolding ftype_fm_def is_ftype_def
using assms sats_fst_fm
by simp
definition
is_name1 :: "(i⇒o)⇒i⇒i⇒o" where
"is_name1(M,x,t2) ≡ is_hcomp(M,is_fst(M),is_snd(M),x,t2)"
definition
name1_fm :: "[i,i] ⇒ i" where
"name1_fm(x,t) ≡ hcomp_fm(fst_fm,snd_fm,x,t)"
lemma sats_name1_fm [simp]:
"⟦ x ∈ nat; y ∈ nat;env ∈ list(A) ⟧ ⟹
(A, env ⊨ name1_fm(x,y)) ⟷ is_name1(##A, nth(x,env), nth(y,env))"
unfolding name1_fm_def is_name1_def
using sats_fst_fm sats_snd_fm sats_hcomp_fm[of A "is_fst(##A)" _ fst_fm "is_snd(##A)"]
by simp
lemma is_name1_iff_sats [iff_sats]:
assumes
"nth(a,env) = x" "nth(b,env) = y" "a∈nat" "b∈nat" "env ∈ list(A)"
shows
"is_name1(##A,x,y) ⟷ A , env ⊨ name1_fm(a,b)"
using assms sats_name1_fm
by simp
definition
is_snd_snd :: "(i⇒o)⇒i⇒i⇒o" where
"is_snd_snd(M,x,t) ≡ is_hcomp(M,is_snd(M),is_snd(M),x,t)"
definition
snd_snd_fm :: "[i,i]⇒i" where
"snd_snd_fm(x,t) ≡ hcomp_fm(snd_fm,snd_fm,x,t)"
lemma sats_snd2_fm [simp]:
"⟦ x ∈ nat; y ∈ nat;env ∈ list(A) ⟧ ⟹
(A, env ⊨ snd_snd_fm(x,y)) ⟷ is_snd_snd(##A, nth(x,env), nth(y,env))"
unfolding snd_snd_fm_def is_snd_snd_def
using sats_snd_fm sats_hcomp_fm[of A "is_snd(##A)" _ snd_fm "is_snd(##A)"]
by simp
definition
is_name2 :: "(i⇒o)⇒i⇒i⇒o" where
"is_name2(M,x,t3) ≡ is_hcomp(M,is_fst(M),is_snd_snd(M),x,t3)"
definition
name2_fm :: "[i,i] ⇒ i" where
"name2_fm(x,t3) ≡ hcomp_fm(fst_fm,snd_snd_fm,x,t3)"
lemma sats_name2_fm :
"⟦ x ∈ nat; y ∈ nat;env ∈ list(A) ⟧
⟹ (A , env ⊨ name2_fm(x,y)) ⟷ is_name2(##A, nth(x,env), nth(y,env))"
unfolding name2_fm_def is_name2_def
using sats_fst_fm sats_snd2_fm sats_hcomp_fm[of A "is_fst(##A)" _ fst_fm "is_snd_snd(##A)"]
by simp
lemma is_name2_iff_sats [iff_sats]:
assumes
"nth(a,env) = x" "nth(b,env) = y" "a∈nat" "b∈nat" "env ∈ list(A)"
shows
"is_name2(##A,x,y) ⟷ A, env ⊨ name2_fm(a,b)"
using assms sats_name2_fm
by simp
definition
is_cond_of :: "(i⇒o)⇒i⇒i⇒o" where
"is_cond_of(M,x,t4) ≡ is_hcomp(M,is_snd(M),is_snd_snd(M),x,t4)"
definition
cond_of_fm :: "[i,i] ⇒ i" where
"cond_of_fm(x,t4) ≡ hcomp_fm(snd_fm,snd_snd_fm,x,t4)"
lemma sats_cond_of_fm :
"⟦ x ∈ nat; y ∈ nat;env ∈ list(A) ⟧ ⟹
(A, env ⊨ cond_of_fm(x,y)) ⟷ is_cond_of(##A, nth(x,env), nth(y,env))"
unfolding cond_of_fm_def is_cond_of_def
using sats_snd_fm sats_snd2_fm sats_hcomp_fm[of A "is_snd(##A)" _ snd_fm "is_snd_snd(##A)"]
by simp
lemma is_cond_of_iff_sats [iff_sats]:
assumes
"nth(a,env) = x" "nth(b,env) = y" "a∈nat" "b∈nat" "env ∈ list(A)"
shows
"is_cond_of(##A,x,y) ⟷ A, env ⊨ cond_of_fm(a,b)"
using assms sats_cond_of_fm
by simp
lemma components_type[TC] :
assumes "a∈nat" "b∈nat"
shows
"ftype_fm(a,b)∈formula"
"name1_fm(a,b)∈formula"
"name2_fm(a,b)∈formula"
"cond_of_fm(a,b)∈formula"
using assms
unfolding ftype_fm_def fst_fm_def snd_fm_def snd_snd_fm_def name1_fm_def name2_fm_def
cond_of_fm_def hcomp_fm_def
by simp_all
lemmas components_iff_sats = is_ftype_iff_sats is_name1_iff_sats is_name2_iff_sats
is_cond_of_iff_sats
lemmas components_defs = ftype_fm_def snd_snd_fm_def hcomp_fm_def
name1_fm_def name2_fm_def cond_of_fm_def
definition
is_eclose_n :: "[i⇒o,[i⇒o,i,i]⇒o,i,i] ⇒ o" where
"is_eclose_n(N,is_name,en,t) ≡
∃n1[N].∃s1[N]. is_name(N,t,n1) ∧ is_singleton(N,n1,s1) ∧ is_eclose(N,s1,en)"
definition
eclose_n1_fm :: "[i,i] ⇒ i" where
"eclose_n1_fm(m,t) ≡ Exists(Exists(And(And(name1_fm(t+⇩ω2,0),singleton_fm(0,1)),
is_eclose_fm(1,m+⇩ω2))))"
definition
eclose_n2_fm :: "[i,i] ⇒ i" where
"eclose_n2_fm(m,t) ≡ Exists(Exists(And(And(name2_fm(t+⇩ω2,0),singleton_fm(0,1)),
is_eclose_fm(1,m+⇩ω2))))"
definition
is_ecloseN :: "[i⇒o,i,i] ⇒ o" where
"is_ecloseN(N,t,en) ≡ ∃en1[N].∃en2[N].
is_eclose_n(N,is_name1,en1,t) ∧ is_eclose_n(N,is_name2,en2,t)∧
union(N,en1,en2,en)"
definition
ecloseN_fm :: "[i,i] ⇒ i" where
"ecloseN_fm(en,t) ≡ Exists(Exists(And(eclose_n1_fm(1,t+⇩ω2),
And(eclose_n2_fm(0,t+⇩ω2),union_fm(1,0,en+⇩ω2)))))"
lemma ecloseN_fm_type [TC] :
"⟦ en ∈ nat ; t ∈ nat ⟧ ⟹ ecloseN_fm(en,t) ∈ formula"
unfolding ecloseN_fm_def eclose_n1_fm_def eclose_n2_fm_def by simp
lemma sats_ecloseN_fm [simp]:
"⟦ en ∈ nat; t ∈ nat ; env ∈ list(A) ⟧
⟹ (A, env ⊨ ecloseN_fm(en,t)) ⟷ is_ecloseN(##A,nth(t,env),nth(en,env))"
unfolding ecloseN_fm_def is_ecloseN_def eclose_n1_fm_def eclose_n2_fm_def is_eclose_n_def
using nth_0 nth_ConsI sats_name1_fm sats_name2_fm singleton_iff_sats[symmetric]
by auto
lemma is_ecloseN_iff_sats [iff_sats]:
"⟦ nth(en, env) = ena; nth(t, env) = ta; en ∈ nat; t ∈ nat ; env ∈ list(A) ⟧
⟹ is_ecloseN(##A,ta,ena) ⟷ A, env ⊨ ecloseN_fm(en,t)"
by simp
definition
frecR :: "i ⇒ i ⇒ o" where
"frecR(x,y) ≡
(ftype(x) = 1 ∧ ftype(y) = 0
∧ (name1(x) ∈ domain(name1(y)) ∪ domain(name2(y)) ∧ (name2(x) = name1(y) ∨ name2(x) = name2(y))))
∨ (ftype(x) = 0 ∧ ftype(y) = 1 ∧ name1(x) = name1(y) ∧ name2(x) ∈ domain(name2(y)))"
lemma frecR_ftypeD :
assumes "frecR(x,y)"
shows "(ftype(x) = 0 ∧ ftype(y) = 1) ∨ (ftype(x) = 1 ∧ ftype(y) = 0)"
using assms unfolding frecR_def by auto
lemma frecRI1: "s ∈ domain(n1) ∨ s ∈ domain(n2) ⟹ frecR(⟨1, s, n1, q⟩, ⟨0, n1, n2, q'⟩)"
unfolding frecR_def by (simp add:components_simp)
lemma frecRI1': "s ∈ domain(n1) ∪ domain(n2) ⟹ frecR(⟨1, s, n1, q⟩, ⟨0, n1, n2, q'⟩)"
unfolding frecR_def by (simp add:components_simp)
lemma frecRI2: "s ∈ domain(n1) ∨ s ∈ domain(n2) ⟹ frecR(⟨1, s, n2, q⟩, ⟨0, n1, n2, q'⟩)"
unfolding frecR_def by (simp add:components_simp)
lemma frecRI2': "s ∈ domain(n1) ∪ domain(n2) ⟹ frecR(⟨1, s, n2, q⟩, ⟨0, n1, n2, q'⟩)"
unfolding frecR_def by (simp add:components_simp)
lemma frecRI3: "⟨s, r⟩ ∈ n2 ⟹ frecR(⟨0, n1, s, q⟩, ⟨1, n1, n2, q'⟩)"
unfolding frecR_def by (auto simp add:components_simp)
lemma frecRI3': "s ∈ domain(n2) ⟹ frecR(⟨0, n1, s, q⟩, ⟨1, n1, n2, q'⟩)"
unfolding frecR_def by (auto simp add:components_simp)
lemma frecR_D1 :
"frecR(x,y) ⟹ ftype(y) = 0 ⟹ ftype(x) = 1 ∧
(name1(x) ∈ domain(name1(y)) ∪ domain(name2(y)) ∧ (name2(x) = name1(y) ∨ name2(x) = name2(y)))"
unfolding frecR_def
by auto
lemma frecR_D2 :
"frecR(x,y) ⟹ ftype(y) = 1 ⟹ ftype(x) = 0 ∧
ftype(x) = 0 ∧ ftype(y) = 1 ∧ name1(x) = name1(y) ∧ name2(x) ∈ domain(name2(y))"
unfolding frecR_def
by auto
lemma frecR_DI :
assumes "frecR(⟨a,b,c,d⟩,⟨ftype(y),name1(y),name2(y),cond_of(y)⟩)"
shows "frecR(⟨a,b,c,d⟩,y)"
using assms
unfolding frecR_def
by (force simp add:components_simp)
reldb_add "ftype" "is_ftype"
reldb_add "name1" "is_name1"
reldb_add "name2" "is_name2"
relativize "frecR" "is_frecR"
schematic_goal sats_frecR_fm_auto:
assumes
"i∈nat" "j∈nat" "env∈list(A)"
shows
"is_frecR(##A,nth(i,env),nth(j,env)) ⟷ A, env ⊨ ?fr_fm(i,j)"
unfolding is_frecR_def
by (insert assms ; (rule sep_rules' cartprod_iff_sats components_iff_sats
| simp del:sats_cartprod_fm)+)
synthesize "frecR" from_schematic sats_frecR_fm_auto
text‹Third item of Kunen's observations (p. 257) about the trcl relation.›
lemma eq_ftypep_not_frecrR:
assumes "ftype(x) = ftype(y)"
shows "¬ frecR(x,y)"
using assms frecR_ftypeD by force
definition
rank_names :: "i ⇒ i" where
"rank_names(x) ≡ max(rank(name1(x)),rank(name2(x)))"
lemma rank_names_types [TC]:
shows "Ord(rank_names(x))"
unfolding rank_names_def max_def using Ord_rank Ord_Un by auto
definition
mtype_form :: "i ⇒ i" where
"mtype_form(x) ≡ if rank(name1(x)) < rank(name2(x)) then 0 else 2"
definition
type_form :: "i ⇒ i" where
"type_form(x) ≡ if ftype(x) = 0 then 1 else mtype_form(x)"
lemma type_form_tc [TC]:
shows "type_form(x) ∈ 3"
unfolding type_form_def mtype_form_def by auto
lemma frecR_le_rnk_names :
assumes "frecR(x,y)"
shows "rank_names(x)≤rank_names(y)"
proof -
obtain a b c d where
H: "a = name1(x)" "b = name2(x)"
"c = name1(y)" "d = name2(y)"
"(a ∈ domain(c)∪domain(d) ∧ (b=c ∨ b = d)) ∨ (a = c ∧ b ∈ domain(d))"
using assms
unfolding frecR_def
by force
then
consider
(m) "a ∈ domain(c) ∧ (b = c ∨ b = d) "
| (n) "a ∈ domain(d) ∧ (b = c ∨ b = d)"
| (o) "b ∈ domain(d) ∧ a = c"
by auto
then
show ?thesis
proof(cases)
case m
then
have "rank(a) < rank(c)"
using eclose_rank_lt in_dom_in_eclose
by simp
with ‹rank(a) < rank(c)› H m
show ?thesis
unfolding rank_names_def
using Ord_rank max_cong max_cong2 leI
by auto
next
case n
then
have "rank(a) < rank(d)"
using eclose_rank_lt in_dom_in_eclose
by simp
with ‹rank(a) < rank(d)› H n
show ?thesis
unfolding rank_names_def
using Ord_rank max_cong2 max_cong max_commutes[of "rank(c)" "rank(d)"] leI
by auto
next
case o
then
have "rank(b) < rank(d)" (is "?b < ?d") "rank(a) = rank(c)" (is "?a = _")
using eclose_rank_lt in_dom_in_eclose
by simp_all
with H
show ?thesis
unfolding rank_names_def
using Ord_rank max_commutes max_cong2[OF leI[OF ‹?b < ?d›], of ?a]
by simp
qed
qed
definition
Γ :: "i ⇒ i" where
"Γ(x) = 3 ** rank_names(x) ++ type_form(x)"
lemma Γ_type [TC]:
shows "Ord(Γ(x))"
unfolding Γ_def by simp
lemma Γ_mono :
assumes "frecR(x,y)"
shows "Γ(x) < Γ(y)"
proof -
have F: "type_form(x) < 3" "type_form(y) < 3"
using ltI
by simp_all
from assms
have A: "rank_names(x) ≤ rank_names(y)" (is "?x ≤ ?y")
using frecR_le_rnk_names
by simp
then
have "Ord(?y)"
unfolding rank_names_def
using Ord_rank max_def
by simp
note leE[OF ‹?x≤?y›]
then
show ?thesis
proof(cases)
case 1
then
show ?thesis
unfolding Γ_def
using oadd_lt_mono2 ‹?x < ?y› F
by auto
next
case 2
consider (a) "ftype(x) = 0 ∧ ftype(y) = 1" | (b) "ftype(x) = 1 ∧ ftype(y) = 0"
using frecR_ftypeD[OF ‹frecR(x,y)›]
by auto
then show ?thesis
proof(cases)
case b
moreover from this
have "type_form(y) = 1"
using type_form_def by simp
moreover from calculation
have "name2(x) = name1(y) ∨ name2(x) = name2(y) " (is "?τ = ?σ' ∨ ?τ = ?τ'")
"name1(x) ∈ domain(name1(y)) ∪ domain(name2(y))" (is "?σ ∈ domain(?σ') ∪ domain(?τ')")
using assms unfolding type_form_def frecR_def by auto
moreover from calculation
have E: "rank(?τ) = rank(?σ') ∨ rank(?τ) = rank(?τ')" by auto
from calculation
consider (c) "rank(?σ) < rank(?σ')" | (d) "rank(?σ) < rank(?τ')"
using eclose_rank_lt in_dom_in_eclose by force
then
have "rank(?σ) < rank(?τ)"
proof (cases)
case c
with ‹rank_names(x) = rank_names(y) ›
show ?thesis
unfolding rank_names_def mtype_form_def type_form_def
using max_D2[OF E c] E assms Ord_rank
by simp
next
case d
with ‹rank_names(x) = rank_names(y) ›
show ?thesis
unfolding rank_names_def mtype_form_def type_form_def
using max_D2[OF _ d] max_commutes E assms Ord_rank disj_commute
by simp
qed
with b
have "type_form(x) = 0" unfolding type_form_def mtype_form_def by simp
with ‹rank_names(x) = rank_names(y) › ‹type_form(y) = 1› ‹type_form(x) = 0›
show ?thesis
unfolding Γ_def by auto
next
case a
then
have "name1(x) = name1(y)" (is "?σ = ?σ'")
"name2(x) ∈ domain(name2(y))" (is "?τ ∈ domain(?τ')")
"type_form(x) = 1"
using assms
unfolding type_form_def frecR_def
by auto
then
have "rank(?σ) = rank(?σ')" "rank(?τ) < rank(?τ')"
using eclose_rank_lt in_dom_in_eclose
by simp_all
with ‹rank_names(x) = rank_names(y) ›
have "rank(?τ') ≤ rank(?σ')"
using Ord_rank max_D1
unfolding rank_names_def
by simp
with a
have "type_form(y) = 2"
unfolding type_form_def mtype_form_def
using not_lt_iff_le assms
by simp
with ‹rank_names(x) = rank_names(y) › ‹type_form(y) = 2› ‹type_form(x) = 1›
show ?thesis
unfolding Γ_def by auto
qed
qed
qed
definition
frecrel :: "i ⇒ i" where
"frecrel(A) ≡ Rrel(frecR,A)"
lemma frecrelI :
assumes "x ∈ A" "y∈A" "frecR(x,y)"
shows "⟨x,y⟩∈frecrel(A)"
using assms unfolding frecrel_def Rrel_def by auto
lemma frecrelD :
assumes "⟨x,y⟩ ∈ frecrel(A1×A2×A3×A4)"
shows
"ftype(x) ∈ A1" "ftype(x) ∈ A1"
"name1(x) ∈ A2" "name1(y) ∈ A2"
"name2(x) ∈ A3" "name2(x) ∈ A3"
"cond_of(x) ∈ A4" "cond_of(y) ∈ A4"
"frecR(x,y)"
using assms
unfolding frecrel_def Rrel_def ftype_def by (auto simp add:components_simp)
lemma wf_frecrel :
shows "wf(frecrel(A))"
proof -
have "frecrel(A) ⊆ measure(A,Γ)"
unfolding frecrel_def Rrel_def measure_def
using Γ_mono
by force
then
show ?thesis
using wf_subset wf_measure by auto
qed
lemma core_induction_aux:
fixes A1 A2 :: "i"
assumes
"Transset(A1)"
"⋀τ θ p. p ∈ A2 ⟹ ⟦⋀q σ. ⟦ q∈A2 ; σ∈domain(θ)⟧ ⟹ Q(0,τ,σ,q)⟧ ⟹ Q(1,τ,θ,p)"
"⋀τ θ p. p ∈ A2 ⟹ ⟦⋀q σ. ⟦ q∈A2 ; σ∈domain(τ) ∪ domain(θ)⟧ ⟹ Q(1,σ,τ,q) ∧ Q(1,σ,θ,q)⟧ ⟹ Q(0,τ,θ,p)"
shows "a∈2×A1×A1×A2 ⟹ Q(ftype(a),name1(a),name2(a),cond_of(a))"
proof (induct a rule:wf_induct[OF wf_frecrel[of "2×A1×A1×A2"]])
case (1 x)
let ?τ = "name1(x)"
let ?θ = "name2(x)"
let ?D = "2×A1×A1×A2"
assume "x ∈ ?D"
then
have "cond_of(x)∈A2"
by (auto simp add:components_simp)
from ‹x∈?D›
consider (eq) "ftype(x)=0" | (mem) "ftype(x)=1"
by (auto simp add:components_simp)
then
show ?case
proof cases
case eq
then
have "Q(1, σ, ?τ, q) ∧ Q(1, σ, ?θ, q)" if "σ ∈ domain(?τ) ∪ domain(?θ)" and "q∈A2" for q σ
proof -
from 1
have "?τ∈A1" "?θ∈A1" "?τ∈eclose(A1)" "?θ∈eclose(A1)"
using arg_into_eclose
by (auto simp add:components_simp)
moreover from ‹Transset(A1)› that(1)
have "σ∈eclose(?τ) ∪ eclose(?θ)"
using in_dom_in_eclose
by auto
then
have "σ∈A1"
using mem_eclose_subset[OF ‹?τ∈A1›] mem_eclose_subset[OF ‹?θ∈A1›]
Transset_eclose_eq_arg[OF ‹Transset(A1)›]
by auto
with ‹q∈A2› ‹?θ ∈ A1› ‹cond_of(x)∈A2› ‹?τ∈A1›
have "frecR(⟨1, σ, ?τ, q⟩, x)" (is "frecR(?T,_)")
"frecR(⟨1, σ, ?θ, q⟩, x)" (is "frecR(?U,_)")
using frecRI1'[OF that(1)] frecR_DI ‹ftype(x) = 0›
frecRI2'[OF that(1)]
by (auto simp add:components_simp)
with ‹x∈?D› ‹σ∈A1› ‹q∈A2›
have "⟨?T,x⟩∈ frecrel(?D)" "⟨?U,x⟩∈ frecrel(?D)"
using frecrelI[of ?T ?D x] frecrelI[of ?U ?D x]
by (auto simp add:components_simp)
with ‹q∈A2› ‹σ∈A1› ‹?τ∈A1› ‹?θ∈A1›
have "Q(1, σ, ?τ, q)"
using 1
by (force simp add:components_simp)
moreover from ‹q∈A2› ‹σ∈A1› ‹?τ∈A1› ‹?θ∈A1› ‹⟨?U,x⟩∈ frecrel(?D)›
have "Q(1, σ, ?θ, q)"
using 1 by (force simp add:components_simp)
ultimately
show ?thesis
by simp
qed
with assms(3) ‹ftype(x) = 0› ‹cond_of(x)∈A2›
show ?thesis
by auto
next
case mem
have "Q(0, ?τ, σ, q)" if "σ ∈ domain(?θ)" and "q∈A2" for q σ
proof -
from 1 assms
have "?τ∈A1" "?θ∈A1" "cond_of(x)∈A2" "?τ∈eclose(A1)" "?θ∈eclose(A1)"
using arg_into_eclose
by (auto simp add:components_simp)
with ‹Transset(A1)› that(1)
have "σ∈ eclose(?θ)"
using in_dom_in_eclose
by auto
then
have "σ∈A1"
using mem_eclose_subset[OF ‹?θ∈A1›] Transset_eclose_eq_arg[OF ‹Transset(A1)›]
by auto
with ‹q∈A2› ‹?θ ∈ A1› ‹cond_of(x)∈A2› ‹?τ∈A1› ‹ftype(x) = 1›
have "frecR(⟨0, ?τ, σ, q⟩, x)" (is "frecR(?T,_)")
using frecRI3'[OF that(1)] frecR_DI
by (auto simp add:components_simp)
with ‹x∈?D› ‹σ∈A1› ‹q∈A2› ‹?τ∈A1›
have "⟨?T,x⟩∈ frecrel(?D)" "?T∈?D"
using frecrelI[of ?T ?D x]
by (auto simp add:components_simp)
with ‹q∈A2› ‹σ∈A1› ‹?τ∈A1› ‹?θ∈A1› 1
show ?thesis
by (force simp add:components_simp)
qed
with assms(2) ‹ftype(x) = 1› ‹cond_of(x)∈A2›
show ?thesis
by auto
qed
qed
lemma def_frecrel : "frecrel(A) = {z∈A×A. ∃x y. z = ⟨x, y⟩ ∧ frecR(x,y)}"
unfolding frecrel_def Rrel_def ..
lemma frecrel_fst_snd:
"frecrel(A) = {z ∈ A×A .
ftype(fst(z)) = 1 ∧
ftype(snd(z)) = 0 ∧ name1(fst(z)) ∈ domain(name1(snd(z))) ∪ domain(name2(snd(z))) ∧
(name2(fst(z)) = name1(snd(z)) ∨ name2(fst(z)) = name2(snd(z)))
∨ (ftype(fst(z)) = 0 ∧
ftype(snd(z)) = 1 ∧ name1(fst(z)) = name1(snd(z)) ∧ name2(fst(z)) ∈ domain(name2(snd(z))))}"
unfolding def_frecrel frecR_def
by (intro equalityI subsetI CollectI; elim CollectE; auto)
end