src/ZF/Constructible/Datatype_absolute.thy
changeset 13423 7ec771711c09
parent 13422 af9bc8d87a75
child 13428 99e52e78eb65
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Thu Jul 25 10:56:35 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Thu Jul 25 18:29:04 2002 +0200
     1.3 @@ -400,6 +400,9 @@
     1.4                 list_replacement2' relativize1_def
     1.5                 iterates_closed [of "is_list_functor(M,A)"])
     1.6  
     1.7 +text{*WARNING: use only with @{text "dest:"} or with variables fixed!*}
     1.8 +lemmas (in M_datatypes) list_into_M = transM [OF _ list_closed]
     1.9 +
    1.10  lemma (in M_datatypes) list_N_abs [simp]:
    1.11       "[|M(A); n\<in>nat; M(Z)|] 
    1.12        ==> is_list_N(M,A,n,Z) <-> Z = list_N(A,n)"
    1.13 @@ -446,6 +449,8 @@
    1.14                    iterates_closed [of "is_formula_functor(M)"])
    1.15  done
    1.16  
    1.17 +lemmas (in M_datatypes) formula_into_M = transM [OF _ formula_closed]
    1.18 +
    1.19  lemma (in M_datatypes) is_formula_n_abs [simp]:
    1.20       "[|n\<in>nat; M(Z)|] 
    1.21        ==> is_formula_n(M,n,Z) <-> 
    1.22 @@ -718,6 +723,32 @@
    1.23  
    1.24  subsection {*Absoluteness for @{term formula_rec}*}
    1.25  
    1.26 +subsubsection{*@{term is_formula_case}: relativization of @{term formula_case}*}
    1.27 +
    1.28 +constdefs
    1.29 +
    1.30 + is_formula_case :: 
    1.31 +    "[i=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i]=>o, i, i] => o"
    1.32 +  --{*no constraint on non-formulas*}
    1.33 +  "is_formula_case(M, is_a, is_b, is_c, is_d, p, z) == 
    1.34 +      (\<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> is_Member(M,x,y,p) --> is_a(x,y,z)) &
    1.35 +      (\<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> is_Equal(M,x,y,p) --> is_b(x,y,z)) &
    1.36 +      (\<forall>x[M]. \<forall>y[M]. x\<in>formula --> y\<in>formula --> 
    1.37 +                     is_Nand(M,x,y,p) --> is_c(x,y,z)) &
    1.38 +      (\<forall>x[M]. x\<in>formula --> is_Forall(M,x,p) --> is_d(x,z))"
    1.39 +
    1.40 +lemma (in M_datatypes) formula_case_abs [simp]: 
    1.41 +     "[| Relativize2(M,nat,nat,is_a,a); Relativize2(M,nat,nat,is_b,b); 
    1.42 +         Relativize2(M,formula,formula,is_c,c); Relativize1(M,formula,is_d,d); 
    1.43 +         p \<in> formula; M(z) |] 
    1.44 +      ==> is_formula_case(M,is_a,is_b,is_c,is_d,p,z) <-> 
    1.45 +          z = formula_case(a,b,c,d,p)"
    1.46 +apply (simp add: formula_into_M is_formula_case_def)
    1.47 +apply (erule formula.cases) 
    1.48 +   apply (simp_all add: Relativize1_def Relativize2_def) 
    1.49 +done
    1.50 +
    1.51 +
    1.52  subsubsection{*@{term quasiformula}: For Case-Splitting with @{term formula_case'}*}
    1.53  
    1.54  constdefs
    1.55 @@ -762,10 +793,10 @@
    1.56      "formula_case'(a,b,c,d,p) == 
    1.57         if quasiformula(p) then formula_case(a,b,c,d,p) else 0"  
    1.58  
    1.59 -  is_formula_case :: 
    1.60 +  is_formula_case' :: 
    1.61        "[i=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i]=>o, i, i] => o"
    1.62      --{*Returns 0 for non-formulas*}
    1.63 -    "is_formula_case(M, is_a, is_b, is_c, is_d, p, z) == 
    1.64 +    "is_formula_case'(M, is_a, is_b, is_c, is_d, p, z) == 
    1.65  	(\<forall>x[M]. \<forall>y[M]. is_Member(M,x,y,p) --> is_a(x,y,z)) &
    1.66  	(\<forall>x[M]. \<forall>y[M]. is_Equal(M,x,y,p) --> is_b(x,y,z)) &
    1.67  	(\<forall>x[M]. \<forall>y[M]. is_Nand(M,x,y,p) --> is_c(x,y,z)) &
    1.68 @@ -818,16 +849,16 @@
    1.69       \<forall>x[M]. x\<in>formula --> M(d(x))|] ==> M(formula_case(a,b,c,d,p))"
    1.70  by (erule formula.cases, simp_all) 
    1.71  
    1.72 -lemma (in M_triv_axioms) formula_case_abs [simp]: 
    1.73 +lemma (in M_triv_axioms) formula_case'_abs [simp]: 
    1.74       "[| relativize2(M,is_a,a); relativize2(M,is_b,b); 
    1.75           relativize2(M,is_c,c); relativize1(M,is_d,d); M(p); M(z) |] 
    1.76 -      ==> is_formula_case(M,is_a,is_b,is_c,is_d,p,z) <-> 
    1.77 +      ==> is_formula_case'(M,is_a,is_b,is_c,is_d,p,z) <-> 
    1.78            z = formula_case'(a,b,c,d,p)"
    1.79  apply (case_tac "quasiformula(p)") 
    1.80   prefer 2 
    1.81 - apply (simp add: is_formula_case_def non_formula_case) 
    1.82 + apply (simp add: is_formula_case'_def non_formula_case) 
    1.83   apply (force simp add: quasiformula_def) 
    1.84 -apply (simp add: quasiformula_def is_formula_case_def)
    1.85 +apply (simp add: quasiformula_def is_formula_case'_def)
    1.86  apply (elim disjE exE) 
    1.87   apply (simp_all add: relativize1_def relativize2_def) 
    1.88  done