# 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
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]

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
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```