Theory Arities
section‹Arities of internalized formulas›
theory Arities
imports
Discipline_Base
begin
lemmas FOL_arities [simp del, arity] = arity_And arity_Or arity_Implies arity_Iff arity_Exists
declare pred_Un_distrib[arity_aux]
context
notes FOL_arities[simp]
begin
lemma arity_upair_fm [arity] : "⟦ t1∈nat ; t2∈nat ; up∈nat ⟧ ⟹
arity(upair_fm(t1,t2,up)) = ⋃ {succ(t1),succ(t2),succ(up)}"
unfolding upair_fm_def
using union_abs1 union_abs2 pred_Un
by auto
end
lemma Un_trasposition_aux1: "r ∪ s ∪ r = r ∪ s" by auto
lemma Un_trasposition_aux2:
"r ∪ (s ∪ (r ∪ u))= r ∪ (s ∪ u)"
"r ∪ (s ∪ (t ∪ (r ∪ u)))= r ∪ (s ∪ (t ∪ u))" by auto
text‹We use the previous lemmas to guide automatic arity calculations.›
context
notes Un_assoc[symmetric,simp] Un_trasposition_aux1[simp]
begin
arity_theorem for "pair_fm"
arity_theorem for "composition_fm"
arity_theorem for "domain_fm"
arity_theorem for "range_fm"
arity_theorem for "union_fm"
arity_theorem for "image_fm"
arity_theorem for "pre_image_fm"
arity_theorem for "big_union_fm"
arity_theorem for "fun_apply_fm"
arity_theorem for "field_fm"
arity_theorem for "empty_fm"
arity_theorem for "cons_fm"
arity_theorem for "succ_fm"
arity_theorem for "number1_fm"
arity_theorem for "function_fm"
arity_theorem for "relation_fm"
arity_theorem for "restriction_fm"
arity_theorem for "typed_function_fm"
arity_theorem for "subset_fm"
arity_theorem for "transset_fm"
arity_theorem for "ordinal_fm"
arity_theorem for "limit_ordinal_fm"
arity_theorem for "finite_ordinal_fm"
arity_theorem for "omega_fm"
arity_theorem for "cartprod_fm"
arity_theorem for "singleton_fm"
arity_theorem for "Memrel_fm"
arity_theorem for "quasinat_fm"
end
context
notes FOL_arities[simp]
begin
lemma arity_is_recfun_fm [arity]:
"⟦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^4(i))"
unfolding is_recfun_fm_def
using arity_upair_fm arity_pair_fm arity_pre_image_fm arity_restriction_fm
union_abs2 pred_Un_distrib
by auto
lemma arity_is_wfrec_fm [arity]:
"⟦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^5(i))"
unfolding is_wfrec_fm_def
using arity_succ_fm arity_is_recfun_fm
union_abs2 pred_Un_distrib
by auto
lemma arity_is_nat_case_fm [arity]:
"⟦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
union_abs2 pred_Un_distrib
by auto
lemma arity_iterates_MH_fm [arity]:
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^4(i))"
proof -
let ?φ = "(⋅∃⋅⋅g +⇩ω 3`2 is 0⋅ ∧ (⋅∀⋅⋅0 = 2⋅ → isF⋅⋅)⋅⋅)"
let ?ar = "(g +⇩ω 3) ∪ pred(pred(i))"
from assms
have "arity(?φ) =?ar" "?φ∈formula"
using arity_fun_apply_fm
union_abs1 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(?φ) = ?ar›] assms pred_succ_eq pred_Un_distrib
by auto
qed
lemma arity_is_iterates_fm [arity]:
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^11(i))"
proof -
let ?φ = "iterates_MH_fm(p, 7+⇩ωv, 2, 1, 0)"
let ?ψ = "is_wfrec_fm(?φ, 0, n +⇩ω 2, Z +⇩ω 2)"
from ‹v∈_›
have "arity(?φ) = (8+⇩ωv) ∪ (pred^4(i))" "?φ∈formula"
using assms arity_iterates_MH_fm union_abs2
by simp_all
then
have "arity(?ψ) = n +⇩ω 3 ∪ (Z +⇩ω 3) ∪ (3+⇩ωv) ∪ (pred^9(i))"
using assms arity_is_wfrec_fm[OF ‹?φ∈_› _ _ _ _ ‹arity(?φ) = _›] union_abs1 pred_Un_distrib
by auto
then
show ?thesis
unfolding is_iterates_fm_def
using arity_Memrel_fm arity_succ_fm assms union_abs1 pred_Un_distrib
by auto
qed
lemma arity_eclose_n_fm [arity]:
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 union_abs2
by auto
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 [arity]:
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 union_abs2
by simp
with assms
show ?thesis
unfolding mem_eclose_fm_def
using arity_finite_ordinal_fm union_abs2 pred_Un_distrib
by simp
qed
lemma arity_is_eclose_fm [arity]:
"⟦x∈nat ; t∈nat⟧ ⟹ arity(is_eclose_fm(x,t)) = succ(x) ∪ succ(t)"
unfolding is_eclose_fm_def
using arity_mem_eclose_fm union_abs2 pred_Un_distrib
by auto
lemma arity_Collect_fm [arity]:
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
schematic_goal arity_least_fm':
assumes
"i ∈ nat" "q ∈ formula"
shows
"arity(least_fm(q,i)) ≡ ?ar"
unfolding least_fm_def
using assms pred_Un_distrib arity_And arity_Or arity_Neg arity_Implies arity_ordinal_fm
arity_empty_fm Un_assoc[symmetric] Un_commute
by auto
lemma arity_least_fm [arity]:
assumes
"i ∈ nat" "q ∈ formula"
shows
"arity(least_fm(q,i)) = succ(i) ∪ pred(arity(q))"
using assms arity_least_fm'
by auto
lemma arity_Replace_fm [arity]:
"⟦p∈formula ; v∈nat ; n∈nat; i∈nat⟧ ⟹ arity(p) = i ⟹
arity(Replace_fm(v,p,n)) = succ(n) ∪ succ(v) ∪ pred(pred(i))"
unfolding Replace_fm_def
using union_abs2 pred_Un_distrib
by auto
lemma arity_lambda_fm [arity]:
"⟦p∈formula; v∈nat ; n∈nat; i∈nat⟧ ⟹ arity(p) = i ⟹
arity(lambda_fm(p,v,n)) = succ(n) ∪ (succ(v) ∪ (pred^3(i)))"
unfolding lambda_fm_def
using arity_pair_fm pred_Un_distrib union_abs1 union_abs2
by simp
lemma arity_transrec_fm [arity]:
"⟦p∈formula ; v∈nat ; n∈nat; i∈nat⟧ ⟹ arity(p) = i ⟹
arity(is_transrec_fm(p,v,n)) = succ(v) ∪ succ(n) ∪ (pred^8(i))"
unfolding is_transrec_fm_def
using arity Un_assoc[symmetric] pred_Un_distrib
by simp
lemma arity_wfrec_replacement_fm :
"⟦p∈formula ; v∈nat ; n∈nat; Z∈nat ; i∈nat⟧ ⟹ arity(p) = i ⟹
arity(Exists(And(pair_fm(1,0,2),is_wfrec_fm(p,v,n,Z))))
= 2 ∪ v ∪ n ∪ Z ∪ (pred^6(i))"
unfolding is_wfrec_fm_def
using arity_succ_fm arity_is_recfun_fm union_abs2 pred_Un_distrib arity_pair_fm
by auto
end
declare arity_subset_fm [simp del] arity_ordinal_fm[simp del, arity] arity_transset_fm[simp del]
context
notes Un_assoc[symmetric,simp] Un_trasposition_aux1[simp]
begin
arity_theorem for "rtran_closure_mem_fm"
arity_theorem for "rtran_closure_fm"
arity_theorem for "tran_closure_fm"
end
context
notes Un_assoc[simp] Un_trasposition_aux2[simp]
begin
arity_theorem for "injection_fm"
arity_theorem for "surjection_fm"
arity_theorem for "bijection_fm"
arity_theorem for "order_isomorphism_fm"
end
arity_theorem for "Inl_fm"
arity_theorem for "Inr_fm"
arity_theorem for "pred_set_fm"
end