Theory Internalizations

section‹Aids to internalize formulas›
theory Internalizations
  imports 
    "ZF-Constructible.DPow_absolute"
    Synthetic_Definition
begin

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

end