Theory Separation_Instances

subsectionMore Instances of Separation

theory Separation_Instances
  imports
    Interface
begin

textThe following instances are mostly the same repetitive task; and we just
copied and pasted, tweaking some lemmas if needed (for example, we might have
needed to use some closure results).

definition radd_body :: "[i,i,i]  o" where
  "radd_body(R,S)  λz. (x y. z = Inl(x), Inr(y)) 
                  (x' x. z = Inl(x'), Inl(x)  x', x  R) 
                  (y' y. z = Inr(y'), Inr(y)  y', y  S)"

relativize functional "radd_body" "radd_body_rel"
relationalize "radd_body_rel" "is_radd_body"

synthesize "is_radd_body" from_definition
arity_theorem for "is_radd_body_fm"

definition rmult_body :: "[i,i,i]  o" where
  "rmult_body(b,d)  λz. x' y' x y. z = x', y', x, y  (x', x  b 
                              x' = x  y', y  d)"

relativize functional "rmult_body" "rmult_body_rel"
relationalize "rmult_body_rel" "is_rmult_body"

synthesize "is_rmult_body" from_definition
arity_theorem for "is_rmult_body_fm"

lemma (in M_replacement) separation_well_ord_iso:
  "(M)(f)  (M)(r)  (M)(A)  separation
        (M, λx. x  A  (y[M]. p[M]. is_apply(M, f, x, y)  pair(M, y, x, p)  p  r))"
  using separation_imp separation_in lam_replacement_identity lam_replacement_constant
    lam_replacement_apply[of f] lam_replacement_product
  by simp

definition is_obase_body :: "[io,i,i,i]  o" where
  "is_obase_body(N,A,r,x)  x  A 
                  ¬ (y[N].
                         g[N].
                            ordinal(N, y) 
                            (my[N].
                                pxr[N].
                                   membership(N, y, my) 
                                   pred_set(N, A, x, r, pxr) 
                                   order_isomorphism(N, pxr, r, y, my, g)))"

synthesize "is_obase_body" from_definition
arity_theorem for "is_obase_body_fm"

definition is_obase_equals :: "[io,i,i,i]  o" where
  "is_obase_equals(N,A,r,a)  x[N].
                     g[N].
                        mx[N].
                           par[N].
                              ordinal(N, x) 
                              membership(N, x, mx) 
                              pred_set(N, A, a, r, par)  order_isomorphism(N, par, r, x, mx, g)"


synthesize "is_obase_equals" from_definition
arity_theorem for "is_obase_equals_fm"

synthesize "PiP_rel" from_definition assuming "nonempty"
arity_theorem for "PiP_rel_fm"

synthesize "injP_rel" from_definition assuming "nonempty"
arity_theorem for "injP_rel_fm"

synthesize "surjP_rel" from_definition assuming "nonempty"
arity_theorem for "surjP_rel_fm"

context M_ZF1_trans
begin

lemma radd_body_abs:
  assumes "(##M)(R)" "(##M)(S)" "(##M)(x)"
  shows "is_radd_body(##M,R,S,x)  radd_body(R,S,x)"
  using assms pair_in_M_iff Inl_in_M_iff Inr_in_M_iff
  unfolding radd_body_def is_radd_body_def
  by (auto)

lemma separation_radd_body:
 "(##M)(R)  (##M)(S)  separation
        (##M, λz. (x y. z = Inl(x), Inr(y)) 
                  (x' x. z = Inl(x'), Inl(x)  x', x  R) 
                  (y' y. z = Inr(y'), Inr(y)  y', y  S))"
  using separation_in_ctm[where φ="is_radd_body_fm(1,2,0)" and env="[R,S]"]
    is_radd_body_def arity_is_radd_body_fm ord_simp_union is_radd_body_fm_type radd_body_abs
  unfolding radd_body_def
  by simp

lemma rmult_body_abs:
  assumes "(##M)(b)" "(##M)(d)" "(##M)(x)"
  shows "is_rmult_body(##M,b,d,x)  rmult_body(b,d,x)"
  using assms pair_in_M_iff apply_closed
  unfolding rmult_body_def is_rmult_body_def
  by (auto)

lemma separation_rmult_body:
 "(##M)(b)  (##M)(d)  separation
        (##M, λz. x' y' x y. z = x', y', x, y  (x', x  b  x' = x  y', y  d))"
  using separation_in_ctm[where φ="is_rmult_body_fm(1,2,0)" and env="[b,d]"]
    is_rmult_body_def arity_is_rmult_body_fm ord_simp_union is_rmult_body_fm_type rmult_body_abs
  unfolding rmult_body_def
  by simp

lemma separation_is_obase:
 "(##M)(f)  (##M)(r)  (##M)(A)  separation
        (##M, λx. x  A 
                  ¬ (y[##M].
                         g[##M].
                            ordinal(##M, y) 
                            (my[##M].
                                pxr[##M].
                                   membership(##M, y, my) 
                                   pred_set(##M, A, x, r, pxr) 
                                   order_isomorphism(##M, pxr, r, y, my, g))))"
  using separation_in_ctm[where φ="is_obase_body_fm(1,2,0)" and env="[A,r]"]
    is_obase_body_def arity_is_obase_body_fm ord_simp_union is_obase_body_fm_type
  by simp

lemma separation_obase_equals:
 "(##M)(f)  (##M)(r)  (##M)(A)  separation
        (##M, λa. x[##M].
                     g[##M].
                        mx[##M].
                           par[##M].
                              ordinal(##M, x) 
                              membership(##M, x, mx) 
                              pred_set(##M, A, a, r, par)  order_isomorphism(##M, par, r, x, mx, g))"
  using separation_in_ctm[where φ="is_obase_equals_fm(1,2,0)" and env="[A,r]"]
    is_obase_equals_def arity_is_obase_equals_fm ord_simp_union is_obase_equals_fm_type
  by simp

lemma separation_PiP_rel:
 "(##M)(A)  separation(##M, PiP_rel(##M,A))"
  using separation_in_ctm[where env="[A]" and φ="PiP_rel_fm(1,0)"]
    nonempty PiP_rel_iff_sats[symmetric] arity_PiP_rel_fm PiP_rel_fm_type
  by(simp_all add: ord_simp_union)

lemma separation_injP_rel:
 "(##M)(A)  separation(##M, injP_rel(##M,A))"
  using separation_in_ctm[where env="[A]" and φ="injP_rel_fm(1,0)"]
    nonempty injP_rel_iff_sats[symmetric] arity_injP_rel_fm injP_rel_fm_type
  by(simp_all add: ord_simp_union)

lemma separation_surjP_rel:
 "(##M)(A)  (##M)(B)  separation(##M, surjP_rel(##M,A,B))"
  using separation_in_ctm[where env="[A,B]" and φ="surjP_rel_fm(1,2,0)"]
    nonempty surjP_rel_iff_sats[symmetric] arity_surjP_rel_fm surjP_rel_fm_type
  by(simp_all add: ord_simp_union)

lemma separation_is_function:
 "separation(##M, is_function(##M))"
  using separation_in_ctm[where env="[]" and φ="function_fm(0)"] arity_function_fm
  by simp

end ― ‹localeM_ZF1_trans

(* Instances in M_replacement*)

definition fstsnd_in_sndsnd :: "[i]  o" where
  "fstsnd_in_sndsnd  λx. fst(snd(x))  snd(snd(x))"
relativize "fstsnd_in_sndsnd" "is_fstsnd_in_sndsnd"
synthesize "is_fstsnd_in_sndsnd" from_definition assuming "nonempty"
arity_theorem for "is_fstsnd_in_sndsnd_fm"

definition sndfst_eq_fstsnd :: "[i]  o" where
  "sndfst_eq_fstsnd  λx. snd(fst(x)) = fst(snd(x))"
relativize "sndfst_eq_fstsnd" "is_sndfst_eq_fstsnd"
synthesize "is_sndfst_eq_fstsnd" from_definition assuming "nonempty"
arity_theorem for "is_sndfst_eq_fstsnd_fm"

context M_ZF1_trans
begin

lemma fstsnd_in_sndsnd_abs:
  assumes "(##M)(x)"
  shows "is_fstsnd_in_sndsnd(##M,x)  fstsnd_in_sndsnd(x)"
  using assms pair_in_M_iff fst_abs snd_abs fst_snd_closed
  unfolding fstsnd_in_sndsnd_def is_fstsnd_in_sndsnd_def
  by auto

lemma separation_fstsnd_in_sndsnd:
 "separation(##M, λx. fst(snd(x))  snd(snd(x)))"
  using separation_in_ctm[where env="[]" and φ="is_fstsnd_in_sndsnd_fm(0)" and Q=fstsnd_in_sndsnd]
    nonempty fstsnd_in_sndsnd_abs arity_is_fstsnd_in_sndsnd_fm
  unfolding fstsnd_in_sndsnd_def
  by simp

lemma sndfst_eq_fstsnd_abs:
  assumes "(##M)(x)"
  shows "is_sndfst_eq_fstsnd(##M,x)  sndfst_eq_fstsnd(x)"
  using assms pair_in_M_iff fst_abs snd_abs fst_snd_closed
  unfolding sndfst_eq_fstsnd_def is_sndfst_eq_fstsnd_def
  by auto

lemma separation_sndfst_eq_fstsnd:
 "separation(##M, λx. snd(fst(x)) = fst(snd(x)))"
  using separation_in_ctm[where env="[]" and φ="is_sndfst_eq_fstsnd_fm(0)" and Q=sndfst_eq_fstsnd]
    nonempty sndfst_eq_fstsnd_abs arity_is_sndfst_eq_fstsnd_fm
  unfolding sndfst_eq_fstsnd_def
  by simp

end  ― ‹localeM_ZF1_trans

end