Theory Datatype_absolute

(*  Title:      ZF/Constructible/Datatype_absolute.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

section ‹Absoluteness Properties for Recursive Datatypes›

theory Datatype_absolute imports Eclose_Absolute begin

locale M_datatypes = M_trancl +
 assumes list_replacement1:
   "M(A) ==> iterates_replacement(M, is_list_functor(M,A), 0)"
  and list_replacement2:
   "M(A) ==> strong_replacement(M,
         λn y. nnat & is_iterates(M, is_list_functor(M,A), 0, n, y))"
  and formula_replacement1:
   "iterates_replacement(M, is_formula_functor(M), 0)"
  and formula_replacement2:
         λn y. nnat & is_iterates(M, is_formula_functor(M), 0, n, y))"
  and nth_replacement:
   "M(l) ==> iterates_replacement(M, %l t. is_tl(M,l,t), l)"

subsubsection‹Absoluteness of the List Construction›

lemma (in M_datatypes) list_replacement2':
  "M(A) ==> strong_replacement(M, λn y. nnat & y = (λX. {0} + A * X)^n (0))"
apply (insert list_replacement2 [of A])
apply (rule strong_replacement_cong [THEN iffD1])
apply (rule conj_cong [OF iff_refl iterates_abs [of "is_list_functor(M,A)"]])
apply (simp_all add: list_replacement1 relation1_def)

lemma (in M_datatypes) list_closed [intro,simp]:
     "M(A) ==> M(list(A))"
apply (insert list_replacement1)
by  (simp add: RepFun_closed2 list_eq_Union
               list_replacement2' relation1_def
               iterates_closed [of "is_list_functor(M,A)"])

text‹WARNING: use only with dest:› or with variables fixed!›
lemmas (in M_datatypes) list_into_M = transM [OF _ list_closed]

lemma (in M_datatypes) list_N_abs [simp]:
     "[|M(A); nnat; M(Z)|]
      ==> is_list_N(M,A,n,Z)  Z = list_N(A,n)"
apply (insert list_replacement1)
apply (simp add: is_list_N_def list_N_def relation1_def nat_into_M
                 iterates_abs [of "is_list_functor(M,A)" _ "λX. {0} + A*X"])

lemma (in M_datatypes) list_N_closed [intro,simp]:
     "[|M(A); nnat|] ==> M(list_N(A,n))"
apply (insert list_replacement1)
apply (simp add: is_list_N_def list_N_def relation1_def nat_into_M
                 iterates_closed [of "is_list_functor(M,A)"])

lemma (in M_datatypes) mem_list_abs [simp]:
     "M(A) ==> mem_list(M,A,l)  l  list(A)"
apply (insert list_replacement1)
apply (simp add: mem_list_def list_N_def relation1_def list_eq_Union
                 iterates_closed [of "is_list_functor(M,A)"])

lemma (in M_datatypes) list_abs [simp]:
     "[|M(A); M(Z)|] ==> is_list(M,A,Z)  Z = list(A)"
apply (simp add: is_list_def, safe)
apply (rule M_equalityI, simp_all)

subsubsection‹Absoluteness of Formulas›

lemma (in M_datatypes) formula_replacement2':
  "strong_replacement(M, λn y. nnat & y = (λX. ((nat*nat) + (nat*nat)) + (X*X + X))^n (0))"
apply (insert formula_replacement2)
apply (rule strong_replacement_cong [THEN iffD1])
apply (rule conj_cong [OF iff_refl iterates_abs [of "is_formula_functor(M)"]])
apply (simp_all add: formula_replacement1 relation1_def)

lemma (in M_datatypes) formula_closed [intro,simp]:
apply (insert formula_replacement1)
apply  (simp add: RepFun_closed2 formula_eq_Union
                  formula_replacement2' relation1_def
                  iterates_closed [of "is_formula_functor(M)"])

lemmas (in M_datatypes) formula_into_M = transM [OF _ formula_closed]

lemma (in M_datatypes) formula_N_abs [simp]:
     "[|nnat; M(Z)|]
      ==> is_formula_N(M,n,Z)  Z = formula_N(n)"
apply (insert formula_replacement1)
apply (simp add: is_formula_N_def formula_N_def relation1_def nat_into_M
                 iterates_abs [of "is_formula_functor(M)" _
                                  "λX. ((nat*nat) + (nat*nat)) + (X*X + X)"])

lemma (in M_datatypes) formula_N_closed [intro,simp]:
     "nnat ==> M(formula_N(n))"
apply (insert formula_replacement1)
apply (simp add: is_formula_N_def formula_N_def relation1_def nat_into_M
                 iterates_closed [of "is_formula_functor(M)"])

lemma (in M_datatypes) mem_formula_abs [simp]:
     "mem_formula(M,l)  l  formula"
apply (insert formula_replacement1)
apply (simp add: mem_formula_def relation1_def formula_eq_Union formula_N_def
                 iterates_closed [of "is_formula_functor(M)"])

lemma (in M_datatypes) formula_abs [simp]:
     "[|M(Z)|] ==> is_formula(M,Z)  Z = formula"
apply (simp add: is_formula_def, safe)
apply (rule M_equalityI, simp_all)

lemma (in M_datatypes) length_abs [simp]:
     "[|M(A); l  list(A); n  nat|] ==> is_length(M,A,l,n)  n = length(l)"
apply (subgoal_tac "M(l) & M(n)")
 prefer 2 apply (blast dest: transM)
apply (simp add: is_length_def)
apply (blast intro: list_imp_list_N nat_into_Ord list_N_imp_eq_length
             dest: list_N_imp_length_lt)

  is_nth :: "[i=>o,i,i,i] => o" where
    "is_nth(M,n,l,Z) ==
      X[M]. is_iterates(M, is_tl(M), l, n, X) & is_hd(M,X,Z)"

lemma (in M_datatypes) nth_abs [simp]:
     "[|M(A); n  nat; l  list(A); M(Z)|]
      ==> is_nth(M,n,l,Z)  Z = nth(n,l)"
apply (subgoal_tac "M(l)")
 prefer 2 apply (blast intro: transM)
apply (simp add: is_nth_def nth_eq_hd_iterates_tl nat_into_M
                 tl'_closed iterates_tl'_closed
                 iterates_abs [OF _ relation1_tl] nth_replacement)

lemma (in M_datatypes) depth_abs [simp]:
     "[|p  formula; n  nat|] ==> is_depth(M,p,n)  n = depth(p)"
apply (subgoal_tac "M(p) & M(n)")
 prefer 2 apply (blast dest: transM)
apply (simp add: is_depth_def)
apply (blast intro: formula_imp_formula_N nat_into_Ord formula_N_imp_eq_depth
             dest: formula_N_imp_depth_lt)

subsubsectiontermis_formula_case: relativization of termformula_case

 is_formula_case ::
    "[i=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i]=>o, i, i] => o" where
  ― ‹no constraint on non-formulas›
  "is_formula_case(M, is_a, is_b, is_c, is_d, p, z) ==
      (x[M]. y[M]. finite_ordinal(M,x)  finite_ordinal(M,y) 
                      is_Member(M,x,y,p)  is_a(x,y,z)) &
      (x[M]. y[M]. finite_ordinal(M,x)  finite_ordinal(M,y) 
                      is_Equal(M,x,y,p)  is_b(x,y,z)) &
      (x[M]. y[M]. mem_formula(M,x)  mem_formula(M,y) 
                     is_Nand(M,x,y,p)  is_c(x,y,z)) &
      (x[M]. mem_formula(M,x)  is_Forall(M,x,p)  is_d(x,z))"

lemma (in M_datatypes) formula_case_abs [simp]:
     "[| Relation2(M,nat,nat,is_a,a); Relation2(M,nat,nat,is_b,b);
         Relation2(M,formula,formula,is_c,c); Relation1(M,formula,is_d,d);
         p  formula; M(z) |]
      ==> is_formula_case(M,is_a,is_b,is_c,is_d,p,z) 
          z = formula_case(a,b,c,d,p)"
apply (simp add: formula_into_M is_formula_case_def)
apply (erule formula.cases)
   apply (simp_all add: Relation1_def Relation2_def)

lemma (in M_datatypes) formula_case_closed [intro,simp]:
  "[|p  formula;
     x[M]. y[M]. xnat  ynat  M(a(x,y));
     x[M]. y[M]. xnat  ynat  M(b(x,y));
     x[M]. y[M]. xformula  yformula  M(c(x,y));
     x[M]. xformula  M(d(x))|] ==> M(formula_case(a,b,c,d,p))"
by (erule formula.cases, simp_all)

subsubsection ‹Absoluteness for termformula_rec: Final Results›

  is_formula_rec :: "[i=>o, [i,i,i]=>o, i, i] => o" where
    ― ‹predicate to relativize the functional termformula_rec
   "is_formula_rec(M,MH,p,z)  ==
      dp[M]. i[M]. f[M]. finite_ordinal(M,dp) & is_depth(M,p,dp) &
             successor(M,dp,i) & fun_apply(M,f,p,z) & is_transrec(M,MH,i,f)"

text‹Sufficient conditions to relativize the instance of termformula_case
      in termformula_rec
lemma (in M_datatypes) Relation1_formula_rec_case:
     "[|Relation2(M, nat, nat, is_a, a);
        Relation2(M, nat, nat, is_b, b);
        Relation2 (M, formula, formula,
           is_c, λu v. c(u, v, h`succ(depth(u))`u, h`succ(depth(v))`v));
        Relation1(M, formula,
           is_d, λu. d(u, h ` succ(depth(u)) ` u));
        M(h) |]
      ==> Relation1(M, formula,
                         is_formula_case (M, is_a, is_b, is_c, is_d),
                         formula_rec_case(a, b, c, d, h))"
apply (simp (no_asm) add: formula_rec_case_def Relation1_def)
apply (simp)

text‹This locale packages the premises of the following theorems,
      which is the normal purpose of locales.  It doesn't accumulate
      constraints on the class termM, as in most of this development.›
locale Formula_Rec = M_eclose + M_datatypes +
  fixes a and is_a and b and is_b and c and is_c and d and is_d and MH
      "MH(u::i,f,z) ==
        fml[M]. is_formula(M,fml) 
         (M, fml, is_formula_case (M, is_a, is_b, is_c(f), is_d(f)), z)"

  assumes a_closed: "[|xnat; ynat|] ==> M(a(x,y))"
      and a_rel:    "Relation2(M, nat, nat, is_a, a)"
      and b_closed: "[|xnat; ynat|] ==> M(b(x,y))"
      and b_rel:    "Relation2(M, nat, nat, is_b, b)"
      and c_closed: "[|x  formula; y  formula; M(gx); M(gy)|]
                     ==> M(c(x, y, gx, gy))"
      and c_rel:
         "M(f) ==>
          Relation2 (M, formula, formula, is_c(f),
             λu v. c(u, v, f ` succ(depth(u)) ` u, f ` succ(depth(v)) ` v))"
      and d_closed: "[|x  formula; M(gx)|] ==> M(d(x, gx))"
      and d_rel:
         "M(f) ==>
          Relation1(M, formula, is_d(f), λu. d(u, f ` succ(depth(u)) ` u))"
      and fr_replace: "n  nat ==> transrec_replacement(M,MH,n)"
      and fr_lam_replace:
           "M(g) ==>
              (M, λx y. x  formula &
                  y = x, formula_rec_case(a,b,c,d,g,x))"

lemma (in Formula_Rec) formula_rec_case_closed:
    "[|M(g); p  formula|] ==> M(formula_rec_case(a, b, c, d, g, p))"
by (simp add: formula_rec_case_def a_closed b_closed c_closed d_closed)

lemma (in Formula_Rec) formula_rec_lam_closed:
    "M(g) ==> M(Lambda (formula, formula_rec_case(a,b,c,d,g)))"
by (simp add: lam_closed2 fr_lam_replace formula_rec_case_closed)

lemma (in Formula_Rec) MH_rel2:
     "relation2 (M, MH,
             λx h. Lambda (formula, formula_rec_case(a,b,c,d,h)))"
apply (simp add: relation2_def MH_def, clarify)
apply (rule lambda_abs2)
apply (rule Relation1_formula_rec_case)
apply (simp_all add: a_rel b_rel c_rel d_rel formula_rec_case_closed)

lemma (in Formula_Rec) fr_transrec_closed:
    "n  nat
     ==> M(transrec
          (n, λx h. Lambda(formula, formula_rec_case(a, b, c, d, h))))"
by (simp add: transrec_closed [OF fr_replace MH_rel2]
              nat_into_M formula_rec_lam_closed)

text‹The main two results: termformula_rec is absolute for termM.›
theorem (in Formula_Rec) formula_rec_closed:
    "p  formula ==> M(formula_rec(a,b,c,d,p))"
by (simp add: formula_rec_eq fr_transrec_closed
              transM [OF _ formula_closed])

theorem (in Formula_Rec) formula_rec_abs:
  "[| p  formula; M(z)|]
   ==> is_formula_rec(M,MH,p,z)  z = formula_rec(a,b,c,d,p)"
by (simp add: is_formula_rec_def formula_rec_eq transM [OF _ formula_closed]
              transrec_abs [OF fr_replace MH_rel2] depth_type
              fr_transrec_closed formula_rec_lam_closed eq_commute)