# Theory Internalizations

```section‹Aids to internalize formulas›

theory Internalizations
imports
DPow_absolute
Synthetic_Definition
Nat_Miscellanea
begin

hide_const (open) Order.pred

definition
infinity_ax :: "(i ⇒ o) ⇒ o" where
"infinity_ax(M) ≡
(∃I[M]. (∃z[M]. empty(M,z) ∧ z∈I) ∧ (∀y[M]. y∈I ⟶ (∃sy[M]. successor(M,y,sy) ∧ sy∈I)))"

definition
wellfounded_trancl :: "[i=>o,i,i,i] => o" where
"wellfounded_trancl(M,Z,r,p) ≡
∃w[M]. ∃wx[M]. ∃rp[M].
w ∈ Z & pair(M,w,p,wx) & tran_closure(M,r,rp) & wx ∈ rp"

lemma empty_intf :
"infinity_ax(M) ⟹
(∃z[M]. empty(M,z))"
by (auto simp add: empty_def infinity_ax_def)

lemma Transset_intf :
"Transset(M) ⟹  y∈x ⟹ x ∈ M ⟹ y ∈ M"

definition
choice_ax :: "(i⇒o) ⇒ o" where
"choice_ax(M) ≡ ∀x[M]. ∃a[M]. ∃f[M]. ordinal(M,a) ∧ surjection(M,a,x,f)"

lemma (in M_basic) choice_ax_abs :
"choice_ax(M) ⟷ (∀x[M]. ∃a[M]. ∃f[M]. Ord(a) ∧ f ∈ surj(a,x))"
unfolding choice_ax_def
by simp

txt‹Setting up notation for internalized formulas›

abbreviation
dec10  :: i   ("10") where "10 ≡ succ(9)"
abbreviation
dec11  :: i   ("11") where "11 ≡ succ(10)"
abbreviation
dec12  :: i   ("12") where "12 ≡ succ(11)"
abbreviation
dec13  :: i   ("13") where "13 ≡ succ(12)"
abbreviation
dec14  :: i   ("14") where "14 ≡ succ(13)"
abbreviation
dec15  :: i   ("15") where "15 ≡ succ(14)"
abbreviation
dec16  :: i   ("16") where "16 ≡ succ(15)"
abbreviation
dec17  :: i   ("17") where "17 ≡ succ(16)"
abbreviation
dec18  :: i   ("18") where "18 ≡ succ(17)"
abbreviation
dec19  :: i   ("19") where "19 ≡ succ(18)"
abbreviation
dec20  :: i   ("20") where "20 ≡ succ(19)"
abbreviation
dec21  :: i   ("21") where "21 ≡ succ(20)"
abbreviation
dec22  :: i   ("22") where "22 ≡ succ(21)"
abbreviation
dec23  :: i   ("23") where "23 ≡ succ(22)"
abbreviation
dec24  :: i   ("24") where "24 ≡ succ(23)"
abbreviation
dec25  :: i   ("25") where "25 ≡ succ(24)"
abbreviation
dec26  :: i   ("26") where "26 ≡ succ(25)"
abbreviation
dec27  :: i   ("27") where "27 ≡ succ(26)"
abbreviation
dec28  :: i   ("28") where "28 ≡ succ(27)"
abbreviation
dec29  :: i   ("29") where "29 ≡ succ(28)"

notation Member (‹⋅_ ∈/ _⋅›)
notation Equal (‹⋅_ =/ _⋅›)
notation Nand (‹⋅¬'(_ ∧/ _')⋅›)
notation And (‹⋅_ ∧/ _⋅›)
notation Or (‹⋅_ ∨/ _⋅›)
notation Iff (‹⋅_ ↔/ _⋅›)
notation Implies (‹⋅_ →/ _⋅›)
notation Neg (‹⋅¬_⋅›)
notation Forall (‹'(⋅∀(/_)⋅')›)
notation Exists (‹'(⋅∃(/_)⋅')›)

notation subset_fm (‹⋅_ ⊆/ _⋅›)
notation succ_fm (‹⋅succ'(_') is _⋅›)
notation empty_fm (‹⋅_ is empty⋅›)
notation fun_apply_fm (‹⋅_`_ is _⋅›)
notation big_union_fm (‹⋅⋃_ is _⋅›)
notation upair_fm (‹⋅{_,_} is _ ⋅›)
notation ordinal_fm (‹⋅_ is ordinal⋅›)

notation pair_fm (‹⋅⟨_,_⟩ is _ ⋅›)
notation composition_fm (‹⋅_ ∘ _ is _ ⋅›)
notation domain_fm (‹⋅dom'(_') is _ ⋅›)
notation range_fm (‹⋅ran'(_') is _ ⋅›)
notation union_fm (‹⋅_ ∪ _ is _ ⋅›)
notation image_fm (‹⋅_ `` _ is _ ⋅›)
notation pre_image_fm (‹⋅_ -`` _ is _ ⋅›)
notation field_fm (‹⋅fld'(_') is _ ⋅›)
notation cons_fm (‹⋅cons'(_,_') is _ ⋅›)
notation number1_fm (‹⋅_ is the number one⋅›)
notation function_fm (‹⋅_ is funct⋅›)
notation relation_fm (‹⋅_ is relat⋅›)
notation restriction_fm (‹⋅_ ↾ _ is _ ⋅›)
notation transset_fm (‹⋅_ is transitive⋅›)
notation limit_ordinal_fm (‹⋅_ is limit⋅›)
notation finite_ordinal_fm (‹⋅_ is finite ord⋅›)
notation omega_fm (‹⋅_ is ω⋅›)
notation cartprod_fm (‹⋅_ × _ is _⋅›)
notation Memrel_fm (‹⋅Memrel'(_') is _⋅›)
notation quasinat_fm (‹⋅_ is qnat⋅›)
(* notation rtran_closure_mem_fm (‹⋅{_,_} is _ ⋅›)
notation rtran_closure_fm (‹⋅{_,_} is _ ⋅›)
notation tran_closure_fm (‹⋅_ is  ⋅›)
notation order_isomorphism_fm (‹⋅{_,_} is _ ⋅›) *)
notation Inl_fm (‹⋅Inl'(_') is _ ⋅›)
notation Inr_fm (‹⋅Inr'(_') is _ ⋅›)
notation pred_set_fm (‹⋅_-predecessors of _ are _⋅›)

abbreviation
fm_typedfun :: "[i,i,i] ⇒ i" (‹⋅_ : _ → _⋅›) where
"fm_typedfun(f,A,B) ≡ typed_function_fm(A,B,f)"

abbreviation
fm_surjection :: "[i,i,i] ⇒ i" (‹⋅_ surjects _ to _⋅›) where
"fm_surjection(f,A,B) ≡ surjection_fm(A,B,f)"

abbreviation
fm_injection :: "[i,i,i] ⇒ i" (‹⋅_ injects _ to _⋅›) where
"fm_injection(f,A,B) ≡ injection_fm(A,B,f)"

abbreviation
fm_bijection :: "[i,i,i] ⇒ i" (‹⋅_ bijects _ to _⋅›) where
"fm_bijection(f,A,B) ≡ bijection_fm(A,B,f)"

text‹We found it useful to have slightly different versions of some
results in ZF-Constructible:›
lemma nth_closed :
assumes "env∈list(A)" "0∈A"
shows "nth(n,env)∈A"
using assms unfolding nth_def by (induct env; simp)

lemma conj_setclass_model_iff_sats [iff_sats]:
"[| 0 ∈ A; nth(i,env) = x; env ∈ list(A);
P ⟷ sats(A,p,env); env ∈ list(A) |]
==> (P ∧ (##A)(x)) ⟷ sats(A, p, env)"
"[| 0 ∈ A; nth(i,env) = x; env ∈ list(A);
P ⟷ sats(A,p,env); env ∈ list(A) |]
==> ((##A)(x) ∧ P) ⟷ sats(A, p, env)"
using nth_closed[of env A i]
by auto

lemma conj_mem_model_iff_sats [iff_sats]:
"[| 0 ∈ A; nth(i,env) = x; env ∈ list(A);
P ⟷ sats(A,p,env); env ∈ list(A) |]
==> (P ∧ x ∈ A) ⟷ sats(A, p, env)"
"[| 0 ∈ A; nth(i,env) = x; env ∈ list(A);
P ⟷ sats(A,p,env); env ∈ list(A) |]
==> (x ∈ A ∧ P) ⟷ sats(A, p, env)"
using nth_closed[of env A i]
by auto

(* lemma [iff_sats]:
"[| 0 ∈ A; nth(i,env) = x; env ∈ list(A);
P ⟷ sats(A,p,env); env ∈ list(A) |]
==> (x ∈ A ⟷ P) ⟷ sats(A, p, env)"
"[| 0 ∈ A; nth(i,env) = x; env ∈ list(A);
P ⟷ sats(A,p,env); env ∈ list(A) |]
==> (P ⟷ x ∈ A) ⟷ sats(A, p, env)"

"[| 0 ∈ A; nth(i,env) = x; env ∈ list(A);
P ⟷ sats(A,p,env); env ∈ list(A) |]
==> (x ∈ A ⟶ P) ⟷ sats(A, p, env)"

using nth_closed[of env A i]
by auto *)

lemma mem_model_iff_sats [iff_sats]:
"[| 0 ∈ A; nth(i,env) = x; env ∈ list(A)|]
==> (x∈A) ⟷ sats(A, Exists(Equal(0,0)), env)"
using nth_closed[of env A i]
by auto

lemma subset_iff_sats[iff_sats]:
"nth(i, env) = x ⟹ nth(j, env) = y ⟹ i∈nat ⟹ j∈nat ⟹
env ∈ list(A) ⟹ subset(##A, x, y) ⟷ sats(A, subset_fm(i, j), env)"
using sats_subset_fm' by simp

lemma not_mem_model_iff_sats [iff_sats]:
"[| 0 ∈ A; nth(i,env) = x; env ∈ list(A)|]
==> (∀ x . x ∉ A) ⟷ sats(A, Neg(Exists(Equal(0,0))), env)"
by auto

lemma top_iff_sats [iff_sats]:
"env ∈ list(A) ⟹ 0 ∈ A ⟹ sats(A, Exists(Equal(0,0)), env)"
by auto

lemma prefix1_iff_sats[iff_sats]:
assumes
"x ∈ nat" "env ∈ list(A)" "0 ∈ A" "a ∈ A"
shows
"a = nth(x,env) ⟷ sats(A, Equal(0,x+⇩ω1), Cons(a,env))"
"nth(x,env) = a ⟷ sats(A, Equal(x+⇩ω1,0), Cons(a,env))"
"a ∈ nth(x,env) ⟷ sats(A, Member(0,x+⇩ω1), Cons(a,env))"
"nth(x,env) ∈ a ⟷ sats(A, Member(x+⇩ω1,0), Cons(a,env))"
using assms nth_closed
by simp_all

lemma prefix2_iff_sats[iff_sats]:
assumes
"x ∈ nat" "env ∈ list(A)" "0 ∈ A" "a ∈ A" "b ∈ A"
shows
"b = nth(x,env) ⟷ sats(A, Equal(1,x+⇩ω2), Cons(a,Cons(b,env)))"
"nth(x,env) = b ⟷ sats(A, Equal(x+⇩ω2,1), Cons(a,Cons(b,env)))"
"b ∈ nth(x,env) ⟷ sats(A, Member(1,x+⇩ω2), Cons(a,Cons(b,env)))"
"nth(x,env) ∈ b ⟷ sats(A, Member(x+⇩ω2,1), Cons(a,Cons(b,env)))"
using assms nth_closed
by simp_all

lemma prefix3_iff_sats[iff_sats]:
assumes
"x ∈ nat" "env ∈ list(A)" "0 ∈ A" "a ∈ A" "b ∈ A" "c ∈ A"
shows
"c = nth(x,env) ⟷ sats(A, Equal(2,x+⇩ω3), Cons(a,Cons(b,Cons(c,env))))"
"nth(x,env) = c ⟷ sats(A, Equal(x+⇩ω3,2), Cons(a,Cons(b,Cons(c,env))))"
"c ∈ nth(x,env) ⟷ sats(A, Member(2,x+⇩ω3), Cons(a,Cons(b,Cons(c,env))))"
"nth(x,env) ∈ c ⟷ sats(A, Member(x+⇩ω3,2), Cons(a,Cons(b,Cons(c,env))))"
using assms nth_closed
by simp_all

lemmas FOL_sats_iff = sats_Nand_iff sats_Forall_iff sats_Neg_iff sats_And_iff
sats_Or_iff sats_Implies_iff sats_Iff_iff sats_Exists_iff

lemma nth_ConsI: "⟦nth(n,l) = x; n ∈ nat⟧ ⟹ nth(succ(n), Cons(a,l)) = x"
by simp

lemmas nth_rules = nth_0 nth_ConsI nat_0I nat_succI
lemmas sep_rules = nth_0 nth_ConsI FOL_iff_sats function_iff_sats
fun_plus_iff_sats successor_iff_sats
omega_iff_sats FOL_sats_iff Replace_iff_sats

text‹Also a different compilation of lemmas (term‹sep_rules›) used in formula
synthesis›
lemmas fm_defs =
omega_fm_def limit_ordinal_fm_def empty_fm_def typed_function_fm_def
pair_fm_def upair_fm_def domain_fm_def function_fm_def succ_fm_def
cons_fm_def fun_apply_fm_def image_fm_def big_union_fm_def union_fm_def
relation_fm_def composition_fm_def field_fm_def ordinal_fm_def range_fm_def
transset_fm_def subset_fm_def Replace_fm_def

lemmas formulas_def [fm_definitions] = fm_defs
is_iterates_fm_def iterates_MH_fm_def is_wfrec_fm_def is_recfun_fm_def is_transrec_fm_def
is_nat_case_fm_def quasinat_fm_def number1_fm_def ordinal_fm_def finite_ordinal_fm_def
cartprod_fm_def sum_fm_def Inr_fm_def Inl_fm_def
formula_functor_fm_def
Memrel_fm_def transset_fm_def subset_fm_def pre_image_fm_def restriction_fm_def
list_functor_fm_def tl_fm_def quasilist_fm_def Cons_fm_def Nil_fm_def

lemmas sep_rules' [iff_sats]  = nth_0 nth_ConsI FOL_iff_sats function_iff_sats
fun_plus_iff_sats omega_iff_sats

lemmas  more_iff_sats [iff_sats] = rtran_closure_iff_sats tran_closure_iff_sats
is_eclose_iff_sats Inl_iff_sats Inr_iff_sats fun_apply_iff_sats cartprod_iff_sats
Collect_iff_sats

end```