author  paulson 
Thu, 11 Jul 2002 13:43:24 +0200  
changeset 13348  374d05460db4 
parent 13339  0f89104dd377 
child 13350  626b79677dfa 
permissions  rwrr 
13306  1 
header {*Absoluteness Properties for Recursive Datatypes*} 
2 

13269  3 
theory Datatype_absolute = Formula + WF_absolute: 
13268  4 

5 

6 
subsection{*The lfp of a continuous function can be expressed as a union*} 

7 

8 
constdefs 

9 
contin :: "[i=>i]=>o" 

10 
"contin(h) == (\<forall>A. A\<noteq>0 > h(\<Union>A) = (\<Union>X\<in>A. h(X)))" 

11 

12 
lemma bnd_mono_iterates_subset: "[bnd_mono(D, h); n \<in> nat] ==> h^n (0) <= D" 

13 
apply (induct_tac n) 

14 
apply (simp_all add: bnd_mono_def, blast) 

15 
done 

16 

17 

18 
lemma contin_iterates_eq: 

19 
"contin(h) \<Longrightarrow> h(\<Union>n\<in>nat. h^n (0)) = (\<Union>n\<in>nat. h^n (0))" 

20 
apply (simp add: contin_def) 

21 
apply (rule trans) 

22 
apply (rule equalityI) 

23 
apply (simp_all add: UN_subset_iff) 

24 
apply safe 

25 
apply (erule_tac [2] natE) 

26 
apply (rule_tac a="succ(x)" in UN_I) 

27 
apply simp_all 

28 
apply blast 

29 
done 

30 

31 
lemma lfp_subset_Union: 

32 
"[bnd_mono(D, h); contin(h)] ==> lfp(D,h) <= (\<Union>n\<in>nat. h^n(0))" 

33 
apply (rule lfp_lowerbound) 

34 
apply (simp add: contin_iterates_eq) 

35 
apply (simp add: contin_def bnd_mono_iterates_subset UN_subset_iff) 

36 
done 

37 

38 
lemma Union_subset_lfp: 

39 
"bnd_mono(D,h) ==> (\<Union>n\<in>nat. h^n(0)) <= lfp(D,h)" 

40 
apply (simp add: UN_subset_iff) 

41 
apply (rule ballI) 

13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13306
diff
changeset

42 
apply (induct_tac n, simp_all) 
13268  43 
apply (rule subset_trans [of _ "h(lfp(D,h))"]) 
44 
apply (blast dest: bnd_monoD2 [OF _ _ lfp_subset] ) 

45 
apply (erule lfp_lemma2) 

46 
done 

47 

48 
lemma lfp_eq_Union: 

49 
"[bnd_mono(D, h); contin(h)] ==> lfp(D,h) = (\<Union>n\<in>nat. h^n(0))" 

50 
by (blast del: subsetI 

51 
intro: lfp_subset_Union Union_subset_lfp) 

52 

53 

54 
subsection {*lists without univ*} 

55 

56 
lemmas datatype_univs = A_into_univ Inl_in_univ Inr_in_univ 

57 
Pair_in_univ zero_in_univ 

58 

59 
lemma list_fun_bnd_mono: "bnd_mono(univ(A), \<lambda>X. {0} + A*X)" 

60 
apply (rule bnd_monoI) 

61 
apply (intro subset_refl zero_subset_univ A_subset_univ 

62 
sum_subset_univ Sigma_subset_univ) 

63 
apply (blast intro!: subset_refl sum_mono Sigma_mono del: subsetI) 

64 
done 

65 

66 
lemma list_fun_contin: "contin(\<lambda>X. {0} + A*X)" 

67 
by (simp add: contin_def, blast) 

68 

69 
text{*Reexpresses lists using sum and product*} 

70 
lemma list_eq_lfp2: "list(A) = lfp(univ(A), \<lambda>X. {0} + A*X)" 

71 
apply (simp add: list_def) 

72 
apply (rule equalityI) 

73 
apply (rule lfp_lowerbound) 

74 
prefer 2 apply (rule lfp_subset) 

75 
apply (clarify, subst lfp_unfold [OF list_fun_bnd_mono]) 

76 
apply (simp add: Nil_def Cons_def) 

77 
apply blast 

78 
txt{*Opposite inclusion*} 

79 
apply (rule lfp_lowerbound) 

80 
prefer 2 apply (rule lfp_subset) 

81 
apply (clarify, subst lfp_unfold [OF list.bnd_mono]) 

82 
apply (simp add: Nil_def Cons_def) 

83 
apply (blast intro: datatype_univs 

84 
dest: lfp_subset [THEN subsetD]) 

85 
done 

86 

87 
text{*Reexpresses lists using "iterates", no univ.*} 

88 
lemma list_eq_Union: 

89 
"list(A) = (\<Union>n\<in>nat. (\<lambda>X. {0} + A*X) ^ n (0))" 

90 
by (simp add: list_eq_lfp2 lfp_eq_Union list_fun_bnd_mono list_fun_contin) 

91 

92 

93 
subsection {*Absoluteness for "Iterates"*} 

94 

95 
lemma (in M_trancl) iterates_relativize: 

96 
"[n \<in> nat; M(v); \<forall>x[M]. M(F(x)); 

97 
strong_replacement(M, 

98 
\<lambda>x z. \<exists>y[M]. \<exists>g[M]. pair(M, x, y, z) & 

99 
is_recfun (Memrel(succ(n)), x, 

100 
\<lambda>n f. nat_case(v, \<lambda>m. F(f`m), n), g) & 

101 
y = nat_case(v, \<lambda>m. F(g`m), x))] 

102 
==> iterates(F,n,v) = z <> 

103 
(\<exists>g[M]. is_recfun(Memrel(succ(n)), n, 

104 
\<lambda>n g. nat_case(v, \<lambda>m. F(g`m), n), g) & 

105 
z = nat_case(v, \<lambda>m. F(g`m), n))" 

106 
by (simp add: iterates_nat_def recursor_def transrec_def 

107 
eclose_sing_Ord_eq trans_wfrec_relativize nat_into_M 

108 
wf_Memrel trans_Memrel relation_Memrel nat_case_closed) 

109 

110 

111 
lemma (in M_wfrank) iterates_closed [intro,simp]: 

112 
"[n \<in> nat; M(v); \<forall>x[M]. M(F(x)); 

113 
strong_replacement(M, 

114 
\<lambda>x z. \<exists>y[M]. \<exists>g[M]. pair(M, x, y, z) & 

115 
is_recfun (Memrel(succ(n)), x, 

116 
\<lambda>n f. nat_case(v, \<lambda>m. F(f`m), n), g) & 

117 
y = nat_case(v, \<lambda>m. F(g`m), x))] 

118 
==> M(iterates(F,n,v))" 

119 
by (simp add: iterates_nat_def recursor_def transrec_def 

120 
eclose_sing_Ord_eq trans_wfrec_closed nat_into_M 

121 
wf_Memrel trans_Memrel relation_Memrel nat_case_closed) 

122 

123 

124 
locale M_datatypes = M_wfrank + 

125 
(*THEY NEED RELATIVIZATION*) 

126 
assumes list_replacement1: 

127 
"[M(A); n \<in> nat] ==> 

128 
strong_replacement(M, 

13269  129 
\<lambda>x z. \<exists>y[M]. \<exists>g[M]. \<exists>sucn[M]. \<exists>memr[M]. 
130 
pair(M,x,y,z) & successor(M,n,sucn) & 

131 
membership(M,sucn,memr) & 

132 
is_recfun (memr, x, 

13268  133 
\<lambda>n f. nat_case(0, \<lambda>m. {0} + A \<times> f`m, n), g) & 
134 
y = nat_case(0, \<lambda>m. {0} + A \<times> g`m, x))" 

13348  135 
and list_replacement2: 
13268  136 
"M(A) ==> strong_replacement(M, \<lambda>x y. y = (\<lambda>X. {0} + A \<times> X)^x (0))" 
137 

138 

139 
lemma (in M_datatypes) list_replacement1': 

140 
"[M(A); n \<in> nat] 

141 
==> strong_replacement 

13293  142 
(M, \<lambda>x y. \<exists>z[M]. y = \<langle>x,z\<rangle> & 
143 
(\<exists>g[M]. is_recfun (Memrel(succ(n)), x, 

13269  144 
\<lambda>n f. nat_case(0, \<lambda>m. {0} + A \<times> f`m, n), g) & 
13293  145 
z = nat_case(0, \<lambda>m. {0} + A \<times> g ` m, x)))" 
13269  146 
by (insert list_replacement1, simp add: nat_into_M) 
13268  147 

13348  148 
lemma (in M_datatypes) list_replacement2': 
149 
"M(A) ==> strong_replacement(M, \<lambda>x y. y = (\<lambda>X. {0} + A \<times> X)^x (0))" 

150 
by (insert list_replacement2, simp add: nat_into_M) 

151 

13268  152 

153 
lemma (in M_datatypes) list_closed [intro,simp]: 

154 
"M(A) ==> M(list(A))" 

155 
by (simp add: list_eq_Union list_replacement1' list_replacement2') 

156 

13293  157 

13268  158 
end 