Theory Internalizations

section‹Aids to internalize formulas›

theory Internalizations
  imports
    "ZF-Constructible.DPow_absolute"
    Synthetic_Definition
begin

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

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⋅›)

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

abbreviation
  fm_typedfun :: "[i,i,i] ⇒ i" (‹⋅_ : _ → _⋅›) where
  "fm_typedfun(f,A,B) ≡ typed_function_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 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 FOL_sats_iff (* NOTE: why FOL_sats_iff? *)

declare rtran_closure_iff_sats [iff_sats] tran_closure_iff_sats [iff_sats]
  is_eclose_iff_sats [iff_sats]
arity_theorem for "rtran_closure_fm"
arity_theorem for "tran_closure_fm"
arity_theorem for "rtran_closure_mem_fm"

end