Quelle  FrecR.thy

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
  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+_\<omega>2,0),singleton_fm(0,1)),
                                       is_eclose_fm(1,m+_\<omega>2))))"

definition
  eclose_n2_fm :: "[i,i] ==> i" where
  "eclose_n2_fm(m,t) ≡ Exists(Exists(And(And(name2_fm(t+_\<omega>2,0),singleton_fm(0,1)),
                                       is_eclose_fm(1,m+_\<omega>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+_\<omega>2),
                            And(eclose_n2_fm(0,t+_\<omega>2),union_fm(1,0,en+_\<omega>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'⟩)"
  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