Session Transitive_Models

Theory Nat_Miscellanea

section‹Auxiliary results on arithmetic›

theory Nat_Miscellanea
  imports
    Delta_System_Lemma.ZF_Library
begin

(* no_notation add (infixl ‹#+› 65)
no_notation diff (infixl ‹#-› 65) *)
notation add (infixl ‹+ω› 65)
notation diff (infixl ‹-ω› 65)

text‹Most of these results will get used at some point for the
calculation of arities.›

lemmas nat_succI =  Ord_succ_mem_iff [THEN iffD2,OF nat_into_Ord]

lemma nat_succD : "m ∈ nat ⟹  succ(n) ∈ succ(m) ⟹ n ∈ m"
  by (drule_tac j="succ(m)" in ltI,auto elim:ltD)

lemmas zero_in_succ = ltD [OF nat_0_le]

lemma in_n_in_nat :  "m ∈ nat ⟹ n ∈ m ⟹ n ∈ nat"
  by(drule ltI[of "n"],auto simp add: lt_nat_in_nat)

lemma ltI_neg : "x ∈ nat ⟹ j ≤ x ⟹ j ≠ x ⟹ j < x"
  by (simp add: le_iff)

lemma succ_pred_eq  :  "m ∈ nat ⟹ m ≠ 0  ⟹ succ(pred(m)) = m"
  by (auto elim: natE)

lemma succ_ltI : "succ(j) < n ⟹ j < n"
  by (simp add: succ_leE[OF leI])

lemmas succ_leD = succ_leE[OF leI]

lemma succpred_leI : "n ∈ nat ⟹  n ≤ succ(pred(n))"
  by (auto elim: natE)

lemma succpred_n0 : "succ(n) ∈ p ⟹ p≠0"
  by (auto)

lemmas natEin = natE [OF lt_nat_in_nat]

lemmas Un_least_lt_iffn =  Un_least_lt_iff [OF nat_into_Ord nat_into_Ord]

lemma pred_type : "m ∈ nat ⟹ n ≤ m ⟹ n∈nat"
  by (rule leE,auto simp:in_n_in_nat ltD)

lemma pred_le : "m ∈ nat ⟹ n ≤ succ(m) ⟹ pred(n) ≤ m"
  by(rule_tac n="n" in natE,auto simp add:pred_type[of "succ(m)"])

lemma pred_le2 : "n∈ nat ⟹ m ∈ nat ⟹ pred(n) ≤ m ⟹ n ≤ succ(m)"
  by(subgoal_tac "n∈nat",rule_tac n="n" in natE,auto)

lemma Un_leD1 : "Ord(i)⟹ Ord(j)⟹ Ord(k)⟹  i ∪ j ≤ k ⟹ i ≤ k"
  by (rule Un_least_lt_iff[THEN iffD1[THEN conjunct1]],simp_all)

lemma Un_leD2 : "Ord(i)⟹ Ord(j)⟹ Ord(k)⟹  i ∪ j ≤k ⟹ j ≤ k"
  by (rule Un_least_lt_iff[THEN iffD1[THEN conjunct2]],simp_all)

lemma gt1 : "n ∈ nat ⟹ i ∈ n ⟹ i ≠ 0 ⟹ i ≠ 1 ⟹ 1<i"
  by(rule_tac n="i" in natE,erule in_n_in_nat,auto intro: Ord_0_lt)

lemma pred_mono : "m ∈ nat ⟹ n ≤ m ⟹ pred(n) ≤ pred(m)"
  by(rule_tac n="n" in natE,auto simp add:le_in_nat,erule_tac n="m" in natE,auto)

lemma succ_mono : "m ∈ nat ⟹ n ≤ m ⟹ succ(n) ≤ succ(m)"
  by auto

lemma union_abs1 :
  "⟦ i ≤ j ⟧ ⟹ i ∪ j = j"
  by (rule Un_absorb1,erule le_imp_subset)

lemma union_abs2 :
  "⟦ i ≤ j ⟧ ⟹ j ∪ i = j"
  by (rule Un_absorb2,erule le_imp_subset)

lemma ord_un_max : "Ord(i) ⟹ Ord(j) ⟹ i ∪ j = max(i,j)"
  using max_def union_abs1 not_lt_iff_le leI union_abs2
  by auto

lemma ord_max_ty : "Ord(i) ⟹Ord(j) ⟹ Ord(max(i,j))"
  unfolding max_def by simp

lemmas ord_simp_union = ord_un_max ord_max_ty max_def

lemma le_succ : "x∈nat ⟹ x≤succ(x)" by simp

lemma le_pred : "x∈nat ⟹ pred(x)≤x"
  using pred_le[OF _ le_succ] pred_succ_eq
  by simp

lemma not_le_anti_sym : "x∈nat ⟹ y ∈ nat ⟹ ¬ x≤y ⟹ ¬y≤x ⟹ y=x"
  using Ord_linear not_le_iff_lt ltD lt_trans
  by auto

lemma Un_le_compat : "o ≤ p ⟹ q ≤ r ⟹ Ord(o) ⟹ Ord(p) ⟹ Ord(q) ⟹ Ord(r) ⟹ o ∪ q ≤ p ∪ r"
  using le_trans[of q r "p∪r",OF _ Un_upper2_le] le_trans[of o p "p∪r",OF _ Un_upper1_le]
    ord_simp_union
  by auto

lemma Un_le : "p ≤ r ⟹ q ≤ r ⟹
               Ord(p) ⟹ Ord(q) ⟹ Ord(r) ⟹
                p ∪ q ≤ r"
  using ord_simp_union by auto

lemma Un_leI3 : "o ≤ r ⟹ p ≤ r ⟹ q ≤ r ⟹
                Ord(o) ⟹ Ord(p) ⟹ Ord(q) ⟹ Ord(r) ⟹
                o ∪ p ∪ q ≤ r"
  using ord_simp_union by auto

lemma diff_mono :
  assumes "m ∈ nat" "n∈nat" "p ∈ nat" "m < n" "p≤m"
  shows "m#-p < n#-p"
proof -
  from assms
  have "m#-p ∈ nat" "m#-p +ωp = m"
    using add_diff_inverse2 by simp_all
  with assms
  show ?thesis
    using less_diff_conv[of n p "m #- p",THEN iffD2] by simp
qed

lemma pred_Un:
  "x ∈ nat ⟹ y ∈ nat ⟹ pred(succ(x) ∪ y) = x ∪ pred(y)"
  "x ∈ nat ⟹ y ∈ nat ⟹ pred(x ∪ succ(y)) = pred(x) ∪ y"
  using pred_Un_distrib pred_succ_eq by simp_all

lemma le_natI : "j ≤ n ⟹ n ∈ nat ⟹ j∈nat"
  by(drule ltD,rule in_n_in_nat,rule nat_succ_iff[THEN iffD2,of n],simp_all)

lemma le_natE : "n∈nat ⟹ j < n ⟹  j∈n"
  by(rule ltE[of j n],simp+)

lemma leD : assumes "n∈nat" "j ≤ n"
  shows "j < n | j = n"
  using leE[OF ‹j≤n›,of "j<n | j = n"] by auto

lemma pred_nat_eq :
  assumes "n∈nat"
  shows "pred(n) = ⋃ n"
  using assms
proof(induct)
  case 0
  then show ?case by simp
next
  case (succ x)
  then show ?case using pred_succ_eq Ord_Union_succ_eq
    by simp
qed

subsection‹Some results in ordinal arithmetic›
text‹The following results are auxiliary to the proof of
wellfoundedness of the relation term‹frecR››

lemma max_cong :
  assumes "x ≤ y" "Ord(y)" "Ord(z)"
  shows "max(x,y) ≤ max(y,z)"
proof (cases "y ≤ z")
  case True
  then show ?thesis
    unfolding max_def using assms by simp
next
  case False
  then have "z ≤ y"  using assms not_le_iff_lt leI by simp
  then show ?thesis
    unfolding max_def using assms by simp
qed

lemma max_commutes :
  assumes "Ord(x)" "Ord(y)"
  shows "max(x,y) = max(y,x)"
  using assms Un_commute ord_simp_union(1) ord_simp_union(1)[symmetric] by auto

lemma max_cong2 :
  assumes "x ≤ y" "Ord(y)" "Ord(z)" "Ord(x)"
  shows "max(x,z) ≤ max(y,z)"
proof -
  from assms
  have " x ∪ z ≤ y ∪ z"
    using lt_Ord Ord_Un Un_mono[OF  le_imp_subset[OF ‹x≤y›]]  subset_imp_le by auto
  then show ?thesis
    using  ord_simp_union ‹Ord(x)› ‹Ord(z)› ‹Ord(y)› by simp
qed

lemma max_D1 :
  assumes "x = y" "w < z"  "Ord(x)"  "Ord(w)" "Ord(z)" "max(x,w) = max(y,z)"
  shows "z≤y"
proof -
  from assms
  have "w <  x ∪ w" using Un_upper2_lt[OF ‹w<z›] assms ord_simp_union by simp
  then
  have "w < x" using assms lt_Un_iff[of x w w] lt_not_refl by auto
  then
  have "y = y ∪ z" using assms max_commutes ord_simp_union assms leI by simp
  then
  show ?thesis using Un_leD2 assms by simp
qed

lemma max_D2 :
  assumes "w = y ∨ w = z" "x < y"  "Ord(x)"  "Ord(w)" "Ord(y)" "Ord(z)" "max(x,w) = max(y,z)"
  shows "x<w"
proof -
  from assms
  have "x < z ∪ y" using Un_upper2_lt[OF ‹x<y›] by simp
  then
  consider (a) "x < y" | (b) "x < w"
    using assms ord_simp_union by simp
  then show ?thesis proof (cases)
    case a
    consider (c) "w = y" | (d) "w = z"
      using assms by auto
    then show ?thesis proof (cases)
      case c
      with a show ?thesis by simp
    next
      case d
      with a
      show ?thesis
      proof (cases "y <w")
        case True
        then show ?thesis using lt_trans[OF ‹x<y›] by simp
      next
        case False
        then
        have "w ≤ y"
          using not_lt_iff_le[OF assms(5) assms(4)] by simp
        with ‹w=z›
        have "max(z,y) = y"  unfolding max_def using assms by simp
        with assms
        have "... = x ∪ w" using ord_simp_union max_commutes  by simp
        then show ?thesis using le_Un_iff assms by blast
      qed
    qed
  next
    case b
    then show ?thesis .
  qed
qed

lemma oadd_lt_mono2 :
  assumes  "Ord(n)" "Ord(α)" "Ord(β)" "α < β" "x < n" "y < n" "0 <n"
  shows "n ** α + x < n **β + y"
proof -
  consider (0) "β=0" | (s) γ where  "Ord(γ)" "β = succ(γ)" | (l) "Limit(β)"
    using Ord_cases[OF ‹Ord(β)›,of ?thesis] by force
  then show ?thesis
  proof cases
    case 0
    then show ?thesis using ‹α<β› by auto
  next
    case s
    then
    have "α≤γ" using ‹α<β› using leI by auto
    then
    have "n ** α ≤ n ** γ" using omult_le_mono[OF _ ‹α≤γ›] ‹Ord(n)› by simp
    then
    have "n ** α + x < n ** γ + n" using oadd_lt_mono[OF _ ‹x<n›] by simp
    also
    have "... = n ** β" using ‹β=succ(_)› omult_succ ‹Ord(β)› ‹Ord(n)› by simp
    finally
    have "n ** α + x < n ** β" by auto
    then
    show ?thesis using oadd_le_self ‹Ord(β)› lt_trans2 ‹Ord(n)› by auto
  next
    case l
    have "Ord(x)" using ‹x<n› lt_Ord by simp
    with l
    have "succ(α) < β" using Limit_has_succ ‹α<β› by simp
    have "n ** α + x < n ** α + n"
      using oadd_lt_mono[OF le_refl[OF Ord_omult[OF _ ‹Ord(α)›]] ‹x<n›] ‹Ord(n)› by simp
    also
    have "... = n ** succ(α)" using omult_succ ‹Ord(α)› ‹Ord(n)› by simp
    finally
    have "n ** α + x < n ** succ(α)" by simp
    with ‹succ(α) < β›
    have "n ** α + x < n ** β" using lt_trans omult_lt_mono ‹Ord(n)› ‹0<n›  by auto
    then show ?thesis using oadd_le_self ‹Ord(β)› lt_trans2 ‹Ord(n)› by auto
  qed
qed
end
body>

Theory ZF_Miscellanea

section‹Various results missing from ZF.›

theory ZF_Miscellanea
  imports
    ZF
    Nat_Miscellanea
begin

lemma function_subset:
  "function(f) ⟹ g⊆f ⟹ function(g)"
  unfolding function_def subset_def by auto

lemma converse_refl : "refl(A,r) ⟹ refl(A,converse(r))"
  unfolding refl_def by simp

lemma Ord_lt_subset : "Ord(b) ⟹ a<b ⟹ a⊆b"
  by(intro subsetI,frule ltD,rule_tac Ord_trans,simp_all)

lemma funcI : "f ∈ A → B ⟹ a ∈ A ⟹ b= f ` a ⟹ ⟨a, b⟩ ∈ f"
  by(simp_all add: apply_Pair)

lemma vimage_fun_sing:
  assumes "f∈A→B" "b∈B"
  shows "{a∈A . f`a=b} = f-``{b}"
  using assms vimage_singleton_iff function_apply_equality Pi_iff funcI by auto

lemma image_fun_subset: "S∈A→B ⟹ C⊆A⟹ {S ` x . x∈ C} = S``C"
  using image_function[symmetric,of S C] domain_of_fun Pi_iff by auto

lemma subset_Diff_Un: "X ⊆ A ⟹ A = (A - X) ∪ X " by auto

lemma Diff_bij:
  assumes "∀A∈F. X ⊆ A" shows "(λA∈F. A-X) ∈ bij(F, {A-X. A∈F})"
  using assms unfolding bij_def inj_def surj_def
  by (auto intro:lam_type, subst subset_Diff_Un[of X]) auto

lemma function_space_nonempty:
  assumes "b∈B"
  shows "(λx∈A. b) : A → B"
  using assms lam_type by force

lemma vimage_lam: "(λx∈A. f(x)) -`` B = { x∈A . f(x) ∈ B }"
  using lam_funtype[of A f, THEN [2] domain_type]
    lam_funtype[of A f, THEN [2] apply_equality] lamI[of _ A f]
  by auto blast

lemma range_fun_subset_codomain:
  assumes "h:B → C"
  shows "range(h) ⊆ C"
  unfolding range_def domain_def converse_def using range_type[OF _ assms]  by auto

lemma Pi_rangeD:
  assumes "f∈Pi(A,B)" "b ∈ range(f)"
  shows "∃a∈A. f`a = b"
  using assms apply_equality[OF _ assms(1), of _ b]
    domain_type[OF _ assms(1)] by auto

lemma Pi_range_eq: "f ∈ Pi(A,B) ⟹ range(f) = {f ` x . x ∈ A}"
  using Pi_rangeD[of f A B] apply_rangeI[of f A B]
  by blast

lemma Pi_vimage_subset : "f ∈ Pi(A,B) ⟹ f-``C ⊆ A"
  unfolding Pi_def by auto

definition
  minimum :: "i ⇒ i ⇒ i" where
  "minimum(r,B) ≡ THE b. first(b,B,r)"

lemma minimum_in: "⟦ well_ord(A,r); B⊆A; B≠0 ⟧ ⟹ minimum(r,B) ∈ B"
  using the_first_in unfolding minimum_def by simp

lemma well_ord_surj_imp_inj_inverse:
  assumes "well_ord(A,r)" "h ∈ surj(A,B)"
  shows "(λb∈B. minimum(r, {a∈A. h`a=b})) ∈ inj(B,A)"
proof -
  let ?f="λb∈B. minimum(r, {a∈A. h`a=b})"
  have "minimum(r, {a ∈ A . h ` a = b}) ∈ {a∈A. h`a=b}" if "b∈B" for b
  proof -
    from ‹h ∈ surj(A,B)› that
    have "{a∈A. h`a=b} ≠ 0"
      unfolding surj_def by blast
    with ‹well_ord(A,r)›
    show "minimum(r,{a∈A. h`a=b}) ∈ {a∈A. h`a=b}"
      using minimum_in by blast
  qed
  moreover from this
  have "?f : B → A"
    using lam_type[of B _ "λ_.A"] by simp
  moreover
  have "?f ` w = ?f ` x ⟹ w = x" if "w∈B" "x∈B" for w x
  proof -
    from calculation that
    have "w = h ` minimum(r,{a∈A. h`a=w})"
      "x = h ` minimum(r,{a∈A. h`a=x})"
      by simp_all
    moreover
    assume "?f ` w = ?f ` x"
    moreover from this and that
    have "minimum(r, {a ∈ A . h ` a = w}) = minimum(r, {a ∈ A . h ` a = x})"
      unfolding minimum_def by simp_all
    moreover from calculation(1,2,4)
    show "w=x" by simp
  qed
  ultimately
  show ?thesis
    unfolding inj_def by blast
qed

lemma well_ord_surj_imp_lepoll:
  assumes "well_ord(A,r)" "h ∈ surj(A,B)"
  shows "B≲A"
  unfolding lepoll_def using well_ord_surj_imp_inj_inverse[OF assms]
  by blast

― ‹New result›
lemma surj_imp_well_ord:
  assumes "well_ord(A,r)" "h ∈ surj(A,B)"
  shows "∃s. well_ord(B,s)"
  using assms lepoll_well_ord[OF well_ord_surj_imp_lepoll]
  by force

lemma Pow_sing : "Pow({a}) = {0,{a}}"
proof(intro equalityI,simp_all)
  have "z ∈ {0,{a}}" if "z ⊆ {a}" for z
    using that by auto
  then
  show " Pow({a}) ⊆ {0, {a}}" by auto
qed

lemma Pow_cons:
  shows "Pow(cons(a,A)) = Pow(A) ∪ {{a} ∪ X . X: Pow(A)}"
  using Un_Pow_subset Pow_sing
proof(intro equalityI,auto simp add:Un_Pow_subset)
  {
    fix C D
    assume "⋀ B . B∈Pow(A) ⟹ C ≠ {a} ∪ B" "C ⊆ {a} ∪ A" "D ∈ C"
    moreover from this
    have "∀x∈C . x=a ∨ x∈A" by auto
    moreover from calculation
    consider (a) "D=a" | (b) "D∈A" by auto
    from this
    have "D∈A"
    proof(cases)
      case a
      with calculation show ?thesis by auto
    next
      case b
      then show ?thesis by simp
    qed
  }
  then show "⋀x xa. (∀xa∈Pow(A). x ≠ {a} ∪ xa) ⟹ x ⊆ cons(a, A) ⟹ xa ∈ x ⟹ xa ∈ A"
    by auto
qed

lemma app_nm :
  assumes "n∈nat" "m∈nat" "f∈n→m" "x ∈ nat"
  shows "f`x ∈ nat"
proof(cases "x∈n")
  case True
  then show ?thesis using assms in_n_in_nat apply_type by simp
next
  case False
  then show ?thesis using assms apply_0 domain_of_fun by simp
qed

lemma Upair_eq_cons: "Upair(a,b) = {a,b}"
  unfolding cons_def by auto

lemma converse_apply_eq : "converse(f) ` x = ⋃(f -`` {x})"
  unfolding apply_def vimage_def by simp

lemmas app_fun = apply_iff[THEN iffD1]

lemma Finite_imp_lesspoll_nat:
  assumes "Finite(A)"
  shows "A ≺ nat"
  using assms subset_imp_lepoll[OF naturals_subset_nat] eq_lepoll_trans
    n_lesspoll_nat eq_lesspoll_trans
  unfolding Finite_def lesspoll_def by auto

end

Theory Renaming

section‹Renaming of variables in internalized formulas›

theory Renaming
  imports
    ZF_Miscellanea
    "ZF-Constructible.Formula"
begin

subsection‹Renaming of free variables›

definition
  union_fun :: "[i,i,i,i] ⇒ i" where
  "union_fun(f,g,m,p) ≡ λj ∈ m ∪ p  . if j∈m then f`j else g`j"

lemma union_fun_type:
  assumes "f ∈ m → n"
    "g ∈ p → q"
  shows "union_fun(f,g,m,p) ∈ m ∪ p → n ∪ q"
proof -
  let ?h="union_fun(f,g,m,p)"
  have
    D: "?h`x ∈ n ∪ q" if "x ∈ m ∪ p" for x
  proof (cases "x ∈ m")
    case True
    then have
      "x ∈ m ∪ p" by simp
    with ‹x∈m›
    have "?h`x = f`x"
      unfolding union_fun_def  beta by simp
    with ‹f ∈ m → n› ‹x∈m›
    have "?h`x ∈ n" by simp
    then show ?thesis ..
  next
    case False
    with ‹x ∈ m ∪ p›
    have "x ∈ p"
      by auto
    with ‹x∉m›
    have "?h`x = g`x"
      unfolding union_fun_def using beta by simp
    with ‹g ∈ p → q› ‹x∈p›
    have "?h`x ∈ q" by simp
    then show ?thesis ..
  qed
  have A:"function(?h)" unfolding union_fun_def using function_lam by simp
  have " x∈ (m ∪ p) × (n ∪ q)" if "x∈ ?h" for x
    using that lamE[of x "m ∪ p" _ "x ∈ (m ∪ p) × (n ∪ q)"] D unfolding union_fun_def
    by auto
  then have B:"?h ⊆ (m ∪ p) × (n ∪ q)" ..
  have "m ∪ p ⊆ domain(?h)"
    unfolding union_fun_def using domain_lam by simp
  with A B
  show ?thesis using  Pi_iff [THEN iffD2] by simp
qed

lemma union_fun_action :
  assumes
    "env ∈ list(M)"
    "env' ∈ list(M)"
    "length(env) = m ∪ p"
    "∀ i . i ∈ m ⟶  nth(f`i,env') = nth(i,env)"
    "∀ j . j ∈ p ⟶ nth(g`j,env') = nth(j,env)"
  shows "∀ i . i ∈ m ∪ p ⟶
          nth(i,env) = nth(union_fun(f,g,m,p)`i,env')"
proof -
  let ?h = "union_fun(f,g,m,p)"
  have "nth(x, env) = nth(?h`x,env')" if "x ∈ m ∪ p" for x
    using that
  proof (cases "x∈m")
    case True
    with ‹x∈m›
    have "?h`x = f`x"
      unfolding union_fun_def  beta by simp
    with assms ‹x∈m›
    have "nth(x,env) = nth(?h`x,env')" by simp
    then show ?thesis .
  next
    case False
    with ‹x ∈ m ∪ p›
    have
      "x ∈ p" "x∉m"  by auto
    then
    have "?h`x = g`x"
      unfolding union_fun_def beta by simp
    with assms ‹x∈p›
    have "nth(x,env) = nth(?h`x,env')" by simp
    then show ?thesis .
  qed
  then show ?thesis by simp
qed


lemma id_fn_type :
  assumes "n ∈ nat"
  shows "id(n) ∈ n → n"
  unfolding id_def using ‹n∈nat› by simp

lemma id_fn_action:
  assumes "n ∈ nat" "env∈list(M)"
  shows "⋀ j . j < n ⟹ nth(j,env) = nth(id(n)`j,env)"
proof -
  show "nth(j,env) = nth(id(n)`j,env)" if "j < n" for j using that ‹n∈nat› ltD by simp
qed


definition
  rsum :: "[i,i,i,i,i] ⇒ i" where
  "rsum(f,g,m,n,p) ≡ λj ∈ m+ωp  . if j<m then f`j else (g`(j#-m))+ωn"

lemma sum_inl:
  assumes "m ∈ nat" "n∈nat"
    "f ∈ m→n" "x ∈ m"
  shows "rsum(f,g,m,n,p)`x = f`x"
proof -
  from ‹m∈nat›
  have "m≤m+ωp"
    using add_le_self[of m] by simp
  with assms
  have "x∈m+ωp"
    using ltI[of x m] lt_trans2[of x m "m+ωp"] ltD by simp
  from assms
  have "x<m"
    using ltI by simp
  with ‹x∈m+ωp›
  show ?thesis unfolding rsum_def by simp
qed

lemma sum_inr:
  assumes "m ∈ nat" "n∈nat" "p∈nat"
    "g∈p→q" "m ≤ x" "x < m+ωp"
  shows "rsum(f,g,m,n,p)`x = g`(x#-m)+ωn"
proof -
  from assms
  have "x∈nat"
    using in_n_in_nat[of "m+ωp"] ltD
    by simp
  with assms
  have "¬ x<m"
    using not_lt_iff_le[THEN iffD2] by simp
  from assms
  have "x∈m+ωp"
    using ltD by simp
  with ‹¬ x<m›
  show ?thesis unfolding rsum_def by simp
qed


lemma sum_action :
  assumes "m ∈ nat" "n∈nat" "p∈nat" "q∈nat"
    "f ∈ m→n" "g∈p→q"
    "env ∈ list(M)"
    "env' ∈ list(M)"
    "env1 ∈ list(M)"
    "env2 ∈ list(M)"
    "length(env) = m"
    "length(env1) = p"
    "length(env') = n"
    "⋀ i . i < m ⟹ nth(i,env) = nth(f`i,env')"
    "⋀ j. j < p ⟹ nth(j,env1) = nth(g`j,env2)"
  shows "∀ i . i < m+ωp ⟶
          nth(i,env@env1) = nth(rsum(f,g,m,n,p)`i,env'@env2)"
proof -
  let ?h = "rsum(f,g,m,n,p)"
  from ‹m∈nat› ‹n∈nat› ‹q∈nat›
  have "m≤m+ωp" "n≤n+ωq" "q≤n+ωq"
    using add_le_self[of m]  add_le_self2[of n q] by simp_all
  from ‹p∈nat›
  have "p = (m+ωp)#-m" using diff_add_inverse2 by simp
  have "nth(x, env @ env1) = nth(?h`x,env'@env2)" if "x<m+ωp" for x
  proof (cases "x<m")
    case True
    then
    have 2: "?h`x= f`x" "x∈m" "f`x ∈ n" "x∈nat"
      using assms sum_inl ltD apply_type[of f m _ x] in_n_in_nat by simp_all
    with ‹x<m› assms
    have "f`x < n" "f`x<length(env')"  "f`x∈nat"
      using ltI in_n_in_nat by simp_all
    with 2 ‹x<m› assms
    have "nth(x,env@env1) = nth(x,env)"
      using nth_append[OF ‹env∈list(M)›] ‹x∈nat› by simp
    also
    have
      "... = nth(f`x,env')"
      using 2 ‹x<m› assms by simp
    also
    have "... = nth(f`x,env'@env2)"
      using nth_append[OF ‹env'∈list(M)›] ‹f`x<length(env')› ‹f`x ∈nat› by simp
    also
    have "... = nth(?h`x,env'@env2)"
      using 2 by simp
    finally
    have "nth(x, env @ env1) = nth(?h`x,env'@env2)" .
    then show ?thesis .
  next
    case False
    have "x∈nat"
      using that in_n_in_nat[of "m+ωp" x] ltD ‹p∈nat› ‹m∈nat› by simp
    with ‹length(env) = m›
    have "m≤x" "length(env) ≤ x"
      using not_lt_iff_le ‹m∈nat› ‹¬x<m› by simp_all
    with ‹¬x<m› ‹length(env) = m›
    have 2 : "?h`x= g`(x#-m)+ωn"  "¬ x <length(env)"
      unfolding rsum_def
      using  sum_inr that beta ltD by simp_all
    from assms ‹x∈nat› ‹p=m+ωp#-m›
    have "x#-m < p"
      using diff_mono[OF _ _ _ ‹x<m+ωp› ‹m≤x›] by simp
    then have "x#-m∈p" using ltD by simp
    with ‹g∈p→q›
    have "g`(x#-m) ∈ q"  by simp
    with ‹q∈nat› ‹length(env') = n›
    have "g`(x#-m) < q" "g`(x#-m)∈nat" using ltI in_n_in_nat by simp_all
    with ‹q∈nat› ‹n∈nat›
    have "(g`(x#-m))+ωn <n+ωq" "n ≤ g`(x#-m)+ωn" "¬ g`(x#-m)+ωn < length(env')"
      using add_lt_mono1[of "g`(x#-m)" _ n,OF _ ‹q∈nat›]
        add_le_self2[of n] ‹length(env') = n›
      by simp_all
    from assms ‹¬ x < length(env)› ‹length(env) = m›
    have "nth(x,env @ env1) = nth(x#-m,env1)"
      using nth_append[OF ‹env∈list(M)› ‹x∈nat›] by simp
    also
    have "... = nth(g`(x#-m),env2)"
      using assms ‹x#-m < p› by simp
    also
    have "... = nth((g`(x#-m)+ωn)#-length(env'),env2)"
      using  ‹length(env') = n›
        diff_add_inverse2 ‹g`(x#-m)∈nat›
      by simp
    also
    have "... = nth((g`(x#-m)+ωn),env'@env2)"
      using  nth_append[OF ‹env'∈list(M)›] ‹n∈nat› ‹¬ g`(x#-m)+ωn < length(env')›
      by simp
    also
    have "... = nth(?h`x,env'@env2)"
      using 2 by simp
    finally
    have "nth(x, env @ env1) = nth(?h`x,env'@env2)" .
    then show ?thesis .
  qed
  then show ?thesis by simp
qed

lemma sum_type  :
  assumes "m ∈ nat" "n∈nat" "p∈nat" "q∈nat"
    "f ∈ m→n" "g∈p→q"
  shows "rsum(f,g,m,n,p) ∈ (m+ωp) → (n+ωq)"
proof -
  let ?h = "rsum(f,g,m,n,p)"
  from ‹m∈nat› ‹n∈nat› ‹q∈nat›
  have "m≤m+ωp" "n≤n+ωq" "q≤n+ωq"
    using add_le_self[of m]  add_le_self2[of n q] by simp_all
  from ‹p∈nat›
  have "p = (m+ωp)#-m" using diff_add_inverse2 by simp
  {fix x
    assume 1: "x∈m+ωp" "x<m"
    with 1 have "?h`x= f`x" "x∈m"
      using assms sum_inl ltD by simp_all
    with ‹f∈m→n›
    have "?h`x ∈ n" by simp
    with ‹n∈nat› have "?h`x < n" using ltI by simp
    with ‹n≤n+ωq›
    have "?h`x < n+ωq" using lt_trans2 by simp
    then
    have "?h`x ∈ n+ωq"  using ltD by simp
  }
  then have 1:"?h`x ∈ n+ωq" if "x∈m+ωp" "x<m" for x using that .
  {fix x
    assume 1: "x∈m+ωp" "m≤x"
    then have "x<m+ωp" "x∈nat" using ltI in_n_in_nat[of "m+ωp"] ltD by simp_all
    with 1
    have 2 : "?h`x= g`(x#-m)+ωn"
      using assms sum_inr ltD by simp_all
    from assms ‹x∈nat› ‹p=m+ωp#-m›
    have "x#-m < p" using diff_mono[OF _ _ _ ‹x<m+ωp› ‹m≤x›] by simp
    then have "x#-m∈p" using ltD by simp
    with ‹g∈p→q›
    have "g`(x#-m) ∈ q"  by simp
    with ‹q∈nat› have "g`(x#-m) < q" using ltI by simp
    with ‹q∈nat›
    have "(g`(x#-m))+ωn <n+ωq" using add_lt_mono1[of "g`(x#-m)" _ n,OF _ ‹q∈nat›] by simp
    with 2
    have "?h`x ∈ n+ωq"  using ltD by simp
  }
  then have 2:"?h`x ∈ n+ωq" if "x∈m+ωp" "m≤x" for x using that .
  have
    D: "?h`x ∈ n+ωq" if "x∈m+ωp" for x
    using that
  proof (cases "x<m")
    case True
    then show ?thesis using 1 that by simp
  next
    case False
    with ‹m∈nat› have "m≤x" using not_lt_iff_le that in_n_in_nat[of "m+ωp"] by simp
    then show ?thesis using 2 that by simp
  qed
  have A:"function(?h)" unfolding rsum_def using function_lam by simp
  have " x∈ (m +ω p) × (n +ω q)" if "x∈ ?h" for x
    using that lamE[of x "m+ωp" _ "x ∈ (m +ω p) × (n +ω q)"] D unfolding rsum_def
    by auto
  then have B:"?h ⊆ (m +ω p) × (n +ω q)" ..
  have "m +ω p ⊆ domain(?h)"
    unfolding rsum_def using domain_lam by simp
  with A B
  show ?thesis using  Pi_iff [THEN iffD2] by simp
qed

lemma sum_type_id :
  assumes
    "f ∈ length(env)→length(env')"
    "env ∈ list(M)"
    "env' ∈ list(M)"
    "env1 ∈ list(M)"
  shows
    "rsum(f,id(length(env1)),length(env),length(env'),length(env1)) ∈
        (length(env)+ωlength(env1)) → (length(env')+ωlength(env1))"
  using assms length_type id_fn_type sum_type
  by simp

lemma sum_type_id_aux2 :
  assumes
    "f ∈ m→n"
    "m ∈ nat" "n ∈ nat"
    "env1 ∈ list(M)"
  shows
    "rsum(f,id(length(env1)),m,n,length(env1)) ∈
        (m+ωlength(env1)) → (n+ωlength(env1))"
  using assms id_fn_type sum_type
  by auto

lemma sum_action_id :
  assumes
    "env ∈ list(M)"
    "env' ∈ list(M)"
    "f ∈ length(env)→length(env')"
    "env1 ∈ list(M)"
    "⋀ i . i < length(env) ⟹ nth(i,env) = nth(f`i,env')"
  shows "⋀ i . i < length(env)+ωlength(env1) ⟹
          nth(i,env@env1) = nth(rsum(f,id(length(env1)),length(env),length(env'),length(env1))`i,env'@env1)"
proof -
  from assms
  have "length(env)∈nat" (is "?m ∈ _") by simp
  from assms have "length(env')∈nat" (is "?n ∈ _") by simp
  from assms have "length(env1)∈nat" (is "?p ∈ _") by simp
  note lenv = id_fn_action[OF ‹?p∈nat› ‹env1∈list(M)›]
  note lenv_ty = id_fn_type[OF ‹?p∈nat›]
  {
    fix i
    assume "i < length(env)+ωlength(env1)"
    have "nth(i,env@env1) = nth(rsum(f,id(length(env1)),?m,?n,?p)`i,env'@env1)"
      using sum_action[OF ‹?m∈nat› ‹?n∈nat› ‹?p∈nat› ‹?p∈nat› ‹f∈?m→?n›
          lenv_ty ‹env∈list(M)› ‹env'∈list(M)›
          ‹env1∈list(M)› ‹env1∈list(M)› _
          _ _  assms(5) lenv
          ] ‹i<?m+ωlength(env1)› by simp
  }
  then show "⋀ i . i < ?m+ωlength(env1) ⟹
          nth(i,env@env1) = nth(rsum(f,id(?p),?m,?n,?p)`i,env'@env1)" by simp
qed

lemma sum_action_id_aux :
  assumes
    "f ∈ m→n"
    "env ∈ list(M)"
    "env' ∈ list(M)"
    "env1 ∈ list(M)"
    "length(env) = m"
    "length(env') = n"
    "length(env1) = p"
    "⋀ i . i < m ⟹ nth(i,env) = nth(f`i,env')"
  shows "⋀ i . i < m+ωlength(env1) ⟹
          nth(i,env@env1) = nth(rsum(f,id(length(env1)),m,n,length(env1))`i,env'@env1)"
  using assms length_type id_fn_type sum_action_id
  by auto


definition
  sum_id :: "[i,i] ⇒ i" where
  "sum_id(m,f) ≡ rsum(λx∈1.x,f,1,1,m)"

lemma sum_id0 : "m∈nat⟹sum_id(m,f)`0 = 0"
  by(unfold sum_id_def,subst sum_inl,auto)

lemma sum_idS : "p∈nat ⟹ q∈nat ⟹ f∈p→q ⟹ x ∈ p ⟹ sum_id(p,f)`(succ(x)) = succ(f`x)"
  by(subgoal_tac "x∈nat",unfold sum_id_def,subst sum_inr,
      simp_all add:ltI,simp_all add: app_nm in_n_in_nat)

lemma sum_id_tc_aux :
  "p ∈ nat ⟹  q ∈ nat ⟹ f ∈ p → q ⟹ sum_id(p,f) ∈ 1+ωp → 1+ωq"
  by (unfold sum_id_def,rule sum_type,simp_all)

lemma sum_id_tc :
  "n ∈ nat ⟹ m ∈ nat ⟹ f ∈ n → m ⟹ sum_id(n,f) ∈ succ(n) → succ(m)"
  by(rule ssubst[of  "succ(n) → succ(m)" "1+ωn → 1+ωm"],
      simp,rule sum_id_tc_aux,simp_all)

subsection‹Renaming of formulas›

consts   ren :: "i⇒i"
primrec
  "ren(Member(x,y)) =
      (λ n ∈ nat . λ m ∈ nat. λf ∈ n → m. Member (f`x, f`y))"

"ren(Equal(x,y)) =
      (λ n ∈ nat . λ m ∈ nat. λf ∈ n → m. Equal (f`x, f`y))"

"ren(Nand(p,q)) =
      (λ n ∈ nat . λ m ∈ nat. λf ∈ n → m. Nand (ren(p)`n`m`f, ren(q)`n`m`f))"

"ren(Forall(p)) =
      (λ n ∈ nat . λ m ∈ nat. λf ∈ n → m. Forall (ren(p)`succ(n)`succ(m)`sum_id(n,f)))"

lemma arity_meml : "l ∈ nat ⟹ Member(x,y) ∈ formula ⟹ arity(Member(x,y)) ≤ l ⟹ x ∈ l"
  by(simp,rule subsetD,rule le_imp_subset,assumption,simp)
lemma arity_memr : "l ∈ nat ⟹ Member(x,y) ∈ formula ⟹ arity(Member(x,y)) ≤ l ⟹ y ∈ l"
  by(simp,rule subsetD,rule le_imp_subset,assumption,simp)
lemma arity_eql : "l ∈ nat ⟹ Equal(x,y) ∈ formula ⟹ arity(Equal(x,y)) ≤ l ⟹ x ∈ l"
  by(simp,rule subsetD,rule le_imp_subset,assumption,simp)
lemma arity_eqr : "l ∈ nat ⟹ Equal(x,y) ∈ formula ⟹ arity(Equal(x,y)) ≤ l ⟹ y ∈ l"
  by(simp,rule subsetD,rule le_imp_subset,assumption,simp)
lemma  nand_ar1 : "p ∈ formula ⟹ q∈formula ⟹arity(p) ≤ arity(Nand(p,q))"
  by (simp,rule Un_upper1_le,simp+)
lemma nand_ar2 : "p ∈ formula ⟹ q∈formula ⟹arity(q) ≤ arity(Nand(p,q))"
  by (simp,rule Un_upper2_le,simp+)

lemma nand_ar1D : "p ∈ formula ⟹ q∈formula ⟹ arity(Nand(p,q)) ≤ n ⟹ arity(p) ≤ n"
  by(auto simp add:  le_trans[OF Un_upper1_le[of "arity(p)" "arity(q)"]])
lemma nand_ar2D : "p ∈ formula ⟹ q∈formula ⟹ arity(Nand(p,q)) ≤ n ⟹ arity(q) ≤ n"
  by(auto simp add:  le_trans[OF Un_upper2_le[of "arity(p)" "arity(q)"]])


lemma ren_tc : "p ∈ formula ⟹
  (⋀ n m f . n ∈ nat ⟹ m ∈ nat ⟹ f ∈ n→m ⟹  ren(p)`n`m`f ∈ formula)"
  by (induct set:formula,auto simp add: app_nm sum_id_tc)


lemma arity_ren :
  fixes "p"
  assumes "p ∈ formula"
  shows "⋀ n m f . n ∈ nat ⟹ m ∈ nat ⟹ f ∈ n→m ⟹ arity(p) ≤ n ⟹ arity(ren(p)`n`m`f)≤m"
  using assms
proof (induct set:formula)
  case (Member x y)
  then have "f`x ∈ m" "f`y ∈ m"
    using Member assms by (simp add: arity_meml apply_funtype,simp add:arity_memr apply_funtype)
  then show ?case using Member by (simp add: Un_least_lt ltI)
next
  case (Equal x y)
  then have "f`x ∈ m" "f`y ∈ m"
    using Equal assms by (simp add: arity_eql apply_funtype,simp add:arity_eqr apply_funtype)
  then show ?case using Equal by (simp add: Un_least_lt ltI)
next
  case (Nand p q)
  then have "arity(p)≤arity(Nand(p,q))"
    "arity(q)≤arity(Nand(p,q))"
    by (subst  nand_ar1,simp,simp,simp,subst nand_ar2,simp+)
  then have "arity(p)≤n"
    and "arity(q)≤n" using Nand
    by (rule_tac j="arity(Nand(p,q))" in le_trans,simp,simp)+
  then have "arity(ren(p)`n`m`f) ≤ m" and  "arity(ren(q)`n`m`f) ≤ m"
    using Nand by auto
  then show ?case using Nand by (simp add:Un_least_lt)
next
  case (Forall p)
  from Forall have "succ(n)∈nat"  "succ(m)∈nat" by auto
  from Forall have 2: "sum_id(n,f) ∈ succ(n)→succ(m)" by (simp add:sum_id_tc)
  from Forall have 3:"arity(p) ≤ succ(n)" by (rule_tac n="arity(p)" in natE,simp+)
  then have "arity(ren(p)`succ(n)`succ(m)`sum_id(n,f))≤succ(m)" using
      Forall ‹succ(n)∈nat› ‹succ(m)∈nat› 2 by force
  then show ?case using Forall 2 3 ren_tc arity_type pred_le by auto
qed

lemma arity_forallE : "p ∈ formula ⟹ m ∈ nat ⟹ arity(Forall(p)) ≤ m ⟹ arity(p) ≤ succ(m)"
  by(rule_tac n="arity(p)" in natE,erule arity_type,simp+)

lemma env_coincidence_sum_id :
  assumes "m ∈ nat" "n ∈ nat"
    "ρ ∈ list(A)" "ρ' ∈ list(A)"
    "f ∈ n → m"
    "⋀ i . i < n ⟹ nth(i,ρ) = nth(f`i,ρ')"
    "a ∈ A" "j ∈ succ(n)"
  shows "nth(j,Cons(a,ρ)) = nth(sum_id(n,f)`j,Cons(a,ρ'))"
proof -
  let ?g="sum_id(n,f)"
  have "succ(n) ∈ nat" using ‹n∈nat› by simp
  then have "j ∈ nat" using ‹j∈succ(n)› in_n_in_nat by blast
  then have "nth(j,Cons(a,ρ)) = nth(?g`j,Cons(a,ρ'))"
  proof (cases rule:natE[OF ‹j∈nat›])
    case 1
    then show ?thesis using assms sum_id0 by simp
  next
    case (2 i)
    with ‹j∈succ(n)› have "succ(i)∈succ(n)" by simp
    with ‹n∈nat› have "i ∈ n" using nat_succD assms by simp
    have "f`i∈m" using ‹f∈n→m› apply_type ‹i∈n› by simp
    then have "f`i ∈ nat" using in_n_in_nat ‹m∈nat› by simp
    have "nth(succ(i),Cons(a,ρ)) = nth(i,ρ)" using ‹i∈nat› by simp
    also have "... = nth(f`i,ρ')" using assms ‹i∈n› ltI by simp
    also have "... = nth(succ(f`i),Cons(a,ρ'))" using ‹f`i∈nat› by simp
    also have "... = nth(?g`succ(i),Cons(a,ρ'))"
      using assms sum_idS[OF ‹n∈nat› ‹m∈nat›  ‹f∈n→m› ‹i ∈ n›] cases by simp
    finally have "nth(succ(i),Cons(a,ρ)) = nth(?g`succ(i),Cons(a,ρ'))" .
    then show ?thesis using ‹j=succ(i)› by simp
  qed
  then show ?thesis .
qed

lemma sats_iff_sats_ren :
  assumes "φ ∈ formula"
  shows  "⟦  n ∈ nat ; m ∈ nat ; ρ ∈ list(M) ; ρ' ∈ list(M) ; f ∈ n → m ;
            arity(φ) ≤ n ;
            ⋀ i . i < n ⟹ nth(i,ρ) = nth(f`i,ρ') ⟧ ⟹
         sats(M,φ,ρ) ⟷ sats(M,ren(φ)`n`m`f,ρ')"
  using ‹φ ∈ formula›
proof(induct φ arbitrary:n m ρ ρ' f)
  case (Member x y)
  have "ren(Member(x,y))`n`m`f = Member(f`x,f`y)" using Member assms arity_type by force
  moreover
  have "x ∈ n" using Member arity_meml by simp
  moreover
  have "y ∈ n" using Member arity_memr by simp
  ultimately
  show ?case using Member ltI by simp
next
  case (Equal x y)
  have "ren(Equal(x,y))`n`m`f = Equal(f`x,f`y)" using Equal assms arity_type by force
  moreover
  have "x ∈ n" using Equal arity_eql by simp
  moreover
  have "y ∈ n" using Equal arity_eqr by simp
  ultimately show ?case using Equal ltI by simp
next
  case (Nand p q)
  have "ren(Nand(p,q))`n`m`f = Nand(ren(p)`n`m`f,ren(q)`n`m`f)" using Nand by simp
  moreover
  have "arity(p) ≤ n" using Nand nand_ar1D by simp
  moreover from this
  have "i ∈ arity(p) ⟹ i ∈ n" for i using subsetD[OF le_imp_subset[OF ‹arity(p) ≤ n›]] by simp
  moreover from this
  have "i ∈ arity(p) ⟹ nth(i,ρ) = nth(f`i,ρ')" for i using Nand ltI by simp
  moreover from this
  have "sats(M,p,ρ) ⟷ sats(M,ren(p)`n`m`f,ρ')" using ‹arity(p)≤n› Nand by simp
  have "arity(q) ≤ n" using Nand nand_ar2D by simp
  moreover from this
  have "i ∈ arity(q) ⟹ i ∈ n" for i using subsetD[OF le_imp_subset[OF ‹arity(q) ≤ n›]] by simp
  moreover from this
  have "i ∈ arity(q) ⟹ nth(i,ρ) = nth(f`i,ρ')" for i using Nand ltI by simp
  moreover from this
  have "sats(M,q,ρ) ⟷ sats(M,ren(q)`n`m`f,ρ')" using assms ‹arity(q)≤n› Nand by simp
  ultimately
  show ?case using Nand by simp
next
  case (Forall p)
  have 0:"ren(Forall(p))`n`m`f = Forall(ren(p)`succ(n)`succ(m)`sum_id(n,f))"
    using Forall by simp
  have 1:"sum_id(n,f) ∈ succ(n) → succ(m)" (is "?g ∈ _") using sum_id_tc Forall by simp
  then have 2: "arity(p) ≤ succ(n)"
    using Forall le_trans[of _ "succ(pred(arity(p)))"] succpred_leI by simp
  have "succ(n)∈nat" "succ(m)∈nat" using Forall by auto
  then have A:"⋀ j .j < succ(n) ⟹ nth(j, Cons(a, ρ)) = nth(?g`j, Cons(a, ρ'))" if "a∈M" for a
    using that env_coincidence_sum_id Forall ltD by force
  have
    "sats(M,p,Cons(a,ρ)) ⟷ sats(M,ren(p)`succ(n)`succ(m)`?g,Cons(a,ρ'))" if "a∈M" for a
  proof -
    have C:"Cons(a,ρ) ∈ list(M)" "Cons(a,ρ')∈list(M)" using Forall that by auto
    have "sats(M,p,Cons(a,ρ)) ⟷ sats(M,ren(p)`succ(n)`succ(m)`?g,Cons(a,ρ'))"
      using Forall(2)[OF ‹succ(n)∈nat› ‹succ(m)∈nat› C(1) C(2) 1 2 A[OF ‹a∈M›]] by simp
    then show ?thesis .
  qed
  then show ?case using Forall 0 1 2 by simp
qed

end
v class="head">

Theory Utils

theory Utils
  imports "ZF-Constructible.Formula"
begin

txt‹This theory encapsulates some ML utilities›
ML_file‹Utils.ml›

end
dy>

File ‹Utils.ml›

signature Utils =
 sig
    val &&& : ('a -> 'b) * ('a -> 'c) -> 'a -> 'b * 'c
    val *** : ('a -> 'b) * ('c -> 'd) -> 'a * 'c -> 'b * 'd
    val @@ : ''a list * ''a list -> ''a list
    val --- : ''a list * ''a list -> ''a list
    val binop : term -> term -> term -> term
    val add_: term -> term -> term
    val add_to_context : string -> Proof.context -> Proof.context
    val app_: term -> term -> term
    val concat_: term -> term -> term
    val dest_apply: term -> term * term
    val dest_abs : string * typ * term -> string * term
    val dest_iff_lhs: term -> term
    val dest_iff_rhs: term -> term
    val dest_iff_tms: term -> term * term
    val dest_lhs_def: term -> term
    val dest_rhs_def: term -> term
    val dest_satisfies_tms: term -> term * term
    val dest_satisfies_frm: term -> term
    val dest_eq_tms: term -> term * term
    val dest_mem_tms: term -> term * term
    val dest_sats_frm: term -> (term * term) * term
    val dest_eq_tms': term -> term * term
    val dest_trueprop: term -> term
    val display : string -> Position.T -> (string * thm list) * Proof.context -> Proof.context
    val eq_: term -> term -> term
    val fix_vars: thm -> string list -> Proof.context -> thm
    val flat : ''a list list -> ''a list
    val formula_: term
    val freeName: term -> string
    val frees : term -> term list
    val length_: term -> term
    val list_: term -> term
    val lt_: term -> term -> term
    val map_option : ('a -> 'b) -> 'a option -> 'b option
    val mem_: term -> term -> term
    val mk_FinSet: term list -> term
    val mk_Pair: term -> term -> term
    val mk_ZFlist: ('a -> term) -> 'a list -> term
    val mk_ZFnat: int -> term
    val nat_: term
    val nth_: term -> term -> term
    val reachable : (''a -> ''a -> bool) -> ''a list -> ''a list -> ''a list
    val subset_: term -> term -> term
    val thm_concl_tm :  Proof.context -> xstring -> (Vars.key * cterm) list  * term * Proof.context
    val to_ML_list: term -> term list
    val tp: term -> term
    val var_i : string -> term
    val zip_with : ('a * 'b -> 'c) -> 'a list -> 'b list -> 'c list
  end

structure Utils : Utils =
struct
(* Smart constructors for ZF-terms *)

fun binop h t u = h $ t $ u

val mk_Pair  = binop @{const Pair}

fun mk_FinSet nil = @{const zero}
  | mk_FinSet (e :: es) = @{const cons} $ e $ mk_FinSet es

fun mk_ZFnat 0 = @{const zero}
  | mk_ZFnat n = @{const succ} $ mk_ZFnat (n-1)

fun mk_ZFlist _ nil = @{const "Nil"}
  | mk_ZFlist f (t :: ts) = @{const "Cons"} $ f t $ mk_ZFlist f ts

fun to_ML_list (@{const Nil}) = nil
  | to_ML_list (@{const Cons} $ t $ ts) = t :: to_ML_list ts
  |   to_ML_list _ = nil

fun freeName (Free (n,_)) = n
  | freeName _ = error "Not a free variable"

val app_ = binop @{const apply}

fun tp x = @{const Trueprop} $ x
fun length_ env = @{const length} $ env
val nth_ = binop @{const nth}
val add_ = binop @{const add}
val mem_ = binop @{const mem}
val subset_ = binop @{const Subset}
val lt_ = binop @{const lt}
val concat_ = binop @{const app}
val eq_ = binop @{const IFOL.eq(i)}

(* Abbreviation for sets *)
fun list_ set = @{const list} $ set
val nat_ = @{const nat}
val formula_ = @{const formula}

(** Destructors of terms **)
fun dest_eq_tms (Const (@{const_name IFOL.eq},_) $ t $ u) = (t, u)
  | dest_eq_tms t = raise TERM ("dest_eq_tms", [t])

fun dest_mem_tms (@{const mem} $ t $ u) = (t, u)
  | dest_mem_tms t = raise TERM ("dest_mem_tms", [t])


fun dest_eq_tms' (Const (@{const_name Pure.eq},_) $ t $ u) = (t, u)
  | dest_eq_tms' t = raise TERM ("dest_eq_tms", [t])

val dest_lhs_def = #1 o dest_eq_tms'
val dest_rhs_def = #2 o dest_eq_tms'

fun dest_apply (@{const apply} $ t $ u) = (t,u)
  | dest_apply t = raise TERM ("dest_applies_op", [t])

fun dest_satisfies_tms (@{const Formula.satisfies} $ A $ f) = (A,f)
  | dest_satisfies_tms t = raise TERM ("dest_satisfies_tms", [t]);

val dest_satisfies_frm = #2 o dest_satisfies_tms

fun dest_sats_frm t = t |> dest_eq_tms |> #1 |> dest_apply |>> dest_satisfies_tms ;

fun dest_trueprop (@{const IFOL.Trueprop} $ t) = t
  | dest_trueprop t = t

fun dest_iff_tms (@{const IFOL.iff} $ t $ u) = (t, u)
  | dest_iff_tms t = raise TERM ("dest_iff_tms", [t])

val dest_iff_lhs = #1 o dest_iff_tms
val dest_iff_rhs = #2 o dest_iff_tms

fun thm_concl_tm ctxt thm_ref =
  let
    val thm = Proof_Context.get_thm ctxt thm_ref
    val thm_vars = rev (Term.add_vars (Thm.full_prop_of thm) [])
    val (((_,inst),thm_tms),ctxt1) = Variable.import true [thm] ctxt
    val vars = map (fn v => (v, the (Vars.lookup inst v))) thm_vars
  in
    (vars, thm_tms |> hd |> Thm.concl_of, ctxt1)
end

fun fix_vars thm vars ctxt = let
  val (_, ctxt1) = Variable.add_fixes vars ctxt
  in singleton (Proof_Context.export ctxt1 ctxt) thm
end

fun display kind pos (thms,thy) =
  let val _ = Proof_Display.print_results true pos thy ((kind,""),[thms])
  in thy
end

(* lists as sets *)

infix 6 @@
fun op @@ (xs, ys) = union (op =) ys xs

fun flat xss = fold (curry op @@) xss []

infix 6 ---
fun op --- (xs, ys) = subtract (op =) ys xs

(* function product *)
infix 6 &&&
fun op &&& (f, g) = fn x => (f x, g x)

infix 6 ***
fun op *** (f, g) = fn (x, y) => (f x, g y)

(* add variable to context *)
fun add_to_context v c = if Variable.is_fixed c v then c else #2 (Variable.add_fixes [v] c)

(* get free variables of a term *)
fun frees t = fold_aterms (fn t => if is_Free t then cons t else I) t []

(* closure of a set wrt a preorder *)
(* the preorder is the reflexive-transitive closure of the given relation p *)
(* u represents the universe, and xs represents the starting points *)
(* [xs]_{p,u} = { v ∈ u . ∃ x ∈ xs . p*(x, v) }*)
fun reachable p u xs =
  let
    val step = map (fn x => filter (p x) (u --- xs)) xs |> flat
    val acc = if null step then [] else reachable p (u --- xs) step
  in
    xs @@ acc
  end

fun zip_with _ [] _ = []
  | zip_with _ _ [] = []
  | zip_with f (x :: xs) (y :: ys) = f (x, y) :: zip_with f xs ys

fun var_i s = Free (s, @{typ "i"})

fun map_option f (SOME a) = SOME (f a)
  | map_option _ NONE = NONE

fun dest_abs (v, ty, t) = (v, Term.subst_bound ((Free (v, ty)), t))

end
ody>

Theory Renaming_Auto

theory Renaming_Auto
  imports
    Renaming
    Utils
keywords
  "rename" :: thy_decl % "ML"
and
  "simple_rename" :: thy_decl % "ML"
and
  "src"
and
  "tgt"
abbrevs
  "simple_rename" = ""

begin

lemmas nat_succI = nat_succ_iff[THEN iffD2]
ML_file‹Renaming_ML.ml›
ML‹
  open Renaming_ML

  fun renaming_def mk_ren name from to ctxt =
    let val to = to |> Syntax.read_term ctxt
        val from = from |> Syntax.read_term ctxt
        val (tc_lemma,action_lemma,fvs,r) = mk_ren from to ctxt
        val (tc_lemma,action_lemma) = (fix_vars tc_lemma fvs ctxt , fix_vars action_lemma fvs ctxt)
        val ren_fun_name = Binding.name (name ^ "_fn")
        val ren_fun_def =  Binding.name (name ^ "_fn_def")
        val ren_thm = Binding.name (name ^ "_thm")
    in
      Local_Theory.note   ((ren_thm, []), [tc_lemma,action_lemma]) ctxt |> snd |>
      Local_Theory.define ((ren_fun_name, NoSyn), ((ren_fun_def, []), r)) |> snd
  end;
›

ML‹
local

  val ren_parser = Parse.position (Parse.string --
      (Parse.$$$ "src" |-- Parse.string --| Parse.$$$ "tgt" -- Parse.string));

  val _ =
   Outer_Syntax.local_theory command_keyword‹rename› "ML setup for synthetic definitions"
     (ren_parser >> (fn ((name,(from,to)),_) => renaming_def sum_rename name from to ))

  val _ =
   Outer_Syntax.local_theory command_keyword‹simple_rename› "ML setup for synthetic definitions"
     (ren_parser >> (fn ((name,(from,to)),_) => renaming_def ren_thm name from to ))

in
end
›
end

File ‹Renaming_ML.ml›

structure Renaming_ML = struct
open Utils

fun sum_ f g m n p = @{const Renaming.rsum} $ f $ g $ m $ n $ p

(*Builds a finite mapping from rho to rho'.*)
fun mk_ren rho rho' ctxt =
  let val rs  = to_ML_list rho
      val rs' = to_ML_list rho'
      val ixs = 0 upto (length rs-1)
      fun err t = "The element " ^ Syntax.string_of_term ctxt t ^ " is missing in the target environment"
      fun mkp i =
          case find_index (fn x => x = nth rs i) rs' of
            ~1 => nth rs i |> err |> error
          |  j => mk_Pair (mk_ZFnat i) (mk_ZFnat j)
  in  map mkp ixs |> mk_FinSet
  end

fun mk_dom_lemma ren rho =
  let val n = rho |> to_ML_list |> length |> mk_ZFnat
  in eq_ n (@{const domain} $ ren) |> tp
end

fun ren_tc_goal fin ren rho rho' =
  let val n = rho |> to_ML_list |> length |> mk_ZFnat
      val m = rho' |> to_ML_list |> length |> mk_ZFnat
      val fun_ty = if fin then @{const_name "FiniteFun"} else @{const_abbrev "function_space"}
      val ty = Const (fun_ty,@{typ "i ⇒ i ⇒ i"}) $ n $ m
  in  mem_ ren ty |> tp
end

fun ren_action_goal ren rho rho' ctxt =
  let val setV = Variable.variant_frees ctxt [] [("A",@{typ i})] |> hd |> Free
      val j = Variable.variant_frees ctxt [] [("j",@{typ i})] |> hd |> Free
      val vs = rho  |> to_ML_list
      val ws = rho' |> to_ML_list |> filter Term.is_Free
      val h1 = subset_ (mk_FinSet vs) setV
      val h2 = lt_ j (length vs |> mk_ZFnat)
      val fvs = [j,setV ] @ ws |> filter Term.is_Free |> map freeName
      val lhs = nth_ j rho
      val rhs = nth_ (app_ ren j)  rho'
      val concl = eq_ lhs rhs
   in (Logic.list_implies([tp h1,tp h2],tp concl),fvs)
  end

  fun sum_tc_goal f m n p =
    let val m_length = m |> to_ML_list |> length |> mk_ZFnat
        val n_length = n |> to_ML_list |> length |> mk_ZFnat
        val p_length = p |> length_
        val id_fun = @{const id} $ p_length
        val sum_fun = sum_ f id_fun m_length n_length p_length
        val dom = add_ m_length p_length
        val codom = add_ n_length p_length
        val fun_ty = @{const_abbrev "function_space"}
        val ty = Const (fun_ty,@{typ "i ⇒ i ⇒ i"}) $ dom $ codom
  in  (sum_fun, mem_ sum_fun ty |> tp)
  end

fun sum_action_goal ren rho rho' ctxt =
  let val setV = Variable.variant_frees ctxt [] [("A",@{typ i})] |> hd |> Free
      val envV = Variable.variant_frees ctxt [] [("env",@{typ i})] |> hd |> Free
      val j = Variable.variant_frees ctxt [] [("j",@{typ i})] |> hd |> Free
      val vs = rho  |> to_ML_list
      val ws = rho' |> to_ML_list |> filter Term.is_Free
      val envL = envV |> length_
      val rhoL = vs |> length |> mk_ZFnat
      val h1 = subset_ (append vs ws |> mk_FinSet) setV
      val h2 = lt_ j (add_ rhoL envL)
      val h3 = mem_ envV (list_ setV)
      val fvs = ([j,setV,envV] @ ws |> filter Term.is_Free) |> map freeName
      val lhs = nth_ j (concat_ rho envV)
      val rhs = nth_ (app_ ren j) (concat_ rho' envV)
      val concl = eq_ lhs rhs
   in (Logic.list_implies([tp h1,tp h2,tp h3],tp concl),fvs)
  end

  (* Tactics *)
  fun fin ctxt =
         REPEAT (resolve_tac ctxt [@{thm nat_succI}] 1)
         THEN   resolve_tac ctxt [@{thm nat_0I}] 1

  fun step ctxt thm =
    asm_full_simp_tac ctxt 1
    THEN asm_full_simp_tac ctxt 1
    THEN EqSubst.eqsubst_tac ctxt [1] [@{thm app_fun} OF [thm]] 1
    THEN simp_tac ctxt 1
    THEN simp_tac ctxt 1

  fun fin_fun_tac ctxt =
    REPEAT (
      resolve_tac ctxt [@{thm consI}] 1
      THEN resolve_tac ctxt [@{thm ltD}] 1
      THEN simp_tac ctxt 1
      THEN resolve_tac ctxt [@{thm ltD}] 1
      THEN simp_tac ctxt 1)
    THEN resolve_tac ctxt [@{thm emptyI}] 1
  THEN REPEAT (simp_tac ctxt 1)

  fun ren_thm e e' ctxt =
   let
    val r = mk_ren e e' ctxt
    val fin_tc_goal = ren_tc_goal true r e e'
    val dom_goal =  mk_dom_lemma r e
    val tc_goal = ren_tc_goal false r e e'
    val (action_goal,fvs) = ren_action_goal r e e' ctxt
    val fin_tc_lemma = Goal.prove ctxt [] [] fin_tc_goal (fn _ => fin_fun_tac ctxt)
    val dom_lemma = Goal.prove ctxt [] [] dom_goal (fn _ => blast_tac ctxt 1)
    val tc_lemma =  Goal.prove ctxt [] [] tc_goal
            (fn _ =>  EqSubst.eqsubst_tac ctxt [1] [dom_lemma] 1
              THEN resolve_tac ctxt [@{thm FiniteFun_is_fun}] 1
              THEN resolve_tac ctxt [fin_tc_lemma] 1)
    val action_lemma = Goal.prove ctxt [] [] action_goal
              (fn _ =>
                  forward_tac ctxt [@{thm le_natI}] 1
                  THEN fin ctxt
                  THEN REPEAT (resolve_tac ctxt [@{thm natE}] 1
                               THEN step ctxt tc_lemma)
                  THEN (step ctxt tc_lemma)
              )
    in (action_lemma, tc_lemma, fvs, r)
  end

(*
Returns the sum renaming, the goal for type_checking, and the actual lemmas
for the left part of the sum.
*)
 fun sum_ren_aux e e' ctxt =
  let val env = Variable.variant_frees ctxt [] [("env",@{typ i})] |> hd |> Free
      val (left_action_lemma,left_tc_lemma,_,r) = ren_thm e e' ctxt
      val (sum_ren,sum_goal_tc) = sum_tc_goal r e e' env
      val setV = Variable.variant_frees ctxt [] [("A",@{typ i})] |> hd |> Free
      fun hyp en = mem_ en (list_ setV)
  in (sum_ren,
      freeName env,
      Logic.list_implies (map (fn e => e |> hyp |> tp) [env], sum_goal_tc),
      left_tc_lemma,
      left_action_lemma)
end

fun sum_tc_lemma rho rho' ctxt =
  let val (sum_ren, envVar, tc_goal, left_tc_lemma, left_action_lemma) = sum_ren_aux rho rho' ctxt
      val (goal,fvs) = sum_action_goal sum_ren rho rho' ctxt
      val r = mk_ren rho rho' ctxt
  in (sum_ren, goal,envVar, r,left_tc_lemma, left_action_lemma ,fvs, Goal.prove ctxt [] [] tc_goal
               (fn _ =>
            resolve_tac ctxt [@{thm sum_type_id_aux2}] 1
            THEN asm_simp_tac ctxt 4
            THEN simp_tac ctxt 1
            THEN resolve_tac ctxt [left_tc_lemma] 1
            THEN (fin ctxt)
            THEN (fin ctxt)
  ))
  end

fun sum_rename rho rho' ctxt =
  let
    val (_, goal, _, left_rename, left_tc_lemma, left_action_lemma, fvs, sum_tc_lemma) =
          sum_tc_lemma rho rho' ctxt
    val action_lemma = fix_vars left_action_lemma fvs ctxt
  in (sum_tc_lemma, Goal.prove ctxt [] [] goal
    (fn _ => resolve_tac ctxt [@{thm sum_action_id_aux}] 1
            THEN (simp_tac ctxt 4)
            THEN (simp_tac ctxt 1)
            THEN (resolve_tac ctxt [left_tc_lemma]  1)
            THEN (asm_full_simp_tac ctxt 1)
            THEN (asm_full_simp_tac ctxt 1)
            THEN (simp_tac ctxt 1)
            THEN (simp_tac ctxt 1)
            THEN (simp_tac ctxt 1)
            THEN (full_simp_tac ctxt 1)
            THEN (resolve_tac ctxt [action_lemma] 1)
            THEN (blast_tac ctxt  1)
            THEN (full_simp_tac ctxt  1)
            THEN (full_simp_tac ctxt  1)

   ), fvs, left_rename
   )
end ;
end

Theory M_Basic_No_Repl

theory M_Basic_No_Repl
  imports "ZF-Constructible.Relative"
begin

txt‹This locale is exactly locale‹M_basic› without its only replacement
instance.›

locale M_basic_no_repl = M_trivial +
  assumes Inter_separation:
    "M(A) ==> separation(M, λx. ∀y[M]. y∈A ⟶ x∈y)"
    and Diff_separation:
    "M(B) ==> separation(M, λx. x ∉ B)"
    and cartprod_separation:
    "[| M(A); M(B) |]
      ==> separation(M, λz. ∃x[M]. x∈A & (∃y[M]. y∈B & pair(M,x,y,z)))"
    and image_separation:
    "[| M(A); M(r) |]
      ==> separation(M, λy. ∃p[M]. p∈r & (∃x[M]. x∈A & pair(M,x,y,p)))"
    and converse_separation:
    "M(r) ==> separation(M,
         λz. ∃p[M]. p∈r & (∃x[M]. ∃y[M]. pair(M,x,y,p) & pair(M,y,x,z)))"
    and restrict_separation:
    "M(A) ==> separation(M, λz. ∃x[M]. x∈A & (∃y[M]. pair(M,x,y,z)))"
    and comp_separation:
    "[| M(r); M(s) |]
      ==> separation(M, λxz. ∃x[M]. ∃y[M]. ∃z[M]. ∃xy[M]. ∃yz[M].
                  pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz) &
                  xy∈s & yz∈r)"
    and pred_separation:
    "[| M(r); M(x) |] ==> separation(M, λy. ∃p[M]. p∈r & pair(M,y,x,p))"
    and Memrel_separation:
    "separation(M, λz. ∃x[M]. ∃y[M]. pair(M,x,y,z) & x ∈ y)"
    and is_recfun_separation:
    ― ‹for well-founded recursion: used to prove ‹is_recfun_equal››
    "[| M(r); M(f); M(g); M(a); M(b) |]
     ==> separation(M,
            λx. ∃xa[M]. ∃xb[M].
                pair(M,x,a,xa) & xa ∈ r & pair(M,x,b,xb) & xb ∈ r &
                (∃fx[M]. ∃gx[M]. fun_apply(M,f,x,fx) & fun_apply(M,g,x,gx) &
                                   fx ≠ gx))"
    and power_ax:         "power_ax(M)"

lemma (in M_basic_no_repl) cartprod_iff:
  "[| M(A); M(B); M(C) |]
      ==> cartprod(M,A,B,C) ⟷
          (∃p1[M]. ∃p2[M]. powerset(M,A ∪ B,p1) & powerset(M,p1,p2) &
                   C = {z ∈ p2. ∃x∈A. ∃y∈B. z = <x,y>})"
  apply (simp add: Pair_def cartprod_def, safe)
    defer 1
    apply (simp add: powerset_def)
   apply blast
  txt‹Final, difficult case: the left-to-right direction of the theorem.›
  apply (insert power_ax, simp add: power_ax_def)
  apply (frule_tac x="A ∪ B" and P="λx. rex(M,Q(x))" for Q in rspec)
   apply (blast, clarify)
  apply (drule_tac x=z and P="λx. rex(M,Q(x))" for Q in rspec)
   apply assumption
  apply (blast intro: cartprod_iff_lemma)
  done

lemma (in M_basic_no_repl) cartprod_closed_lemma:
  "[| M(A); M(B) |] ==> ∃C[M]. cartprod(M,A,B,C)"
  apply (simp del: cartprod_abs add: cartprod_iff)
  apply (insert power_ax, simp add: power_ax_def)
  apply (frule_tac x="A ∪ B" and P="λx. rex(M,Q(x))" for Q in rspec)
   apply (blast, clarify)
  apply (drule_tac x=z and P="λx. rex(M,Q(x))" for Q in rspec, auto)
  apply (intro rexI conjI, simp+)
  apply (insert cartprod_separation [of A B], simp)
  done

text‹All the lemmas above are necessary because Powerset is not absolute.
      I should have used Replacement instead!›
lemma (in M_basic_no_repl) cartprod_closed [intro,simp]:
  "[| M(A); M(B) |] ==> M(A*B)"
  by (frule cartprod_closed_lemma, assumption, force)

lemma (in M_basic_no_repl) sum_closed [intro,simp]:
  "[| M(A); M(B) |] ==> M(A+B)"
  by (simp add: sum_def)

lemma (in M_basic_no_repl) sum_abs [simp]:
  "[| M(A); M(B); M(Z) |] ==> is_sum(M,A,B,Z) ⟷ (Z = A+B)"
  by (simp add: is_sum_def sum_def singleton_0 nat_into_M)

lemma (in M_basic_no_repl) M_converse_iff:
  "M(r) ==>
      converse(r) =
      {z ∈ ⋃(⋃(r)) * ⋃(⋃(r)).
       ∃p∈r. ∃x[M]. ∃y[M]. p = ⟨x,y⟩ & z = ⟨y,x⟩}"
  apply (rule equalityI)
   prefer 2 apply (blast dest: transM, clarify, simp)
  apply (simp add: Pair_def)
  apply (blast dest: transM)
  done

lemma (in M_basic_no_repl) converse_closed [intro,simp]:
  "M(r) ==> M(converse(r))"
  apply (simp add: M_converse_iff)
  apply (insert converse_separation [of r], simp)
  done

lemma (in M_basic_no_repl) converse_abs [simp]:
  "[| M(r); M(z) |] ==> is_converse(M,r,z) ⟷ z = converse(r)"
  apply (simp add: is_converse_def)
  apply (rule iffI)
   prefer 2 apply blast
  apply (rule M_equalityI)
    apply simp
    apply (blast dest: transM)+
  done


subsubsection ‹image, preimage, domain, range›

lemma (in M_basic_no_repl) image_closed [intro,simp]:
  "[| M(A); M(r) |] ==> M(r``A)"
  apply (simp add: image_iff_Collect)
  apply (insert image_separation [of A r], simp)
  done

lemma (in M_basic_no_repl) vimage_abs [simp]:
  "[| M(r); M(A); M(z) |] ==> pre_image(M,r,A,z) ⟷ z = r-``A"
  apply (simp add: pre_image_def)
  apply (rule iffI)
   apply (blast intro!: equalityI dest: transM, blast)
  done

lemma (in M_basic_no_repl) vimage_closed [intro,simp]:
  "[| M(A); M(r) |] ==> M(r-``A)"
  by (simp add: vimage_def)


subsubsection‹Domain, range and field›

lemma (in M_basic_no_repl) domain_closed [intro,simp]:
  "M(r) ==> M(domain(r))"
  apply (simp add: domain_eq_vimage)
  done

lemma (in M_basic_no_repl) range_closed [intro,simp]:
  "M(r) ==> M(range(r))"
  apply (simp add: range_eq_image)
  done

lemma (in M_basic_no_repl) field_abs [simp]:
  "[| M(r); M(z) |] ==> is_field(M,r,z) ⟷ z = field(r)"
  by (simp add: is_field_def field_def)

lemma (in M_basic_no_repl) field_closed [intro,simp]:
  "M(r) ==> M(field(r))"
  by (simp add: field_def)


subsubsection‹Relations, functions and application›

lemma (in M_basic_no_repl) apply_closed [intro,simp]:
  "[|M(f); M(a)|] ==> M(f`a)"
  by (simp add: apply_def)

lemma (in M_basic_no_repl) apply_abs [simp]:
  "[| M(f); M(x); M(y) |] ==> fun_apply(M,f,x,y) ⟷ f`x = y"
  apply (simp add: fun_apply_def apply_def, blast)
  done

lemma (in M_basic_no_repl) injection_abs [simp]:
  "[| M(A); M(f) |] ==> injection(M,A,B,f) ⟷ f ∈ inj(A,B)"
  apply (simp add: injection_def apply_iff inj_def)
  apply (blast dest: transM [of _ A])
  done

lemma (in M_basic_no_repl) surjection_abs [simp]:
  "[| M(A); M(B); M(f) |] ==> surjection(M,A,B,f) ⟷ f ∈ surj(A,B)"
  by (simp add: surjection_def surj_def)

lemma (in M_basic_no_repl) bijection_abs [simp]:
  "[| M(A); M(B); M(f) |] ==> bijection(M,A,B,f) ⟷ f ∈ bij(A,B)"
  by (simp add: bijection_def bij_def)


subsubsection‹Composition of relations›

lemma (in M_basic_no_repl) M_comp_iff:
  "[| M(r); M(s) |]
      ==> r O s =
          {xz ∈ domain(s) * range(r).
            ∃x[M]. ∃y[M]. ∃z[M]. xz = ⟨x,z⟩ & ⟨x,y⟩ ∈ s & ⟨y,z⟩ ∈ r}"
  apply (simp add: comp_def)
  apply (rule equalityI)
   apply clarify
   apply simp
   apply  (blast dest:  transM)+
  done

lemma (in M_basic_no_repl) comp_closed [intro,simp]:
  "[| M(r); M(s) |] ==> M(r O s)"
  apply (simp add: M_comp_iff)
  apply (insert comp_separation [of r s], simp)
  done

lemma (in M_basic_no_repl) composition_abs [simp]:
  "[| M(r); M(s); M(t) |] ==> composition(M,r,s,t) ⟷ t = r O s"
  apply safe
  txt‹Proving term‹composition(M, r, s, r O s)››
   prefer 2
   apply (simp add: composition_def comp_def)
   apply (blast dest: transM)
  txt‹Opposite implication›
  apply (rule M_equalityI)
    apply (simp add: composition_def comp_def)
    apply (blast del: allE dest: transM)+
  done

text‹no longer needed›
lemma (in M_basic_no_repl) restriction_is_function:
  "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |]
      ==> function(z)"
  apply (simp add: restriction_def ball_iff_equiv)
  apply (unfold function_def, blast)
  done

lemma (in M_basic_no_repl) restrict_closed [intro,simp]:
  "[| M(A); M(r) |] ==> M(restrict(r,A))"
  apply (simp add: M_restrict_iff)
  apply (insert restrict_separation [of A], simp)
  done

lemma (in M_basic_no_repl) Inter_closed [intro,simp]:
  "M(A) ==> M(⋂(A))"
  by (insert Inter_separation, simp add: Inter_def)

lemma (in M_basic_no_repl) Int_closed [intro,simp]:
  "[| M(A); M(B) |] ==> M(A ∩ B)"
  apply (subgoal_tac "M({A,B})")
   apply (frule Inter_closed, force+)
  done

lemma (in M_basic_no_repl) Diff_closed [intro,simp]:
  "[|M(A); M(B)|] ==> M(A-B)"
  by (insert Diff_separation, simp add: Diff_def)

subsubsection‹Some Facts About Separation Axioms›

lemma (in M_basic_no_repl) separation_conj:
  "[|separation(M,P); separation(M,Q)|] ==> separation(M, λz. P(z) & Q(z))"
  by (simp del: separation_closed
      add: separation_iff Collect_Int_Collect_eq [symmetric])

lemma (in M_basic_no_repl) separation_disj:
  "[|separation(M,P); separation(M,Q)|] ==> separation(M, λz. P(z) | Q(z))"
  by (simp del: separation_closed
      add: separation_iff Collect_Un_Collect_eq [symmetric])

lemma (in M_basic_no_repl) separation_neg:
  "separation(M,P) ==> separation(M, λz. ~P(z))"
  by (simp del: separation_closed
      add: separation_iff Diff_Collect_eq [symmetric])

lemma (in M_basic_no_repl) separation_imp:
  "[|separation(M,P); separation(M,Q)|]
      ==> separation(M, λz. P(z) ⟶ Q(z))"
  by (simp add: separation_neg separation_disj not_disj_iff_imp [symmetric])

text‹This result is a hint of how little can be done without the Reflection
  Theorem.  The quantifier has to be bounded by a set.  We also need another
  instance of Separation!›
lemma (in M_basic_no_repl) separation_rall:
  "[|M(Y); ∀y[M]. separation(M, λx. P(x,y));
        ∀z[M]. strong_replacement(M, λx y. y = {u ∈ z . P(u,x)})|]
      ==> separation(M, λx. ∀y[M]. y∈Y ⟶ P(x,y))"
  apply (simp del: separation_closed rall_abs
      add: separation_iff Collect_rall_eq)
  apply (blast intro!:  RepFun_closed dest: transM)
  done


subsubsection‹Functions and function space›

lemma (in M_basic_no_repl) succ_fun_eq2:
  "[|M(B); M(n->B)|] ==>
      succ(n) -> B =
      ⋃{z. p ∈ (n->B)*B, ∃f[M]. ∃b[M]. p = <f,b> & z = {cons(<n,b>, f)}}"
  apply (simp add: succ_fun_eq)
  apply (blast dest: transM)
  done

(* lemma (in M_basic_no_repl) funspace_succ:
     "[|M(n); M(B); M(n->B) |] ==> M(succ(n) -> B)"
apply (insert funspace_succ_replacement [of n], simp)
apply (force simp add: succ_fun_eq2 univalent_def)
done

text‹term‹M› contains all finite function spaces.  Needed to prove the
absoluteness of transitive closure.  See the definition of
‹rtrancl_alt› in in ‹WF_absolute.thy›.›
lemma (in M_basic_no_repl) finite_funspace_closed [intro,simp]:
     "[|n∈nat; M(B)|] ==> M(n->B)"
apply (induct_tac n, simp)
apply (simp add: funspace_succ nat_into_M)
done
 *)

lemma (in M_basic_no_repl) list_case'_closed [intro,simp]:
  "[|M(k); M(a); ∀x[M]. ∀y[M]. M(b(x,y))|] ==> M(list_case'(a,b,k))"
  apply (case_tac "quasilist(k)")
   apply (simp add: quasilist_def, force)
  apply (simp add: non_list_case)
  done

lemma (in M_basic_no_repl) tl'_closed: "M(x) ==> M(tl'(x))"
  apply (simp add: tl'_def)
  apply (force simp add: quasilist_def)
  done

sublocale M_basic ⊆ mbnr:M_basic_no_repl
  using Inter_separation Diff_separation cartprod_separation image_separation
    converse_separation restrict_separation comp_separation pred_separation
    Memrel_separation is_recfun_separation power_ax by unfold_locales

end
body>

Theory Recursion_Thms

section‹Some enhanced theorems on recursion›

theory Recursion_Thms
  imports "ZF-Constructible.Datatype_absolute"

begin

― ‹Removing arities from inherited simpset›
declare arity_And [simp del] arity_Or[simp del] arity_Implies[simp del]
  arity_Exists[simp del] arity_Iff[simp del]
  arity_subset_fm [simp del] arity_ordinal_fm[simp del] arity_transset_fm[simp del]

text‹We prove results concerning definitions by well-founded
recursion on some relation term‹R› and its transitive closure
term‹R^*››
  (* Restrict the relation r to the field A*A *)

lemma fld_restrict_eq : "a ∈ A ⟹ (r ∩ A×A)-``{a} = (r-``{a} ∩ A)"
  by(force)

lemma fld_restrict_mono : "relation(r) ⟹ A ⊆ B ⟹ r ∩ A×A ⊆ r ∩ B×B"
  by(auto)

lemma fld_restrict_dom :
  assumes "relation(r)" "domain(r) ⊆ A" "range(r)⊆ A"
  shows "r∩ A×A = r"
proof (rule equalityI,blast,rule subsetI)
  { fix x
    assume xr: "x ∈ r"
    from xr assms have "∃ a b . x = ⟨a,b⟩" by (simp add: relation_def)
    then obtain a b where "⟨a,b⟩ ∈ r" "⟨a,b⟩ ∈ r∩A×A" "x ∈ r∩A×A"
      using assms xr
      by force
    then have "x∈ r ∩ A×A" by simp
  }
  then show "x ∈ r ⟹ x∈ r∩A×A" for x .
qed

definition tr_down :: "[i,i] ⇒ i"
  where "tr_down(r,a) = (r^+)-``{a}"

lemma tr_downD : "x ∈ tr_down(r,a) ⟹ ⟨x,a⟩ ∈ r^+"
  by (simp add: tr_down_def vimage_singleton_iff)

lemma pred_down : "relation(r) ⟹ r-``{a} ⊆ tr_down(r,a)"
  by(simp add: tr_down_def vimage_mono r_subset_trancl)

lemma tr_down_mono : "relation(r) ⟹ x ∈ r-``{a} ⟹ tr_down(r,x) ⊆ tr_down(r,a)"
  by(rule subsetI,simp add:tr_down_def,auto dest: underD,force simp add: underI r_into_trancl trancl_trans)

lemma rest_eq :
  assumes "relation(r)" and "r-``{a} ⊆ B" and "a ∈ B"
  shows "r-``{a} = (r∩B×B)-``{a}"
proof (intro equalityI subsetI)
  fix x
  assume "x ∈ r-``{a}"
  then
  have "x ∈ B" using assms by (simp add: subsetD)
  from ‹x∈ r-``{a}›
  have "⟨x,a⟩ ∈ r" using underD by simp
  then
  show "x ∈ (r∩B×B)-``{a}" using ‹x∈B› ‹a∈B› underI by simp
next
  from assms
  show "x ∈ r -`` {a}" if  "x ∈ (r ∩ B×B) -`` {a}" for x
    using vimage_mono that by auto
qed

lemma wfrec_restr_eq : "r' = r ∩ A×A ⟹ wfrec[A](r,a,H) = wfrec(r',a,H)"
  by(simp add:wfrec_on_def)

lemma wfrec_restr :
  assumes rr: "relation(r)" and wfr:"wf(r)"
  shows  "a ∈ A ⟹ tr_down(r,a) ⊆ A ⟹ wfrec(r,a,H) = wfrec[A](r,a,H)"
proof (induct a arbitrary:A rule:wf_induct_raw[OF wfr] )
  case (1 a)
  have wfRa : "wf[A](r)"
    using wf_subset wfr wf_on_def Int_lower1 by simp
  from pred_down rr
  have "r -`` {a} ⊆ tr_down(r, a)" .
  with 1
  have "r-``{a} ⊆ A" by (force simp add: subset_trans)
  {
    fix x
    assume x_a : "x ∈ r-``{a}"
    with ‹r-``{a} ⊆ A›
    have "x ∈ A" ..
    from pred_down rr
    have b : "r -``{x} ⊆ tr_down(r,x)" .
    then
    have "tr_down(r,x) ⊆ tr_down(r,a)"
      using tr_down_mono x_a rr by simp
    with 1
    have "tr_down(r,x) ⊆ A" using subset_trans by force
    have "⟨x,a⟩ ∈ r" using x_a  underD by simp
    with 1 ‹tr_down(r,x) ⊆ A› ‹x ∈ A›
    have "wfrec(r,x,H) = wfrec[A](r,x,H)" by simp
  }
  then
  have "x∈ r-``{a} ⟹ wfrec(r,x,H) =  wfrec[A](r,x,H)" for x  .
  then
  have Eq1 :"(λ x ∈ r-``{a} . wfrec(r,x,H)) = (λ x ∈ r-``{a} . wfrec[A](r,x,H))"
    using lam_cong by simp

  from assms
  have "wfrec(r,a,H) = H(a,λ x ∈ r-``{a} . wfrec(r,x,H))" by (simp add:wfrec)
  also
  have "... = H(a,λ x ∈ r-``{a} . wfrec[A](r,x,H))"
    using assms Eq1 by simp
  also from 1 ‹r-``{a} ⊆ A›
  have "... = H(a,λ x ∈ (r∩A×A)-``{a} . wfrec[A](r,x,H))"
    using assms rest_eq  by simp
  also from ‹a∈A›
  have "... = H(a,λ x ∈ (r-``{a})∩A . wfrec[A](r,x,H))"
    using fld_restrict_eq by simp
  also from ‹a∈A› ‹wf[A](r)›
  have "... = wfrec[A](r,a,H)" using wfrec_on by simp
  finally show ?case .
qed

lemmas wfrec_tr_down = wfrec_restr[OF _ _ _ subset_refl]

lemma wfrec_trans_restr : "relation(r) ⟹ wf(r) ⟹ trans(r) ⟹ r-``{a}⊆A ⟹ a ∈ A ⟹
  wfrec(r, a, H) = wfrec[A](r, a, H)"
  by(subgoal_tac "tr_down(r,a) ⊆ A",auto simp add : wfrec_restr tr_down_def trancl_eq_r)


lemma field_trancl : "field(r^+) = field(r)"
  by (blast intro: r_into_trancl dest!: trancl_type [THEN subsetD])

definition
  Rrel :: "[i⇒i⇒o,i] ⇒ i" where
  "Rrel(R,A) ≡ {z∈A×A. ∃x y. z = ⟨x, y⟩ ∧ R(x,y)}"

lemma RrelI : "x ∈ A ⟹ y ∈ A ⟹ R(x,y) ⟹ ⟨x,y⟩ ∈ Rrel(R,A)"
  unfolding Rrel_def by simp

lemma Rrel_mem: "Rrel(mem,x) = Memrel(x)"
  unfolding Rrel_def Memrel_def ..

lemma relation_Rrel: "relation(Rrel(R,d))"
  unfolding Rrel_def relation_def by simp

lemma field_Rrel: "field(Rrel(R,d)) ⊆  d"
  unfolding Rrel_def by auto

lemma Rrel_mono : "A ⊆ B ⟹ Rrel(R,A) ⊆ Rrel(R,B)"
  unfolding Rrel_def by blast

lemma Rrel_restr_eq : "Rrel(R,A) ∩ B×B = Rrel(R,A∩B)"
  unfolding Rrel_def by blast

(* now a consequence of the previous lemmas *)
lemma field_Memrel : "field(Memrel(A)) ⊆ A"
  (* unfolding field_def using Ordinal.Memrel_type by blast *)
  using Rrel_mem field_Rrel by blast

lemma restrict_trancl_Rrel:
  assumes "R(w,y)"
  shows "restrict(f,Rrel(R,d)-``{y})`w
       = restrict(f,(Rrel(R,d)^+)-``{y})`w"
proof (cases "y∈d")
  let ?r="Rrel(R,d)" and ?s="(Rrel(R,d))^+"
  case True
  show ?thesis
  proof (cases "w∈d")
    case True
    with ‹y∈d› assms
    have "⟨w,y⟩∈?r"
      unfolding Rrel_def by blast
    then
    have "⟨w,y⟩∈?s"
      using r_subset_trancl[of ?r] relation_Rrel[of R d] by blast
    with ‹⟨w,y⟩∈?r›
    have "w∈?r-``{y}" "w∈?s-``{y}"
      using vimage_singleton_iff by simp_all
    then
    show ?thesis by simp
  next
    case False
    then
    have "w∉domain(restrict(f,?r-``{y}))"
      using subsetD[OF field_Rrel[of R d]] by auto
    moreover from ‹w∉d›
    have "w∉domain(restrict(f,?s-``{y}))"
      using subsetD[OF field_Rrel[of R d], of w] field_trancl[of ?r]
        fieldI1[of w y ?s] by auto
    ultimately
    have "restrict(f,?r-``{y})`w = 0" "restrict(f,?s-``{y})`w = 0"
      unfolding apply_def by auto
    then show ?thesis by simp
  qed
next
  let ?r="Rrel(R,d)"
  let ?s="?r^+"
  case False
  then
  have "?r-``{y}=0"
    unfolding Rrel_def by blast
  then
  have "w∉?r-``{y}" by simp
  with ‹y∉d› assms
  have "y∉field(?s)"
    using field_trancl subsetD[OF field_Rrel[of R d]] by force
  then
  have "w∉?s-``{y}"
    using vimage_singleton_iff by blast
  with ‹w∉?r-``{y}›
  show ?thesis by simp
qed

lemma restrict_trans_eq:
  assumes "w ∈ y"
  shows "restrict(f,Memrel(eclose({x}))-``{y})`w
       = restrict(f,(Memrel(eclose({x}))^+)-``{y})`w"
  using assms restrict_trancl_Rrel[of mem ] Rrel_mem by (simp)

lemma wf_eq_trancl:
  assumes "⋀ f y . H(y,restrict(f,R-``{y})) = H(y,restrict(f,R^+-``{y}))"
  shows  "wfrec(R, x, H) = wfrec(R^+, x, H)" (is "wfrec(?r,_,_) = wfrec(?r',_,_)")
proof -
  have "wfrec(R, x, H) = wftrec(?r^+, x, λy f. H(y, restrict(f,?r-``{y})))"
    unfolding wfrec_def ..
  also
  have " ... = wftrec(?r^+, x, λy f. H(y, restrict(f,(?r^+)-``{y})))"
    using assms by simp
  also
  have " ... =  wfrec(?r^+, x, H)"
    unfolding wfrec_def using trancl_eq_r[OF relation_trancl trans_trancl] by simp
  finally
  show ?thesis .
qed

lemma transrec_equal_on_Ord:
  assumes
    "⋀x f . Ord(x) ⟹ foo(x,f) = bar(x,f)"
    "Ord(α)"
  shows
    "transrec(α, foo) = transrec(α, bar)"
proof -
  have "transrec(β,foo) = transrec(β,bar)" if "Ord(β)" for β
    using that
  proof (induct rule:trans_induct)
    case (step β)
    have "transrec(β, foo) = foo(β, λx∈β. transrec(x, foo))"
      using def_transrec[of "λx. transrec(x, foo)" foo] by blast
    also from assms and step
    have " … = bar(β, λx∈β. transrec(x, foo))"
      by simp
    also from step
    have " … = bar(β, λx∈β. transrec(x, bar))"
      by (auto)
    also
    have " … = transrec(β, bar)"
      using def_transrec[of "λx. transrec(x, bar)" bar, symmetric]
      by blast
    finally
    show "transrec(β, foo) = transrec(β, bar)" .
  qed
  with assms
  show ?thesis by simp
qed

― ‹Next theorem is very similar to @{thm transrec_equal_on_Ord}›
lemma (in M_eclose) transrec_equal_on_M:
  assumes
    "⋀x f . M(x) ⟹ M(f) ⟹ foo(x,f) = bar(x,f)"
    "⋀β. M(β) ⟹ transrec_replacement(M,is_foo,β)" "relation2(M,is_foo,foo)"
    "strong_replacement(M, λx y. y = ⟨x, transrec(x, foo)⟩)"
    "∀x[M]. ∀g[M]. function(g) ⟶ M(foo(x,g))"
    "M(α)" "Ord(α)"
  shows
    "transrec(α, foo) = transrec(α, bar)"
proof -
  have "M(transrec(x, foo))" if "Ord(x)" and "M(x)" for x
    using that assms transrec_closed[of is_foo]
    by simp
  have "transrec(β,foo) = transrec(β,bar)" "M(transrec(β,foo))" if "Ord(β)" "M(β)" for β
    using that
  proof (induct rule:trans_induct)
    case (step β)
    moreover
    assume "M(β)"
    moreover
    note ‹Ord(β)⟹ M(β) ⟹ M(transrec(β, foo))›
    ultimately
    show "M(transrec(β, foo))" by blast
    with step ‹M(β)› ‹⋀x. Ord(x)⟹ M(x) ⟹ M(transrec(x, foo))›
      ‹strong_replacement(M, λx y. y = ⟨x, transrec(x, foo)⟩)›
    have "M(λx∈β. transrec(x, foo))"
      using Ord_in_Ord transM[of _ β]
      by (rule_tac lam_closed) auto
    have "transrec(β, foo) = foo(β, λx∈β. transrec(x, foo))"
      using def_transrec[of "λx. transrec(x, foo)" foo] by blast
    also from assms and ‹M(λx∈β. transrec(x, foo))› ‹M(β)›
    have " … = bar(β, λx∈β. transrec(x, foo))"
      by simp
    also from step and ‹M(β)›
    have " … = bar(β, λx∈β. transrec(x, bar))"
      using transM[of _ β] by (auto)
    also
    have " … = transrec(β, bar)"
      using def_transrec[of "λx. transrec(x, bar)" bar, symmetric]
      by blast
    finally
    show "transrec(β, foo) = transrec(β, bar)" .
  qed
  with assms
  show ?thesis by simp
qed


lemma ordermap_restr_eq:
  assumes "well_ord(X,r)"
  shows "ordermap(X, r) = ordermap(X, r ∩ X×X)"
proof -
  let ?A="λx . Order.pred(X, x, r)"
  let ?B="λx . Order.pred(X, x, r ∩ X × X)"
  let ?F="λx f. f `` ?A(x)"
  let ?G="λx f. f `` ?B(x)"
  let ?P="λ z. z∈X ⟶ wfrec(r ∩ X × X,z,λx f. f `` ?A(x)) = wfrec(r ∩ X × X,z,λx f. f `` ?B(x))"
  have pred_eq:
    "Order.pred(X, x, r ∩ X × X) = Order.pred(X, x, r)" if "x∈X" for x
    unfolding Order.pred_def using that by auto
  from assms
  have wf_onX:"wf(r ∩ X × X)" unfolding well_ord_def wf_on_def by simp
  {
    have "?P(z)" for z
    proof(induct rule:wf_induct[where P="?P",OF wf_onX])
      case (1 x)
      {
        assume "x∈X"
        from 1
        have lam_eq:
          "(λw∈(r ∩ X × X) -`` {x}. wfrec(r ∩ X × X, w, ?F)) =
             (λw∈(r ∩ X × X) -`` {x}. wfrec(r ∩ X × X, w, ?G))" (is "?L=?R")
        proof -
          have "wfrec(r ∩ X × X, w, ?F) = wfrec(r ∩ X × X, w, ?G)" if "w∈(r∩X×X)-``{x}" for w
            using 1 that by auto
          then show ?thesis using lam_cong[OF refl] by simp
        qed
        then
        have "wfrec(r ∩ X × X, x, ?F) = ?L `` ?A(x)"
          using wfrec[OF wf_onX,of x ?F] by simp
        also have "... =  ?R `` ?B(x)"
          using lam_eq pred_eq[OF ‹x∈_›] by simp
        also
        have "... = wfrec(r ∩ X × X, x, ?G)"
          using wfrec[OF wf_onX,of x ?G] by simp
        finally
        have "wfrec(r ∩ X × X, x, ?F) = wfrec(r ∩ X × X, x, ?G)" by simp
      }
      then
      show ?case by simp
    qed
  }
  then
  show ?thesis
    unfolding ordermap_def wfrec_on_def using Int_ac by simp
qed

end
d>

Theory Synthetic_Definition

section‹Automatic synthesis of formulas›
theory Synthetic_Definition
  imports
    Utils
  keywords
    "synthesize" :: thy_decl % "ML"
    and
    "synthesize_notc" :: thy_decl % "ML"
    and
    "generate_schematic" :: thy_decl % "ML"
    and
    "arity_theorem" :: thy_decl % "ML"
    and
    "manual_schematic" :: thy_goal_stmt % "ML"
    and
    "manual_arity" :: thy_goal_stmt % "ML"
    and
    "from_schematic"
    and
    "for"
    and
    "from_definition"
    and
    "assuming"
    and
    "intermediate"

begin

named_theorems fm_definitions "Definitions of synthetized formulas."

named_theorems iff_sats "Theorems for synthetising formulas."

named_theorems arity "Theorems for arity of formulas."

named_theorems arity_aux "Auxiliary theorems for calculating arities."

ML‹
val $` = curry ((op $) o swap)
infix $`

infix 6 &&&
val op &&& = Utils.&&&

infix 6 ***
val op *** = Utils.***

fun arity_goal intermediate def_name lthy =
  let
    val thm = Proof_Context.get_thm lthy (def_name ^ "_def")
    val (_, tm, _) = Utils.thm_concl_tm lthy (def_name ^ "_def")
    val (def, tm) = tm |> Utils.dest_eq_tms'
    fun first_lambdas (Abs (body as (_, ty, _))) =
        if ty = @{typ "i"}
          then (op ::) (Utils.dest_abs body |>> Utils.var_i ||> first_lambdas)
          else Utils.dest_abs body |> first_lambdas o #2
      | first_lambdas _ = []
    val (def, vars) = Term.strip_comb def
    val vs = vars @ first_lambdas tm
    val def = fold (op $`) vs def
    val hyps = map (fn v => Utils.mem_ v Utils.nat_ |> Utils.tp) vs
    val concl = @{const IFOL.eq(i)} $ (@{const arity} $ def) $ Var (("ar", 0), @{typ "i"})
    val g_iff = Logic.list_implies (hyps, Utils.tp concl)
    val attribs = if intermediate then [] else @{attributes [arity]}
  in
    (g_iff, "arity_" ^ def_name ^ (if intermediate then "'" else ""), attribs, thm, vs)
  end

fun manual_arity intermediate def_name pos lthy =
  let
    val (goal, thm_name, attribs, _, _) = arity_goal intermediate def_name lthy
  in
    Proof.theorem NONE (fn thmss => Utils.display "theorem" pos
                                    o Local_Theory.note ((Binding.name thm_name, attribs), hd thmss))
    [[(goal, [])]] lthy
  end

fun prove_arity thms goal ctxt =
  let
    val rules = (Named_Theorems.get ctxt named_theorems‹arity›) @
      (Named_Theorems.get ctxt named_theorems‹arity_aux›)
  in
    Goal.prove ctxt [] [] goal
    (K (rewrite_goal_tac ctxt thms 1 THEN Method.insert_tac ctxt rules 1 THEN asm_simp_tac ctxt 1))
  end

fun auto_arity intermediate def_name pos lthy =
  let
    val (goal, thm_name, attribs, def_thm, vs) = arity_goal intermediate def_name lthy
    val intermediate_text = if intermediate then "intermediate" else ""
    val help = "You can manually prove the arity_theorem by typing:\n"
             ^ "manual_arity " ^ intermediate_text ^ " for \"" ^ def_name ^ "\"\n"
    val thm = prove_arity [def_thm] goal lthy
              handle ERROR s => help ^ "\n\n" ^ s |> Exn.reraise o ERROR
    val thm = Utils.fix_vars thm (map Utils.freeName vs) lthy
  in
    Local_Theory.note ((Binding.name thm_name, attribs), [thm]) lthy |> Utils.display "theorem" pos
  end

fun prove_tc_form goal thms ctxt =
  Goal.prove ctxt [] [] goal (K (rewrite_goal_tac ctxt thms 1 THEN auto_tac ctxt))

fun prove_sats_tm thm_auto thms goal ctxt =
  let
    val ctxt' = ctxt |> Simplifier.add_simp (hd thm_auto)
  in
    Goal.prove ctxt [] [] goal
    (K (rewrite_goal_tac ctxt thms 1 THEN PARALLEL_ALLGOALS (asm_simp_tac ctxt')))
  end

fun prove_sats_iff goal ctxt = Goal.prove ctxt [] [] goal (K (asm_simp_tac ctxt 1))

fun is_mem (@{const mem} $ _ $  _) = true
  | is_mem _ = false

fun pre_synth_thm_sats term set env vars vs lthy =
  let
    val (_, tm, ctxt1) = Utils.thm_concl_tm lthy term
    val