section‹Aids to internalize formulas› theory Internalizations imports "ZF-Constructible-Trans.Formula" "ZF-Constructible-Trans.L_axioms" "ZF-Constructible-Trans.DPow_absolute" begin text‹We found it useful to have slightly different versions of some results in ZF-Constructible:› lemma nth_closed : assumes "0∈A" "env∈list(A)" shows "nth(n,env)∈A" using assms(2,1) unfolding nth_def by (induct env; simp) 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 end