# Theory FrecR

section‹Well-founded relation on names›
theory FrecR
imports
Transitive_Models.Discipline_Function
Edrel
begin

texttermfrecR is the well-founded relation on names that allows
us to define forcing for atomic formulas.›

definition
ftype :: "ii" where
"ftype  fst"

definition
name1 :: "ii" where
"name1(x)  fst(snd(x))"

definition
name2 :: "ii" where
"name2(x)  fst(snd(snd(x)))"

definition
cond_of :: "ii" 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 :: "[ii,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)  xeclose(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) "ueclose({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 :: "(io)iio" 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" "anat" "bnat" "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 :: "(io)iio" 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" "anat" "bnat" "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 :: "(io)iio" 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 :: "(io)iio" 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" "anat" "bnat" "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 :: "(io)iio" 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" "anat" "bnat" "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 "anat" "bnat"
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 :: "[io,[io,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 :: "[io,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

(* Relation of forces *)
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')"

lemma frecRI1': "s  domain(n1)  domain(n2)  frecR(1, s, n1, q, 0, n1, n2, q')"

lemma frecRI2: "s  domain(n1)  s  domain(n2)  frecR(1, s, n2, q, 0, n1, n2, q')"

lemma frecRI2': "s  domain(n1)  domain(n2)  frecR(1, s, n2, q, 0, n1, n2, q')"

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

relativize "frecR" "is_frecR"

schematic_goal sats_frecR_fm_auto:
assumes
"inat" "jnat" "envlist(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" "yA" "frecR(x,y)"
shows "x,yfrecrel(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 σ.  qA2 ; σdomain(θ)  Q(0,τ,σ,q)  Q(1,τ,θ,p)"
"τ θ p.  p  A2  q σ.  qA2 ; σdomain(τ)  domain(θ)  Q(1,σ,τ,q)  Q(1,σ,θ,q)  Q(0,τ,θ,p)"
shows "a2×A1×A1×A2  Q(ftype(a),name1(a),name2(a),cond_of(a))"
proof (induct a rule:wf_induct[OF wf_frecrel[of "A1A1A2"]])
case (1 x)
let  = "name1(x)"
let  = "name2(x)"
let ?D = "2×A1×A1×A2"
assume "x  ?D"
then
have "cond_of(x)A2"
from x?D
consider (eq) "ftype(x)=0" | (mem) "ftype(x)=1"
then
show ?case
proof cases
case eq
then
have "Q(1, σ, , q)  Q(1, σ, , q)" if "σ  domain()  domain()" and "qA2" for q σ
proof -
from 1
have "A1" "A1" "eclose(A1)" "eclose(A1)"
using  arg_into_eclose
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 qA2   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)]
with x?D σA1 qA2
have "?T,x frecrel(?D)" "?U,x frecrel(?D)"
using frecrelI[of ?T ?D x]  frecrelI[of ?U ?D x]
with qA2 σA1 A1 A1
have "Q(1, σ, , q)"
using 1
moreover from qA2 σ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 "qA2" for q σ
proof -
from 1 assms
have "A1" "A1" "cond_of(x)A2" "eclose(A1)" "eclose(A1)"
using arg_into_eclose
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 qA2   A1 cond_of(x)A2 A1 ftype(x) = 1
have "frecR(0, , σ, q, x)" (is "frecR(?T,_)")
using frecRI3'[OF that(1)] frecR_DI
with x?D σA1 qA2 A1
have "?T,x frecrel(?D)" "?T?D"
using frecrelI[of ?T ?D x]
with qA2 σA1 A1 A1 1
show ?thesis
qed
with assms(2) ftype(x) = 1 cond_of(x)A2
show ?thesis
by auto
qed
qed

lemma def_frecrel : "frecrel(A) = {zA×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