section‹Arities of internalized formulas› theory Arities imports FrecR begin lemma arity_upair_fm : "⟦ t1∈nat ; t2∈nat ; up∈nat ⟧ ⟹ arity(upair_fm(t1,t2,up)) = ⋃ {succ(t1),succ(t2),succ(up)}" unfolding upair_fm_def using nat_union_abs1 nat_union_abs2 pred_Un by auto lemma arity_pair_fm : "⟦ t1∈nat ; t2∈nat ; p∈nat ⟧ ⟹ arity(pair_fm(t1,t2,p)) = ⋃ {succ(t1),succ(t2),succ(p)}" unfolding pair_fm_def using arity_upair_fm nat_union_abs1 nat_union_abs2 pred_Un by auto lemma arity_composition_fm : "⟦ r∈nat ; s∈nat ; t∈nat ⟧ ⟹ arity(composition_fm(r,s,t)) = ⋃ {succ(r), succ(s), succ(t)}" unfolding composition_fm_def using arity_pair_fm nat_union_abs1 nat_union_abs2 pred_Un_distrib by auto lemma arity_domain_fm : "⟦ r∈nat ; z∈nat ⟧ ⟹ arity(domain_fm(r,z)) = succ(r) ∪ succ(z)" unfolding domain_fm_def using arity_pair_fm nat_union_abs1 nat_union_abs2 pred_Un_distrib by auto lemma arity_range_fm : "⟦ r∈nat ; z∈nat ⟧ ⟹ arity(range_fm(r,z)) = succ(r) ∪ succ(z)" unfolding range_fm_def using arity_pair_fm nat_union_abs1 nat_union_abs2 pred_Un_distrib by auto lemma arity_union_fm : "⟦ x∈nat ; y∈nat ; z∈nat ⟧ ⟹ arity(union_fm(x,y,z)) = ⋃ {succ(x), succ(y), succ(z)}" unfolding union_fm_def using nat_union_abs1 nat_union_abs2 pred_Un_distrib by auto lemma arity_image_fm : "⟦ x∈nat ; y∈nat ; z∈nat ⟧ ⟹ arity(image_fm(x,y,z)) = ⋃ {succ(x), succ(y), succ(z)}" unfolding image_fm_def using arity_pair_fm nat_union_abs1 nat_union_abs2 pred_Un_distrib by auto lemma arity_pre_image_fm : "⟦ x∈nat ; y∈nat ; z∈nat ⟧ ⟹ arity(pre_image_fm(x,y,z)) = ⋃ {succ(x), succ(y), succ(z)}" unfolding pre_image_fm_def using arity_pair_fm nat_union_abs1 nat_union_abs2 pred_Un_distrib by auto lemma arity_big_union_fm : "⟦ x∈nat ; y∈nat ⟧ ⟹ arity(big_union_fm(x,y)) = succ(x) ∪ succ(y)" unfolding big_union_fm_def using nat_union_abs1 nat_union_abs2 pred_Un_distrib by auto lemma arity_fun_apply_fm : "⟦ x∈nat ; y∈nat ; f∈nat ⟧ ⟹ arity(fun_apply_fm(f,x,y)) = succ(f) ∪ succ(x) ∪ succ(y)" unfolding fun_apply_fm_def using arity_upair_fm arity_image_fm arity_big_union_fm nat_union_abs2 pred_Un_distrib by auto lemma arity_field_fm : "⟦ r∈nat ; z∈nat ⟧ ⟹ arity(field_fm(r,z)) = succ(r) ∪ succ(z)" unfolding field_fm_def using arity_pair_fm arity_domain_fm arity_range_fm arity_union_fm nat_union_abs1 nat_union_abs2 pred_Un_distrib by auto lemma arity_empty_fm : "⟦ r∈nat ⟧ ⟹ arity(empty_fm(r)) = succ(r)" unfolding empty_fm_def using nat_union_abs1 nat_union_abs2 pred_Un_distrib by simp lemma arity_succ_fm : "⟦x∈nat;y∈nat⟧ ⟹ arity(succ_fm(x,y)) = succ(x) ∪ succ(y)" unfolding succ_fm_def cons_fm_def using arity_upair_fm arity_union_fm nat_union_abs2 pred_Un_distrib by auto lemma number1arity__fm : "⟦ r∈nat ⟧ ⟹ arity(number1_fm(r)) = succ(r)" unfolding number1_fm_def using arity_empty_fm arity_succ_fm nat_union_abs1 nat_union_abs2 pred_Un_distrib by simp lemma arity_function_fm : "⟦ r∈nat ⟧ ⟹ arity(function_fm(r)) = succ(r)" unfolding function_fm_def using arity_pair_fm nat_union_abs1 nat_union_abs2 pred_Un_distrib by simp lemma arity_relation_fm : "⟦ r∈nat ⟧ ⟹ arity(relation_fm(r)) = succ(r)" unfolding relation_fm_def using arity_pair_fm nat_union_abs1 nat_union_abs2 pred_Un_distrib by simp lemma arity_restriction_fm : "⟦ r∈nat ; z∈nat ; A∈nat ⟧ ⟹ arity(restriction_fm(A,z,r)) = succ(A) ∪ succ(r) ∪ succ(z)" unfolding restriction_fm_def using arity_pair_fm nat_union_abs2 pred_Un_distrib by auto lemma arity_typed_function_fm : "⟦ x∈nat ; y∈nat ; f∈nat ⟧ ⟹ arity(typed_function_fm(f,x,y)) = ⋃ {succ(f), succ(x), succ(y)}" unfolding typed_function_fm_def using arity_pair_fm arity_relation_fm arity_function_fm arity_domain_fm nat_union_abs2 pred_Un_distrib by auto lemma arity_subset_fm : "⟦x∈nat ; y∈nat⟧ ⟹ arity(subset_fm(x,y)) = succ(x) ∪ succ(y)" unfolding subset_fm_def using nat_union_abs2 pred_Un_distrib by auto lemma arity_transset_fm : "⟦x∈nat⟧ ⟹ arity(transset_fm(x)) = succ(x)" unfolding transset_fm_def using arity_subset_fm nat_union_abs2 pred_Un_distrib by auto lemma arity_ordinal_fm : "⟦x∈nat⟧ ⟹ arity(ordinal_fm(x)) = succ(x)" unfolding ordinal_fm_def using arity_transset_fm nat_union_abs2 pred_Un_distrib by auto lemma arity_limit_ordinal_fm : "⟦x∈nat⟧ ⟹ arity(limit_ordinal_fm(x)) = succ(x)" unfolding limit_ordinal_fm_def using arity_ordinal_fm arity_succ_fm arity_empty_fm nat_union_abs2 pred_Un_distrib by auto lemma arity_finite_ordinal_fm : "⟦x∈nat⟧ ⟹ arity(finite_ordinal_fm(x)) = succ(x)" unfolding finite_ordinal_fm_def using arity_ordinal_fm arity_limit_ordinal_fm arity_succ_fm arity_empty_fm nat_union_abs2 pred_Un_distrib by auto lemma arity_omega_fm : "⟦x∈nat⟧ ⟹ arity(omega_fm(x)) = succ(x)" unfolding omega_fm_def using arity_limit_ordinal_fm nat_union_abs2 pred_Un_distrib by auto lemma arity_cartprod_fm : "⟦ A∈nat ; B∈nat ; z∈nat ⟧ ⟹ arity(cartprod_fm(A,B,z)) = succ(A) ∪ succ(B) ∪ succ(z)" unfolding cartprod_fm_def using arity_pair_fm nat_union_abs2 pred_Un_distrib by auto lemma arity_fst_fm : "⟦x∈nat ; t∈nat⟧ ⟹ arity(fst_fm(x,t)) = succ(x) ∪ succ(t)" unfolding fst_fm_def using arity_pair_fm arity_empty_fm nat_union_abs2 pred_Un_distrib by auto lemma arity_snd_fm : "⟦x∈nat ; t∈nat⟧ ⟹ arity(snd_fm(x,t)) = succ(x) ∪ succ(t)" unfolding snd_fm_def using arity_pair_fm arity_empty_fm nat_union_abs2 pred_Un_distrib by auto lemma arity_snd_snd_fm : "⟦x∈nat ; t∈nat⟧ ⟹ arity(snd_snd_fm(x,t)) = succ(x) ∪ succ(t)" unfolding snd_snd_fm_def hcomp_fm_def using arity_snd_fm arity_empty_fm nat_union_abs2 pred_Un_distrib by auto lemma arity_ftype_fm : "⟦x∈nat ; t∈nat⟧ ⟹ arity(ftype_fm(x,t)) = succ(x) ∪ succ(t)" unfolding ftype_fm_def using arity_fst_fm by auto lemma name1arity__fm : "⟦x∈nat ; t∈nat⟧ ⟹ arity(name1_fm(x,t)) = succ(x) ∪ succ(t)" unfolding name1_fm_def hcomp_fm_def using arity_fst_fm arity_snd_fm nat_union_abs2 pred_Un_distrib by auto lemma name2arity__fm : "⟦x∈nat ; t∈nat⟧ ⟹ arity(name2_fm(x,t)) = succ(x) ∪ succ(t)" unfolding name2_fm_def hcomp_fm_def using arity_fst_fm arity_snd_snd_fm nat_union_abs2 pred_Un_distrib by auto lemma arity_cond_of_fm : "⟦x∈nat ; t∈nat⟧ ⟹ arity(cond_of_fm(x,t)) = succ(x) ∪ succ(t)" unfolding cond_of_fm_def hcomp_fm_def using arity_snd_fm arity_snd_snd_fm nat_union_abs2 pred_Un_distrib by auto lemma arity_singleton_fm : "⟦x∈nat ; t∈nat⟧ ⟹ arity(singleton_fm(x,t)) = succ(x) ∪ succ(t)" unfolding singleton_fm_def cons_fm_def using arity_union_fm arity_upair_fm arity_empty_fm nat_union_abs2 pred_Un_distrib by auto lemma arity_Memrel_fm : "⟦x∈nat ; t∈nat⟧ ⟹ arity(Memrel_fm(x,t)) = succ(x) ∪ succ(t)" unfolding Memrel_fm_def using arity_pair_fm nat_union_abs2 pred_Un_distrib by auto lemma arity_quasinat_fm : "⟦x∈nat⟧ ⟹ arity(quasinat_fm(x)) = succ(x)" unfolding quasinat_fm_def cons_fm_def using arity_succ_fm arity_empty_fm nat_union_abs2 pred_Un_distrib by auto lemma arity_is_recfun_fm : "⟦p∈formula ; v∈nat ; n∈nat; Z∈nat;i∈nat⟧ ⟹ arity(p) = i ⟹ arity(is_recfun_fm(p,v,n,Z)) = succ(v) ∪ succ(n) ∪ succ(Z) ∪ pred(pred(pred(pred(i))))" unfolding is_recfun_fm_def using arity_upair_fm arity_pair_fm arity_pre_image_fm arity_restriction_fm nat_union_abs2 pred_Un_distrib by auto lemma arity_is_wfrec_fm : "⟦p∈formula ; v∈nat ; n∈nat; Z∈nat ; i∈nat⟧ ⟹ arity(p) = i ⟹ arity(is_wfrec_fm(p,v,n,Z)) = succ(v) ∪ succ(n) ∪ succ(Z) ∪ pred(pred(pred(pred(pred(i)))))" unfolding is_wfrec_fm_def using arity_succ_fm arity_is_recfun_fm nat_union_abs2 pred_Un_distrib by auto lemma arity_is_nat_case_fm : "⟦p∈formula ; v∈nat ; n∈nat; Z∈nat; i∈nat⟧ ⟹ arity(p) = i ⟹ arity(is_nat_case_fm(v,p,n,Z)) = succ(v) ∪ succ(n) ∪ succ(Z) ∪ pred(pred(i))" unfolding is_nat_case_fm_def using arity_succ_fm arity_empty_fm arity_quasinat_fm nat_union_abs2 pred_Un_distrib by auto lemma arity_iterates_MH_fm : assumes "isF∈formula" "v∈nat" "n∈nat" "g∈nat" "z∈nat" "i∈nat" "arity(isF) = i" shows "arity(iterates_MH_fm(isF,v,n,g,z)) = succ(v) ∪ succ(n) ∪ succ(g) ∪ succ(z) ∪ pred(pred(pred(pred(i))))" proof - let ?φ = "Exists(And(fun_apply_fm(succ(succ(succ(g))), 2, 0), Forall(Implies(Equal(0, 2), isF))))" let ?ar = "succ(succ(succ(g))) ∪ pred(pred(i))" from assms have "arity(?φ) =?ar" "?φ∈formula" using arity_fun_apply_fm nat_union_abs1 nat_union_abs2 pred_Un_distrib succ_Un_distrib Un_assoc[symmetric] by simp_all then show ?thesis unfolding iterates_MH_fm_def using arity_is_nat_case_fm[OF ‹?φ∈_› _ _ _ _ ‹arity(?φ) = _›] assms pred_succ_eq pred_Un_distrib by auto qed lemma arity_is_iterates_fm : assumes "p∈formula" "v∈nat" "n∈nat" "Z∈nat" "i∈nat" "arity(p) = i" shows "arity(is_iterates_fm(p,v,n,Z)) = succ(v) ∪ succ(n) ∪ succ(Z) ∪ pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(i)))))))))))" proof - let ?φ = "iterates_MH_fm(p, 7#+v, 2, 1, 0)" let ?ψ = "is_wfrec_fm(?φ, 0, succ(succ(n)),succ(succ(Z)))" from ‹v∈_› have "arity(?φ) = (8#+v) ∪ pred(pred(pred(pred(i))))" "?φ∈formula" using assms arity_iterates_MH_fm nat_union_abs2 by simp_all then have "arity(?ψ) = succ(succ(succ(n))) ∪ succ(succ(succ(Z))) ∪ (3#+v) ∪ pred(pred(pred(pred(pred(pred(pred(pred(pred(i)))))))))" using assms arity_is_wfrec_fm[OF ‹?φ∈_› _ _ _ _ ‹arity(?φ) = _›] nat_union_abs1 pred_Un_distrib by auto then show ?thesis unfolding is_iterates_fm_def using arity_Memrel_fm arity_succ_fm assms nat_union_abs1 pred_Un_distrib by auto qed lemma arity_eclose_n_fm : assumes "A∈nat" "x∈nat" "t∈nat" shows "arity(eclose_n_fm(A,x,t)) = succ(A) ∪ succ(x) ∪ succ(t)" proof - let ?φ = "big_union_fm(1,0)" have "arity(?φ) = 2" "?φ∈formula" using arity_big_union_fm nat_union_abs2 by simp_all with assms show ?thesis unfolding eclose_n_fm_def using arity_is_iterates_fm[OF ‹?φ∈_› _ _ _,of _ _ _ 2] by auto qed lemma arity_mem_eclose_fm : assumes "x∈nat" "t∈nat" shows "arity(mem_eclose_fm(x,t)) = succ(x) ∪ succ(t)" proof - let ?φ="eclose_n_fm(x #+ 2, 1, 0)" from ‹x∈nat› have "arity(?φ) = x#+3" using arity_eclose_n_fm nat_union_abs2 by simp with assms show ?thesis unfolding mem_eclose_fm_def using arity_finite_ordinal_fm nat_union_abs2 pred_Un_distrib by simp qed lemma arity_is_eclose_fm : "⟦x∈nat ; t∈nat⟧ ⟹ arity(is_eclose_fm(x,t)) = succ(x) ∪ succ(t)" unfolding is_eclose_fm_def using arity_mem_eclose_fm nat_union_abs2 pred_Un_distrib by auto lemma eclose_n1arity__fm : "⟦x∈nat ; t∈nat⟧ ⟹ arity(eclose_n1_fm(x,t)) = succ(x) ∪ succ(t)" unfolding eclose_n1_fm_def using arity_is_eclose_fm arity_singleton_fm name1arity__fm nat_union_abs2 pred_Un_distrib by auto lemma eclose_n2arity__fm : "⟦x∈nat ; t∈nat⟧ ⟹ arity(eclose_n2_fm(x,t)) = succ(x) ∪ succ(t)" unfolding eclose_n2_fm_def using arity_is_eclose_fm arity_singleton_fm name2arity__fm nat_union_abs2 pred_Un_distrib by auto lemma arity_ecloseN_fm : "⟦x∈nat ; t∈nat⟧ ⟹ arity(ecloseN_fm(x,t)) = succ(x) ∪ succ(t)" unfolding ecloseN_fm_def using eclose_n1arity__fm eclose_n2arity__fm arity_union_fm nat_union_abs2 pred_Un_distrib by auto lemma arity_frecR_fm : "⟦a∈nat;b∈nat⟧ ⟹ arity(frecR_fm(a,b)) = succ(a) ∪ succ(b)" unfolding frecR_fm_def using arity_ftype_fm name1arity__fm name2arity__fm arity_domain_fm number1arity__fm arity_empty_fm nat_union_abs2 pred_Un_distrib by auto lemma arity_Collect_fm : assumes "x ∈ nat" "y ∈ nat" "p∈formula" shows "arity(Collect_fm(x,p,y)) = succ(x) ∪ succ(y) ∪ pred(arity(p))" unfolding Collect_fm_def using assms pred_Un_distrib by auto end