section‹The Forcing Theorems› theory Forcing_Theorems imports Cohen_Posets_Relative Forces_Definition Names begin context forcing_data1 begin subsection‹The forcing relation in context› lemma separation_forces : assumes fty: "φ∈formula" and far: "arity(φ)≤length(env)" and envty: "env∈list(M)" shows "separation(##M,λp. (p ⊩ φ env))" using separation_ax arity_forces far fty envty arity_forces_le transitivity[of _ ℙ] by simp lemma Collect_forces : assumes "φ∈formula" and "arity(φ)≤length(env)" and "env∈list(M)" shows "{p∈ℙ . p ⊩ φ env} ∈ M" using assms separation_forces separation_closed by simp lemma forces_mem_iff_dense_below: "p∈ℙ ⟹ p forces⇩_{a}(t1 ∈ t2) ⟷ dense_below( {q∈ℙ. ∃s. ∃r. r∈ℙ ∧ ⟨s,r⟩ ∈ t2 ∧ q≼r ∧ q forces⇩_{a}(t1 = s)} ,p)" using def_forces_mem[of p t1 t2] by blast subsection‹Kunen 2013, Lemma IV.2.37(a)› lemma strengthening_eq: assumes "p∈ℙ" "r∈ℙ" "r≼p" "p forces⇩_{a}(t1 = t2)" shows "r forces⇩_{a}(t1 = t2)" using assms def_forces_eq[of _ t1 t2] leq_transD by blast (* Long proof *) (* proof - { fix s q assume "q≼ r" "q∈ℙ" with assms have "q≼p" using leq_preord unfolding preorder_on_def trans_on_def by blast moreover note ‹q∈ℙ› assms moreover assume "s∈domain(t1) ∪ domain(t2)" ultimately have "q forces⇩_{a}( s ∈ t1) ⟷ q forces⇩_{a}( s ∈ t2)" using def_forces_eq[of p t1 t2] by simp } with ‹r∈ℙ› show ?thesis using def_forces_eq[of r t1 t2] by blast qed *) subsection‹Kunen 2013, Lemma IV.2.37(a)› lemma strengthening_mem: assumes "p∈ℙ" "r∈ℙ" "r≼p" "p forces⇩_{a}(t1 ∈ t2)" shows "r forces⇩_{a}(t1 ∈ t2)" using assms forces_mem_iff_dense_below dense_below_under by auto subsection‹Kunen 2013, Lemma IV.2.37(b)› lemma density_mem: assumes "p∈ℙ" shows "p forces⇩_{a}(t1 ∈ t2) ⟷ dense_below({q∈ℙ. q forces⇩_{a}(t1 ∈ t2)},p)" proof assume "p forces⇩_{a}(t1 ∈ t2)" with assms show "dense_below({q∈ℙ. q forces⇩_{a}(t1 ∈ t2)},p)" using forces_mem_iff_dense_below strengthening_mem[of p] ideal_dense_below by auto next assume "dense_below({q ∈ ℙ . q forces⇩_{a}( t1 ∈ t2)}, p)" with assms have "dense_below({q∈ℙ. dense_below({q'∈ℙ. ∃s r. r ∈ ℙ ∧ ⟨s,r⟩∈t2 ∧ q'≼r ∧ q' forces⇩_{a}(t1 = s)},q) },p)" using forces_mem_iff_dense_below by simp with assms show "p forces⇩_{a}(t1 ∈ t2)" using dense_below_dense_below forces_mem_iff_dense_below[of p t1 t2] by blast qed lemma aux_density_eq: assumes "dense_below( {q'∈ℙ. ∀q. q∈ℙ ∧ q≼q' ⟶ q forces⇩_{a}(s ∈ t1) ⟷ q forces⇩_{a}(s ∈ t2)} ,p)" "q forces⇩_{a}(s ∈ t1)" "q∈ℙ" "p∈ℙ" "q≼p" shows "dense_below({r∈ℙ. r forces⇩_{a}(s ∈ t2)},q)" proof fix r assume "r∈ℙ" "r≼q" moreover from this and ‹p∈ℙ› ‹q≼p› ‹q∈ℙ› have "r≼p" using leq_transD by simp moreover note ‹q forces⇩_{a}(s ∈ t1)› ‹dense_below(_,p)› ‹q∈ℙ› ultimately obtain q1 where "q1≼r" "q1∈ℙ" "q1 forces⇩_{a}(s ∈ t2)" using strengthening_mem[of q _ s t1] refl_leq leq_transD[of _ r q] by blast then show "∃d∈{r ∈ ℙ . r forces⇩_{a}( s ∈ t2)}. d ∈ ℙ ∧ d≼ r" by blast qed (* Kunen 2013, Lemma IV.2.37(b) *) lemma density_eq: assumes "p∈ℙ" shows "p forces⇩_{a}(t1 = t2) ⟷ dense_below({q∈ℙ. q forces⇩_{a}(t1 = t2)},p)" proof assume "p forces⇩_{a}(t1 = t2)" with ‹p∈ℙ› show "dense_below({q∈ℙ. q forces⇩_{a}(t1 = t2)},p)" using strengthening_eq ideal_dense_below by auto next assume "dense_below({q∈ℙ. q forces⇩_{a}(t1 = t2)},p)" { fix s q let ?D1="{q'∈ℙ. ∀s∈domain(t1) ∪ domain(t2). ∀q. q ∈ ℙ ∧ q≼q' ⟶ q forces⇩_{a}(s ∈ t1)⟷q forces⇩_{a}(s ∈ t2)}" let ?D2="{q'∈ℙ. ∀q. q∈ℙ ∧ q≼q' ⟶ q forces⇩_{a}(s ∈ t1) ⟷ q forces⇩_{a}(s ∈ t2)}" assume "s∈domain(t1) ∪ domain(t2)" then have "?D1⊆?D2" by blast with ‹dense_below(_,p)› have "dense_below({q'∈ℙ. ∀s∈domain(t1) ∪ domain(t2). ∀q. q ∈ ℙ ∧ q≼q' ⟶ q forces⇩_{a}(s ∈ t1)⟷q forces⇩_{a}(s ∈ t2)},p)" using dense_below_cong'[OF ‹p∈ℙ› def_forces_eq[of _ t1 t2]] by simp with ‹p∈ℙ› ‹?D1⊆?D2› have "dense_below({q'∈ℙ. ∀q. q∈ℙ ∧ q≼q' ⟶ q forces⇩_{a}(s ∈ t1) ⟷ q forces⇩_{a}(s ∈ t2)},p)" using dense_below_mono by simp moreover from this (* Automatic tools can't handle this symmetry in order to apply aux_density_eq below *) have "dense_below({q'∈ℙ. ∀q. q∈ℙ ∧ q≼q' ⟶ q forces⇩_{a}(s ∈ t2) ⟷ q forces⇩_{a}(s ∈ t1)},p)" by blast moreover assume "q ∈ ℙ" "q≼p" moreover note ‹p∈ℙ› ultimately (*We can omit the next step but it is slower *) have "q forces⇩_{a}(s ∈ t1) ⟹ dense_below({r∈ℙ. r forces⇩_{a}(s ∈ t2)},q)" "q forces⇩_{a}(s ∈ t2) ⟹ dense_below({r∈ℙ. r forces⇩_{a}(s ∈ t1)},q)" using aux_density_eq by simp_all then have "q forces⇩_{a}( s ∈ t1) ⟷ q forces⇩_{a}( s ∈ t2)" using density_mem[OF ‹q∈ℙ›] by blast } with ‹p∈ℙ› show "p forces⇩_{a}(t1 = t2)" using def_forces_eq by blast qed subsection‹Kunen 2013, Lemma IV.2.38› lemma not_forces_neq: assumes "p∈ℙ" shows "p forces⇩_{a}(t1 = t2) ⟷ ¬ (∃q∈ℙ. q≼p ∧ q forces⇩_{a}(t1 ≠ t2))" using assms density_eq unfolding forces_neq_def by blast lemma not_forces_nmem: assumes "p∈ℙ" shows "p forces⇩_{a}(t1 ∈ t2) ⟷ ¬ (∃q∈ℙ. q≼p ∧ q forces⇩_{a}(t1 ∉ t2))" using assms density_mem unfolding forces_nmem_def by blast subsection‹The relation of forcing and atomic formulas› lemma Forces_Equal: assumes "p∈ℙ" "t1∈M" "t2∈M" "env∈list(M)" "nth(n,env) = t1" "nth(m,env) = t2" "n∈nat" "m∈nat" shows "(p ⊩ Equal(n,m) env) ⟷ p forces⇩_{a}(t1 = t2)" using assms sats_forces_Equal forces_eq_abs transitivity by simp lemma Forces_Member: assumes "p∈ℙ" "t1∈M" "t2∈M" "env∈list(M)" "nth(n,env) = t1" "nth(m,env) = t2" "n∈nat" "m∈nat" shows "(p ⊩ Member(n,m) env) ⟷ p forces⇩_{a}(t1 ∈ t2)" using assms sats_forces_Member forces_mem_abs transitivity by simp lemma Forces_Neg: assumes "p∈ℙ" "env ∈ list(M)" "φ∈formula" shows "(p ⊩ Neg(φ) env) ⟷ ¬(∃q∈M. q∈ℙ ∧ q≼p ∧ (q ⊩ φ env))" using assms sats_forces_Neg transitivity pair_in_M_iff leq_abs by simp subsection‹The relation of forcing and connectives› lemma Forces_Nand: assumes "p∈ℙ" "env ∈ list(M)" "φ∈formula" "ψ∈formula" shows "(p ⊩ Nand(φ,ψ) env) ⟷ ¬(∃q∈M. q∈ℙ ∧ q≼p ∧ (q ⊩ φ env) ∧ (q ⊩ ψ env))" using assms sats_forces_Nand transitivity pair_in_M_iff leq_abs by simp lemma Forces_And_aux: assumes "p∈ℙ" "env ∈ list(M)" "φ∈formula" "ψ∈formula" shows "p ⊩ And(φ,ψ) env ⟷ (∀q∈M. q∈ℙ ∧ q≼p ⟶ (∃r∈M. r∈ℙ ∧ r≼q ∧ (r ⊩ φ env) ∧ (r ⊩ ψ env)))" unfolding And_def using assms Forces_Neg Forces_Nand by (auto simp only:) lemma Forces_And_iff_dense_below: assumes "p∈ℙ" "env ∈ list(M)" "φ∈formula" "ψ∈formula" shows "(p ⊩ And(φ,ψ) env) ⟷ dense_below({r∈ℙ. (r ⊩ φ env) ∧ (r ⊩ ψ env) },p)" unfolding dense_below_def using Forces_And_aux assms by (auto dest:transitivity[OF _ P_in_M]; rename_tac q; drule_tac x=q in bspec)+ lemma Forces_Forall: assumes "p∈ℙ" "env ∈ list(M)" "φ∈formula" shows "(p ⊩ Forall(φ) env) ⟷ (∀x∈M. (p ⊩ φ ([x] @ env)))" using sats_forces_Forall assms transitivity[OF _ P_in_M] by simp (* "x∈val(G,π) ⟹ ∃θ. ∃p∈G. ⟨θ,p⟩∈π ∧ val(G,θ) = x" *) bundle some_rules = elem_of_val_pair [dest] context includes some_rules begin lemma elem_of_valI: "∃θ. ∃p∈ℙ. p∈G ∧ ⟨θ,p⟩∈π ∧ val(G,θ) = x ⟹ x∈val(G,π)" by (subst def_val, auto) lemma GenExt_iff: "x∈M[G] ⟷ (∃τ∈M. x = val(G,τ))" unfolding GenExt_def by simp end end context G_generic1 begin subsection‹Kunen 2013, Lemma IV.2.29› lemma generic_inter_dense_below: assumes "D∈M" "dense_below(D,p)" "p∈G" shows "D ∩ G ≠ 0" proof - let ?D="{q∈ℙ. p⊥q ∨ q∈D}" have "dense(?D)" proof fix r assume "r∈ℙ" show "∃d∈{q ∈ ℙ . p ⊥ q ∨ q ∈ D}. d ≼ r" proof (cases "p ⊥ r") case True with ‹r∈ℙ› (* Automatic tools can't handle this case for some reason... *) show ?thesis using refl_leq[of r] by (intro bexI) (blast+) next case False then obtain s where "s∈ℙ" "s≼p" "s≼r" by blast with assms ‹r∈ℙ› show ?thesis using dense_belowD[OF assms(2), of s] leq_transD[of _ s r] by blast qed qed have "?D⊆ℙ" by auto let ?d_fm="⋅⋅¬compat_in_fm(1, 2, 3, 0) ⋅ ∨ ⋅0 ∈ 4⋅⋅" from ‹p∈G› have "p∈M" using G_subset_M subsetD by simp moreover have "?d_fm∈formula" by simp moreover have "arity(?d_fm) = 5" by (auto simp add: arity) moreover from ‹D∈M› ‹p∈M› have "(M, [q,ℙ,leq,p,D] ⊨ ?d_fm) ⟷ (¬ is_compat_in(##M,ℙ,leq,p,q) ∨ q∈D)" if "q∈M" for q using that sats_compat_in_fm zero_in_M by simp moreover from ‹p∈M› have "(¬ is_compat_in(##M,ℙ,leq,p,q) ∨ q∈D) ⟷ p⊥q ∨ q∈D" if "q∈M" for q unfolding compat_def using that compat_in_abs by simp ultimately have "?D∈M" using Collect_in_M[of ?d_fm "[ℙ,leq,p,D]"] ‹D∈M› by simp note asm = ‹dense(?D)› ‹?D⊆ℙ› ‹?D∈M› obtain x where "x∈G" "x∈?D" using M_generic_denseD[OF asm] by force (* by (erule bexE) does it, but the other automatic tools don't *) moreover from this have "x∈D" using M_generic_compatD[OF _ ‹p∈G›, of x] refl_leq compatI[of _ p x] by force ultimately show ?thesis by auto qed subsection‹Auxiliary results for Lemma IV.2.40(a)› lemma (in forcing_data1) IV240a_mem_Collect: assumes "π∈M" "τ∈M" shows "{q∈ℙ. ∃σ. ∃r. r∈ℙ ∧ ⟨σ,r⟩ ∈ τ ∧ q≼r ∧ q forces⇩_{a}(π = σ)}∈M" proof - let ?rel_pred= "λM x a1 a2 a3 a4. ∃σ[M]. ∃r[M]. ∃σr[M]. r∈a1 ∧ pair(M,σ,r,σr) ∧ σr∈a4 ∧ is_leq(M,a2,x,r) ∧ is_forces_eq'(M,a1,a2,x,a3,σ)" let ?φ="Exists(Exists(Exists(And(Member(1,4),And(pair_fm(2,1,0), And(Member(0,7),And(is_leq_fm(5,3,1),forces_eq_fm(4,5,3,6,2))))))))" have "σ∈M ∧ r∈M" if "⟨σ, r⟩ ∈ τ" for σ r using that ‹τ∈M› pair_in_M_iff transitivity[of "⟨σ,r⟩" τ] by simp then have "?rel_pred(##M,q,ℙ,leq,π,τ) ⟷ (∃σ. ∃r. r∈ℙ ∧ ⟨σ,r⟩ ∈ τ ∧ q≼r ∧ q forces⇩_{a}(π = σ))" if "q∈M" for q unfolding forces_eq_def using assms that leq_abs forces_eq'_abs pair_in_M_iff by auto moreover have "(M, [q,ℙ,leq,π,τ] ⊨ ?φ) ⟷ ?rel_pred(##M,q,ℙ,leq,π,τ)" if "q∈M" for q using assms that sats_forces_eq_fm sats_is_leq_fm zero_in_M by simp moreover have "?φ∈formula" by simp moreover have "arity(?φ)=5" using arity_forces_eq_fm by (simp add:ord_simp_union arity) ultimately show ?thesis unfolding forces_eq_def using assms Collect_in_M[of ?φ "[ℙ,leq,π,τ]"] by simp qed (* Lemma IV.2.40(a), membership *) lemma IV240a_mem: assumes "p∈G" "π∈M" "τ∈M" "p forces⇩_{a}(π ∈ τ)" "⋀q σ. q∈ℙ ⟹ q∈G ⟹ σ∈domain(τ) ⟹ q forces⇩_{a}(π = σ) ⟹ val(G,π) = val(G,σ)" (* inductive hypothesis *) shows "val(G,π)∈val(G,τ)" proof (intro elem_of_valI) let ?D="{q∈ℙ. ∃σ. ∃r. r∈ℙ ∧ ⟨σ,r⟩ ∈ τ ∧ q≼r ∧ q forces⇩_{a}(π = σ)}" from ‹p∈G› have "p∈ℙ" by blast moreover note ‹π∈M› ‹τ∈M› ultimately have "?D ∈ M" using IV240a_mem_Collect by simp moreover from assms ‹p∈ℙ› have "dense_below(?D,p)" using forces_mem_iff_dense_below by simp moreover note ‹p∈G› ultimately obtain q where "q∈G" "q∈?D" using generic_inter_dense_below[of ?D p] by blast then obtain σ r where "r∈ℙ" "⟨σ,r⟩ ∈ τ" "q≼r" "q forces⇩_{a}(π = σ)" by blast moreover from this and ‹q∈G› assms have "r ∈ G" "val(G,π) = val(G,σ)" by blast+ ultimately show "∃ σ. ∃p∈ℙ. p ∈ G ∧ ⟨σ, p⟩ ∈ τ ∧ val(G, σ) = val(G, π)" by auto qed (* Example IV.2.36 (next two lemmas) *) lemma refl_forces_eq:"p∈ℙ ⟹ p forces⇩_{a}(x = x)" using def_forces_eq by simp lemma forces_memI: "⟨σ,r⟩∈τ ⟹ p∈ℙ ⟹ r∈ℙ ⟹ p≼r ⟹ p forces⇩_{a}(σ ∈ τ)" using refl_forces_eq[of _ σ] leq_transD refl_leq by (blast intro:forces_mem_iff_dense_below[THEN iffD2]) (* Lemma IV.2.40(a), equality, first inclusion *) lemma IV240a_eq_1st_incl: includes some_rules assumes "p∈G" "p forces⇩_{a}(τ = θ)" and IH:"⋀q σ. q∈ℙ ⟹ q∈G ⟹ σ∈domain(τ) ∪ domain(θ) ⟹ (q forces⇩_{a}(σ ∈ τ) ⟶ val(G,σ) ∈ val(G,τ)) ∧ (q forces⇩_{a}(σ ∈ θ) ⟶ val(G,σ) ∈ val(G,θ))" (* Strong enough for this case: *) (* IH:"⋀q σ. q∈ℙ ⟹ σ∈domain(τ) ⟹ q forces⇩_{a}(σ ∈ θ) ⟹ val(G,σ) ∈ val(G,θ)" *) shows "val(G,τ) ⊆ val(G,θ)" proof fix x assume "x∈val(G,τ)" then obtain σ r where "⟨σ,r⟩∈τ" "r∈G" "val(G,σ)=x" by blast moreover from this and ‹p∈G› obtain q where "q∈G" "q≼p" "q≼r" by force moreover from this and ‹p∈G› have "q∈ℙ" "p∈ℙ" by blast+ moreover from calculation have "q forces⇩_{a}(σ ∈ τ)" using forces_memI by auto moreover note ‹p forces⇩_{a}(τ = θ)› ultimately have "q forces⇩_{a}(σ ∈ θ)" using def_forces_eq by auto with ‹q∈ℙ› ‹q∈G› IH[of q σ] ‹⟨σ,r⟩∈τ› ‹val(G,σ) = x› show "x∈val(G,θ)" by blast qed (* Lemma IV.2.40(a), equality, second inclusion--- COℙY-ℙASTE *) lemma IV240a_eq_2nd_incl: includes some_rules assumes "p∈G" "p forces⇩_{a}(τ = θ)" and IH:"⋀q σ. q∈ℙ ⟹ q∈G ⟹ σ∈domain(τ) ∪ domain(θ) ⟹ (q forces⇩_{a}(σ ∈ τ) ⟶ val(G,σ) ∈ val(G,τ)) ∧ (q forces⇩_{a}(σ ∈ θ) ⟶ val(G,σ) ∈ val(G,θ))" shows "val(G,θ) ⊆ val(G,τ)" proof fix x assume "x∈val(G,θ)" then obtain σ r where "⟨σ,r⟩∈θ" "r∈G" "val(G,σ)=x" by blast moreover from this and ‹p∈G› obtain q where "q∈G" "q≼p" "q≼r" by force moreover from this and ‹p∈G› have "q∈ℙ" "p∈ℙ" by blast+ moreover from calculation have "q forces⇩_{a}(σ ∈ θ)" using forces_memI by auto moreover note ‹p forces⇩_{a}(τ = θ)› ultimately have "q forces⇩_{a}(σ ∈ τ)" using def_forces_eq by auto with ‹q∈ℙ› ‹q∈G› IH[of q σ] ‹⟨σ,r⟩∈θ› ‹val(G,σ) = x› show "x∈val(G,τ)" by blast qed (* Lemma IV.2.40(a), equality, second inclusion--- COℙY-ℙASTE *) lemma IV240a_eq: includes some_rules assumes "p∈G" "p forces⇩_{a}(τ = θ)" and IH:"⋀q σ. q∈ℙ ⟹ q∈G ⟹ σ∈domain(τ) ∪ domain(θ) ⟹ (q forces⇩_{a}(σ ∈ τ) ⟶ val(G,σ) ∈ val(G,τ)) ∧ (q forces⇩_{a}(σ ∈ θ) ⟶ val(G,σ) ∈ val(G,θ))" shows "val(G,τ) = val(G,θ)" using IV240a_eq_1st_incl[OF assms] IV240a_eq_2nd_incl[OF assms] IH by blast subsection‹Induction on names› lemma (in forcing_data1) core_induction: assumes "⋀τ θ p. p ∈ ℙ ⟹ ⟦⋀q σ. ⟦q∈ℙ ; σ∈domain(θ)⟧ ⟹ Q(0,τ,σ,q)⟧ ⟹ Q(1,τ,θ,p)" "⋀τ θ p. p ∈ ℙ ⟹ ⟦⋀q σ. ⟦q∈ℙ ; σ∈domain(τ) ∪ domain(θ)⟧ ⟹ Q(1,σ,τ,q) ∧ Q(1,σ,θ,q)⟧ ⟹ Q(0,τ,θ,p)" "ft ∈ 2" "p ∈ ℙ" shows "Q(ft,τ,θ,p)" proof - { fix ft p τ θ have "Transset(eclose({τ,θ}))" (is "Transset(?e)") using Transset_eclose by simp have "τ ∈ ?e" "θ ∈ ?e" using arg_into_eclose by simp_all moreover assume "ft ∈ 2" "p ∈ ℙ" ultimately have "⟨ft,τ,θ,p⟩∈ 2×?e×?e×ℙ" (is "?a∈2×?e×?e×ℙ") by simp then have "Q(ftype(?a), name1(?a), name2(?a), cond_of(?a))" using core_induction_aux[of ?e ℙ Q ?a,OF ‹Transset(?e)› assms(1,2) ‹?a∈_›] by (clarify) (blast) then have "Q(ft,τ,θ,p)" by (simp add:components_simp) } then show ?thesis using assms by simp qed lemma (in forcing_data1) forces_induction_with_conds: assumes "⋀τ θ p. p ∈ ℙ ⟹ ⟦⋀q σ. ⟦q∈ℙ ; σ∈domain(θ)⟧ ⟹ Q(q,τ,σ)⟧ ⟹ R(p,τ,θ)" "⋀τ θ p. p ∈ ℙ ⟹ ⟦⋀q σ. ⟦q∈ℙ ; σ∈domain(τ) ∪ domain(θ)⟧ ⟹ R(q,σ,τ) ∧ R(q,σ,θ)⟧ ⟹ Q(p,τ,θ)" "p ∈ ℙ" shows "Q(p,τ,θ) ∧ R(p,τ,θ)" proof - let ?Q="λft τ θ p. (ft = 0 ⟶ Q(p,τ,θ)) ∧ (ft = 1 ⟶ R(p,τ,θ))" from assms(1) have "⋀τ θ p. p ∈ ℙ ⟹ ⟦⋀q σ. ⟦q∈ℙ ; σ∈domain(θ)⟧ ⟹ ?Q(0,τ,σ,q)⟧ ⟹ ?Q(1,τ,θ,p)" by simp moreover from assms(2) have "⋀τ θ p. p ∈ ℙ ⟹ ⟦⋀q σ. ⟦q∈ℙ ; σ∈domain(τ) ∪ domain(θ)⟧ ⟹ ?Q(1,σ,τ,q) ∧ ?Q(1,σ,θ,q)⟧ ⟹ ?Q(0,τ,θ,p)" by simp moreover note ‹p∈ℙ› ultimately have "?Q(ft,τ,θ,p)" if "ft∈2" for ft by (rule core_induction[OF _ _ that, of ?Q]) then show ?thesis by auto qed lemma (in forcing_data1) forces_induction: assumes "⋀τ θ. ⟦⋀σ. σ∈domain(θ) ⟹ Q(τ,σ)⟧ ⟹ R(τ,θ)" "⋀τ θ. ⟦⋀σ. σ∈domain(τ) ∪ domain(θ) ⟹ R(σ,τ) ∧ R(σ,θ)⟧ ⟹ Q(τ,θ)" shows "Q(τ,θ) ∧ R(τ,θ)" proof (intro forces_induction_with_conds[OF _ _ one_in_P ]) fix τ θ p assume "q ∈ ℙ ⟹ σ ∈ domain(θ) ⟹ Q(τ, σ)" for q σ with assms(1) show "R(τ,θ)" using one_in_P by simp next fix τ θ p assume "q ∈ ℙ ⟹ σ ∈ domain(τ) ∪ domain(θ) ⟹ R(σ,τ) ∧ R(σ,θ)" for q σ with assms(2) show "Q(τ,θ)" using one_in_P by simp qed subsection‹Lemma IV.2.40(a), in full› lemma IV240a: shows "(τ∈M ⟶ θ∈M ⟶ (∀p∈G. p forces⇩_{a}(τ = θ) ⟶ val(G,τ) = val(G,θ))) ∧ (τ∈M ⟶ θ∈M ⟶ (∀p∈G. p forces⇩_{a}(τ ∈ θ) ⟶ val(G,τ) ∈ val(G,θ)))" (is "?Q(τ,θ) ∧ ?R(τ,θ)") proof (intro forces_induction[of ?Q ?R] impI) fix τ θ assume "τ∈M" "θ∈M" "σ∈domain(θ) ⟹ ?Q(τ,σ)" for σ moreover from this have "σ∈domain(θ) ⟹ q forces⇩_{a}(τ = σ) ⟹ val(G, τ) = val(G, σ)" if "q∈ℙ" "q∈G" for q σ using that domain_closed[of θ] transitivity by auto ultimately show "∀p∈G. p forces⇩_{a}(τ ∈ θ) ⟶ val(G,τ) ∈ val(G,θ)" using IV240a_mem domain_closed transitivity by simp next fix τ θ assume "τ∈M" "θ∈M" and d:"σ ∈ domain(τ) ∪ domain(θ) ⟹ ?R(σ,τ) ∧ ?R(σ,θ)" for σ moreover from this have IH':"(q forces⇩_{a}(σ ∈ τ) ⟶ val(G, σ) ∈ val(G, τ)) ∧ (q forces⇩_{a}(σ ∈ θ) ⟶ val(G, σ) ∈ val(G, θ))" if "σ ∈ domain(τ) ∪ domain(θ)" "q∈G" for q σ proof - from d that have A:"?R(σ,τ)" "?R(σ,θ)" by auto from ‹τ∈_› ‹θ∈M› ‹q∈G› ‹σ∈_› show ?thesis using transitivity[of σ] domain_closed A[rule_format,of q] by auto qed show "∀p∈G. p forces⇩_{a}(τ = θ) ⟶ val(G,τ) = val(G,θ)" using IV240a_eq[OF _ _ IH'] by simp qed subsection‹Lemma IV.2.40(b)› (* Lemma IV.2.40(b), membership *) lemma IV240b_mem: includes some_rules assumes "val(G,π)∈val(G,τ)" "π∈M" "τ∈M" and IH:"⋀σ. σ∈domain(τ) ⟹ val(G,π) = val(G,σ) ⟹ ∃p∈G. p forces⇩_{a}(π = σ)" (* inductive hypothesis *) shows "∃p∈G. p forces⇩_{a}(π ∈ τ)" proof - from ‹val(G,π)∈val(G,τ)› obtain σ r where "r∈G" "⟨σ,r⟩∈τ" "val(G,π) = val(G,σ)" by auto moreover from this and IH obtain p' where "p'∈G" "p' forces⇩_{a}(π = σ)" by blast ultimately obtain p where "p≼r" "p≼p'" "p∈G" "p forces⇩_{a}(π = σ)" using M_generic_compatD strengthening_eq[of p'] M_genericD by auto moreover from calculation have "q forces⇩_{a}(π = σ)" if "q∈ℙ" "q≼p" for q using that strengthening_eq by blast moreover note ‹⟨σ,r⟩∈τ› ‹r∈G› ultimately have "r∈ℙ ∧ ⟨σ,r⟩ ∈ τ ∧ q≼r ∧ q forces⇩_{a}(π = σ)" if "q∈ℙ" "q≼p" for q using that leq_transD[of _ p r] by blast then have "dense_below({q∈ℙ. ∃s r. r∈ℙ ∧ ⟨s,r⟩ ∈ τ ∧ q≼r ∧ q forces⇩_{a}(π = s)},p)" using refl_leq by blast moreover note ‹p∈G› moreover from calculation have "p forces⇩_{a}(π ∈ τ)" using forces_mem_iff_dense_below by blast ultimately show ?thesis by blast qed end ― ‹\<^locale>‹G_generic1›› context forcing_data1 begin lemma Collect_forces_eq_in_M: assumes "τ ∈ M" "θ ∈ M" shows "{p∈ℙ. p forces⇩_{a}(τ = θ)} ∈ M" using assms Collect_in_M[of "forces_eq_fm(1,2,0,3,4)" "[ℙ,leq,τ,θ]"] arity_forces_eq_fm sats_forces_eq_fm forces_eq_abs forces_eq_fm_type by (simp add: union_abs1 Un_commute) lemma IV240b_eq_Collects: assumes "τ ∈ M" "θ ∈ M" shows "{p∈ℙ. ∃σ∈domain(τ) ∪ domain(θ). p forces⇩_{a}(σ ∈ τ) ∧ p forces⇩_{a}(σ ∉ θ)}∈M" and "{p∈ℙ. ∃σ∈domain(τ) ∪ domain(θ). p forces⇩_{a}(σ ∉ τ) ∧ p forces⇩_{a}(σ ∈ θ)}∈M" proof - let ?rel_pred="λM x a1 a2 a3 a4. ∃σ[M]. ∃u[M]. ∃da3[M]. ∃da4[M]. is_domain(M,a3,da3) ∧ is_domain(M,a4,da4) ∧ union(M,da3,da4,u) ∧ σ∈u ∧ is_forces_mem'(M,a1,a2,x,σ,a3) ∧ is_forces_nmem'(M,a1,a2,x,σ,a4)" let ?φ="Exists(Exists(Exists(Exists(And(domain_fm(7,1),And(domain_fm(8,0), And(union_fm(1,0,2),And(Member(3,2),And(forces_mem_fm(5,6,4,3,7), forces_nmem_fm(5,6,4,3,8))))))))))" have 1:"σ∈M" if "⟨σ,y⟩∈δ" "δ∈M" for σ δ y using that pair_in_M_iff transitivity[of "⟨σ,y⟩" δ] by simp have abs1:"?rel_pred(##M,p,ℙ,leq,τ,θ) ⟷ (∃σ∈domain(τ) ∪ domain(θ). forces_mem'(ℙ,leq,p,σ,τ) ∧ forces_nmem'(ℙ,leq,p,σ,θ))" if "p∈M" for p unfolding forces_mem_def forces_nmem_def using assms that forces_mem'_abs forces_nmem'_abs domain_closed Un_closed by (auto simp add:1[of _ _ τ] 1[of _ _ θ]) have abs2:"?rel_pred(##M,p,ℙ,leq,θ,τ) ⟷ (∃σ∈domain(τ) ∪ domain(θ). forces_nmem'(ℙ,leq,p,σ,τ) ∧ forces_mem'(ℙ,leq,p,σ,θ))" if "p∈M" for p unfolding forces_mem_def forces_nmem_def using assms that forces_mem'_abs forces_nmem'_abs domain_closed Un_closed by (auto simp add:1[of _ _ τ] 1[of _ _ θ]) have fsats1:"(M,[p,ℙ,leq,τ,θ] ⊨ ?φ) ⟷ ?rel_pred(##M,p,ℙ,leq,τ,θ)" if "p∈M" for p using that assms sats_forces_mem_fm sats_forces_nmem_fm zero_in_M domain_closed Un_closed by simp have fsats2:"(M,[p,ℙ,leq,θ,τ] ⊨ ?φ) ⟷ ?rel_pred(##M,p,ℙ,leq,θ,τ)" if "p∈M" for p using that assms sats_forces_mem_fm sats_forces_nmem_fm zero_in_M domain_closed Un_closed by simp have fty:"?φ∈formula" by simp have farit:"arity(?φ)=5" by (simp add:ord_simp_union arity) show "{p ∈ ℙ . ∃σ∈domain(τ) ∪ domain(θ). p forces⇩_{a}(σ ∈ τ) ∧ p forces⇩_{a}(σ ∉ θ)} ∈ M" and "{p ∈ ℙ . ∃σ∈domain(τ) ∪ domain(θ). p forces⇩_{a}(σ ∉ τ) ∧ p forces⇩_{a}(σ ∈ θ)} ∈ M" unfolding forces_mem_def using abs1 fty fsats1 farit assms forces_nmem Collect_in_M[of ?φ "[ℙ,leq,τ,θ]"] using abs2 fty fsats2 farit assms forces_nmem domain_closed Un_closed Collect_in_M[of ?φ "[ℙ,leq,θ,τ]"] by simp_all qed end ― ‹\<^locale>‹forcing_data1›› context G_generic1 begin (* Lemma IV.2.40(b), equality *) lemma IV240b_eq: includes some_rules assumes "val(G,τ) = val(G,θ)" "τ∈M" "θ∈M" and IH:"⋀σ. σ∈domain(τ)∪domain(θ) ⟹ (val(G,σ)∈val(G,τ) ⟶ (∃q∈G. q forces⇩_{a}(σ ∈ τ))) ∧ (val(G,σ)∈val(G,θ) ⟶ (∃q∈G. q forces⇩_{a}(σ ∈ θ)))" (* inductive hypothesis *) shows "∃p∈G. p forces⇩_{a}(τ = θ)" proof - let ?D1="{p∈ℙ. p forces⇩_{a}(τ = θ)}" let ?D2="{p∈ℙ. ∃σ∈domain(τ) ∪ domain(θ). p forces⇩_{a}(σ ∈ τ) ∧ p forces⇩_{a}(σ ∉ θ)}" let ?D3="{p∈ℙ. ∃σ∈domain(τ) ∪ domain(θ). p forces⇩_{a}(σ ∉ τ) ∧ p forces⇩_{a}(σ ∈ θ)}" let ?D="?D1 ∪ ?D2 ∪ ?D3" note assms moreover from this have "domain(τ) ∪ domain(θ)∈M" (is "?B∈M") using domain_closed Un_closed by auto moreover from calculation have "?D2∈M" and "?D3∈M" using IV240b_eq_Collects by simp_all ultimately have "?D∈M" using Collect_forces_eq_in_M Un_closed by auto moreover have "dense(?D)" proof fix p assume "p∈ℙ" have "∃d∈ℙ. (d forces⇩_{a}(τ = θ) ∨ (∃σ∈domain(τ) ∪ domain(θ). d forces⇩_{a}(σ ∈ τ) ∧ d forces⇩_{a}(σ ∉ θ)) ∨ (∃σ∈domain(τ) ∪ domain(θ). d forces⇩_{a}(σ ∉ τ) ∧ d forces⇩_{a}(σ ∈ θ))) ∧ d ≼ p" proof (cases "p forces⇩_{a}(τ = θ)") case True with ‹p∈ℙ› show ?thesis using refl_leq by blast next case False moreover note ‹p∈ℙ› moreover from calculation obtain σ q where "σ∈domain(τ)∪domain(θ)" "q∈ℙ" "q≼p" "(q forces⇩_{a}(σ ∈ τ) ∧ ¬ q forces⇩_{a}(σ ∈ θ)) ∨ (¬ q forces⇩_{a}(σ ∈ τ) ∧ q forces⇩_{a}(σ ∈ θ))" using def_forces_eq by blast moreover from this obtain r where "r≼q" "r∈ℙ" "(r forces⇩_{a}(σ ∈ τ) ∧ r forces⇩_{a}(σ ∉ θ)) ∨ (r forces⇩_{a}(σ ∉ τ) ∧ r forces⇩_{a}(σ ∈ θ))" using not_forces_nmem strengthening_mem by blast ultimately show ?thesis using leq_transD by blast qed then show "∃d∈?D . d ≼ p" by blast qed moreover have "?D ⊆ ℙ" by auto ultimately obtain p where "p∈G" "p∈?D" using M_generic_denseD[of ?D] by blast then consider (1) "p forces⇩_{a}(τ = θ)" | (2) "∃σ∈domain(τ) ∪ domain(θ). p forces⇩_{a}(σ ∈ τ) ∧ p forces⇩_{a}(σ ∉ θ)" | (3) "∃σ∈domain(τ) ∪ domain(θ). p forces⇩_{a}(σ ∉ τ) ∧ p forces⇩_{a}(σ ∈ θ)" by blast then show ?thesis proof (cases) case 1 with ‹p∈G› show ?thesis by blast next case 2 then obtain σ where "σ∈domain(τ) ∪ domain(θ)" "p forces⇩_{a}(σ ∈ τ)" "p forces⇩_{a}(σ ∉ θ)" by blast moreover from this and ‹p∈G› and assms have "val(G,σ)∈val(G,τ)" using IV240a[of σ τ] transitivity[OF _ domain_closed[simplified]] by force moreover note ‹val(G,τ) = _› ultimately obtain q where "q∈G" "q forces⇩_{a}(σ ∈ θ)" using IH[OF ‹σ∈_›] by auto moreover from this and ‹p∈G› obtain r where "r∈ℙ" "r≼p" "r≼q" by blast ultimately have "r forces⇩_{a}(σ ∈ θ)" using strengthening_mem by blast with ‹r≼p› ‹p forces⇩_{a}(σ ∉ θ)› ‹r∈ℙ› have "False" unfolding forces_nmem_def by blast then show ?thesis by simp next (* copy-paste from case 2 mutatis mutandis*) case 3 then obtain σ where "σ∈domain(τ) ∪ domain(θ)" "p forces⇩_{a}(σ ∈ θ)" "p forces⇩_{a}(σ ∉ τ)" by blast moreover from this and ‹p∈G› and assms have "val(G,σ)∈val(G,θ)" using IV240a[of σ θ] transitivity[OF _ domain_closed[simplified]] by force moreover note ‹val(G,τ) = _› ultimately obtain q where "q∈G" "q forces⇩_{a}(σ ∈ τ)" using IH[OF ‹σ∈_›] by auto moreover from this and ‹p∈G› obtain r where "r∈ℙ" "r≼p" "r≼q" by blast ultimately have "r forces⇩_{a}(σ ∈ τ)" using strengthening_mem by blast with ‹r≼p› ‹p forces⇩_{a}(σ ∉ τ)› ‹r∈ℙ› have "False" unfolding forces_nmem_def by blast then show ?thesis by simp qed qed (* Lemma IV.2.40(b), full *) lemma IV240b: "(τ∈M⟶θ∈M⟶val(G,τ) = val(G,θ) ⟶ (∃p∈G. p forces⇩_{a}(τ = θ))) ∧ (τ∈M⟶θ∈M⟶val(G,τ) ∈ val(G,θ) ⟶ (∃p∈G. p forces⇩_{a}(τ ∈ θ)))" (is "?Q(τ,θ) ∧ ?R(τ,θ)") proof (intro forces_induction) fix τ θ p assume "σ∈domain(θ) ⟹ ?Q(τ, σ)" for σ then show "?R(τ, θ)" using IV240b_mem domain_closed transitivity by simp next fix τ θ p assume "σ ∈ domain(τ) ∪ domain(θ) ⟹ ?R(σ,τ) ∧ ?R(σ,θ)" for σ moreover from this have IH':"τ∈M ⟹ θ∈M ⟹ σ ∈ domain(τ) ∪ domain(θ) ⟹ (val(G, σ) ∈ val(G, τ) ⟶ (∃q∈G. q forces⇩_{a}(σ ∈ τ))) ∧ (val(G, σ) ∈ val(G, θ) ⟶ (∃q∈G. q forces⇩_{a}(σ ∈ θ)))" for σ using domain_trans[OF trans_M] by blast ultimately show "?Q(τ,θ)" using IV240b_eq by auto qed lemma truth_lemma_mem: assumes "env∈list(M)" "n∈nat" "m∈nat" "n<length(env)" "m<length(env)" shows "(∃p∈G. p ⊩ Member(n,m) env) ⟷ M[G], map(val(G),env) ⊨ Member(n,m)" using assms IV240a[of "nth(n,env)" "nth(m,env)"] IV240b[of "nth(n,env)" "nth(m,env)"] M_genericD Forces_Member[of _ "nth(n,env)" "nth(m,env)" env n m] map_val_in_MG by auto lemma truth_lemma_eq: assumes "env∈list(M)" "n∈nat" "m∈nat" "n<length(env)" "m<length(env)" shows "(∃p∈G. p ⊩ Equal(n,m) env) ⟷ M[G], map(val(G),env) ⊨ Equal(n,m)" using assms IV240a(1)[of "nth(n,env)" "nth(m,env)"] IV240b(1)[of "nth(n,env)" "nth(m,env)"] M_genericD Forces_Equal[of _ "nth(n,env)" "nth(m,env)" env n m] map_val_in_MG by auto end ― ‹\<^locale>‹G_generic1›› lemma arities_at_aux: assumes "n ∈ nat" "m ∈ nat" "env ∈ list(M)" "succ(n) ∪ succ(m) ≤ length(env)" shows "n < length(env)" "m < length(env)" using assms succ_leE[OF Un_leD1, of n "succ(m)" "length(env)"] succ_leE[OF Un_leD2, of "succ(n)" m "length(env)"] by auto subsection‹The Strenghtening Lemma› context forcing_data1 begin lemma strengthening_lemma: assumes "p∈ℙ" "φ∈formula" "r∈ℙ" "r≼p" "env∈list(M)" "arity(φ)≤length(env)" shows "p ⊩ φ env ⟹ r ⊩ φ env" using assms(2-) proof (induct arbitrary:env) case (Member n m) then have "n<length(env)" "m<length(env)" using arities_at_aux by simp_all moreover assume "env∈list(M)" moreover note assms Member ultimately show ?case using Forces_Member[of _ "nth(n,env)" "nth(m,env)" env n m] strengthening_mem[of p r "nth(n,env)" "nth(m,env)"] by simp next case (Equal n m) then have "n<length(env)" "m<length(env)" using arities_at_aux by simp_all moreover assume "env∈list(M)" moreover note assms Equal ultimately show ?case using Forces_Equal[of _ "nth(n,env)" "nth(m,env)" env n m] strengthening_eq[of p r "nth(n,env)" "nth(m,env)"] by simp next case (Nand φ ψ) with assms show ?case using Forces_Nand transitivity[OF _ P_in_M] pair_in_M_iff transitivity[OF _ leq_in_M] leq_transD by auto next case (Forall φ) with assms have "p ⊩ φ ([x] @ env)" if "x∈M" for x using that Forces_Forall by simp with Forall have "r ⊩ φ ([x] @ env)" if "x∈M" for x using that pred_le2 by (simp) with assms Forall show ?case using Forces_Forall by simp qed subsection‹The Density Lemma› lemma arity_Nand_le: assumes "φ ∈ formula" "ψ ∈ formula" "arity(Nand(φ, ψ)) ≤ length(env)" "env∈list(A)" shows "arity(φ) ≤ length(env)" "arity(ψ) ≤ length(env)" using assms by (rule_tac Un_leD1, rule_tac [5] Un_leD2, auto) lemma dense_below_imp_forces: assumes "p∈ℙ" "φ∈formula" "env∈list(M)" "arity(φ)≤length(env)" shows "dense_below({q∈ℙ. (q ⊩ φ env)},p) ⟹ (p ⊩ φ env)" using assms(2-) proof (induct arbitrary:env) case (Member n m) then have "n<length(env)" "m<length(env)" using arities_at_aux by simp_all moreover assume "env∈list(M)" moreover note assms Member ultimately show ?case using Forces_Member[of _ "nth(n,env)" "nth(m,env)" env n m] density_mem[of p "nth(n,env)" "nth(m,env)"] by simp next case (Equal n m) then have "n<length(env)" "m<length(env)" using arities_at_aux by simp_all moreover assume "env∈list(M)" moreover note assms Equal ultimately show ?case using Forces_Equal[of _ "nth(n,env)" "nth(m,env)" env n m] density_eq[of p "nth(n,env)" "nth(m,env)"] by simp next case (Nand φ ψ) { fix q assume "q∈M" "q∈ℙ" "q≼ p" "q ⊩ φ env" moreover note Nand moreover from calculation obtain d where "d∈ℙ" "d ⊩ Nand(φ, ψ) env" "d≼ q" using dense_belowI by auto moreover from calculation have "¬(d⊩ ψ env)" if "d ⊩ φ env" using that Forces_Nand refl_leq transitivity[OF _ P_in_M, of d] by auto moreover note arity_Nand_le[of φ ψ] moreover from calculation have "d ⊩ φ env" using strengthening_lemma[of q φ d env] Un_leD1 by auto ultimately have "¬ (q ⊩ ψ env)" using strengthening_lemma[of q ψ d env] by auto } with ‹p∈ℙ› show ?case using Forces_Nand[symmetric, OF _ Nand(6,1,3)] by blast next case (Forall φ) have "dense_below({q∈ℙ. q ⊩ φ ([a]@env)},p)" if "a∈M" for a proof fix r assume "r∈ℙ" "r≼p" with ‹dense_below(_,p)› obtain q where "q∈ℙ" "q≼r" "q ⊩ Forall(φ) env" by blast moreover note Forall ‹a∈M› moreover from calculation have "q ⊩ φ ([a]@env)" using Forces_Forall by simp ultimately show "∃d ∈ {q∈ℙ. q ⊩ φ ([a]@env)}. d ∈ ℙ ∧ d≼r" by auto qed moreover note Forall(2)[of "Cons(_,env)"] Forall(1,3-5) ultimately have "p ⊩ φ ([a]@env)" if "a∈M" for a using that pred_le2 by simp with assms Forall show ?case using Forces_Forall by simp qed lemma density_lemma: assumes "p∈ℙ" "φ∈formula" "env∈list(M)" "arity(φ)≤length(env)" shows "p ⊩ φ env ⟷ dense_below({q∈ℙ. (q ⊩ φ env)},p)" proof assume "dense_below({q∈ℙ. (q ⊩ φ env)},p)" with assms show "(p ⊩ φ env)" using dense_below_imp_forces by simp next assume "p ⊩ φ env" with assms show "dense_below({q∈ℙ. q ⊩ φ env},p)" using strengthening_lemma refl_leq by auto qed subsection‹The Truth Lemma› lemma Forces_And: assumes "p∈ℙ" "env ∈ list(M)" "φ∈formula" "ψ∈formula" "arity(φ) ≤ length(env)" "arity(ψ) ≤ length(env)" shows "p ⊩ And(φ,ψ) env ⟷ (p ⊩ φ env) ∧ (p ⊩ ψ env)" proof assume "p ⊩ And(φ, ψ) env" with assms have "dense_below({r ∈ ℙ . (r ⊩ φ env) ∧ (r ⊩ ψ env)}, p)" using Forces_And_iff_dense_below by simp then have "dense_below({r ∈ ℙ . (r ⊩ φ env)}, p)" "dense_below({r ∈ ℙ . (r ⊩ ψ env)}, p)" by blast+ with assms show "(p ⊩ φ env) ∧ (p ⊩ ψ env)" using density_lemma[symmetric] by simp next assume "(p ⊩ φ env) ∧ (p ⊩ ψ env)" have "dense_below({r ∈ ℙ . (r ⊩ φ env) ∧ (r ⊩ ψ env)}, p)" proof (intro dense_belowI bexI conjI, assumption) fix q assume "q∈ℙ" "q≼ p" with assms ‹(p ⊩ φ env) ∧ (p ⊩ ψ env)› show "q∈{r ∈ ℙ . (r ⊩ φ env) ∧ (r ⊩ ψ env)}" "q≼ q" using strengthening_lemma refl_leq by auto qed with assms show "p ⊩ And(φ,ψ) env" using Forces_And_iff_dense_below by simp qed lemma Forces_Nand_alt: assumes "p∈ℙ" "env ∈ list(M)" "φ∈formula" "ψ∈formula" "arity(φ) ≤ length(env)" "arity(ψ) ≤ length(env)" shows "(p ⊩ Nand(φ,ψ) env) ⟷ (p ⊩ Neg(And(φ,ψ)) env)" using assms Forces_Nand Forces_And Forces_Neg by auto end context G_generic1 begin lemma truth_lemma_Neg: assumes "φ∈formula" "env∈list(M)" "arity(φ)≤length(env)" and IH: "(∃p∈G. p ⊩ φ env) ⟷ M[G], map(val(G),env) ⊨ φ" shows "(∃p∈G. p ⊩ Neg(φ) env) ⟷ M[G], map(val(G),env) ⊨ Neg(φ)" proof (intro iffI, elim bexE, rule ccontr) (* Direct implication by contradiction *) fix p assume "p∈G" "p ⊩ Neg(φ) env" "¬(M[G],map(val(G),env) ⊨ Neg(φ))" moreover note assms moreover from calculation have "M[G], map(val(G),env) ⊨ φ" "p∈ℙ" using map_val_in_MG by auto with IH obtain r where "r ⊩ φ env" "r∈G" "r∈ℙ" by blast moreover from this and ‹p∈G› obtain q where "q≼p" "q≼r" "q∈G" "q∈ℙ" "q∈M" using transitivity[OF _ P_in_M] by blast moreover from calculation have "q ⊩ φ env" using strengthening_lemma by simp with assms ‹p ⊩ _ _› ‹q≼p› ‹q∈M› ‹p∈ℙ› ‹q∈ℙ› show "False" using Forces_Neg by auto next assume "M[G], map(val(G),env) ⊨ Neg(φ)" with assms have "¬ (M[G], map(val(G),env) ⊨ φ)" using map_val_in_MG by simp let ?D="{p∈ℙ. (p ⊩ φ env) ∨ (p ⊩ Neg(φ) env)}" from assms have "?D ∈ M" using separation_disj separation_closed separation_forces by simp moreover have "?D ⊆ ℙ" by auto moreover have "dense(?D)" proof fix q assume "q∈ℙ" with assms show "∃d∈{p ∈ ℙ . (p ⊩ φ env) ∨ (p ⊩ Neg(φ) env)}. d≼ q" using refl_leq Forces_Neg by (cases "q ⊩ Neg(φ) env", auto) qed ultimately obtain p where "p∈G" "(p ⊩ φ env) ∨ (p ⊩ Neg(φ) env)" by blast then consider (1) "p ⊩ φ env" | (2) "p ⊩ Neg(φ) env" by blast then show "∃p∈G. (p ⊩ Neg(φ) env)" proof (cases) case 1 with ‹¬ (M[G],map(val(G),env) ⊨ φ)› ‹p∈G› IH show ?thesis by blast next case 2 with ‹p∈G› show ?thesis by blast qed qed lemma truth_lemma_And: assumes "env∈list(M)" "φ∈formula" "ψ∈formula" "arity(φ)≤length(env)" "arity(ψ) ≤ length(env)" and IH: "(∃p∈G. p ⊩ φ env) ⟷ M[G], map(val(G),env) ⊨ φ" "(∃p∈G. p ⊩ ψ env) ⟷ M[G], map(val(G),env) ⊨ ψ" shows "(∃p∈G. (p ⊩ And(φ,ψ) env)) ⟷ M[G] , map(val(G),env) ⊨ And(φ,ψ)" using assms map_val_in_MG Forces_And[OF M_genericD assms(1-5)] proof (intro iffI, elim bexE) fix p assume "p∈G" "p ⊩ And(φ,ψ) env" with assms show "M[G], map(val(G),env) ⊨ And(φ,ψ)" using Forces_And[of _ _ φ ψ] map_val_in_MG M_genericD by auto next assume "M[G], map(val(G),env) ⊨ And(φ,ψ)" moreover note assms moreover from calculation obtain q r where "q ⊩ φ env" "r ⊩ ψ env" "q∈G" "r∈G" "r∈ℙ" "q∈ℙ" using map_val_in_MG Forces_And[OF M_genericD assms(1-5)] M_genericD by auto moreover from calculation obtain p where "p≼q" "p≼r" "p∈G" by auto moreover from calculation have "(p ⊩ φ env) ∧ (p ⊩ ψ env)" (* can't solve as separate goals *) using strengthening_lemma[OF M_genericD] by force ultimately show "∃p∈G. (p ⊩ And(φ,ψ) env)" using Forces_And[OF M_genericD assms(1-5)] by auto qed end definition ren_truth_lemma :: "i⇒i" where "ren_truth_lemma(φ) ≡ Exists(Exists(Exists(Exists(Exists( And(Equal(0,5),And(Equal(1,8),And(Equal(2,9),And(Equal(3,10),And(Equal(4,6), iterates(λp. incr_bv(p)`5 , 6, φ)))))))))))" lemma ren_truth_lemma_type[TC] : "φ∈formula ⟹ ren_truth_lemma(φ) ∈formula" unfolding ren_truth_lemma_def by simp lemma arity_ren_truth : assumes "φ∈formula" shows "arity(ren_truth_lemma(φ)) ≤ 6 ∪ succ(arity(φ))" proof - consider (lt) "5 <arity(φ)" | (ge) "¬ 5 < arity(φ)" by auto then show ?thesis proof cases case lt consider (a) "5<arity(φ)+⇩_{ω}5" | (b) "arity(φ)+⇩_{ω}5 ≤ 5" using not_lt_iff_le ‹φ∈_› by force then show ?thesis proof cases case a with ‹φ∈_› lt have "5 < succ(arity(φ))" "5<arity(φ)+⇩_{ω}2" "5<arity(φ)+⇩_{ω}3" "5<arity(φ)+⇩_{ω}4" using succ_ltI by auto with ‹φ∈_› have c:"arity(iterates(λp. incr_bv(p)`5,5,φ)) = 5+⇩_{ω}arity(φ)" (is "arity(?φ') = _") using arity_incr_bv_lemma lt a by simp with ‹φ∈_› have "arity(incr_bv(?φ')`5) = 6+⇩_{ω}arity(φ)" using arity_incr_bv_lemma[of ?φ' 5] a by auto with ‹φ∈_› show ?thesis unfolding ren_truth_lemma_def using pred_Un_distrib union_abs1 Un_assoc[symmetric] a c union_abs2 by (simp add:arity) next case b with ‹φ∈_› lt have "5 < succ(arity(φ))" "5<arity(φ)+⇩_{ω}2" "5<arity(φ)+⇩_{ω}3" "5<arity(φ)+⇩_{ω}4" "5<arity(φ)+⇩_{ω}5" using succ_ltI by auto with ‹φ∈_› have "arity(iterates(λp. incr_bv(p)`5,6,φ)) = 6+⇩_{ω}arity(φ)" (is "arity(?φ') = _") using arity_incr_bv_lemma lt by simp with ‹φ∈_› show ?thesis unfolding ren_truth_lemma_def using pred_Un_distrib union_abs1 Un_assoc[symmetric] union_abs2 by (simp add:arity) qed next case ge with ‹φ∈_› have "arity(φ) ≤ 5" "pred^5(arity(φ)) ≤ 5" using not_lt_iff_le le_trans[OF le_pred] by auto with ‹φ∈_› have "arity(iterates(λp. incr_bv(p)`5,6,φ)) = arity(φ)" "arity(φ)≤6" "pred^5(arity(φ)) ≤ 6" using arity_incr_bv_lemma ge le_trans[OF ‹arity(φ)≤5›] le_trans[OF ‹pred^5(arity(φ))≤5›] by auto with ‹arity(φ) ≤ 5› ‹φ∈_› ‹pred^5(_) ≤ 5› show ?thesis unfolding ren_truth_lemma_def using pred_Un_distrib union_abs1 Un_assoc[symmetric] union_abs2 by (simp add:arity) qed qed lemma sats_ren_truth_lemma: "[q,b,d,a1,a2,a3] @ env ∈ list(M) ⟹ φ ∈ formula ⟹ (M, [q,b,d,a1,a2,a3] @ env ⊨ ren_truth_lemma(φ) ) ⟷ (M, [q,a1,a2,a3,b] @ env ⊨ φ)" unfolding ren_truth_lemma_def by (insert sats_incr_bv_iff [of _ _ M _ "[q,a1,a2,a3,b]"], simp) context forcing_data1 begin lemma truth_lemma' : assumes "φ∈formula" "env∈list(M)" "arity(φ) ≤ succ(length(env))" shows "separation(##M,λd. ∃b∈M. ∀q∈ℙ. q≼d ⟶ ¬(q ⊩ φ ([b]@env)))" proof - let ?rel_pred="λM x a1 a2 a3. ∃b∈M. ∀q∈M. q∈a1 ∧ is_leq(##M,a2,q,x) ⟶ ¬(M, [q,a1,a2,a3,b] @ env ⊨ forces(φ))" let ?ψ="Exists(Forall(Implies(And(Member(0,3),is_leq_fm(4,0,2)), Neg(ren_truth_lemma(forces(φ))))))" have "q∈M" if "q∈ℙ" for q using that transitivity[OF _ P_in_M] by simp then have 1:"∀q∈M. q∈ℙ ∧ R(q) ⟶ Q(q) ⟹ (∀q∈ℙ. R(q) ⟶ Q(q))" for R Q by auto then have "⟦b ∈ M; ∀q∈M. q ∈ ℙ ∧ q ≼ d ⟶ ¬(q ⊩ φ ([b]@env))⟧ ⟹ ∃c∈M. ∀q∈ℙ. q ≼ d ⟶ ¬(q ⊩ φ ([c]@env))" for b d by (rule bexI,simp_all) then have "?rel_pred(M,d,ℙ,leq,𝟭) ⟷ (∃b∈M. ∀q∈ℙ. q≼d ⟶ ¬(q ⊩ φ ([b]@env)))" if "d∈M" for d using that leq_abs assms by auto moreover have "?ψ∈formula" using assms by simp moreover have "(M, [d,ℙ,leq,𝟭]@env ⊨ ?ψ) ⟷ ?rel_pred(M,d,ℙ,leq,𝟭)" if "d∈M" for d using assms that sats_is_leq_fm sats_ren_truth_lemma zero_in_M by simp moreover have "arity(?ψ) ≤ 4+⇩_{ω}length(env)" proof - have eq:"arity(is_leq_fm(4, 0, 2)) = 5" using arity_is_leq_fm succ_Un_distrib ord_simp_union by simp with ‹φ∈_› have "arity(?ψ) = 3 ∪ (pred^2(arity(ren_truth_lemma(forces(φ)))))" using union_abs1 pred_Un_distrib by (simp add:arity) moreover have "... ≤ 3 ∪ (pred(pred(6 ∪ succ(arity(forces(φ))))))" (is "_ ≤ ?r") using ‹φ∈_› Un_le_compat[OF le_refl[of 3]] le_imp_subset arity_ren_truth[of "forces(φ)"] pred_mono by auto finally have "arity(?ψ) ≤ ?r" by simp have i:"?r ≤ 4 ∪ pred(arity(forces(φ)))" using pred_Un_distrib pred_succ_eq ‹φ∈_› Un_assoc[symmetric] union_abs1 by simp have h:"4 ∪ pred(arity(forces(φ))) ≤ 4 ∪ (4+⇩_{ω}length(env))" using ‹env∈_› add_commute ‹φ∈_› Un_le_compat[of 4 4,OF _ pred_mono[OF _ arity_forces_le[OF _ _ ‹arity(φ)≤_›]] ] ‹env∈_› by auto with ‹φ∈_› ‹env∈_› show ?thesis using le_trans[OF ‹arity(?ψ) ≤ ?r› le_trans[OF i h]] ord_simp_union by simp qed ultimately show ?thesis using assms separation_ax[of "?ψ" "[ℙ,leq,𝟭]@env"] separation_cong[of "##M" "λy. (M, [y,ℙ,leq,𝟭]@env ⊨?ψ)"] by simp qed end context G_generic1 begin lemma truth_lemma: assumes "φ∈formula" "env∈list(M)" "arity(φ)≤length(env)" shows "(∃p∈G. p ⊩ φ env) ⟷ M[G], map(val(G),env) ⊨ φ" using assms proof (induct arbitrary:env) case (Member x y) then show ?case using truth_lemma_mem[OF ‹env∈list(M)› ‹x∈nat› ‹y∈nat›] arities_at_aux by simp next case (Equal x y) then show ?case using truth_lemma_eq[OF ‹env∈list(M)› ‹x∈nat› ‹y∈nat›] arities_at_aux by simp next case (Nand φ ψ) then show ?case using truth_lemma_And truth_lemma_Neg[of "⋅φ ∧ ψ⋅"] Forces_Nand_alt M_genericD map_val_in_MG arity_Nand_le[of φ ψ] FOL_arities by auto next case (Forall φ) then show ?case proof (intro iffI) assume "∃p∈G. (p ⊩ Forall(φ) env)" then obtain p where "p∈G" "p∈M" "p∈ℙ" "p ⊩ Forall(φ) env" using transitivity[OF _ P_in_M] by auto with ‹env∈list(M)› ‹φ∈formula› have "p ⊩ φ ([x]@env)" if "x∈M" for x using that Forces_Forall by simp with ‹p∈G› ‹φ∈formula› ‹env∈_› ‹arity(Forall(φ)) ≤ length(env)› Forall(2)[of "Cons(_,env)"] show "M[G], map(val(G),env) ⊨ Forall(φ)" using pred_le2 map_val_in_MG by (auto iff:GenExt_iff) next assume "M[G], map(val(G),env) ⊨ Forall(φ)" let ?D1="{d∈ℙ. (d ⊩ Forall(φ) env)}" let ?D2="{d∈ℙ. ∃b∈M. ∀q∈ℙ. q≼d ⟶ ¬(q ⊩ φ ([b]@env))}" define D where "D ≡ ?D1 ∪ ?D2" note ‹arity(Forall(φ)) ≤ length(env)› ‹φ∈formula› ‹env∈list(M)› moreover from this have arφ:"arity(φ)≤succ(length(env))" using pred_le2 by simp moreover from calculation have "?D1∈M" using Collect_forces by simp moreover from ‹env∈list(M)› ‹φ∈formula› have "?D2∈M" using truth_lemma'[of φ] separation_closed arφ by simp ultimately have "D∈M" unfolding D_def using Un_closed by simp moreover have "D ⊆ ℙ" unfolding D_def by auto moreover have "dense(D)" proof fix p assume "p∈ℙ" show "∃d∈D. d≼ p" proof (cases "p ⊩ Forall(φ) env") case True with ‹p∈ℙ› show ?thesis unfolding D_def using refl_leq by blast next case False with Forall ‹p∈ℙ› obtain b where "b∈M" "¬(p ⊩ φ ([b]@env))" using Forces_Forall by blast moreover from this ‹p∈ℙ› Forall have "¬dense_below({q∈ℙ. q ⊩ φ ([b]@env)},p)" using density_lemma pred_le2 by auto moreover from this obtain d where "d≼p" "∀q∈ℙ. q≼d ⟶ ¬(q ⊩ φ ([b] @ env))" "d∈ℙ" by blast ultimately show ?thesis unfolding D_def by auto qed qed moreover note generic ultimately obtain d where "d ∈ D" "d ∈ G" by blast then consider (1) "d∈?D1" | (2) "d∈?D2" unfolding D_def by blast then show "∃p∈G. (p ⊩ Forall(φ) env)" proof (cases) case 1 with ‹d∈G› show ?thesis by blast next case 2 then obtain b where "b∈M" "∀q∈ℙ. q≼d ⟶¬(q ⊩ φ ([b] @ env))" by blast moreover from this(1) and ‹M[G], _ ⊨ Forall(φ)› and Forall(2)[of "Cons(b,env)"] Forall(1,3-) obtain p where "p∈G" "p∈ℙ" "p ⊩ φ ([b] @ env)" using pred_le2 map_val_in_MG M_genericD by (auto iff:GenExt_iff) moreover note ‹d∈G› ultimately obtain q where "q∈G" "q∈ℙ" "q≼d" "q≼p" using M_genericD by force moreover from this and ‹p ⊩ φ ([b] @ env)› Forall ‹b∈M› ‹p∈ℙ› have "q ⊩ φ ([b] @ env)" using pred_le2 strengthening_lemma by simp moreover note ‹∀q∈ℙ. q≼d ⟶¬(q ⊩ φ ([b] @ env))› ultimately show ?thesis by simp qed qed qed end context forcing_data1 begin subsection‹The ``Definition of forcing''› lemma definition_of_forcing: assumes "p∈ℙ" "φ∈formula" "env∈list(M)" "arity(φ)≤length(env)" shows "(p ⊩ φ env) ⟷ (∀G. M_generic(G) ∧ p∈G ⟶ M[G], map(val(G),env) ⊨ φ)" proof (intro iffI allI impI, elim conjE) fix G assume "(p ⊩ φ env)" "M_generic(G)" "p ∈ G" moreover from this interpret G_generic1 ℙ leq 𝟭 M enum G by (unfold_locales,simp) from calculation assms show "M[G], map(val(G),env) ⊨ φ" using truth_lemma[of φ] by auto next assume 1: "∀G.(M_generic(G)∧ p∈G) ⟶ M[G] , map(val(G),env) ⊨ φ" { fix r assume 2: "r∈ℙ" "r≼p" then obtain G where "r∈G" "M_generic(G)" text‹Here we're using countability (via the existence of generic filters) of \<^term>‹M› as a shortcut.› using generic_filter_existence by auto moreover from this interpret G_generic1 ℙ leq 𝟭 M enum G by (unfold_locales,simp) from calculation 2 ‹p∈ℙ› have "p∈G" using filter_leqD by auto moreover note 1 ultimately have "M[G], map(val(G),env) ⊨ φ" by simp moreover note assms moreover from calculation obtain s where "s∈G" "(s ⊩ φ env)" using truth_lemma[of φ] by blast moreover from this ‹r∈G› obtain q where "q∈G" "q≼s" "q≼r" "s∈ℙ" "q∈ℙ" by blast ultimately have "∃q∈ℙ. q≼r ∧ (q ⊩ φ env)" using strengthening_lemma[of s] by auto } then have "dense_below({q∈ℙ. (q ⊩ φ env)},p)" unfolding dense_below_def by blast with assms show "(p ⊩ φ env)" using density_lemma by blast qed lemmas definability = forces_type end ― ‹\<^locale>‹forcing_data1›› end