section‹Well-founded relation on names›
theory FrecR imports Names Synthetic_Definition begin
lemmas sep_rules' = nth_0 nth_ConsI FOL_iff_sats function_iff_sats
fun_plus_iff_sats
omega_iff_sats FOL_sats_iff
text‹\<^term>‹frecR› is the well-founded relation on names that allows
us to define forcing for atomic formulas.›
definition
is_hcomp :: "[i⇒o,i⇒i⇒o,i⇒i⇒o,i,i] ⇒ o" where
"is_hcomp(M,is_f,is_g,a,w) == ∃z[M]. is_g(a,z) ∧ is_f(z,w)"
lemma (in M_trivial) hcomp_abs:
assumes
is_f_abs:"⋀a z. M(a) ⟹ M(z) ⟹ is_f(a,z) ⟷ z = f(a)" and
is_g_abs:"⋀a z. M(a) ⟹ M(z) ⟹ is_g(a,z) ⟷ z = g(a)" and
g_closed:"⋀a. M(a) ⟹ M(g(a))"
"M(a)" "M(w)"
shows
"is_hcomp(M,is_f,is_g,a,w) ⟷ w = f(g(a))"
unfolding is_hcomp_def using assms by simp
definition
hcomp_fm :: "[i⇒i⇒i,i⇒i⇒i,i,i] ⇒ i" where
"hcomp_fm(pf,pg,a,w) ≡ Exists(And(pg(succ(a),0),pf(0,succ(w))))"
lemma sats_hcomp_fm:
assumes
f_iff_sats:"⋀a b z. a∈nat ⟹ b∈nat ⟹ z∈M ⟹
is_f(nth(a,Cons(z,env)),nth(b,Cons(z,env))) ⟷ sats(M,pf(a,b),Cons(z,env))"
and
g_iff_sats:"⋀a b z. a∈nat ⟹ b∈nat ⟹ z∈M ⟹
is_g(nth(a,Cons(z,env)),nth(b,Cons(z,env))) ⟷ sats(M,pg(a,b),Cons(z,env))"
and
"a∈nat" "w∈nat" "env∈list(M)"
shows
"sats(M,hcomp_fm(pf,pg,a,w),env) ⟷ is_hcomp(##M,is_f,is_g,nth(a,env),nth(w,env))"
proof -
have "sats(M, pf(0, succ(w)), Cons(x, env)) ⟷ is_f(x,nth(w,env))" if "x∈M" "w∈nat" for x w
using f_iff_sats[of 0 "succ(w)" x] that by simp
moreover
have "sats(M, pg(succ(a), 0), Cons(x, env)) ⟷ is_g(nth(a,env),x)" if "x∈M" "a∈nat" for x a
using g_iff_sats[of "succ(a)" 0 x] that by simp
ultimately
show ?thesis unfolding hcomp_fm_def is_hcomp_def using assms by simp
qed
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)"
shows "x ∈ ecloseN(<f,n1,n2,c>)"
proof -
from assms
have "x∈eclose({n1})"
using eclose_sing by simp
then show "x ∈ ecloseN(<f,n1,n2,c>)"
unfolding ecloseN_def eclose_n_def
using names_simp
by simp
qed
lemma ecloseNI2 :
assumes "y ∈ eclose(n2)"
shows "y ∈ ecloseN(<f,n1,n2,c>)"
proof -
from assms
have "y∈eclose({n2})"
using eclose_sing by simp_all
then show "y ∈ ecloseN(<f,n1,n2,c>)"
unfolding ecloseN_def eclose_n_def
using names_simp
by simp
qed
lemmas ecloseNI = ecloseNI1 ecloseNI2
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_fst :: "(i⇒o)⇒i⇒i⇒o" where
"is_fst(M,x,t) == (∃z[M]. pair(M,t,z,x)) ∨
(¬(∃z[M]. ∃w[M]. pair(M,w,z,x)) ∧ empty(M,t))"
definition
fst_fm :: "[i,i] ⇒ i" where
"fst_fm(x,t) ≡ Or(Exists(pair_fm(succ(t),0,succ(x))),
And(Neg(Exists(Exists(pair_fm(0,1,2 #+ x)))),empty_fm(t)))"
lemma sats_fst_fm :
"⟦ x ∈ nat; y ∈ nat;env ∈ list(A) ⟧
⟹ sats(A, fst_fm(x,y), env) ⟷
is_fst(##A, nth(x,env), nth(y,env))"
by (simp add: fst_fm_def is_fst_def)
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 sats_ftype_fm :
"⟦ x ∈ nat; y ∈ nat;env ∈ list(A) ⟧
⟹ sats(A, ftype_fm(x,y), env) ⟷
is_ftype(##A, nth(x,env), nth(y,env))"
unfolding ftype_fm_def is_ftype_def
by (simp add:sats_fst_fm)
lemma is_ftype_iff_sats:
assumes
"nth(a,env) = aa" "nth(b,env) = bb" "a∈nat" "b∈nat" "env ∈ list(A)"
shows
"is_ftype(##A,aa,bb) ⟷ sats(A,ftype_fm(a,b), env)"
using assms
by (simp add:sats_ftype_fm)
definition
is_snd :: "(i⇒o)⇒i⇒i⇒o" where
"is_snd(M,x,t) == (∃z[M]. pair(M,z,t,x)) ∨
(¬(∃z[M]. ∃w[M]. pair(M,z,w,x)) ∧ empty(M,t))"
definition
snd_fm :: "[i,i] ⇒ i" where
"snd_fm(x,t) ≡ Or(Exists(pair_fm(0,succ(t),succ(x))),
And(Neg(Exists(Exists(pair_fm(1,0,2 #+ x)))),empty_fm(t)))"
lemma sats_snd_fm :
"⟦ x ∈ nat; y ∈ nat;env ∈ list(A) ⟧
⟹ sats(A, snd_fm(x,y), env) ⟷
is_snd(##A, nth(x,env), nth(y,env))"
by (simp add: snd_fm_def is_snd_def)
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 :
"⟦ x ∈ nat; y ∈ nat;env ∈ list(A) ⟧
⟹ sats(A, name1_fm(x,y), env) ⟷
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:
assumes
"nth(a,env) = aa" "nth(b,env) = bb" "a∈nat" "b∈nat" "env ∈ list(A)"
shows
"is_name1(##A,aa,bb) ⟷ sats(A,name1_fm(a,b), env)"
using assms
by (simp add:sats_name1_fm)
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 :
"⟦ x ∈ nat; y ∈ nat;env ∈ list(A) ⟧
⟹ sats(A,snd_snd_fm(x,y), env) ⟷
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) ⟧
⟹ sats(A,name2_fm(x,y), env) ⟷
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:
assumes
"nth(a,env) = aa" "nth(b,env) = bb" "a∈nat" "b∈nat" "env ∈ list(A)"
shows
"is_name2(##A,aa,bb) ⟷ sats(A,name2_fm(a,b), env)"
using assms
by (simp add:sats_name2_fm)
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) ⟧
⟹ sats(A,cond_of_fm(x,y), env) ⟷
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:
assumes
"nth(a,env) = aa" "nth(b,env) = bb" "a∈nat" "b∈nat" "env ∈ list(A)"
shows
"is_cond_of(##A,aa,bb) ⟷ sats(A,cond_of_fm(a,b), env)"
using assms
by (simp add:sats_cond_of_fm)
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 sats_components_fm = sats_ftype_fm sats_name1_fm sats_name2_fm sats_cond_of_fm
lemmas components_iff_sats = is_ftype_iff_sats is_name1_iff_sats is_name2_iff_sats
is_cond_of_iff_sats
lemmas components_defs = fst_fm_def ftype_fm_def snd_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,en,t) == ∃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)|]
==> sats(A, ecloseN_fm(en,t), env) ⟷ is_ecloseN(##A,nth(en,env),nth(t,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
is_singleton_iff_sats[symmetric]
by auto
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_iff :
"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)))"
unfolding frecR_def ..
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)))"
using frecR_iff
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))"
using frecR_iff
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)
definition
is_frecR :: "[i⇒o,i,i] ⇒ o" where
"is_frecR(M,x,y) ≡ ∃ ftx[M]. ∃ n1x[M]. ∃n2x[M]. ∃fty[M]. ∃n1y[M]. ∃n2y[M]. ∃dn1[M]. ∃dn2[M].
is_ftype(M,x,ftx) ∧ is_name1(M,x,n1x)∧ is_name2(M,x,n2x) ∧
is_ftype(M,y,fty) ∧ is_name1(M,y,n1y) ∧ is_name2(M,y,n2y)
∧ is_domain(M,n1y,dn1) ∧ is_domain(M,n2y,dn2) ∧
( (number1(M,ftx) ∧ empty(M,fty) ∧ (n1x ∈ dn1 ∨ n1x ∈ dn2) ∧ (n2x = n1y ∨ n2x = n2y))
∨ (empty(M,ftx) ∧ number1(M,fty) ∧ n1x = n1y ∧ n2x ∈ dn2))"
schematic_goal sats_frecR_fm_auto:
assumes
"a∈nat" "b∈nat" "env∈list(A)"
shows
"is_frecR(##A,nth(a,env),nth(b,env)) ⟷ sats(A,?fr_fm(a),env)"
unfolding is_frecR_def is_Collect_def
by (insert assms ; (rule sep_rules' cartprod_iff_sats components_iff_sats
| simp del:sats_cartprod_fm)+)
synthesize "frecR_fm" from_schematic "sats_frecR_fm_auto"
lemma frecR_fm_type[TC] :
"⟦a∈nat;b∈nat⟧ ⟹ frecR_fm(a,b)∈formula"
unfolding frecR_fm_def by simp
lemma sats_frecR_fm :
assumes "a∈nat" "b∈nat" "env∈list(A)"
shows "sats(A,frecR_fm(a,b),env) ⟷ is_frecR(##A,nth(a,env),nth(b,env))"
unfolding is_frecR_def frecR_fm_def
using assms by (simp add: sats_components_fm)
lemma is_frecR_iff_sats:
assumes
"nth(a,env) = aa" "nth(b,env) = bb" "a∈nat" "b∈nat" "env ∈ list(A)"
shows
"is_frecR(##A,aa,bb) ⟷ sats(A, frecR_fm(a,b), env)"
using assms
by (simp add:sats_frecR_fm)
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
then
have "type_form(y) = 1"
using type_form_def by simp
from b
have H: "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
then
have E: "rank(?τ) = rank(?σ') ∨ rank(?τ) = rank(?τ')" by auto
from H
consider (a) "rank(?σ) < rank(?σ')" | (b) "rank(?σ) < rank(?τ')"
using eclose_rank_lt in_dom_in_eclose by force
then
have "rank(?σ) < rank(?τ)" proof (cases)
case a
with ‹rank_names(x) = rank_names(y) ›
show ?thesis unfolding rank_names_def mtype_form_def type_form_def using max_D2[OF E a]
E assms Ord_rank by simp
next
case b
with ‹rank_names(x) = rank_names(y) ›
show ?thesis unfolding rank_names_def mtype_form_def type_form_def
using max_D2[OF _ b] max_commutes E assms Ord_rank disj_commute by auto
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(?σ')"
unfolding rank_names_def using Ord_rank max_D1 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 A: "?τ∈A1" "?θ∈A1" "?τ∈eclose(A1)" "?θ∈eclose(A1)"
using arg_into_eclose by (auto simp add:components_simp)
with ‹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 A:"Q(1, σ, ?τ, q)" using 1 by (force simp add:components_simp)
from ‹q∈A2› ‹σ∈A1› ‹?τ∈A1› ‹?θ∈A1› ‹<?U,x>∈ frecrel(?D)›
have "Q(1, σ, ?θ, q)" using 1 by (force simp add:components_simp)
then
show ?thesis using A by simp
qed
then show ?thesis using assms(3) ‹ftype(x) = 0› ‹cond_of(x)∈A2› by auto
next
case mem
have "Q(0, ?τ, σ, q)" if "σ ∈ domain(?θ)" and "q∈A2" for q σ
proof -
from 1 assms
have A: "?τ∈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›
have "frecR(<0, ?τ, σ, q>, x)" (is "frecR(?T,_)")
using frecRI3'[OF that(1)] frecR_DI ‹ftype(x) = 1›
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›
show ?thesis using 1 by (force simp add:components_simp)
qed
then show ?thesis using assms(2) ‹ftype(x) = 1› ‹cond_of(x)∈A2› 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