Theory Forces_Definition
section‹The definition of \<^term>‹forces››
theory Forces_Definition imports Arities FrecR Synthetic_Definition FrecR_Arities begin
text‹This is the core of our development.›
subsection‹The relation \<^term>‹frecrel››
definition
frecrelP :: "[i⇒o,i] ⇒ o" where
"frecrelP(M,xy) ≡ (∃x[M]. ∃y[M]. pair(M,x,y,xy) ∧ is_frecR(M,x,y))"
synthesize "frecrelP" from_definition
lemma arity_frecrelP_fm :
"a∈nat ⟹ arity(frecrelP_fm(a)) = succ(a)"
unfolding frecrelP_fm_def
using arity_frecR_fm arity_pair_fm pred_Un_distrib
by simp
definition
is_frecrel :: "[i⇒o,i,i] ⇒ o" where
"is_frecrel(M,A,r) ≡ ∃A2[M]. cartprod(M,A,A,A2) ∧ is_Collect(M,A2, frecrelP(M) ,r)"
declare cartprod_iff_sats [iff_sats]
declare Collect_iff_sats [iff_sats]
synthesize "frecrel" from_definition "is_frecrel"
lemma arity_frecrel_fm :
assumes "a∈nat" "b∈nat"
shows "arity(frecrel_fm(a,b)) = succ(a) ∪ succ(b)"
unfolding frecrel_fm_def
using assms arity_Collect_fm arity_cartprod_fm arity_frecrelP_fm pred_Un_distrib
by auto
definition
names_below :: "i ⇒ i ⇒ i" where
"names_below(P,x) ≡ 2×ecloseN(x)×ecloseN(x)×P"
lemma names_belowsD :
assumes "x ∈ names_below(P,z)"
obtains f n1 n2 p where
"x = ⟨f,n1,n2,p⟩" "f∈2" "n1∈ecloseN(z)" "n2∈ecloseN(z)" "p∈P"
using assms unfolding names_below_def by auto
synthesize "number2" from_definition
lemma number2_iff :
"(A)(c) ⟹ number2(A,c) ⟷ (∃b[A]. ∃a[A]. successor(A, b, c) ∧ successor(A, a, b) ∧ empty(A, a))"
unfolding number2_def number1_def by auto
lemma arity_number2_fm :
"a∈nat ⟹ arity(number2_fm(a)) = succ(a)"
unfolding number2_fm_def
using arity_number1_fm arity_succ_fm union_abs2 pred_Un_distrib
by simp
reldb_add "ecloseN" "is_ecloseN"
relativize "names_below" "is_names_below"
synthesize "is_names_below" from_definition
lemma arity_is_names_below_fm :
"⟦P∈nat;x∈nat;nb∈nat⟧ ⟹ arity(is_names_below_fm(P,x,nb)) = succ(P) ∪ succ(x) ∪ succ(nb)"
unfolding is_names_below_fm_def
using arity_cartprod_fm arity_succ_fm arity_empty_fm arity_ecloseN_fm union_abs2 pred_Un_distrib
by auto
definition
is_tuple :: "[i⇒o,i,i,i,i,i] ⇒ o" where
"is_tuple(M,z,t1,t2,p,t) ≡ ∃t1t2p[M]. ∃t2p[M]. pair(M,t2,p,t2p) ∧ pair(M,t1,t2p,t1t2p) ∧
pair(M,z,t1t2p,t)"
synthesize "is_tuple" from_definition
lemma arity_is_tuple_fm : "⟦ z∈nat ; t1∈nat ; t2∈nat ; p∈nat ; tup∈nat ⟧ ⟹
arity(is_tuple_fm(z,t1,t2,p,tup)) = ⋃ {succ(z),succ(t1),succ(t2),succ(p),succ(tup)}"
unfolding is_tuple_fm_def
using arity_pair_fm union_abs1 union_abs2 pred_Un_distrib
by auto
subsection‹Definition of \<^term>‹forces› for equality and membership›
definition
eq_case :: "[i,i,i,i,i,i] ⇒ o" where
"eq_case(t1,t2,p,P,leq,f) ≡ ∀s. s∈domain(t1) ∪ domain(t2) ⟶
(∀q. q∈P ∧ ⟨q,p⟩∈leq ⟶ (f`⟨1,s,t1,q⟩=1 ⟷ f`⟨1,s,t2,q⟩ =1))"
relativize "eq_case" "is_eq_case"
synthesize "eq_case" from_definition "is_eq_case"
lemma arity_eq_case_fm :
assumes
"n1∈nat" "n2∈nat" "p∈nat" "P∈nat" "leq∈nat" "f∈nat"
shows
"arity(eq_case_fm(n1,n2,p,P,leq,f)) =
succ(n1) ∪ succ(n2) ∪ succ(p) ∪ succ(P) ∪ succ(leq) ∪ succ(f)"
unfolding eq_case_fm_def
using assms arity_pair_fm arity_is_tuple_fm arity_succ_fm arity_fun_apply_fm arity_empty_fm
arity_domain_fm pred_Un_distrib arity_union_fm
by auto
definition
mem_case :: "[i,i,i,i,i,i] ⇒ o" where
"mem_case(t1,t2,p,P,leq,f) ≡ ∀v∈P. ⟨v,p⟩∈leq ⟶
(∃q. ∃s. ∃r. r∈P ∧ q∈P ∧ ⟨q,v⟩∈leq ∧ ⟨s,r⟩ ∈ t2 ∧ ⟨q,r⟩∈leq ∧ f`⟨0,t1,s,q⟩ = 1)"
relativize "mem_case" "is_mem_case"
synthesize "mem_case" from_definition "is_mem_case"
lemma arity_mem_case_fm :
assumes
"n1∈nat" "n2∈nat" "p∈nat" "P∈nat" "leq∈nat" "f∈nat"
shows
"arity(mem_case_fm(n1,n2,p,P,leq,f)) =
succ(n1) ∪ succ(n2) ∪ succ(p) ∪ succ(P) ∪ succ(leq) ∪ succ(f)"
unfolding mem_case_fm_def
using assms arity_pair_fm arity_is_tuple_fm arity_succ_fm arity_fun_apply_fm arity_empty_fm
pred_Un_distrib
by auto
definition
Hfrc :: "[i,i,i,i] ⇒ o" where
"Hfrc(P,leq,fnnc,f) ≡ ∃ft. ∃n1. ∃n2. ∃c. c∈P ∧ fnnc = ⟨ft,n1,n2,c⟩ ∧
( ft = 0 ∧ eq_case(n1,n2,c,P,leq,f)
∨ ft = 1 ∧ mem_case(n1,n2,c,P,leq,f))"
relativize "Hfrc" "is_Hfrc"
synthesize "Hfrc" from_definition "is_Hfrc"
lemma arity_Hfrc_fm :
assumes
"P∈nat" "leq∈nat" "fnnc∈nat" "f∈nat"
shows
"arity(Hfrc_fm(P,leq,fnnc,f)) = succ(P) ∪ succ(leq) ∪ succ(fnnc) ∪ succ(f)"
unfolding Hfrc_fm_def
using assms arity_pair_fm arity_mem_case_fm arity_eq_case_fm
arity_empty_fm arity_succ_fm pred_Un_distrib
by auto
definition
is_Hfrc_at :: "[i⇒o,i,i,i,i,i] ⇒ o" where
"is_Hfrc_at(M,P,leq,fnnc,f,z) ≡
(empty(M,z) ∧ ¬ is_Hfrc(M,P,leq,fnnc,f))
∨ (number1(M,z) ∧ is_Hfrc(M,P,leq,fnnc,f))"
synthesize "Hfrc_at" from_definition "is_Hfrc_at"
lemma arity_Hfrc_at_fm :
assumes
"P∈nat" "leq∈nat" "fnnc∈nat" "f∈nat" "z∈nat"
shows
"arity(Hfrc_at_fm(P,leq,fnnc,f,z)) = succ(P) ∪ succ(leq) ∪ succ(fnnc) ∪ succ(f) ∪ succ(z)"
unfolding Hfrc_at_fm_def
using assms arity_Hfrc_fm arity_empty_fm arity_number1_fm pred_Un_distrib
by auto
subsection‹The well-founded relation \<^term>‹forcerel››
definition
forcerel :: "i ⇒ i ⇒ i" where
"forcerel(P,x) ≡ frecrel(names_below(P,x))^+"
definition
is_forcerel :: "[i⇒o,i,i,i] ⇒ o" where
"is_forcerel(M,P,x,z) ≡ ∃r[M]. ∃nb[M]. tran_closure(M,r,z) ∧
(is_names_below(M,P,x,nb) ∧ is_frecrel(M,nb,r))"
definition
forcerel_fm :: "i⇒ i ⇒ i ⇒ i" where
"forcerel_fm(p,x,z) ≡ Exists(Exists(And(trans_closure_fm(1, z#+2),
And(is_names_below_fm(p#+2,x#+2,0),frecrel_fm(0,1)))))"
lemma arity_forcerel_fm :
"⟦p∈nat;x∈nat;z∈nat⟧ ⟹ arity(forcerel_fm(p,x,z)) = succ(p) ∪ succ(x) ∪ succ(z)"
unfolding forcerel_fm_def
using arity_frecrel_fm arity_tran_closure_fm arity_is_names_below_fm pred_Un_distrib
by auto
lemma forcerel_fm_type [TC]:
"⟦p∈nat;x∈nat;z∈nat⟧ ⟹ forcerel_fm(p,x,z)∈formula"
unfolding forcerel_fm_def by simp
lemma sats_forcerel_fm :
assumes
"p∈nat" "x∈nat" "z∈nat" "env∈list(A)"
shows
"sats(A,forcerel_fm(p,x,z),env) ⟷ is_forcerel(##A,nth(p,env),nth(x, env),nth(z, env))"
proof -
have "sats(A,trans_closure_fm(1,z #+ 2),Cons(nb,Cons(r,env))) ⟷
tran_closure(##A, r, nth(z, env))" if "r∈A" "nb∈A" for r nb
using that assms trans_closure_iff_sats[of 1 "[nb,r]@env" _ "z#+2",symmetric] by simp
moreover
have "sats(A, is_names_below_fm(succ(succ(p)), succ(succ(x)), 0), Cons(nb, Cons(r, env))) ⟷
is_names_below(##A, nth(p,env), nth(x, env), nb)"
if "r∈A" "nb∈A" for nb r
using assms that sats_is_names_below_fm[of "p #+ 2" "x #+ 2" 0 "[nb,r]@env"] by simp
moreover
have "sats(A, frecrel_fm(0, 1), Cons(nb, Cons(r, env))) ⟷
is_frecrel(##A, nb, r)"
if "r∈A" "nb∈A" for r nb
using assms that sats_frecrel_fm[of 0 1 "[nb,r]@env"] by simp
ultimately
show ?thesis using assms unfolding is_forcerel_def forcerel_fm_def by simp
qed
subsection‹\<^term>‹frc_at›, forcing for atomic formulas›
definition
frc_at :: "[i,i,i] ⇒ i" where
"frc_at(P,leq,fnnc) ≡ wfrec(frecrel(names_below(P,fnnc)),fnnc,
λx f. bool_of_o(Hfrc(P,leq,x,f)))"
definition
is_frc_at :: "[i⇒o,i,i,i,i] ⇒ o" where
"is_frc_at(M,P,leq,x,z) ≡ ∃r[M]. is_forcerel(M,P,x,r) ∧
is_wfrec(M,is_Hfrc_at(M,P,leq),r,x,z)"
definition
frc_at_fm :: "[i,i,i,i] ⇒ i" where
"frc_at_fm(p,l,x,z) ≡ Exists(And(forcerel_fm(succ(p),succ(x),0),
is_wfrec_fm(Hfrc_at_fm(6#+p,6#+l,2,1,0),0,succ(x),succ(z))))"
lemma frc_at_fm_type [TC] :
"⟦p∈nat;l∈nat;x∈nat;z∈nat⟧ ⟹ frc_at_fm(p,l,x,z)∈formula"
unfolding frc_at_fm_def by simp
lemma arity_frc_at_fm :
assumes "p∈nat" "l∈nat" "x∈nat" "z∈nat"
shows "arity(frc_at_fm(p,l,x,z)) = succ(p) ∪ succ(l) ∪ succ(x) ∪ succ(z)"
proof -
let ?φ = "Hfrc_at_fm(6 #+ p, 6 #+ l, 2, 1, 0)"
from assms
have "arity(?φ) = (7#+p) ∪ (7#+l)" "?φ ∈ formula"
using arity_Hfrc_at_fm ord_simp_union
by auto
with assms
have W: "arity(is_wfrec_fm(?φ, 0, succ(x), succ(z))) = 2#+p ∪ (2#+l) ∪ (2#+x) ∪ (2#+z)"
using arity_is_wfrec_fm[OF ‹?φ∈_› _ _ _ _ ‹arity(?φ) = _›] pred_Un_distrib pred_succ_eq
union_abs1
by auto
from assms
have "arity(forcerel_fm(succ(p),succ(x),0)) = succ(succ(p)) ∪ succ(succ(x))"
using arity_forcerel_fm ord_simp_union
by auto
with W assms
show ?thesis
unfolding frc_at_fm_def
using arity_forcerel_fm pred_Un_distrib
by auto
qed
lemma sats_frc_at_fm :
assumes
"p∈nat" "l∈nat" "i∈nat" "j∈nat" "env∈list(A)" "i < length(env)" "j < length(env)"
shows
"sats(A,frc_at_fm(p,l,i,j),env) ⟷
is_frc_at(##A,nth(p,env),nth(l,env),nth(i,env),nth(j,env))"
proof -
{
fix r pp ll
assume "r∈A"
have 0:"is_Hfrc_at(##A,nth(p,env),nth(l,env),a2, a1, a0) ⟷
sats(A, Hfrc_at_fm(6#+p,6#+l,2,1,0), [a0,a1,a2,a3,a4,r]@env)"
if "a0∈A" "a1∈A" "a2∈A" "a3∈A" "a4∈A" for a0 a1 a2 a3 a4
using that assms ‹r∈A›
Hfrc_at_iff_sats[of "6#+p" "6#+l" 2 1 0 "[a0,a1,a2,a3,a4,r]@env" A] by simp
have "sats(A,is_wfrec_fm(Hfrc_at_fm(6 #+ p, 6 #+ l, 2, 1, 0), 0, succ(i), succ(j)),[r]@env) ⟷
is_wfrec(##A, is_Hfrc_at(##A, nth(p,env), nth(l,env)), r,nth(i, env), nth(j, env))"
using assms ‹r∈A›
sats_is_wfrec_fm[OF 0[simplified]]
by simp
}
moreover
have "sats(A, forcerel_fm(succ(p), succ(i), 0), Cons(r, env)) ⟷
is_forcerel(##A,nth(p,env),nth(i,env),r)" if "r∈A" for r
using assms sats_forcerel_fm that by simp
ultimately
show ?thesis unfolding is_frc_at_def frc_at_fm_def
using assms by simp
qed
definition
forces_eq' :: "[i,i,i,i,i] ⇒ o" where
"forces_eq'(P,l,p,t1,t2) ≡ frc_at(P,l,⟨0,t1,t2,p⟩) = 1"
definition
forces_mem' :: "[i,i,i,i,i] ⇒ o" where
"forces_mem'(P,l,p,t1,t2) ≡ frc_at(P,l,⟨1,t1,t2,p⟩) = 1"
definition
forces_neq' :: "[i,i,i,i,i] ⇒ o" where
"forces_neq'(P,l,p,t1,t2) ≡ ¬ (∃q∈P. ⟨q,p⟩∈l ∧ forces_eq'(P,l,q,t1,t2))"
definition
forces_nmem' :: "[i,i,i,i,i] ⇒ o" where
"forces_nmem'(P,l,p,t1,t2) ≡ ¬ (∃q∈P. ⟨q,p⟩∈l ∧ forces_mem'(P,l,q,t1,t2))"
definition
is_forces_eq' :: "[i⇒o,i,i,i,i,i] ⇒ o" where
"is_forces_eq'(M,P,l,p,t1,t2) ≡ ∃o[M]. ∃z[M]. ∃t[M]. number1(M,o) ∧ empty(M,z) ∧
is_tuple(M,z,t1,t2,p,t) ∧ is_frc_at(M,P,l,t,o)"
definition
is_forces_mem' :: "[i⇒o,i,i,i,i,i] ⇒ o" where
"is_forces_mem'(M,P,l,p,t1,t2) ≡ ∃o[M]. ∃t[M]. number1(M,o) ∧
is_tuple(M,o,t1,t2,p,t) ∧ is_frc_at(M,P,l,t,o)"
definition
is_forces_neq' :: "[i⇒o,i,i,i,i,i] ⇒ o" where
"is_forces_neq'(M,P,l,p,t1,t2) ≡
¬ (∃q[M]. q∈P ∧ (∃qp[M]. pair(M,q,p,qp) ∧ qp∈l ∧ is_forces_eq'(M,P,l,q,t1,t2)))"
definition
is_forces_nmem' :: "[i⇒o,i,i,i,i,i] ⇒ o" where
"is_forces_nmem'(M,P,l,p,t1,t2) ≡
¬ (∃q[M]. ∃qp[M]. q∈P ∧ pair(M,q,p,qp) ∧ qp∈l ∧ is_forces_mem'(M,P,l,q,t1,t2))"
definition
forces_eq_fm :: "[i,i,i,i,i] ⇒ i" where
"forces_eq_fm(p,l,q,t1,t2) ≡
Exists(Exists(Exists(And(number1_fm(2),And(empty_fm(1),
And(is_tuple_fm(1,t1#+3,t2#+3,q#+3,0),frc_at_fm(p#+3,l#+3,0,2) ))))))"
definition
forces_mem_fm :: "[i,i,i,i,i] ⇒ i" where
"forces_mem_fm(p,l,q,t1,t2) ≡ Exists(Exists(And(number1_fm(1),
And(is_tuple_fm(1,t1#+2,t2#+2,q#+2,0),frc_at_fm(p#+2,l#+2,0,1)))))"
definition
forces_neq_fm :: "[i,i,i,i,i] ⇒ i" where
"forces_neq_fm(p,l,q,t1,t2) ≡ Neg(Exists(Exists(And(Member(1,p#+2),
And(pair_fm(1,q#+2,0),And(Member(0,l#+2),forces_eq_fm(p#+2,l#+2,1,t1#+2,t2#+2)))))))"
definition
forces_nmem_fm :: "[i,i,i,i,i] ⇒ i" where
"forces_nmem_fm(p,l,q,t1,t2) ≡ Neg(Exists(Exists(And(Member(1,p#+2),
And(pair_fm(1,q#+2,0),And(Member(0,l#+2),forces_mem_fm(p#+2,l#+2,1,t1#+2,t2#+2)))))))"
lemma forces_eq_fm_type [TC]:
"⟦ p∈nat;l∈nat;q∈nat;t1∈nat;t2∈nat⟧ ⟹ forces_eq_fm(p,l,q,t1,t2) ∈ formula"
unfolding forces_eq_fm_def
by simp
lemma forces_mem_fm_type [TC]:
"⟦ p∈nat;l∈nat;q∈nat;t1∈nat;t2∈nat⟧ ⟹ forces_mem_fm(p,l,q,t1,t2) ∈ formula"
unfolding forces_mem_fm_def
by simp
lemma forces_neq_fm_type [TC]:
"⟦ p∈nat;l∈nat;q∈nat;t1∈nat;t2∈nat⟧ ⟹ forces_neq_fm(p,l,q,t1,t2) ∈ formula"
unfolding forces_neq_fm_def
by simp
lemma forces_nmem_fm_type [TC]:
"⟦ p∈nat;l∈nat;q∈nat;t1∈nat;t2∈nat⟧ ⟹ forces_nmem_fm(p,l,q,t1,t2) ∈ formula"
unfolding forces_nmem_fm_def
by simp
lemma arity_forces_eq_fm :
"p∈nat ⟹ l∈nat ⟹ q∈nat ⟹ t1 ∈ nat ⟹ t2 ∈ nat ⟹
arity(forces_eq_fm(p,l,q,t1,t2)) = succ(t1) ∪ succ(t2) ∪ succ(q) ∪ succ(p) ∪ succ(l)"
unfolding forces_eq_fm_def
using arity_number1_fm arity_empty_fm arity_is_tuple_fm arity_frc_at_fm
pred_Un_distrib
by auto
lemma arity_forces_mem_fm :
"p∈nat ⟹ l∈nat ⟹ q∈nat ⟹ t1 ∈ nat ⟹ t2 ∈ nat ⟹
arity(forces_mem_fm(p,l,q,t1,t2)) = succ(t1) ∪ succ(t2) ∪ succ(q) ∪ succ(p) ∪ succ(l)"
unfolding forces_mem_fm_def
using arity_number1_fm arity_empty_fm arity_is_tuple_fm arity_frc_at_fm
pred_Un_distrib
by auto
lemma sats_forces_eq'_fm :
assumes "p∈nat" "l∈nat" "q∈nat" "t1∈nat" "t2∈nat" "env∈list(M)"
shows "sats(M,forces_eq_fm(p,l,q,t1,t2),env) ⟷
is_forces_eq'(##M,nth(p,env),nth(l,env),nth(q,env),nth(t1,env),nth(t2,env))"
unfolding forces_eq_fm_def is_forces_eq'_def using assms sats_is_tuple_fm sats_frc_at_fm
by simp
lemma sats_forces_mem'_fm :
assumes "p∈nat" "l∈nat" "q∈nat" "t1∈nat" "t2∈nat" "env∈list(M)"
shows "sats(M,forces_mem_fm(p,l,q,t1,t2),env) ⟷
is_forces_mem'(##M,nth(p,env),nth(l,env),nth(q,env),nth(t1,env),nth(t2,env))"
unfolding forces_mem_fm_def is_forces_mem'_def using assms sats_is_tuple_fm sats_frc_at_fm
by simp
lemma sats_forces_neq'_fm :
assumes "p∈nat" "l∈nat" "q∈nat" "t1∈nat" "t2∈nat" "env∈list(M)"
shows "sats(M,forces_neq_fm(p,l,q,t1,t2),env) ⟷
is_forces_neq'(##M,nth(p,env),nth(l,env),nth(q,env),nth(t1,env),nth(t2,env))"
unfolding forces_neq_fm_def is_forces_neq'_def
using assms sats_forces_eq'_fm sats_is_tuple_fm sats_frc_at_fm
by simp
lemma sats_forces_nmem'_fm :
assumes "p∈nat" "l∈nat" "q∈nat" "t1∈nat" "t2∈nat" "env∈list(M)"
shows "sats(M,forces_nmem_fm(p,l,q,t1,t2),env) ⟷
is_forces_nmem'(##M,nth(p,env),nth(l,env),nth(q,env),nth(t1,env),nth(t2,env))"
unfolding forces_nmem_fm_def is_forces_nmem'_def
using assms sats_forces_mem'_fm sats_is_tuple_fm sats_frc_at_fm
by simp
context forcing_data
begin
lemma ftype_abs :
"⟦x∈M; y∈M ⟧ ⟹ is_ftype(##M,x,y) ⟷ y = ftype(x)"
unfolding ftype_def is_ftype_def by (simp add:absolut)
lemma name1_abs :
"⟦x∈M; y∈M ⟧ ⟹ is_name1(##M,x,y) ⟷ y = name1(x)"
unfolding name1_def is_name1_def
by (rule is_hcomp_abs[OF fst_abs],simp_all add: fst_snd_closed[simplified] absolut)
lemma snd_snd_abs :
"⟦x∈M; y∈M ⟧ ⟹ is_snd_snd(##M,x,y) ⟷ y = snd(snd(x))"
unfolding is_snd_snd_def
by (rule is_hcomp_abs[OF snd_abs],
simp_all add: conjunct2[OF fst_snd_closed,simplified] absolut)
lemma name2_abs :
"⟦x∈M; y∈M ⟧ ⟹ is_name2(##M,x,y) ⟷ y = name2(x)"
unfolding name2_def is_name2_def
by (rule is_hcomp_abs[OF fst_abs snd_snd_abs],simp_all add:absolut conjunct2[OF fst_snd_closed,simplified])
lemma cond_of_abs :
"⟦x∈M; y∈M ⟧ ⟹ is_cond_of(##M,x,y) ⟷ y = cond_of(x)"
unfolding cond_of_def is_cond_of_def
by (rule is_hcomp_abs[OF snd_abs snd_snd_abs];simp_all add:fst_snd_closed[simplified])
lemma tuple_abs :
"⟦z∈M;t1∈M;t2∈M;p∈M;t∈M⟧ ⟹
is_tuple(##M,z,t1,t2,p,t) ⟷ t = ⟨z,t1,t2,p⟩"
unfolding is_tuple_def using pair_in_M_iff by simp
lemmas components_abs= ftype_abs name1_abs name2_abs cond_of_abs
tuple_abs
lemma oneN_in_M [simp]: "1∈M"
by (simp flip: setclass_iff)
lemma twoN_in_M : "2∈M"
by (simp flip: setclass_iff)
lemma comp_in_M :
"p ≼ q ⟹ p∈M"
"p ≼ q ⟹ q∈M"
using leq_in_M transitivity[of _ leq] pair_in_M_iff by auto
lemma eq_case_abs [simp]:
assumes
"t1∈M" "t2∈M" "p∈M" "f∈M"
shows
"is_eq_case(##M,t1,t2,p,P,leq,f) ⟷ eq_case(t1,t2,p,P,leq,f)"
proof -
have "q ≼ p ⟹ q∈M" for q
using comp_in_M by simp
moreover
have "⟨s,y⟩∈t ⟹ s∈domain(t)" if "t∈M" for s y t
using that unfolding domain_def by auto
ultimately
have
"(∀s∈M. s ∈ domain(t1) ∨ s ∈ domain(t2) ⟶ (∀q∈M. q∈P ∧ q ≼ p ⟶
(f ` ⟨1, s, t1, q⟩ =1 ⟷ f ` ⟨1, s, t2, q⟩=1))) ⟷
(∀s. s ∈ domain(t1) ∨ s ∈ domain(t2) ⟶ (∀q. q∈P ∧ q ≼ p ⟶
(f ` ⟨1, s, t1, q⟩ =1 ⟷ f ` ⟨1, s, t2, q⟩=1)))"
using assms domain_trans[OF trans_M,of t1]
domain_trans[OF trans_M,of t2] by auto
then show ?thesis
unfolding eq_case_def is_eq_case_def
using assms pair_in_M_iff nat_into_M[of 1] domain_closed
apply_closed leq_in_M nonempty Un_closed
by (simp add:components_abs)
qed
lemma mem_case_abs [simp]:
assumes
"t1∈M" "t2∈M" "p∈M" "f∈M"
shows
"is_mem_case(##M,t1,t2,p,P,leq,f) ⟷ mem_case(t1,t2,p,P,leq,f)"
proof
{
fix v
assume "v∈P" "v ≼ p" "is_mem_case(##M,t1,t2,p,P,leq,f)"
moreover
from this
have "v∈M" "⟨v,p⟩ ∈ M" "(##M)(v)"
using transitivity[OF _ P_in_M,of v] transitivity[OF _ leq_in_M]
by simp_all
moreover
from calculation assms
obtain q r s where
"r ∈ P ∧ q ∈ P ∧ ⟨q, v⟩ ∈ M ∧ ⟨s, r⟩ ∈ M ∧ ⟨q, r⟩ ∈ M ∧ 0 ∈ M ∧
⟨0, t1, s, q⟩ ∈ M ∧ q ≼ v ∧ ⟨s, r⟩ ∈ t2 ∧ q ≼ r ∧ f ` ⟨0, t1, s, q⟩ = 1"
unfolding is_mem_case_def by (auto simp add:components_abs)
then
have "∃q s r. r ∈ P ∧ q ∈ P ∧ q ≼ v ∧ ⟨s, r⟩ ∈ t2 ∧ q ≼ r ∧ f ` ⟨0, t1, s, q⟩ = 1"
by auto
}
then
show "mem_case(t1, t2, p, P, leq, f)" if "is_mem_case(##M, t1, t2, p, P, leq, f)"
unfolding mem_case_def using that assms by auto
next
{ fix v
assume "v ∈ M" "v ∈ P" "⟨v, p⟩ ∈ M" "v ≼ p" "mem_case(t1, t2, p, P, leq, f)"
moreover
from this
obtain q s r where "r ∈ P ∧ q ∈ P ∧ q ≼ v ∧ ⟨s, r⟩ ∈ t2 ∧ q ≼ r ∧ f ` ⟨0, t1, s, q⟩ = 1"
unfolding mem_case_def by auto
moreover
from this ‹t2∈M›
have "r∈M" "q∈M" "s∈M" "r ∈ P ∧ q ∈ P ∧ q ≼ v ∧ ⟨s, r⟩ ∈ t2 ∧ q ≼ r ∧ f ` ⟨0, t1, s, q⟩ = 1"
using transitivity P_in_M domain_closed[of t2] by auto
moreover
note ‹t1∈M›
ultimately
have "∃q∈M . ∃s∈M. ∃r∈M.
r ∈ P ∧ q ∈ P ∧ ⟨q, v⟩ ∈ M ∧ ⟨s, r⟩ ∈ M ∧ ⟨q, r⟩ ∈ M ∧ 0 ∈ M ∧
⟨0, t1, s, q⟩ ∈ M ∧ q ≼ v ∧ ⟨s, r⟩ ∈ t2 ∧ q ≼ r ∧ f ` ⟨0, t1, s, q⟩ = 1"
using pair_in_M_iff zero_in_M by auto
}
then
show "is_mem_case(##M, t1, t2, p, P, leq, f)" if "mem_case(t1, t2, p, P, leq, f)"
unfolding is_mem_case_def
using assms that nonempty pair_in_M_iff apply_closed
by (auto simp add:components_abs)
qed
lemma Hfrc_abs :
"⟦fnnc∈M; f∈M⟧ ⟹
is_Hfrc(##M,P,leq,fnnc,f) ⟷ Hfrc(P,leq,fnnc,f)"
unfolding is_Hfrc_def Hfrc_def using pair_in_M_iff nonempty
by (auto simp add:components_abs)
lemma Hfrc_at_abs :
"⟦fnnc∈M; f∈M ; z∈M⟧ ⟹
is_Hfrc_at(##M,P,leq,fnnc,f,z) ⟷ z = bool_of_o(Hfrc(P,leq,fnnc,f)) "
unfolding is_Hfrc_at_def using Hfrc_abs
by auto
lemma components_closed :
"x∈M ⟹ (##M)(ftype(x))"
"x∈M ⟹ (##M)(name1(x))"
"x∈M ⟹ (##M)(name2(x))"
"x∈M ⟹ (##M)(cond_of(x))"
unfolding ftype_def name1_def name2_def cond_of_def using fst_snd_closed by simp_all
lemma ecloseN_closed :
"(##M)(A) ⟹ (##M)(ecloseN(A))"
"(##M)(A) ⟹ (##M)(eclose_n(name1,A))"
"(##M)(A) ⟹ (##M)(eclose_n(name2,A))"
unfolding ecloseN_def eclose_n_def
using components_closed eclose_closed singleton_closed Un_closed by auto
lemma eclose_n_abs :
assumes "x∈M" "ec∈M"
shows "is_eclose_n(##M,is_name1,ec,x) ⟷ ec = eclose_n(name1,x)"
"is_eclose_n(##M,is_name2,ec,x) ⟷ ec = eclose_n(name2,x)"
unfolding is_eclose_n_def eclose_n_def
using assms name1_abs name2_abs eclose_abs singleton_closed components_closed
by auto
lemma ecloseN_abs :
"⟦x∈M;ec∈M⟧ ⟹ is_ecloseN(##M,x,ec) ⟷ ec = ecloseN(x)"
unfolding is_ecloseN_def ecloseN_def
using eclose_n_abs Un_closed union_abs ecloseN_closed
by auto
lemma frecR_abs :
"x∈M ⟹ y∈M ⟹ frecR(x,y) ⟷ is_frecR(##M,x,y)"
unfolding frecR_def is_frecR_def
using nonempty domain_closed Un_closed components_closed
by (auto simp add: components_abs)
lemma frecrelP_abs :
"z∈M ⟹ frecrelP(##M,z) ⟷ (∃x y. z = ⟨x,y⟩ ∧ frecR(x,y))"
using pair_in_M_iff frecR_abs unfolding frecrelP_def by auto
lemma frecrel_abs :
assumes
"A∈M" "r∈M"
shows
"is_frecrel(##M,A,r) ⟷ r = frecrel(A)"
proof -
from ‹A∈M›
have "z∈M" if "z∈A×A" for z
using cartprod_closed transitivity that by simp
then
have "Collect(A×A,frecrelP(##M)) = Collect(A×A,λz. (∃x y. z = ⟨x,y⟩ ∧ frecR(x,y)))"
using Collect_cong[of "A×A" "A×A" "frecrelP(##M)"] assms frecrelP_abs by simp
with assms
show ?thesis unfolding is_frecrel_def def_frecrel using cartprod_closed
by simp
qed
lemma frecrel_closed :
assumes
"x∈M"
shows
"frecrel(x)∈M"
proof -
have "Collect(x×x,λz. (∃x y. z = ⟨x,y⟩ ∧ frecR(x,y)))∈M"
using Collect_in_M[of "frecrelP_fm(0)" "[]"] arity_frecrelP_fm sats_frecrelP_fm
frecrelP_abs ‹x∈M› cartprod_closed by simp
then show ?thesis
unfolding frecrel_def Rrel_def frecrelP_def by simp
qed
lemma field_frecrel : "field(frecrel(names_below(P,x))) ⊆ names_below(P,x)"
unfolding frecrel_def
using field_Rrel by simp
lemma forcerelD : "uv ∈ forcerel(P,x) ⟹ uv∈ names_below(P,x) × names_below(P,x)"
unfolding forcerel_def
using trancl_type field_frecrel by blast
lemma wf_forcerel :
"wf(forcerel(P,x))"
unfolding forcerel_def using wf_trancl wf_frecrel .
lemma restrict_trancl_forcerel :
assumes "frecR(w,y)"
shows "restrict(f,frecrel(names_below(P,x))-``{y})`w
= restrict(f,forcerel(P,x)-``{y})`w"
unfolding forcerel_def frecrel_def using assms restrict_trancl_Rrel[of frecR]
by simp
lemma names_belowI :
assumes "frecR(⟨ft,n1,n2,p⟩,⟨a,b,c,d⟩)" "p∈P"
shows "⟨ft,n1,n2,p⟩ ∈ names_below(P,⟨a,b,c,d⟩)" (is "?x ∈ names_below(_,?y)")
proof -
from assms
have "ft ∈ 2" "a ∈ 2"
unfolding frecR_def by (auto simp add:components_simp)
from assms
consider (e) "n1 ∈ domain(b) ∪ domain(c) ∧ (n2 = b ∨ n2 =c)"
| (m) "n1 = b ∧ n2 ∈ domain(c)"
unfolding frecR_def by (auto simp add:components_simp)
then show ?thesis
proof cases
case e
then
have "n1 ∈ eclose(b) ∨ n1 ∈ eclose(c)"
using Un_iff in_dom_in_eclose by auto
with e
have "n1 ∈ ecloseN(?y)" "n2 ∈ ecloseN(?y)"
using ecloseNI components_in_eclose by auto
with ‹ft∈2› ‹p∈P›
show ?thesis unfolding names_below_def by auto
next
case m
then
have "n1 ∈ ecloseN(?y)" "n2 ∈ ecloseN(?y)"
using mem_eclose_trans ecloseNI
in_dom_in_eclose components_in_eclose by auto
with ‹ft∈2› ‹p∈P›
show ?thesis unfolding names_below_def
by auto
qed
qed
lemma names_below_tr :
assumes "x∈ names_below(P,y)"
"y∈ names_below(P,z)"
shows "x∈ names_below(P,z)"
proof -
let ?A="λy . names_below(P,y)"
from assms
obtain fx x1 x2 px where
"x = ⟨fx,x1,x2,px⟩" "fx∈2" "x1∈ecloseN(y)" "x2∈ecloseN(y)" "px∈P"
unfolding names_below_def by auto
from assms
obtain fy y1 y2 py where
"y = ⟨fy,y1,y2,py⟩" "fy∈2" "y1∈ecloseN(z)" "y2∈ecloseN(z)" "py∈P"
unfolding names_below_def by auto
from ‹x1∈_› ‹x2∈_› ‹y1∈_› ‹y2∈_› ‹x=_› ‹y=_›
have "x1∈ecloseN(z)" "x2∈ecloseN(z)"
using ecloseN_mono names_simp by auto
with ‹fx∈2› ‹px∈P› ‹x=_›
have "x∈?A(z)"
unfolding names_below_def by simp
then show ?thesis using subsetI by simp
qed
lemma arg_into_names_below2 :
assumes "⟨x,y⟩ ∈ frecrel(names_below(P,z))"
shows "x ∈ names_below(P,y)"
proof -
{
from assms
have "x∈names_below(P,z)" "y∈names_below(P,z)" "frecR(x,y)"
unfolding frecrel_def Rrel_def
by auto
obtain f n1 n2 p where
"x = ⟨f,n1,n2,p⟩" "f∈2" "n1∈ecloseN(z)" "n2∈ecloseN(z)" "p∈P"
using ‹x∈names_below(P,z)›
unfolding names_below_def by auto
moreover
obtain fy m1 m2 q where
"q∈P" "y = ⟨fy,m1,m2,q⟩"
using ‹y∈names_below(P,z)›
unfolding names_below_def by auto
moreover
note ‹frecR(x,y)›
ultimately
have "x∈names_below(P,y)" using names_belowI by simp
}
then show ?thesis .
qed
lemma arg_into_names_below :
assumes "⟨x,y⟩ ∈ frecrel(names_below(P,z))"
shows "x ∈ names_below(P,x)"
proof -
{
from assms
have "x∈names_below(P,z)"
unfolding frecrel_def Rrel_def
by auto
from ‹x∈names_below(P,z)›
obtain f n1 n2 p where
"x = ⟨f,n1,n2,p⟩" "f∈2" "n1∈ecloseN(z)" "n2∈ecloseN(z)" "p∈P"
unfolding names_below_def by auto
then
have "n1∈ecloseN(x)" "n2∈ecloseN(x)"
using components_in_eclose by simp_all
with ‹f∈2› ‹p∈P› ‹x = ⟨f,n1,n2,p⟩›
have "x∈names_below(P,x)"
unfolding names_below_def by simp
}
then show ?thesis .
qed
lemma forcerel_arg_into_names_below :
assumes "⟨x,y⟩ ∈ forcerel(P,z)"
shows "x ∈ names_below(P,x)"
using assms
unfolding forcerel_def
by(rule trancl_induct;auto simp add: arg_into_names_below)
lemma names_below_mono :
assumes "⟨x,y⟩ ∈ frecrel(names_below(P,z))"
shows "names_below(P,x) ⊆ names_below(P,y)"
proof -
from assms
have "x∈names_below(P,y)"
using arg_into_names_below2 by simp
then
show ?thesis
using names_below_tr subsetI by simp
qed
lemma frecrel_mono :
assumes "⟨x,y⟩ ∈ frecrel(names_below(P,z))"
shows "frecrel(names_below(P,x)) ⊆ frecrel(names_below(P,y))"
unfolding frecrel_def
using Rrel_mono names_below_mono assms by simp
lemma forcerel_mono2 :
assumes "⟨x,y⟩ ∈ frecrel(names_below(P,z))"
shows "forcerel(P,x) ⊆ forcerel(P,y)"
unfolding forcerel_def
using trancl_mono frecrel_mono assms by simp
lemma forcerel_mono_aux :
assumes "⟨x,y⟩ ∈ frecrel(names_below(P, w))^+"
shows "forcerel(P,x) ⊆ forcerel(P,y)"
using assms
by (rule trancl_induct,simp_all add: subset_trans forcerel_mono2)
lemma forcerel_mono :
assumes "⟨x,y⟩ ∈ forcerel(P,z)"
shows "forcerel(P,x) ⊆ forcerel(P,y)"
using forcerel_mono_aux assms unfolding forcerel_def by simp
lemma forcerel_eq_aux : "x ∈ names_below(P, w) ⟹ ⟨x,y⟩ ∈ forcerel(P,z) ⟹
(y ∈ names_below(P, w) ⟶ ⟨x,y⟩ ∈ forcerel(P,w))"
unfolding forcerel_def
proof(rule_tac a=x and b=y and P="λ y . y ∈ names_below(P, w) ⟶ ⟨x,y⟩ ∈ frecrel(names_below(P,w))^+" in trancl_induct,simp)
let ?A="λ a . names_below(P, a)"
let ?R="λ a . frecrel(?A(a))"
let ?fR="λ a .forcerel(a)"
show "u∈?A(w) ⟶ ⟨x,u⟩∈?R(w)^+" if "x∈?A(w)" "⟨x,y⟩∈?R(z)^+" "⟨x,u⟩∈?R(z)" for u
using that frecrelD frecrelI r_into_trancl unfolding names_below_def by simp
{
fix u v
assume "x ∈ ?A(w)"
"⟨x, y⟩ ∈ ?R(z)^+"
"⟨x, u⟩ ∈ ?R(z)^+"
"⟨u, v⟩ ∈ ?R(z)"
"u ∈ ?A(w) ⟹ ⟨x, u⟩ ∈ ?R(w)^+"
then
have "v ∈ ?A(w) ⟹ ⟨x, v⟩ ∈ ?R(w)^+"
proof -
assume "v ∈?A(w)"
from ‹⟨u,v⟩∈_›
have "u∈?A(v)"
using arg_into_names_below2 by simp
with ‹v ∈?A(w)›
have "u∈?A(w)"
using names_below_tr by simp
with ‹v∈_› ‹⟨u,v⟩∈_›
have "⟨u,v⟩∈ ?R(w)"
using frecrelD frecrelI r_into_trancl unfolding names_below_def by simp
with ‹u ∈ ?A(w) ⟹ ⟨x, u⟩ ∈ ?R(w)^+› ‹u∈?A(w)›
have "⟨x, u⟩ ∈ ?R(w)^+" by simp
with ‹⟨u,v⟩∈ ?R(w)›
show "⟨x,v⟩∈ ?R(w)^+" using trancl_trans r_into_trancl
by simp
qed
}
then show "v ∈ ?A(w) ⟶ ⟨x, v⟩ ∈ ?R(w)^+"
if "x ∈ ?A(w)"
"⟨x, y⟩ ∈ ?R(z)^+"
"⟨x, u⟩ ∈ ?R(z)^+"
"⟨u, v⟩ ∈ ?R(z)"
"u ∈ ?A(w) ⟶ ⟨x, u⟩ ∈ ?R(w)^+" for u v
using that by simp
qed
lemma forcerel_eq :
assumes "⟨z,x⟩ ∈ forcerel(P,x)"
shows "forcerel(P,z) = forcerel(P,x) ∩ names_below(P,z)×names_below(P,z)"
using assms forcerel_eq_aux forcerelD forcerel_mono[of z x x] subsetI
by auto
lemma forcerel_below_aux :
assumes "⟨z,x⟩ ∈ forcerel(P,x)" "⟨u,z⟩ ∈ forcerel(P,x)"
shows "u ∈ names_below(P,z)"
using assms(2)
unfolding forcerel_def
proof(rule trancl_induct)
show "u ∈ names_below(P,y)" if " ⟨u, y⟩ ∈ frecrel(names_below(P, x))" for y
using that vimage_singleton_iff arg_into_names_below2 by simp
next
show "u ∈ names_below(P,z)"
if "⟨u, y⟩ ∈ frecrel(names_below(P, x))^+"
"⟨y, z⟩ ∈ frecrel(names_below(P, x))"
"u ∈ names_below(P, y)"
for y z
using that arg_into_names_below2[of y z x] names_below_tr by simp
qed
lemma forcerel_below :
assumes "⟨z,x⟩ ∈ forcerel(P,x)"
shows "forcerel(P,x) -`` {z} ⊆ names_below(P,z)"
using vimage_singleton_iff assms forcerel_below_aux by auto
lemma relation_forcerel :
shows "relation(forcerel(P,z))" "trans(forcerel(P,z))"
unfolding forcerel_def using relation_trancl trans_trancl by simp_all
lemma Hfrc_restrict_trancl : "bool_of_o(Hfrc(P, leq, y, restrict(f,frecrel(names_below(P,x))-``{y})))
= bool_of_o(Hfrc(P, leq, y, restrict(f,(frecrel(names_below(P,x))^+)-``{y})))"
unfolding Hfrc_def bool_of_o_def eq_case_def mem_case_def
using restrict_trancl_forcerel frecRI1 frecRI2 frecRI3
unfolding forcerel_def
by simp
lemma frc_at_trancl : "frc_at(P,leq,z) = wfrec(forcerel(P,z),z,λx f. bool_of_o(Hfrc(P,leq,x,f)))"
unfolding frc_at_def forcerel_def using wf_eq_trancl Hfrc_restrict_trancl by simp
lemma forcerelI1 :
assumes "n1 ∈ domain(b) ∨ n1 ∈ domain(c)" "p∈P" "d∈P"
shows "⟨⟨1, n1, b, p⟩, ⟨0,b,c,d⟩⟩∈ forcerel(P,⟨0,b,c,d⟩)"
proof -
let ?x="⟨1, n1, b, p⟩"
let ?y="⟨0,b,c,d⟩"
from assms
have "frecR(?x,?y)"
using frecRI1 by simp
then
have "?x∈names_below(P,?y)" "?y ∈ names_below(P,?y)"
using names_belowI assms components_in_eclose
unfolding names_below_def by auto
with ‹frecR(?x,?y)›
show ?thesis
unfolding forcerel_def frecrel_def
using subsetD[OF r_subset_trancl[OF relation_Rrel]] RrelI
by auto
qed
lemma forcerelI2 :
assumes "n1 ∈ domain(b) ∨ n1 ∈ domain(c)" "p∈P" "d∈P"
shows "⟨⟨1, n1, c, p⟩, ⟨0,b,c,d⟩⟩∈ forcerel(P,⟨0,b,c,d⟩)"
proof -
let ?x="⟨1, n1, c, p⟩"
let ?y="⟨0,b,c,d⟩"
from assms
have "frecR(?x,?y)"
using frecRI2 by simp
then
have "?x∈names_below(P,?y)" "?y ∈ names_below(P,?y)"
using names_belowI assms components_in_eclose
unfolding names_below_def by auto
with ‹frecR(?x,?y)›
show ?thesis
unfolding forcerel_def frecrel_def
using subsetD[OF r_subset_trancl[OF relation_Rrel]] RrelI
by auto
qed
lemma forcerelI3 :
assumes "⟨n2, r⟩ ∈ c" "p∈P" "d∈P" "r ∈ P"
shows "⟨⟨0, b, n2, p⟩,⟨1, b, c, d⟩⟩ ∈ forcerel(P,⟨1,b,c,d⟩)"
proof -
let ?x="⟨0, b, n2, p⟩"
let ?y="⟨1, b, c, d⟩"
from assms
have "frecR(?x,?y)"
using assms frecRI3 by simp
then
have "?x∈names_below(P,?y)" "?y ∈ names_below(P,?y)"
using names_belowI assms components_in_eclose
unfolding names_below_def by auto
with ‹frecR(?x,?y)›
show ?thesis
unfolding forcerel_def frecrel_def
using subsetD[OF r_subset_trancl[OF relation_Rrel]] RrelI
by auto
qed
lemmas forcerelI= forcerelI1[THEN vimage_singleton_iff[THEN iffD2]]
forcerelI2[THEN vimage_singleton_iff[THEN iffD2]]
forcerelI3[THEN vimage_singleton_iff[THEN iffD2]]
lemma aux_def_frc_at:
assumes "z ∈ forcerel(P,x) -`` {x}"
shows "wfrec(forcerel(P,x), z, H) = wfrec(forcerel(P,z), z, H)"
proof -
let ?A="names_below(P,z)"
from assms
have "⟨z,x⟩ ∈ forcerel(P,x)"
using vimage_singleton_iff by simp
then
have "z ∈ ?A"
using forcerel_arg_into_names_below by simp
from ‹⟨z,x⟩ ∈ forcerel(P,x)›
have E:"forcerel(P,z) = forcerel(P,x) ∩ (?A×?A)"
"forcerel(P,x) -`` {z} ⊆ ?A"
using forcerel_eq forcerel_below
by auto
with ‹z∈?A›
have "wfrec(forcerel(P,x), z, H) = wfrec[?A](forcerel(P,x), z, H)"
using wfrec_trans_restr[OF relation_forcerel(1) wf_forcerel relation_forcerel(2), of x z ?A]
by simp
then show ?thesis
using E wfrec_restr_eq by simp
qed
subsection‹Recursive expression of \<^term>‹frc_at››
lemma def_frc_at :
assumes "p∈P"
shows
"frc_at(P,leq,⟨ft,n1,n2,p⟩) =
bool_of_o( p ∈P ∧
( ft = 0 ∧ (∀s. s∈domain(n1) ∪ domain(n2) ⟶
(∀q. q∈P ∧ q ≼ p ⟶ (frc_at(P,leq,⟨1,s,n1,q⟩) =1 ⟷ frc_at(P,leq,⟨1,s,n2,q⟩) =1)))
∨ ft = 1 ∧ ( ∀v∈P. v ≼ p ⟶
(∃q. ∃s. ∃r. r∈P ∧ q∈P ∧ q ≼ v ∧ ⟨s,r⟩ ∈ n2 ∧ q ≼ r ∧ frc_at(P,leq,⟨0,n1,s,q⟩) = 1))))"
proof -
let ?r="λy. forcerel(P,y)" and ?Hf="λx f. bool_of_o(Hfrc(P,leq,x,f))"
let ?t="λy. ?r(y) -`` {y}"
let ?arg="⟨ft,n1,n2,p⟩"
from wf_forcerel
have wfr: "∀w . wf(?r(w))" ..
with wfrec [of "?r(?arg)" ?arg ?Hf]
have "frc_at(P,leq,?arg) = ?Hf( ?arg, λx∈?r(?arg) -`` {?arg}. wfrec(?r(?arg), x, ?Hf))"
using frc_at_trancl by simp
also
have " ... = ?Hf( ?arg, λx∈?r(?arg) -`` {?arg}. frc_at(P,leq,x))"
using aux_def_frc_at frc_at_trancl by simp
finally
show ?thesis
unfolding Hfrc_def mem_case_def eq_case_def
using forcerelI assms
by auto
qed
subsection‹Absoluteness of \<^term>‹frc_at››
lemma forcerel_in_M :
assumes
"x∈M"
shows
"forcerel(P,x)∈M"
unfolding forcerel_def def_frecrel names_below_def
proof -
let ?Q = "2 × ecloseN(x) × ecloseN(x) × P"
have "?Q × ?Q ∈ M"
using ‹x∈M› P_in_M twoN_in_M ecloseN_closed cartprod_closed by simp
moreover
have "separation(##M,λz. ∃x y. z = ⟨x, y⟩ ∧ frecR(x, y))"
proof -
have "arity(frecrelP_fm(0)) = 1"
unfolding number1_fm_def frecrelP_fm_def
by (simp del:FOL_sats_iff pair_abs empty_abs
add: fm_definitions components_defs ord_simp_union)
then
have "separation(##M, λz. sats(M,frecrelP_fm(0) , [z]))"
using separation_ax by simp
moreover
have "frecrelP(##M,z) ⟷ sats(M,frecrelP_fm(0),[z])"
if "z∈M" for z
using that sats_frecrelP_fm[of 0 "[z]"] by simp
ultimately
have "separation(##M,frecrelP(##M))"
unfolding separation_def by (simp del:sats_frecrelP_fm)
then
show ?thesis using frecrelP_abs
separation_cong[of "##M" "frecrelP(##M)" "λz. ∃x y. z = ⟨x, y⟩ ∧ frecR(x, y)"]
by simp
qed
ultimately
show "{z ∈ ?Q × ?Q . ∃x y. z = ⟨x, y⟩ ∧ frecR(x, y)}^+ ∈ M"
using separation_closed frecrelP_abs trancl_closed by simp
qed
lemma relation2_Hfrc_at_abs :
"relation2(##M,is_Hfrc_at(##M,P,leq),λx f. bool_of_o(Hfrc(P,leq,x,f)))"
unfolding relation2_def using Hfrc_at_abs
by simp
lemma Hfrc_at_closed :
"∀x∈M. ∀g∈M. function(g) ⟶ bool_of_o(Hfrc(P,leq,x,g))∈M"
unfolding bool_of_o_def using zero_in_M nat_into_M[of 1] by simp
lemma wfrec_Hfrc_at :
assumes
"X∈M"
shows
"wfrec_replacement(##M,is_Hfrc_at(##M,P,leq),forcerel(P,X))"
proof -
have 0:"is_Hfrc_at(##M,P,leq,a,b,c) ⟷
sats(M,Hfrc_at_fm(8,9,2,1,0),[c,b,a,d,e,y,x,z,P,leq,forcerel(P,X)])"
if "a∈M" "b∈M" "c∈M" "d∈M" "e∈M" "y∈M" "x∈M" "z∈M"
for a b c d e y x z
using that P_in_M leq_in_M ‹X∈M› forcerel_in_M
Hfrc_at_iff_sats[of concl:M P leq a b c 8 9 2 1 0
"[c,b,a,d,e,y,x,z,P,leq,forcerel(P,X)]"] by simp
have 1:"sats(M,is_wfrec_fm(Hfrc_at_fm(8,9,2,1,0),5,1,0),[y,x,z,P,leq,forcerel(P,X)]) ⟷
is_wfrec(##M, is_Hfrc_at(##M,P,leq),forcerel(P,X), x, y)"
if "x∈M" "y∈M" "z∈M" for x y z
using that ‹X∈M› forcerel_in_M P_in_M leq_in_M
sats_is_wfrec_fm[OF 0]
by simp
let
?f="Exists(And(pair_fm(1,0,2),is_wfrec_fm(Hfrc_at_fm(8,9,2,1,0),5,1,0)))"
have satsf:"sats(M, ?f, [x,z,P,leq,forcerel(P,X)]) ⟷
(∃y∈M. pair(##M,x,y,z) & is_wfrec(##M, is_Hfrc_at(##M,P,leq),forcerel(P,X), x, y))"
if "x∈M" "z∈M" for x z
using that 1 ‹X∈M› forcerel_in_M P_in_M leq_in_M by (simp del:pair_abs)
have artyf:"arity(?f) = 5"
unfolding fm_definitions PHcheck_fm_def is_tuple_fm_def
by (simp add:ord_simp_union)
moreover
have "?f∈formula"
unfolding fm_definitions by simp
ultimately
have "strong_replacement(##M,λx z. sats(M,?f,[x,z,P,leq,forcerel(P,X)]))"
using replacement_ax[of ?f] 1 artyf ‹X∈M› forcerel_in_M P_in_M leq_in_M by simp
then
have "strong_replacement(##M,λx z.
∃y∈M. pair(##M,x,y,z) & is_wfrec(##M, is_Hfrc_at(##M,P,leq),forcerel(P,X), x, y))"
using repl_sats[of M ?f "[P,leq,forcerel(P,X)]"] satsf by (simp del:pair_abs)
then
show ?thesis unfolding wfrec_replacement_def by simp
qed
lemma names_below_abs :
"⟦Q∈M;x∈M;nb∈M⟧ ⟹ is_names_below(##M,Q,x,nb) ⟷ nb = names_below(Q,x)"
unfolding is_names_below_def names_below_def
using succ_in_M_iff zero_in_M cartprod_closed ecloseN_abs ecloseN_closed
by auto
lemma names_below_closed :
"⟦Q∈M;x∈M⟧ ⟹ names_below(Q,x) ∈ M"
unfolding names_below_def
using zero_in_M cartprod_closed ecloseN_closed succ_in_M_iff
by simp
lemma "names_below_productE" :
assumes "Q ∈ M" "x ∈ M"
"⋀A1 A2 A3 A4. A1 ∈ M ⟹ A2 ∈ M ⟹ A3 ∈ M ⟹ A4 ∈ M ⟹ R(A1 × A2 × A3 × A4)"
shows "R(names_below(Q,x))"
unfolding names_below_def using assms zero_in_M ecloseN_closed[of x] twoN_in_M by auto
lemma forcerel_abs :
"⟦x∈M;z∈M⟧ ⟹ is_forcerel(##M,P,x,z) ⟷ z = forcerel(P,x)"
unfolding is_forcerel_def forcerel_def
using frecrel_abs names_below_abs trancl_abs P_in_M twoN_in_M ecloseN_closed names_below_closed
names_below_productE[of concl:"λp. is_frecrel(##M,p,_) ⟷ _ = frecrel(p)"] frecrel_closed
by simp
lemma frc_at_abs :
assumes "fnnc∈M" "z∈M"
shows "is_frc_at(##M,P,leq,fnnc,z) ⟷ z = frc_at(P,leq,fnnc)"
proof -
from assms
have "(∃r∈M. is_forcerel(##M,P,fnnc, r) ∧ is_wfrec(##M, is_Hfrc_at(##M, P, leq), r, fnnc, z))
⟷ is_wfrec(##M, is_Hfrc_at(##M, P, leq), forcerel(P,fnnc), fnnc, z)"
using forcerel_abs forcerel_in_M by simp
then
show ?thesis
unfolding frc_at_trancl is_frc_at_def
using assms wfrec_Hfrc_at[of fnnc] wf_forcerel relation_forcerel forcerel_in_M
Hfrc_at_closed relation2_Hfrc_at_abs
trans_wfrec_abs[of "forcerel(P,fnnc)" fnnc z "is_Hfrc_at(##M,P,leq)" "λx f. bool_of_o(Hfrc(P,leq,x,f))"]
by (simp flip:setclass_iff)
qed
lemma forces_eq'_abs :
"⟦p∈M ; t1∈M ; t2∈M⟧ ⟹ is_forces_eq'(##M,P,leq,p,t1,t2) ⟷ forces_eq'(P,leq,p,t1,t2)"
unfolding is_forces_eq'_def forces_eq'_def
using frc_at_abs zero_in_M pair_in_M_iff by (auto simp add:components_abs)
lemma forces_mem'_abs :
"⟦p∈M ; t1∈M ; t2∈M⟧ ⟹ is_forces_mem'(##M,P,leq,p,t1,t2) ⟷ forces_mem'(P,leq,p,t1,t2)"
unfolding is_forces_mem'_def forces_mem'_def
using frc_at_abs zero_in_M pair_in_M_iff by (auto simp add:components_abs)
lemma forces_neq'_abs :
assumes
"p∈M" "t1∈M" "t2∈M"
shows
"is_forces_neq'(##M,P,leq,p,t1,t2) ⟷ forces_neq'(P,leq,p,t1,t2)"
proof -
have "q∈M" if "q∈P" for q
using that transitivity P_in_M by simp
then show ?thesis
unfolding is_forces_neq'_def forces_neq'_def
using assms forces_eq'_abs pair_in_M_iff
by (auto simp add:components_abs,blast)
qed
lemma forces_nmem'_abs :
assumes
"p∈M" "t1∈M" "t2∈M"
shows
"is_forces_nmem'(##M,P,leq,p,t1,t2) ⟷ forces_nmem'(P,leq,p,t1,t2)"
proof -
have "q∈M" if "q∈P" for q
using that transitivity P_in_M by simp
then show ?thesis
unfolding is_forces_nmem'_def forces_nmem'_def
using assms forces_mem'_abs pair_in_M_iff
by (auto simp add:components_abs,blast)
qed
end
subsection‹Forcing for general formulas›
definition
ren_forces_nand :: "i⇒i" where
"ren_forces_nand(φ) ≡ Exists(And(Equal(0,1),iterates(λp. incr_bv(p)`1 , 2, φ)))"
lemma ren_forces_nand_type [TC] :
"φ∈formula ⟹ ren_forces_nand(φ) ∈formula"
unfolding ren_forces_nand_def
by simp
lemma arity_ren_forces_nand :
assumes "φ∈formula"
shows "arity(ren_forces_nand(φ)) ≤ succ(arity(φ))"
proof -
consider (lt) "1<arity(φ)" | (ge) "¬ 1 < arity(φ)"
by auto
then
show ?thesis
proof cases
case lt
with ‹φ∈_›
have "2 < succ(arity(φ))" "2<arity(φ)#+2"
using succ_ltI by auto
with ‹φ∈_›
have "arity(iterates(λp. incr_bv(p)`1,2,φ)) = 2#+arity(φ)"
using arity_incr_bv_lemma lt
by auto
with ‹φ∈_›
show ?thesis
unfolding ren_forces_nand_def
using lt pred_Un_distrib union_abs1 Un_assoc[symmetric] Un_le_compat
by simp
next
case ge
with ‹φ∈_›
have "arity(φ) ≤ 1" "pred(arity(φ)) ≤ 1"
using not_lt_iff_le le_trans[OF le_pred]
by simp_all
with ‹φ∈_›
have "arity(iterates(λp. incr_bv(p)`1,2,φ)) = (arity(φ))"
using arity_incr_bv_lemma ge
by simp
with ‹arity(φ) ≤ 1› ‹φ∈_› ‹pred(_) ≤ 1›
show ?thesis
unfolding ren_forces_nand_def
using pred_Un_distrib union_abs1 Un_assoc[symmetric] union_abs2
by simp
qed
qed
lemma sats_ren_forces_nand :
"[q,P,leq,o,p] @ env ∈ list(M) ⟹ φ∈formula ⟹
sats(M, ren_forces_nand(φ),[q,p,P,leq,o] @ env) ⟷ sats(M, φ,[q,P,leq,o] @ env)"
unfolding ren_forces_nand_def
using sats_incr_bv_iff [of _ _ M _ "[q]"]
by simp
definition
ren_forces_forall :: "i⇒i" where
"ren_forces_forall(φ) ≡
Exists(Exists(Exists(Exists(Exists(
And(Equal(0,6),And(Equal(1,7),And(Equal(2,8),And(Equal(3,9),
And(Equal(4,5),iterates(λp. incr_bv(p)`5 , 5, φ)))))))))))"
lemma arity_ren_forces_all :
assumes "φ∈formula"
shows "arity(ren_forces_forall(φ)) = 5 ∪ arity(φ)"
proof -
consider (lt) "5<arity(φ)" | (ge) "¬ 5 < arity(φ)"
by auto
then
show ?thesis
proof cases
case lt
with ‹φ∈_›
have "5 < succ(arity(φ))" "5<arity(φ)#+2" "5<arity(φ)#+3" "5<arity(φ)#+4"
using succ_ltI by auto
with ‹φ∈_›
have "arity(iterates(λp. incr_bv(p)`5,5,φ)) = 5#+arity(φ)"
using arity_incr_bv_lemma lt
by simp
with ‹φ∈_›
show ?thesis
unfolding ren_forces_forall_def
using pred_Un_distrib union_abs1 Un_assoc[symmetric] union_abs2
by simp
next
case ge
with ‹φ∈_›
have "arity(φ) ≤ 5" "pred^5(arity(φ)) ≤ 5"
using not_lt_iff_le le_trans[OF le_pred]
by simp_all
with ‹φ∈_›
have "arity(iterates(λp. incr_bv(p)`5,5,φ)) = arity(φ)"
using arity_incr_bv_lemma ge
by simp
with ‹arity(φ) ≤ 5› ‹φ∈_› ‹pred^5(_) ≤ 5›
show ?thesis
unfolding ren_forces_forall_def
using pred_Un_distrib union_abs1 Un_assoc[symmetric] union_abs2
by simp
qed
qed
lemma ren_forces_forall_type [TC] :
"φ∈formula ⟹ ren_forces_forall(φ) ∈formula"
unfolding ren_forces_forall_def by simp
lemma sats_ren_forces_forall :
"[x,P,leq,o,p] @ env ∈ list(M) ⟹ φ∈formula ⟹
sats(M, ren_forces_forall(φ),[x,p,P,leq,o] @ env) ⟷ sats(M, φ,[p,P,leq,o,x] @ env)"
unfolding ren_forces_forall_def
using sats_incr_bv_iff [of _ _ M _ "[p,P,leq,o,x]"]
by simp
definition
is_leq :: "[i⇒o,i,i,i] ⇒ o" where
"is_leq(A,l,q,p) ≡ ∃qp[A]. (pair(A,q,p,qp) ∧ qp∈l)"
lemma (in forcing_data) leq_abs :
"⟦ l∈M ; q∈M ; p∈M ⟧ ⟹ is_leq(##M,l,q,p) ⟷ ⟨q,p⟩∈l"
unfolding is_leq_def using pair_in_M_iff by simp
definition
leq_fm :: "[i,i,i] ⇒ i" where
"leq_fm(leq,q,p) ≡ Exists(And(pair_fm(q#+1,p#+1,0),Member(0,leq#+1)))"
lemma arity_leq_fm :
"⟦leq∈nat;q∈nat;p∈nat⟧ ⟹ arity(leq_fm(leq,q,p)) = succ(q) ∪ succ(p) ∪ succ(leq)"
unfolding leq_fm_def
using arity_pair_fm pred_Un_distrib ord_simp_union
by auto
lemma leq_fm_type [TC] :
"⟦leq∈nat;q∈nat;p∈nat⟧ ⟹ leq_fm(leq,q,p)∈formula"
unfolding leq_fm_def by simp
lemma sats_leq_fm :
"⟦ leq∈nat;q∈nat;p∈nat;env∈list(A) ⟧ ⟹
sats(A,leq_fm(leq,q,p),env) ⟷ is_leq(##A,nth(leq,env),nth(q,env),nth(p,env))"
unfolding leq_fm_def is_leq_def by simp
subsubsection‹The primitive recursion›
consts forces' :: "i⇒i"
primrec
"forces'(Member(x,y)) = forces_mem_fm(1,2,0,x#+4,y#+4)"
"forces'(Equal(x,y)) = forces_eq_fm(1,2,0,x#+4,y#+4)"
"forces'(Nand(p,q)) =
Neg(Exists(And(Member(0,2),And(leq_fm(3,0,1),And(ren_forces_nand(forces'(p)),
ren_forces_nand(forces'(q)))))))"
"forces'(Forall(p)) = Forall(ren_forces_forall(forces'(p)))"
definition
forces :: "i⇒i" where
"forces(φ) ≡ And(Member(0,1),forces'(φ))"
lemma forces'_type [TC]: "φ∈formula ⟹ forces'(φ) ∈ formula"
by (induct φ set:formula; simp)
lemma forces_type [TC] : "φ∈formula ⟹ forces(φ) ∈ formula"
unfolding forces_def by simp
context forcing_data
begin
subsection‹Forcing for atomic formulas in context›
definition
forces_eq :: "[i,i,i] ⇒ o" (‹_ forces⇩a '(_ = _')› [36,1,1] 60) where
"forces_eq ≡ forces_eq'(P,leq)"
definition
forces_mem :: "[i,i,i] ⇒ o" (‹_ forces⇩a '(_ ∈ _')› [36,1,1] 60) where
"forces_mem ≡ forces_mem'(P,leq)"
definition
is_forces_eq :: "[i,i,i] ⇒ o" where
"is_forces_eq ≡ is_forces_eq'(##M,P,leq)"
definition
is_forces_mem :: "[i,i,i] ⇒ o" where
"is_forces_mem ≡ is_forces_mem'(##M,P,leq)"
lemma def_forces_eq : "p∈P ⟹ p forces⇩a (t1 = t2) ⟷
(∀s∈domain(t1) ∪ domain(t2). ∀q. q∈P ∧ q ≼ p ⟶
(q forces⇩a (s ∈ t1) ⟷ q forces⇩a (s ∈ t2)))"
unfolding forces_eq_def forces_mem_def forces_eq'_def forces_mem'_def
using def_frc_at[of p 0 t1 t2 ] unfolding bool_of_o_def
by auto
lemma def_forces_mem : "p∈P ⟹ p forces⇩a (t1 ∈ t2) ⟷
(∀v∈P. v ≼ p ⟶
(∃q. ∃s. ∃r. r∈P ∧ q∈P ∧ q ≼ v ∧ ⟨s,r⟩ ∈ t2 ∧ q ≼ r ∧ q forces⇩a (t1 = s)))"
unfolding forces_eq'_def forces_mem'_def forces_eq_def forces_mem_def
using def_frc_at[of p 1 t1 t2] unfolding bool_of_o_def
by auto
lemma forces_eq_abs :
"⟦p∈M ; t1∈M ; t2∈M⟧ ⟹ is_forces_eq(p,t1,t2) ⟷ p forces⇩a (t1 = t2)"
unfolding is_forces_eq_def forces_eq_def
using forces_eq'_abs by simp
lemma forces_mem_abs :
"⟦p∈M ; t1∈M ; t2∈M⟧ ⟹ is_forces_mem(p,t1,t2) ⟷ p forces⇩a (t1 ∈ t2)"
unfolding is_forces_mem_def forces_mem_def
using forces_mem'_abs by simp
lemma sats_forces_eq_fm :
assumes "p∈nat" "l∈nat" "q∈nat" "t1∈nat" "t2∈nat" "env∈list(M)"
"nth(p,env)=P" "nth(l,env)=leq"
shows "sats(M,forces_eq_fm(p,l,q,t1,t2),env) ⟷
is_forces_eq(nth(q,env),nth(t1,env),nth(t2,env))"
unfolding forces_eq_fm_def is_forces_eq_def is_forces_eq'_def
using assms sats_is_tuple_fm sats_frc_at_fm
by simp
lemma sats_forces_mem_fm :
assumes "p∈nat" "l∈nat" "q∈nat" "t1∈nat" "t2∈nat" "env∈list(M)"
"nth(p,env)=P" "nth(l,env)=leq"
shows "sats(M,forces_mem_fm(p,l,q,t1,t2),env) ⟷
is_forces_mem(nth(q,env),nth(t1,env),nth(t2,env))"
unfolding forces_mem_fm_def is_forces_mem_def is_forces_mem'_def
using assms sats_is_tuple_fm sats_frc_at_fm
by simp
definition
forces_neq :: "[i,i,i] ⇒ o" (‹_ forces⇩a '(_ ≠ _')› [36,1,1] 60) where
"p forces⇩a (t1 ≠ t2) ≡ ¬ (∃q∈P. q≼p ∧ q forces⇩a (t1 = t2))"
definition
forces_nmem :: "[i,i,i] ⇒ o" (‹_ forces⇩a '(_ ∉ _')› [36,1,1] 60) where
"p forces⇩a (t1 ∉ t2) ≡ ¬ (∃q∈P. q≼p ∧ q forces⇩a (t1 ∈ t2))"
lemma forces_neq :
"p forces⇩a (t1 ≠ t2) ⟷ forces_neq'(P,leq,p,t1,t2)"
unfolding forces_neq_def forces_neq'_def forces_eq_def by simp
lemma forces_nmem :
"p forces⇩a (t1 ∉ t2) ⟷ forces_nmem'(P,leq,p,t1,t2)"
unfolding forces_nmem_def forces_nmem'_def forces_mem_def by simp
abbreviation Forces :: "[i, i, i] ⇒ o" ("_ ⊩ _ _" [36,36,36] 60) where
"p ⊩ φ env ≡ M, ([p,P,leq,one] @ env) ⊨ forces(φ)"
lemma sats_forces_Member :
assumes "x∈nat" "y∈nat" "env∈list(M)"
"nth(x,env)=xx" "nth(y,env)=yy" "q∈M"
shows "q ⊩ ⋅x ∈ y⋅ env ⟷ q ∈ P ∧ is_forces_mem(q, xx, yy)"
unfolding forces_def
using assms sats_forces_mem_fm P_in_M leq_in_M one_in_M
by simp
lemma sats_forces_Equal :
assumes "x∈nat" "y∈nat" "env∈list(M)"
"nth(x,env)=xx" "nth(y,env)=yy" "q∈M"
shows "q ⊩ ⋅x = y⋅ env ⟷ q ∈ P ∧ is_forces_eq(q, xx, yy)"
unfolding forces_def
using assms sats_forces_eq_fm P_in_M leq_in_M one_in_M
by simp
lemma sats_forces_Nand :
assumes "φ∈formula" "ψ∈formula" "env∈list(M)" "p∈M"
shows "p ⊩ ⋅¬(φ ∧ ψ)⋅ env ⟷
p∈P ∧ ¬(∃q∈M. q∈P ∧ is_leq(##M,leq,q,p) ∧
(M,[q,P,leq,one]@env ⊨ forces'(φ)) ∧ (M,[q,P,leq,one]@env ⊨ forces'(ψ)))"
unfolding forces_def using sats_leq_fm assms sats_ren_forces_nand P_in_M leq_in_M one_in_M
by simp
lemma sats_forces_Neg :
assumes "φ∈formula" "env∈list(M)" "p∈M"
shows "p ⊩ ⋅¬φ⋅ env ⟷
(p∈P ∧ ¬(∃q∈M. q∈P ∧ is_leq(##M,leq,q,p) ∧
(M, [q, P, leq, one] @ env ⊨ forces'(φ))))"
unfolding Neg_def using assms sats_forces_Nand
by simp
lemma sats_forces_Forall :
assumes "φ∈formula" "env∈list(M)" "p∈M"
shows "p ⊩ (⋅∀φ⋅) env ⟷ p ∈ P ∧ (∀x∈M. M,[p,P,leq,one,x] @ env ⊨ forces'(φ))"
unfolding forces_def using assms sats_ren_forces_forall P_in_M leq_in_M one_in_M
by simp
end
subsection‹The arity of \<^term>‹forces››
lemma arity_forces_at :
assumes "x ∈ nat" "y ∈ nat"
shows "arity(forces(Member(x, y))) = (succ(x) ∪ succ(y)) #+ 4"
"arity(forces(Equal(x, y))) = (succ(x) ∪ succ(y)) #+ 4"
unfolding forces_def
using assms arity_forces_mem_fm arity_forces_eq_fm succ_Un_distrib ord_simp_union
by auto
lemma arity_forces' :
assumes "φ∈formula"
shows "arity(forces'(φ)) ≤ arity(φ) #+ 4"
using assms
proof (induct set:formula)
case (Member x y)
then
show ?case
using arity_forces_mem_fm succ_Un_distrib ord_simp_union
by simp
next
case (Equal x y)
then
show ?case
using arity_forces_eq_fm succ_Un_distrib ord_simp_union
by simp
next
case (Nand φ ψ)
let ?φ' = "ren_forces_nand(forces'(φ))"
let ?ψ' = "ren_forces_nand(forces'(ψ))"
have "arity(leq_fm(3, 0, 1)) = 4"
using arity_leq_fm succ_Un_distrib ord_simp_union
by simp
have "3 ≤ (4#+arity(φ)) ∪ (4#+arity(ψ))" (is "_ ≤ ?rhs")
using ord_simp_union by simp
from ‹φ∈_› Nand
have "pred(arity(?φ')) ≤ ?rhs" "pred(arity(?ψ')) ≤ ?rhs"
proof -
from ‹φ∈_› ‹ψ∈_›
have A:"pred(arity(?φ')) ≤ arity(forces'(φ))"
"pred(arity(?ψ')) ≤ arity(forces'(ψ))"
using pred_mono[OF _ arity_ren_forces_nand] pred_succ_eq
by simp_all
from Nand
have "3 ∪ arity(forces'(φ)) ≤ arity(φ) #+ 4"
"3 ∪ arity(forces'(ψ)) ≤ arity(ψ) #+ 4"
using Un_le by simp_all
with Nand
show "pred(arity(?φ')) ≤ ?rhs"
"pred(arity(?ψ')) ≤ ?rhs"
using le_trans[OF A(1)] le_trans[OF A(2)] le_Un_iff
by simp_all
qed
with Nand ‹_=4›
show ?case
using pred_Un_distrib Un_assoc[symmetric] succ_Un_distrib union_abs1 Un_leI3[OF ‹3 ≤ ?rhs›]
by simp
next
case (Forall φ)
let ?φ' = "ren_forces_forall(forces'(φ))"
show ?case
proof (cases "arity(φ) = 0")
case True
with Forall
show ?thesis
proof -
from Forall True
have "arity(forces'(φ)) ≤ 5"
using le_trans[of _ 4 5] by auto
with ‹φ∈_›
have "arity(?φ') ≤ 5"
using arity_ren_forces_all[OF forces'_type[OF ‹φ∈_›]] union_abs2
by auto
with Forall True
show ?thesis
using pred_mono[OF _ ‹arity(?φ') ≤ 5›]
by simp
qed
next
case False
with Forall
show ?thesis
proof -
from Forall False
have "arity(?φ') = 5 ∪ arity(forces'(φ))"
"arity(forces'(φ)) ≤ 5 #+ arity(φ)"
"4 ≤ succ(succ(succ(arity(φ))))"
using Ord_0_lt arity_ren_forces_all
le_trans[OF _ add_le_mono[of 4 5, OF _ le_refl]]
by auto
with ‹φ∈_›
have "5 ∪ arity(forces'(φ)) ≤ 5#+arity(φ)"
using ord_simp_union by auto
with ‹φ∈_› ‹arity(?φ') = 5 ∪ _›
show ?thesis
using pred_Un_distrib succ_pred_eq[OF _ ‹arity(φ)≠0›]
pred_mono[OF _ Forall(2)] Un_le[OF ‹4≤succ(_)›]
by simp
qed
qed
qed
lemma arity_forces :
assumes "φ∈formula"
shows "arity(forces(φ)) ≤ 4#+arity(φ)"
unfolding forces_def
using assms arity_forces' le_trans ord_simp_union by auto
lemma arity_forces_le :
assumes "φ∈formula" "n∈nat" "arity(φ) ≤ n"
shows "arity(forces(φ)) ≤ 4#+n"
using assms le_trans[OF _ add_le_mono[OF le_refl[of 5] ‹arity(φ)≤_›]] arity_forces
by auto
end