Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/C/Firefox/third_party/rust/camino/   (Firefox Browser Version 153.0.1©)  Datei vom 27.6.2026 mit Größe 8 kB image not shown  

Bilddatei

Arities.thy


products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Forcing/Arities.thy

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