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"
by (simp add: Transset_def,auto)
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 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 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