Theory Forcing_Theorems

theory Forcing_Theorems imports Interface Names begin
   
(* Prototyping Forcing relation and theorems as a locale*)
locale forcing_thms = forcing_data +
  fixes forces :: "i ⇒ i"
  assumes definition_of_forces: "p∈P ⟹ φ∈formula ⟹ env∈list(M) ⟹
                  sats(M,forces(φ), [P,leq,one,p] @ env) ⟷
                  (∀G.(M_generic(G)∧ p∈G)⟶sats(M[G],φ,map(val(G),env)))"
      and  definability[TC]: "φ∈formula ⟹ forces(φ) ∈ formula"
      and  arity_forces:     "φ∈formula ⟹ arity(forces(φ)) = arity(φ) #+ 4"
      and   truth_lemma:     "φ∈formula ⟹ env∈list(M) ⟹ M_generic(G) ⟹
                  (∃p∈G.(sats(M,forces(φ), [P,leq,one,p] @ env))) ⟷
                  sats(M[G],φ,map(val(G),env))"
      and  strengthening:     "p∈P ⟹ φ∈formula ⟹ env∈list(M) ⟹ q∈P ⟹ <q,p>∈leq ⟹
                               sats(M,forces(φ), [P,leq,one,p] @ env) ⟹
                               sats(M,forces(φ), [P,leq,one,q] @ env)"
      and density_lemma:     "p∈P ⟹ φ∈formula ⟹ env∈list(M) ⟹
                    sats(M,forces(φ), [P,leq,one,p] @ env) ⟷ 
                    dense_below({q∈P. sats(M,forces(φ), [P,leq,one,q] @ env)},p)"

begin (******************** CONTEXT: forcing_thms ******** *)
end (* forcing_thms *)
  
locale G_generic = forcing_thms + 
  fixes G :: "i"
  assumes generic : "M_generic(G)" 
begin

lemma zero_in_MG : 
  "0 ∈ M[G]" 
proof -
  from zero_in_M and elem_of_val have 
    "0 = val(G,0)" 
    by auto
  also from GenExtI and zero_in_M have 
    "... ∈ M[G]" 
  by simp
  finally show ?thesis .
qed 

lemma G_nonempty: "G≠0"
proof -
  have "P⊆P" ..
  with P_in_M P_dense ‹P⊆P› show
    "G ≠ 0"
    using generic unfolding M_generic_def by auto
qed

end    (* context: G_generic *)

end