author  wenzelm 
Wed, 15 Jul 2009 23:48:21 +0200  
changeset 32010  cb1a1c94b4cd 
parent 28262  aa7ca36d67fd 
child 32153  a0e57fb1b930 
permissions  rwrr 
17456  1 
(* Title: CCL/Hered.thy 
1474  2 
Author: Martin Coen 
0  3 
Copyright 1993 University of Cambridge 
4 
*) 

5 

17456  6 
header {* Hereditary Termination  cf. Martin Lo\"f *} 
7 

8 
theory Hered 

9 
imports Type 

10 
begin 

11 

12 
text {* 

13 
Note that this is based on an untyped equality and so @{text "lam 

14 
x. b(x)"} is only hereditarily terminating if @{text "ALL x. b(x)"} 

15 
is. Not so useful for functions! 

16 
*} 

0  17 

18 
consts 

19 
(*** Predicates ***) 

20 
HTTgen :: "i set => i set" 

21 
HTT :: "i set" 

22 

17456  23 
axioms 
0  24 
(*** Definitions of Hereditary Termination ***) 
25 

17456  26 
HTTgen_def: 
27 
"HTTgen(R) == {t. t=true  t=false  (EX a b. t=<a,b> & a : R & b : R)  

3837  28 
(EX f. t=lam x. f(x) & (ALL x. f(x) : R))}" 
17456  29 
HTT_def: "HTT == gfp(HTTgen)" 
30 

20140  31 

32 
subsection {* Hereditary Termination *} 

33 

34 
lemma HTTgen_mono: "mono(%X. HTTgen(X))" 

35 
apply (unfold HTTgen_def) 

36 
apply (rule monoI) 

37 
apply blast 

38 
done 

39 

40 
lemma HTTgenXH: 

41 
"t : HTTgen(A) <> t=true  t=false  (EX a b. t=<a,b> & a : A & b : A)  

42 
(EX f. t=lam x. f(x) & (ALL x. f(x) : A))" 

43 
apply (unfold HTTgen_def) 

44 
apply blast 

45 
done 

46 

47 
lemma HTTXH: 

48 
"t : HTT <> t=true  t=false  (EX a b. t=<a,b> & a : HTT & b : HTT)  

49 
(EX f. t=lam x. f(x) & (ALL x. f(x) : HTT))" 

50 
apply (rule HTTgen_mono [THEN HTT_def [THEN def_gfp_Tarski], THEN XHlemma1, unfolded HTTgen_def]) 

51 
apply blast 

52 
done 

53 

54 

55 
subsection {* Introduction Rules for HTT *} 

56 

57 
lemma HTT_bot: "~ bot : HTT" 

58 
by (blast dest: HTTXH [THEN iffD1]) 

59 

60 
lemma HTT_true: "true : HTT" 

61 
by (blast intro: HTTXH [THEN iffD2]) 

62 

63 
lemma HTT_false: "false : HTT" 

64 
by (blast intro: HTTXH [THEN iffD2]) 

65 

66 
lemma HTT_pair: "<a,b> : HTT <> a : HTT & b : HTT" 

67 
apply (rule HTTXH [THEN iff_trans]) 

68 
apply blast 

69 
done 

70 

71 
lemma HTT_lam: "lam x. f(x) : HTT <> (ALL x. f(x) : HTT)" 

72 
apply (rule HTTXH [THEN iff_trans]) 

73 
apply auto 

74 
done 

75 

76 
lemmas HTT_rews1 = HTT_bot HTT_true HTT_false HTT_pair HTT_lam 

77 

78 
lemma HTT_rews2: 

79 
"one : HTT" 

80 
"inl(a) : HTT <> a : HTT" 

81 
"inr(b) : HTT <> b : HTT" 

82 
"zero : HTT" 

83 
"succ(n) : HTT <> n : HTT" 

84 
"[] : HTT" 

85 
"x$xs : HTT <> x : HTT & xs : HTT" 

86 
by (simp_all add: data_defs HTT_rews1) 

87 

88 
lemmas HTT_rews = HTT_rews1 HTT_rews2 

89 

90 

91 
subsection {* Coinduction for HTT *} 

92 

93 
lemma HTT_coinduct: "[ t : R; R <= HTTgen(R) ] ==> t : HTT" 

94 
apply (erule HTT_def [THEN def_coinduct]) 

95 
apply assumption 

96 
done 

97 

98 
ML {* 

27239  99 
fun HTT_coinduct_tac ctxt s i = res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct} i 
20140  100 
*} 
101 

102 
lemma HTT_coinduct3: 

103 
"[ t : R; R <= HTTgen(lfp(%x. HTTgen(x) Un R Un HTT)) ] ==> t : HTT" 

104 
apply (erule HTTgen_mono [THEN [3] HTT_def [THEN def_coinduct3]]) 

105 
apply assumption 

106 
done 

107 

108 
ML {* 

27146  109 
val HTT_coinduct3_raw = rewrite_rule [@{thm HTTgen_def}] @{thm HTT_coinduct3} 
20140  110 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27146
diff
changeset

111 
fun HTT_coinduct3_tac ctxt s i = 
27239  112 
res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct3} i 
20140  113 

114 
val HTTgenIs = 

32010  115 
map (mk_genIs @{theory} @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono}) 
20140  116 
["true : HTTgen(R)", 
117 
"false : HTTgen(R)", 

118 
"[ a : R; b : R ] ==> <a,b> : HTTgen(R)", 

119 
"[ !!x. b(x) : R ] ==> lam x. b(x) : HTTgen(R)", 

120 
"one : HTTgen(R)", 

121 
"a : lfp(%x. HTTgen(x) Un R Un HTT) ==> inl(a) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))", 

122 
"b : lfp(%x. HTTgen(x) Un R Un HTT) ==> inr(b) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))", 

123 
"zero : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))", 

124 
"n : lfp(%x. HTTgen(x) Un R Un HTT) ==> succ(n) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))", 

125 
"[] : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))", 

126 
"[ h : lfp(%x. HTTgen(x) Un R Un HTT); t : lfp(%x. HTTgen(x) Un R Un HTT) ] ==> h$t : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"] 

127 
*} 

128 

129 
ML {* bind_thms ("HTTgenIs", HTTgenIs) *} 

130 

131 

132 
subsection {* Formation Rules for Types *} 

133 

134 
lemma UnitF: "Unit <= HTT" 

135 
by (simp add: subsetXH UnitXH HTT_rews) 

136 

137 
lemma BoolF: "Bool <= HTT" 

138 
by (fastsimp simp: subsetXH BoolXH iff: HTT_rews) 

139 

140 
lemma PlusF: "[ A <= HTT; B <= HTT ] ==> A + B <= HTT" 

141 
by (fastsimp simp: subsetXH PlusXH iff: HTT_rews) 

142 

143 
lemma SigmaF: "[ A <= HTT; !!x. x:A ==> B(x) <= HTT ] ==> SUM x:A. B(x) <= HTT" 

144 
by (fastsimp simp: subsetXH SgXH HTT_rews) 

145 

146 

147 
(*** Formation Rules for Recursive types  using coinduction these only need ***) 

148 
(*** exhaution rule for typeformer ***) 

149 

150 
(*Proof by induction  needs induction rule for type*) 

151 
lemma "Nat <= HTT" 

152 
apply (simp add: subsetXH) 

153 
apply clarify 

154 
apply (erule Nat_ind) 

155 
apply (fastsimp iff: HTT_rews)+ 

156 
done 

157 

158 
lemma NatF: "Nat <= HTT" 

159 
apply clarify 

160 
apply (erule HTT_coinduct3) 

161 
apply (fast intro: HTTgenIs elim!: HTTgen_mono [THEN ci3_RI] dest: NatXH [THEN iffD1]) 

162 
done 

163 

164 
lemma ListF: "A <= HTT ==> List(A) <= HTT" 

165 
apply clarify 

166 
apply (erule HTT_coinduct3) 

167 
apply (fast intro!: HTTgenIs elim!: HTTgen_mono [THEN ci3_RI] 

168 
subsetD [THEN HTTgen_mono [THEN ci3_AI]] 

169 
dest: ListXH [THEN iffD1]) 

170 
done 

171 

172 
lemma ListsF: "A <= HTT ==> Lists(A) <= HTT" 

173 
apply clarify 

174 
apply (erule HTT_coinduct3) 

175 
apply (fast intro!: HTTgenIs elim!: HTTgen_mono [THEN ci3_RI] 

176 
subsetD [THEN HTTgen_mono [THEN ci3_AI]] dest: ListsXH [THEN iffD1]) 

177 
done 

178 

179 
lemma IListsF: "A <= HTT ==> ILists(A) <= HTT" 

180 
apply clarify 

181 
apply (erule HTT_coinduct3) 

182 
apply (fast intro!: HTTgenIs elim!: HTTgen_mono [THEN ci3_RI] 

183 
subsetD [THEN HTTgen_mono [THEN ci3_AI]] dest: IListsXH [THEN iffD1]) 

184 
done 

185 

186 
end 