author paulson Thu, 01 Aug 2002 18:22:46 +0200 changeset 13441 d6d620639243 parent 13440 cdde97e1db1c child 13442 70479ec9f44f
better satisfies rules for is_recfun A satisfies rule for is_wfrec!
```--- a/src/ZF/Constructible/Rec_Separation.thy	Wed Jul 31 18:30:25 2002 +0200
+++ b/src/ZF/Constructible/Rec_Separation.thy	Thu Aug 01 18:22:46 2002 +0200
@@ -237,63 +237,69 @@

subsection{*Well-Founded Recursion!*}

+
+text{*Alternative definition, minimizing nesting of quantifiers around MH*}
+lemma M_is_recfun_iff:
+   "M_is_recfun(M,MH,r,a,f) <->
+    (\<forall>z[M]. z \<in> f <->
+     (\<exists>x[M]. \<exists>f_r_sx[M]. \<exists>y[M].
+             MH(x, f_r_sx, y) & pair(M,x,y,z) &
+             (\<exists>xa[M]. \<exists>sx[M]. \<exists>r_sx[M].
+                pair(M,x,a,xa) & upair(M,x,x,sx) &
+               pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) &
+               xa \<in> r)))"
+apply (rule rall_cong, blast)
+done
+
+
(* M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o"
"M_is_recfun(M,MH,r,a,f) ==
\<forall>z[M]. z \<in> f <->
-            5      4       3       2       1           0
-            (\<exists>x[M]. \<exists>y[M]. \<exists>xa[M]. \<exists>sx[M]. \<exists>r_sx[M]. \<exists>f_r_sx[M].
-               pair(M,x,y,z) & pair(M,x,a,xa) & upair(M,x,x,sx) &
+               2      1           0
+new def     (\<exists>x[M]. \<exists>f_r_sx[M]. \<exists>y[M].
+             MH(x, f_r_sx, y) & pair(M,x,y,z) &
+             (\<exists>xa[M]. \<exists>sx[M]. \<exists>r_sx[M].
+                pair(M,x,a,xa) & upair(M,x,x,sx) &
pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) &
-               xa \<in> r & MH(x, f_r_sx, y))"
+               xa \<in> r)"
*)

-text{*The three arguments of @{term p} are always 5, 0, 4.*}
+text{*The three arguments of @{term p} are always 2, 1, 0 and z*}
constdefs is_recfun_fm :: "[i, i, i, i]=>i"
"is_recfun_fm(p,r,a,f) ==
Forall(Iff(Member(0,succ(f)),
-    Exists(Exists(Exists(Exists(Exists(Exists(
-     And(pair_fm(5,4,6),
-      And(pair_fm(5,a#+7,3),
-       And(upair_fm(5,5,2),
-        And(pre_image_fm(r#+7,2,1),
-         And(restriction_fm(f#+7,1,0),
-          And(Member(3,r#+7), p))))))))))))))"
-
+    Exists(Exists(Exists(
+     And(p,
+      And(pair_fm(2,0,3),
+       Exists(Exists(Exists(
+	And(pair_fm(5,a#+7,2),
+	 And(upair_fm(5,5,1),
+	  And(pre_image_fm(r#+7,1,0),
+	   And(restriction_fm(f#+7,0,4), Member(2,r#+7)))))))))))))))"

lemma is_recfun_type [TC]:
"[| p \<in> formula; x \<in> nat; y \<in> nat; z \<in> nat |]
==> is_recfun_fm(p,x,y,z) \<in> formula"

+
lemma sats_is_recfun_fm:
assumes MH_iff_sats:
-      "!!a0 a1 a2 a3 a4 a5 a6.
-        [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A; a5\<in>A; a6\<in>A|] ==>
-        MH(a5, a0, a4) <->
-       sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,Cons(a5,Cons(a6,env))))))))"
+      "!!a0 a1 a2 a3.
+        [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A|]
+        ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,env)))))"
shows
"[|x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, is_recfun_fm(p,x,y,z), env) <->
M_is_recfun(**A, MH, nth(x,env), nth(y,env), nth(z,env))"
-by (simp add: is_recfun_fm_def M_is_recfun_def MH_iff_sats [THEN iff_sym])
-(*
-apply (rule ball_cong bex_cong iff_cong conj_cong refl iff_refl) +
- sats(A, p,
-   Cons(xf, Cons(xe, Cons(xd, Cons(xc, Cons(xb, Cons(xaa, Cons(xa, env))))))))
-\<longleftrightarrow> MH(xaa, xf, xb)
-
-MH(nth(5,env), nth(0,env), nth(4,env)) <-> sats(A, p, env);
-*)
-
-(*      "!!x y z. [|x\<in>A; y\<in>A; z\<in>A|] ==> MH(x,y,z) <-> sats(A, p, env)"
-*)
+by (simp add: is_recfun_fm_def M_is_recfun_iff MH_iff_sats [THEN iff_sym])

lemma is_recfun_iff_sats:
assumes MH_iff_sats:
-      "!!a0 a1 a2 a3 a4 a5 a6.
-        [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A; a5\<in>A; a6\<in>A|] ==>
-        MH(a5, a0, a4) <->
-       sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,Cons(a5,Cons(a6,env))))))))"
+      "!!a0 a1 a2 a3.
+        [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A|]
+        ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,env)))))"
shows
"[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
@@ -320,9 +326,56 @@
restriction_reflection MH_reflection)
done

-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. *}
+subsubsection{*The Operator @{term is_wfrec}*}
+
+text{*The three arguments of @{term p} are always 2, 1, 0*}
+
+(* is_wfrec :: "[i=>o, i, [i,i,i]=>o, i, i] => o"
+    "is_wfrec(M,MH,r,a,z) ==
+      \<exists>f[M]. M_is_recfun(M,MH,r,a,f) & MH(a,f,z)" *)
+constdefs is_wfrec_fm :: "[i, i, i, i]=>i"
+ "is_wfrec_fm(p,r,a,z) ==
+    Exists(And(is_recfun_fm(p, succ(r), succ(a), 0),
+           Exists(Exists(Exists(Exists(
+             And(Equal(2,a#+5), And(Equal(1,4), And(Equal(0,z#+5), p)))))))))"
+
+text{*We call @{term p} with arguments a, f, z by equating them with
+  the corresponding quantified variables with de Bruijn indices 2, 1, 0.*}
+
+text{*There's an additional existential quantifier to ensure that the
+      environments in both calls to MH have the same length.*}
+
+lemma is_wfrec_type [TC]:
+     "[| p \<in> formula; x \<in> nat; y \<in> nat; z \<in> nat |]
+      ==> is_wfrec_fm(p,x,y,z) \<in> formula"
+
+lemma sats_is_wfrec_fm:
+  assumes MH_iff_sats:
+      "!!a0 a1 a2 a3 a4.
+        [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A|]
+        ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,env))))))"
+  shows
+      "[|x \<in> nat; y < length(env); z < length(env); env \<in> list(A)|]
+       ==> sats(A, is_wfrec_fm(p,x,y,z), env) <->
+           is_wfrec(**A, MH, nth(x,env), nth(y,env), nth(z,env))"
+apply (frule_tac x=z in lt_length_in_nat, assumption)
+apply (frule lt_length_in_nat, assumption)
+apply (simp add: is_wfrec_fm_def sats_is_recfun_fm is_wfrec_def MH_iff_sats [THEN iff_sym], blast)
+done
+
+
+lemma is_wfrec_iff_sats:
+  assumes MH_iff_sats:
+      "!!a0 a1 a2 a3 a4.
+        [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A|]
+        ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,env))))))"
+  shows
+  "[|nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
+      i \<in> nat; j < length(env); k < length(env); env \<in> list(A)|]
+   ==> is_wfrec(**A, MH, x, y, z) <-> sats(A, is_wfrec_fm(p,i,j,k), env)"
+by (simp add: sats_is_wfrec_fm [OF MH_iff_sats])
+
theorem is_wfrec_reflection:
assumes MH_reflection:
"!!f' f g h. REFLECTS[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)),
@@ -360,6 +413,7 @@
apply (rename_tac u)
apply (rule ball_iff_sats imp_iff_sats)+
apply (rule_tac env="[rplus,u,r]" in tran_closure_iff_sats)
+apply (rule sep_rules | simp)+
apply (rule sep_rules is_recfun_iff_sats | simp)+
done

@@ -401,7 +455,7 @@
apply (rename_tac u)
apply (rule bex_iff_sats ball_iff_sats conj_iff_sats)+
apply (rule_tac env = "[x,u,B,r]" in mem_iff_sats)
-apply (rule sep_rules tran_closure_iff_sats is_recfun_iff_sats | simp)+
+apply (rule sep_rules list.intros app_type tran_closure_iff_sats is_recfun_iff_sats | simp)+
done

@@ -710,8 +764,7 @@
sats(A, iterates_MH_fm(p,i',i,j,k), env)"
apply (rule iff_sym)
apply (rule iff_trans)
-apply (rule sats_iterates_MH_fm [of A is_F], blast)
-apply simp_all
+apply (rule sats_iterates_MH_fm [of A is_F], blast, simp_all)
done
(*FIXME: surely proof can be improved?*)

@@ -790,6 +843,7 @@
by (intro FOL_reflections function_reflections is_wfrec_reflection
iterates_MH_reflection list_functor_reflection)

+
lemma list_replacement1:
"L(A) ==> iterates_replacement(L, is_list_functor(L,A), 0)"
apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
@@ -809,12 +863,11 @@
apply (rename_tac v)
apply (rule bex_iff_sats conj_iff_sats)+
apply (rule_tac env = "[u,v,A,n,B,0,Memrel(succ(n))]" in mem_iff_sats)
-apply (rule sep_rules | simp)+
apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats
-            is_recfun_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
+            is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
done

+
lemma list_replacement2_Reflects:
"REFLECTS
[\<lambda>x. \<exists>u[L]. u \<in> B \<and> u \<in> nat \<and>
@@ -852,10 +905,8 @@
apply (rename_tac v)
apply (rule bex_iff_sats conj_iff_sats)+
apply (rule_tac env = "[u,v,A,B,0,nat]" in mem_iff_sats)
-apply (rule sep_rules | simp)+
apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats
-            is_recfun_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
+            is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
done

@@ -934,10 +985,8 @@
apply (rename_tac v)
apply (rule bex_iff_sats conj_iff_sats)+
apply (rule_tac env = "[u,v,n,B,0,Memrel(succ(n))]" in mem_iff_sats)
-apply (rule sep_rules | simp)+
apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats
-            is_recfun_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
+            is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
done

lemma formula_replacement2_Reflects:
@@ -977,10 +1026,8 @@
apply (rename_tac v)
apply (rule bex_iff_sats conj_iff_sats)+
apply (rule_tac env = "[u,v,B,0,nat]" in mem_iff_sats)
-apply (rule sep_rules | simp)+
apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats
-            is_recfun_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
+            is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
done

text{*NB The proofs for type @{term formula} are virtually identical to those
@@ -1239,8 +1286,7 @@
REFLECTS[\<lambda>x. is_bool_of_o(L, P(L,x), f(x)),
\<lambda>i x. is_bool_of_o(**Lset(i), P(**Lset(i),x), f(x))]"
apply (simp (no_asm) only: is_bool_of_o_def setclass_simps)
-apply (intro FOL_reflections function_reflections)
-apply assumption+
+apply (intro FOL_reflections function_reflections, assumption+)
done

@@ -1274,10 +1320,8 @@
apply (rename_tac v)
apply (rule bex_iff_sats conj_iff_sats)+
apply (rule_tac env = "[u,v,A,z,w,Memrel(succ(n))]" in mem_iff_sats)
-apply (rule sep_rules | simp)+
apply (rule sep_rules is_nat_case_iff_sats tl_iff_sats
-            is_recfun_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
+            is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
done

@@ -1295,7 +1339,7 @@
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);
+ apply (rule M_datatypes_axioms_L)
done

lemmas list_closed = M_datatypes.list_closed [OF M_datatypes_L]
@@ -1344,10 +1388,8 @@
apply (rename_tac v)
apply (rule bex_iff_sats conj_iff_sats)+
apply (rule_tac env = "[u,v,A,n,B,Memrel(succ(n))]" in mem_iff_sats)
-apply (rule sep_rules | simp)+
apply (rule sep_rules iterates_MH_iff_sats is_nat_case_iff_sats
-             is_recfun_iff_sats big_union_iff_sats quasinat_iff_sats | simp)+
+             is_wfrec_iff_sats big_union_iff_sats quasinat_iff_sats | simp)+
done

@@ -1387,10 +1429,8 @@
apply (rename_tac v)
apply (rule bex_iff_sats conj_iff_sats)+
apply (rule_tac env = "[u,v,A,B,nat]" in mem_iff_sats)
-apply (rule sep_rules | simp)+