# 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) *)

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"

lemma succ_pred_eq  :  "m â nat â¹ m â  0  â¹ succ(pred(m)) = m"
by (auto elim: natE)

lemma succ_ltI : "succ(j) < n â¹ j < n"

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"
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

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"

lemma vimage_fun_sing:
assumes "fâAâB" "bâB"
shows "{aâA . fa=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} = SC"
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  domain_type]
lam_funtype[of A f, THEN  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. fa = 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. ha=b})) â inj(B,A)"
proof -
let ?f="Î»bâB. minimum(r, {aâA. ha=b})"
have "minimum(r, {a â A . h  a = b}) â {aâA. ha=b}" if "bâB" for b
proof -
from â¹h â surj(A,B)âº that
have "{aâA. ha=b} â  0"
unfolding surj_def by blast
with â¹well_ord(A,r)âº
show "minimum(r,{aâA. ha=b}) â {aâA. ha=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. ha=w})"
"x = h  minimum(r,{aâA. ha=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
{
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 "fx â 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 fj else gj"

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: "?hx â 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 "?hx = fx"
unfolding union_fun_def  beta by simp
with â¹f â m â nâº â¹xâmâº
have "?hx â n" by simp
then show ?thesis ..
next
case False
with â¹x â m âª pâº
have "x â p"
by auto
with â¹xâmâº
have "?hx = gx"
unfolding union_fun_def using beta by simp
with â¹g â p â qâº â¹xâpâº
have "?hx â 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(fi,env') = nth(i,env)"
"â j . j â p â¶ nth(gj,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(?hx,env')" if "x â m âª p" for x
using that
proof (cases "xâm")
case True
with â¹xâmâº
have "?hx = fx"
unfolding union_fun_def  beta by simp
with assms â¹xâmâº
have "nth(x,env) = nth(?hx,env')" by simp
then show ?thesis .
next
case False
with â¹x â m âª pâº
have
"x â p" "xâm"  by auto
then
have "?hx = gx"
unfolding union_fun_def beta by simp
with assms â¹xâpâº
have "nth(x,env) = nth(?hx,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 fj 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 = fx"
proof -
from â¹mânatâº
with assms
using ltI[of x m] lt_trans2[of x m "m+â©Ïp"] ltD by simp
from assms
have "x<m"
using ltI by simp
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"
by simp
with assms
have "Â¬ x<m"
using not_lt_iff_le[THEN iffD2] by simp
from assms
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(fi,env')"
"â j. j < p â¹ nth(j,env1) = nth(gj,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âº
from â¹pânatâº
have "nth(x, env @ env1) = nth(?hx,env'@env2)" if "x<m+â©Ïp" for x
proof (cases "x<m")
case True
then
have 2: "?hx= fx" "xâm" "fx â 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 "fx < n" "fx<length(env')"  "fxâ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(fx,env')"
using 2 â¹x<mâº assms by simp
also
have "... = nth(fx,env'@env2)"
using nth_append[OF â¹env'âlist(M)âº] â¹fx<length(env')âº â¹fx ânatâº by simp
also
have "... = nth(?hx,env'@env2)"
using 2 by simp
finally
have "nth(x, env @ env1) = nth(?hx,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 : "?hx= g(x#-m)+â©Ïn"  "Â¬ x <length(env)"
unfolding rsum_def
using  sum_inr that beta ltD by simp_all
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âº]
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âº
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(?hx,env'@env2)"
using 2 by simp
finally
have "nth(x, env @ env1) = nth(?hx,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"
proof -
let ?h = "rsum(f,g,m,n,p)"
from â¹mânatâº â¹nânatâº â¹qânatâº
from â¹pânatâº
{fix x
with 1 have "?hx= fx" "xâm"
using assms sum_inl ltD by simp_all
with â¹fâmânâº
have "?hx â n" by simp
with â¹nânatâº have "?hx < n" using ltI by simp
have "?hx < n+â©Ïq" using lt_trans2 by simp
then
have "?hx â n+â©Ïq"  using ltD by simp
}
then have 1:"?hx â n+â©Ïq" if "xâm+â©Ïp" "x<m" for x using that .
{fix x
with 1
have 2 : "?hx= g(x#-m)+â©Ïn"
using assms sum_inr ltD by simp_all
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 "?hx â n+â©Ïq"  using ltD by simp
}
then have 2:"?hx â n+â©Ïq" if "xâm+â©Ïp" "mâ¤x" for x using that .
have
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)) â
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)) â
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(fi,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
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
}
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(fi,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(fx)"
by(subgoal_tac "xânat",unfold sum_id_def,subst sum_inr,

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)"
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 (fx, fy))"

"ren(Equal(x,y)) =
(Î» n â nat . Î» m â nat. Î»f â n â m. Equal (fx, fy))"

"ren(Nand(p,q)) =
(Î» n â nat . Î» m â nat. Î»f â n â m. Nand (ren(p)nmf, ren(q)nmf))"

"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)nmf â 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)nmf)â¤m"
using assms
proof (induct set:formula)
case (Member x y)
then have "fx â m" "fy â m"
then show ?case using Member by (simp add: Un_least_lt ltI)
next
case (Equal x y)
then have "fx â m" "fy â m"
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)nmf) â¤ m" and  "arity(ren(q)nmf) â¤ 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(fi,Ï')"
"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(?gj,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 "fiâm" using â¹fânâmâº apply_type â¹iânâº by simp
then have "fi â 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(fi,Ï')" using assms â¹iânâº ltI by simp
also have "... = nth(succ(fi),Cons(a,Ï'))" using â¹fiânatâº by simp
also have "... = nth(?gsucc(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(?gsucc(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(fi,Ï') â§ â¹
sats(M,Ï,Ï) â· sats(M,ren(Ï)nmf,Ï')"
using â¹Ï â formulaâº
proof(induct Ï arbitrary:n m Ï Ï' f)
case (Member x y)
have "ren(Member(x,y))nmf = Member(fx,fy)" 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))nmf = Equal(fx,fy)" 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))nmf = Nand(ren(p)nmf,ren(q)nmf)" 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(fi,Ï')" for i using Nand ltI by simp
moreover from this
have "sats(M,p,Ï) â· sats(M,ren(p)nmf,Ï')" 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(fi,Ï')" for i using Nand ltI by simp
moreover from this
have "sats(M,q,Ï) â· sats(M,ren(q)nmf,Ï')" using assms â¹arity(q)â¤nâº Nand by simp
ultimately
show ?case using Nand by simp
next
case (Forall p)
have 0:"ren(Forall(p))nmf = 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(?gj, 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

# 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  [@{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  [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(rA)" 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(fa)" 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) â· fx = 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 `