separate "axioms" proofs: more flexible for locale reasoning

--- a/src/ZF/Constructible/Rec_Separation.thy	Wed Jul 31 14:39:47 2002 +0200
+++ b/src/ZF/Constructible/Rec_Separation.thy	Wed Jul 31 14:40:40 2002 +0200
@@ -1,3 +1,10 @@
+(*  Title:      ZF/Constructible/Rec_Separation.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   2002  University of Cambridge
+
+FIXME: define nth_fm and prove its "sats" theorem
+*)
 
 header {*Separation for Facts About Recursion*}
 
@@ -199,14 +206,15 @@
 
 subsubsection{*Instantiating the locale @{text M_trancl}*}
 
-theorem M_trancl_L: "PROP M_trancl(L)"
-  apply (rule M_trancl.intro)
-    apply (rule M_axioms.axioms [OF M_axioms_L])+
+lemma M_trancl_axioms_L: "M_trancl_axioms(L)"
   apply (rule M_trancl_axioms.intro)
-   apply (assumption | rule
-     rtrancl_separation wellfounded_trancl_separation)+
+   apply (assumption | rule rtrancl_separation wellfounded_trancl_separation)+
   done
 
+theorem M_trancl_L: "PROP M_trancl(L)"
+by (rule M_trancl.intro
+         [OF M_triv_axioms_L M_axioms_axioms_L M_trancl_axioms_L])
+
 lemmas iterates_abs = M_trancl.iterates_abs [OF M_trancl_L]
   and rtran_closure_rtrancl = M_trancl.rtran_closure_rtrancl [OF M_trancl_L]
   and rtrancl_closed = M_trancl.rtrancl_closed [OF M_trancl_L]
@@ -298,12 +306,15 @@
 (*FIXME: surely proof can be improved?*)
 
 
+text{*The additional variable in the premise, namely @{term f'}, is essential.
+It lets @{term MH} depend upon @{term x}, which seems often necessary.
+The same thing occurs in @{text is_wfrec_reflection}.*}
 theorem is_recfun_reflection:
   assumes MH_reflection:
-    "!!f g h. REFLECTS[\<lambda>x. MH(L, f(x), g(x), h(x)),
-                     \<lambda>i x. MH(**Lset(i), f(x), g(x), h(x))]"
-  shows "REFLECTS[\<lambda>x. M_is_recfun(L, MH(L), f(x), g(x), h(x)),
-               \<lambda>i x. M_is_recfun(**Lset(i), MH(**Lset(i)), f(x), g(x), h(x))]"
+    "!!f' f g h. REFLECTS[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)), 
+                     \<lambda>i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]"
+  shows "REFLECTS[\<lambda>x. M_is_recfun(L, MH(L,x), f(x), g(x), h(x)), 
+             \<lambda>i x. M_is_recfun(**Lset(i), MH(**Lset(i),x), f(x), g(x), h(x))]"
 apply (simp (no_asm_use) only: M_is_recfun_def setclass_simps)
 apply (intro FOL_reflections function_reflections
              restriction_reflection MH_reflection)
@@ -311,13 +322,13 @@
 
 text{*Currently, @{text sats}-theorems for higher-order operators don't seem
 useful.  Reflection theorems do work, though.  This one avoids the repetition
-of the @{text MH}-term.*}
+of the @{text MH}-term. *}
 theorem is_wfrec_reflection:
   assumes MH_reflection:
-    "!!f g h. REFLECTS[\<lambda>x. MH(L, f(x), g(x), h(x)),
-                     \<lambda>i x. MH(**Lset(i), f(x), g(x), h(x))]"
-  shows "REFLECTS[\<lambda>x. is_wfrec(L, MH(L), f(x), g(x), h(x)),
-               \<lambda>i x. is_wfrec(**Lset(i), MH(**Lset(i)), f(x), g(x), h(x))]"
+    "!!f' f g h. REFLECTS[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)), 
+                     \<lambda>i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]"
+  shows "REFLECTS[\<lambda>x. is_wfrec(L, MH(L,x), f(x), g(x), h(x)), 
+               \<lambda>i x. is_wfrec(**Lset(i), MH(**Lset(i),x), f(x), g(x), h(x))]"
 apply (simp (no_asm_use) only: is_wfrec_def setclass_simps)
 apply (intro FOL_reflections MH_reflection is_recfun_reflection)
 done
@@ -435,12 +446,16 @@
 
 subsubsection{*Instantiating the locale @{text M_wfrank}*}
 
+lemma M_wfrank_axioms_L: "M_wfrank_axioms(L)"
+  apply (rule M_wfrank_axioms.intro)
+   apply (assumption | rule
+     wfrank_separation wfrank_strong_replacement Ord_wfrank_separation)+
+  done
+
 theorem M_wfrank_L: "PROP M_wfrank(L)"
   apply (rule M_wfrank.intro)
      apply (rule M_trancl.axioms [OF M_trancl_L])+
-  apply (rule M_wfrank_axioms.intro)
-   apply (assumption | rule
-     wfrank_separation wfrank_strong_replacement Ord_wfrank_separation)+
+  apply (rule M_wfrank_axioms_L) 
   done
 
 lemmas iterates_closed = M_wfrank.iterates_closed [OF M_wfrank_L]
@@ -1123,6 +1138,42 @@
 subsection{*Absoluteness for the Function @{term nth}*}
 
 
+subsubsection{*The Formula @{term is_hd}, Internalized*}
+
+(*   "is_hd(M,xs,H) == 
+       (is_Nil(M,xs) --> empty(M,H)) &
+       (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | H=x) &
+       (is_quasilist(M,xs) | empty(M,H))" *)
+constdefs hd_fm :: "[i,i]=>i"
+    "hd_fm(xs,H) == 
+       And(Implies(Nil_fm(xs), empty_fm(H)),
+           And(Forall(Forall(Or(Neg(Cons_fm(1,0,xs#+2)), Equal(H#+2,1)))),
+               Or(quasilist_fm(xs), empty_fm(H))))"
+
+lemma hd_type [TC]:
+     "[| x \<in> nat; y \<in> nat |] ==> hd_fm(x,y) \<in> formula"
+by (simp add: hd_fm_def) 
+
+lemma sats_hd_fm [simp]:
+   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
+    ==> sats(A, hd_fm(x,y), env) <-> is_hd(**A, nth(x,env), nth(y,env))"
+by (simp add: hd_fm_def is_hd_def)
+
+lemma hd_iff_sats:
+      "[| nth(i,env) = x; nth(j,env) = y;
+          i \<in> nat; j \<in> nat; env \<in> list(A)|]
+       ==> is_hd(**A, x, y) <-> sats(A, hd_fm(i,j), env)"
+by simp
+
+theorem hd_reflection:
+     "REFLECTS[\<lambda>x. is_hd(L,f(x),g(x)), 
+               \<lambda>i x. is_hd(**Lset(i),f(x),g(x))]"
+apply (simp only: is_hd_def setclass_simps)
+apply (intro FOL_reflections Nil_reflection Cons_reflection
+             quasilist_reflection empty_reflection)  
+done
+
+
 subsubsection{*The Formula @{term is_tl}, Internalized*}
 
 (*     "is_tl(M,xs,T) ==
@@ -1159,6 +1210,38 @@
 done
 
 
+subsubsection{*The Formula @{term is_nth}, Internalized*}
+
+(* "is_nth(M,n,l,Z) == 
+      \<exists>X[M]. \<exists>sn[M]. \<exists>msn[M]. 
+       2       1       0
+       successor(M,n,sn) & membership(M,sn,msn) &
+       is_wfrec(M, iterates_MH(M, is_tl(M), l), msn, n, X) &
+       is_hd(M,X,Z)"
+constdefs nth_fm :: "[i,i,i]=>i"
+    "nth_fm(n,l,Z) == 
+       Exists(Exists(Exists(
+         And(successor_fm(n#+3,1),
+          And(membership_fm(1,0),
+           And(
+ *)
+
+theorem nth_reflection:
+     "REFLECTS[\<lambda>x. is_nth(L, f(x), g(x), h(x)),  
+               \<lambda>i x. is_nth(**Lset(i), f(x), g(x), h(x))]"
+apply (simp only: is_nth_def setclass_simps)
+apply (intro FOL_reflections function_reflections is_wfrec_reflection 
+             iterates_MH_reflection hd_reflection tl_reflection) 
+done
+
+theorem bool_of_o_reflection:
+     "REFLECTS[\<lambda>x. is_bool_of_o(L, P(x), f(x)),  
+               \<lambda>i x. is_bool_of_o(**Lset(i), P(x), f(x))]"
+apply (simp only: is_bool_of_o_def setclass_simps)
+apply (intro FOL_reflections function_reflections) 
+done
+
+
 subsubsection{*An Instance of Replacement for @{term nth}*}
 
 lemma nth_replacement_Reflects:
@@ -1199,9 +1282,7 @@
 
 subsubsection{*Instantiating the locale @{text M_datatypes}*}
 
-theorem M_datatypes_L: "PROP M_datatypes(L)"
-  apply (rule M_datatypes.intro)
-      apply (rule M_wfrank.axioms [OF M_wfrank_L])+
+lemma M_datatypes_axioms_L: "M_datatypes_axioms(L)"
   apply (rule M_datatypes_axioms.intro)
       apply (assumption | rule
         list_replacement1 list_replacement2
@@ -1209,6 +1290,12 @@
         nth_replacement)+
   done
 
+theorem M_datatypes_L: "PROP M_datatypes(L)"
+  apply (rule M_datatypes.intro)
+      apply (rule M_wfrank.axioms [OF M_wfrank_L])+
+ apply (rule M_datatypes_axioms_L); 
+ done
+
 lemmas list_closed = M_datatypes.list_closed [OF M_datatypes_L]
   and formula_closed = M_datatypes.formula_closed [OF M_datatypes_L]
   and list_abs = M_datatypes.list_abs [OF M_datatypes_L]
@@ -1307,11 +1394,15 @@
 
 subsubsection{*Instantiating the locale @{text M_eclose}*}
 
+lemma M_eclose_axioms_L: "M_eclose_axioms(L)"
+  apply (rule M_eclose_axioms.intro)
+   apply (assumption | rule eclose_replacement1 eclose_replacement2)+
+  done
+
 theorem M_eclose_L: "PROP M_eclose(L)"
   apply (rule M_eclose.intro)
        apply (rule M_datatypes.axioms [OF M_datatypes_L])+
-  apply (rule M_eclose_axioms.intro)
-   apply (assumption | rule eclose_replacement1 eclose_replacement2)+
+  apply (rule M_eclose_axioms_L)
   done
 
 lemmas eclose_closed [intro, simp] = M_eclose.eclose_closed [OF M_eclose_L]

--- a/src/ZF/Constructible/Separation.thy	Wed Jul 31 14:39:47 2002 +0200
+++ b/src/ZF/Constructible/Separation.thy	Wed Jul 31 14:40:40 2002 +0200
@@ -1,3 +1,9 @@
+(*  Title:      ZF/Constructible/Separation.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   2002  University of Cambridge
+*)
+
 header{*Early Instances of Separation and Strong Replacement*}
 
 theory Separation = L_axioms + WF_absolute:
@@ -69,6 +75,26 @@
 apply (simp_all add: succ_Un_distrib [symmetric])
 done
 
+subsection{*Separation for Set Difference*}
+
+lemma Diff_Reflects:
+     "REFLECTS[\<lambda>x. x \<notin> B, \<lambda>i x. x \<notin> B]"
+by (intro FOL_reflections)  
+
+lemma Diff_separation:
+     "L(B) ==> separation(L, \<lambda>x. x \<notin> B)"
+apply (rule separation_CollectI) 
+apply (rule_tac A="{B,z}" in subset_LsetE, blast ) 
+apply (rule ReflectsE [OF Diff_Reflects], assumption)
+apply (drule subset_Lset_ltD, assumption) 
+apply (erule reflection_imp_L_separation)
+  apply (simp_all add: lt_Ord2, clarify)
+apply (rule DPow_LsetI) 
+apply (rule not_iff_sats) 
+apply (rule_tac env="[x,B]" in mem_iff_sats)
+apply (rule sep_rules | simp)+
+done
+
 subsection{*Separation for Cartesian Product*}
 
 lemma cartprod_Reflects:
@@ -448,19 +474,21 @@
 text{*Separation (and Strong Replacement) for basic set-theoretic constructions
 such as intersection, Cartesian Product and image.*}
 
-theorem M_axioms_L: "PROP M_axioms(L)"
-  apply (rule M_axioms.intro)
-   apply (rule M_triv_axioms_L)
+lemma M_axioms_axioms_L: "M_axioms_axioms(L)"
   apply (rule M_axioms_axioms.intro)
-               apply (assumption | rule
-                 Inter_separation cartprod_separation image_separation
-                 converse_separation restrict_separation
-                 comp_separation pred_separation Memrel_separation
-                 funspace_succ_replacement well_ord_iso_separation
-                 obase_separation obase_equals_separation
-                 omap_replacement is_recfun_separation)+
+       apply (assumption | rule
+	 Inter_separation Diff_separation cartprod_separation image_separation
+	 converse_separation restrict_separation
+	 comp_separation pred_separation Memrel_separation
+	 funspace_succ_replacement well_ord_iso_separation
+	 obase_separation obase_equals_separation
+	 omap_replacement is_recfun_separation)+
   done
 
+theorem M_axioms_L: "PROP M_axioms(L)"
+by (rule M_axioms.intro [OF M_triv_axioms_L M_axioms_axioms_L])
+
+
 lemmas cartprod_iff = M_axioms.cartprod_iff [OF M_axioms_L]
   and cartprod_closed = M_axioms.cartprod_closed [OF M_axioms_L]
   and sum_closed = M_axioms.sum_closed [OF M_axioms_L]