Theory Demonstrations

section‹Some demonstrations›

theory Demonstrations
  imports
    Definitions_Main
begin

text‹The following theory is only intended to explore some details of the
formalization and to show the appearance of relevant internalized formulas.
It is ❙‹not› intended as the entry point of the session. For that purpose,
consult \<^theory>‹Independence_CH.Definitions_Main››


text‹The snippet (by M. Pagano) commented out below outputs a directed
graph picturing the locale structure.›
― ‹
ML‹Locale.pretty_locale_deps @{theory} |>
map (fn n => let val nom = #name n
    in  map (writeln o (fn p => "\"" ^ p ^ "\" -> \"" ^ nom ^ "\";")) (#parents n)
end)
›
›

locale Demo = M_trivial + M_AC +
  fixes t⇩1 t⇩2
  assumes
    ts_in_nat[simp]: "t⇩1∈ω" "t⇩2∈ω"
    and
    power_infty: "power_ax(M)" "M(ω)"
begin

text‹The next fake lemma is intended to explore the instances of the axiom
schemes that are needed to build our forcing models. They are categorized as
plain replacements (using \<^term>‹strong_replacement›), “lambda-replacements”
using a higher order function, replacements  to perform
transfinite and general well-founded recursion (using \<^term>‹transrec_replacement› and
\<^term>‹wfrec_replacement› respectively) and for the construction of fixpoints
(using \<^term>‹iterates_replacement›). Lastly, separations instances.›

lemma
  assumes
    sorried_replacements:
    "⋀P. strong_replacement(M,P)"
    "⋀F. lam_replacement(M,F)"
    "⋀Q S. iterates_replacement(M,Q,S)"
    "⋀Q S. wfrec_replacement(M,Q,S)"
    "⋀Q S. transrec_replacement(M,Q,S)"
    and
    sorried_separations: "⋀Q. separation(M,Q)"
  shows
    "M_master(M)"
  apply unfold_locales
                      apply
    (simp_all add:
      sorried_replacements(1-2)
      sorried_separations
      power_infty)
  oops

― ‹NOTE: Only for pretty-printing purposes, overrides previous
  fundamental notations›
no_notation mem (infixl ‹∈› 50)
no_notation conj  (infixr ‹∧› 35)
no_notation disj (infixr ‹∨› 30)
no_notation iff (infixr ‹⟷› 25)
no_notation imp (infixr ‹⟶› 25)
no_notation not (‹¬ _› [40] 40)
no_notation All (‹'(∀_')›)
no_notation Ex (‹'(∃_')›)

no_notation Member (‹⋅_ ∈/ _⋅›)
no_notation Equal (‹⋅_ =/ _⋅›)
no_notation Nand (‹⋅¬'(_ ∧/ _')⋅›)
no_notation And (‹⋅_ ∧/ _⋅›)
no_notation Or (‹⋅_ ∨/ _⋅›)
no_notation Iff (‹⋅_ ↔/ _⋅›)
no_notation Implies (‹⋅_ →/ _⋅›)
no_notation Neg (‹⋅¬_⋅›)
no_notation Forall (‹'(⋅∀(/_)⋅')›)
no_notation Exists (‹'(⋅∃(/_)⋅')›)

notation Member (infixl ‹∈› 50)
notation Equal (infixl ‹≡› 50)
notation Nand (‹¬'(_ ∧/ _')›)
notation And  (infixr ‹∧› 35)
notation Or (infixr ‹∨› 30)
notation Iff (infixr ‹⟷› 25)
notation Implies (infixr ‹⟶› 25)
notation Neg (‹¬ _› [40] 40)
notation Forall (‹'(∀_')›)
notation Exists (‹'(∃_')›)

lemma "forces(t⇩1∈t⇩2) = (0 ∈ 1 ∧ forces_mem_fm(1, 2, 0, t⇩1+⇩ω4, t⇩2+⇩ω4))"
  unfolding forces_def by simp

(*
― ‹Prefix abbreviated notation›
notation Member (‹M›)
notation Equal (‹Eq›)
notation Nand (‹Na›)
notation And  (‹A›)
notation Or (‹O›)
notation Iff (‹If›)
notation Implies (‹Im›)
notation Neg (‹Ne›)
notation Forall (‹Fo›)
notation Exists (‹Ex›)
*)

(* forces_mem_fm(1, 2, 0, t⇩1+⇩ω4, t⇩1+⇩ω4)
   = forces_mem_fm(1, 2, 0, succ(succ(succ(succ(t⇩1)))), succ(succ(succ(succ(t⇩2)))))
   = … *)

definition forces_0_mem_1 where "forces_0_mem_1≡forces_mem_fm(1,2,0,t⇩1+⇩ω4,t⇩2+⇩ω4)"
thm forces_0_mem_1_def[
    unfolded frc_at_fm_def ftype_fm_def
    name1_fm_def name2_fm_def snd_snd_fm_def hcomp_fm_def
    ecloseN_fm_def eclose_n1_fm_def eclose_n2_fm_def
    is_eclose_fm_def mem_eclose_fm_def eclose_n_fm_def
    is_If_fm_def least_fm_def Replace_fm_def Collect_fm_def
    fm_definitions,simplified]
  (* NOTE: in view of the above, @{thm [source] fm_definitions} might be incomplete *)

named_theorems incr_bv_new_simps

schematic_goal incr_bv_Neg(* [incr_bv_new_simps] *):
  "mem(n,ω) ⟹ mem(φ,formula) ⟹ incr_bv(Neg(φ))`n = ?x"
  unfolding Neg_def by simp

schematic_goal incr_bv_Exists [incr_bv_new_simps]:
  "mem(n,ω) ⟹ mem(φ,formula) ⟹ incr_bv(Exists(φ))`n = ?x"
  unfolding Exists_def by (simp add: incr_bv_Neg)
(*
schematic_goal incr_bv_And [incr_bv_new_simps]:
  "mem(n,ω) ⟹ mem(φ,formula) ⟹mem(ψ,formula)⟹ incr_bv(And(φ,ψ))`n = ?x"
  unfolding And_def by (simp add: incr_bv_Neg)

schematic_goal incr_bv_Or [incr_bv_new_simps]:
  "mem(n,ω) ⟹ mem(φ,formula) ⟹mem(ψ,formula)⟹ incr_bv(Or(φ,ψ))`n = ?x"
  unfolding Or_def by (simp add: incr_bv_Neg)

schematic_goal incr_bv_Implies [incr_bv_new_simps]:
  "mem(n,ω) ⟹ mem(φ,formula) ⟹mem(ψ,formula)⟹ incr_bv(Implies(φ,ψ))`n = ?x"
  unfolding Implies_def by (simp add: incr_bv_Neg)
*)

― ‹The two renamings involved in the definition of \<^term>‹forces› depend on
the recursive function \<^term>‹incr_bv›. Here we have an apparently
exponential bottleneck, since all the propositional connectives (even \<^term>‹Neg›)
duplicate the appearances of \<^term>‹incr_bv›.

Not even the double negation of an atomic formula can be managed by the
system (in version 2021-1).›
(* 

schematic_goal "forces(¬¬0∈1) = ?x"
  unfolding forces_def Neg_def
   by (simp add:ren_forces_nand_def ren_forces_forall_def 
      frc_at_fm_def ftype_fm_def
      name1_fm_def name2_fm_def snd_snd_fm_def hcomp_fm_def
      ecloseN_fm_def eclose_n1_fm_def eclose_n2_fm_def
      is_eclose_fm_def mem_eclose_fm_def eclose_n_fm_def
      is_If_fm_def least_fm_def Collect_fm_def
      fm_definitions incr_bv_Neg incr_bv_Exists)
(* exception Size raised (line 183 of "./basis/LibrarySupport.sml") *)

*)

(*
declare is_ContHyp_fm_def[fm_definitions del]

thm is_ContHyp_fm_def[unfolded is_eclose_fm_def mem_eclose_fm_def eclose_n_fm_def
   is_If_fm_def least_fm_def Replace_fm_def Collect_fm_def
   fm_definitions, simplified] *)

end ― ‹\<^locale>‹Demo››


end