Quelle  FrecR.thy

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
  to define forcing for atomic formulas.›

(* MOVE THIS. absoluteness of higher-order composition *)
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


(* Preliminary *)
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


(* ftype(p) \<equiv> THE a. \<exists>b. p = \<langle>a, b\<rangle> *)

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[simp] = 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

(* 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'⟩)"
  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)

(*
name1(x) \<in> domain(name1(y)) \<union> domain(name2(y)) \<and> 
            (name2(x) = name1(y) \<or> name2(x) = name2(y)) 
          \<or> name1(x) = name1(y) \<and> name2(x) \<in> domain(name2(y))*)
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 
    "i∈nat" "j∈nat" "env∈list(A)" "nth(i,env) = a" "nth(j,env) = b"
  shows
    "is_frecR(##A,a,b) ⟷ sats(A,?fr_fm(i,j),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

(* Third item of Kunen observations about the trcl relation in p. 257. *)
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 "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 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 "?τ∈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› 1
      show ?thesis 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