Theory Demonstrations

sectionSome demonstrations

theory Demonstrations
  imports
    Definitions_Main
begin

textThe 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 theoryIndependence_CH.Definitions_Main


textThe 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 t1 t2
  assumes
    ts_in_nat[simp]: "t1ω" "t2ω"
    and
    power_infty: "power_ax(M)" "M(ω)"
begin

textThe 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 termstrong_replacement), “lambda-replacements”
using a higher order function, replacements  to perform
transfinite and general well-founded recursion (using termtransrec_replacement and
termwfrec_replacement respectively) and for the construction of fixpoints
(using termiterates_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(t1t2) = (0  1  forces_mem_fm(1, 2, 0, t1+ω4, t2+ω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, t1+ω4, t1+ω4)
   = forces_mem_fm(1, 2, 0, succ(succ(succ(succ(t1)))), succ(succ(succ(succ(t2)))))
   = … *)

definition forces_0_mem_1 where "forces_0_mem_1forces_mem_fm(1,2,0,t1+ω4,t2+ω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 termforces depend on
the recursive function termincr_bv. Here we have an apparently
exponential bottleneck, since all the propositional connectives (even termNeg)
duplicate the appearances of termincr_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 ― ‹localeDemo


end