author  wenzelm 
Mon, 16 Jun 2008 22:13:39 +0200  
changeset 27239  f2f42f9fa09d 
parent 27208  5fe899199f85 
child 28262  aa7ca36d67fd 
permissions  rwrr 
17456  1 
(* Title: CCL/Hered.thy 
0  2 
ID: $Id$ 
1474  3 
Author: Martin Coen 
0  4 
Copyright 1993 University of Cambridge 
5 
*) 

6 

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

9 
theory Hered 

10 
imports Type 

11 
begin 

12 

13 
text {* 

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

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

16 
is. Not so useful for functions! 

17 
*} 

0  18 

19 
consts 

20 
(*** Predicates ***) 

21 
HTTgen :: "i set => i set" 

22 
HTT :: "i set" 

23 

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

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

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

20140  32 

33 
subsection {* Hereditary Termination *} 

34 

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

36 
apply (unfold HTTgen_def) 

37 
apply (rule monoI) 

38 
apply blast 

39 
done 

40 

41 
lemma HTTgenXH: 

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

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

44 
apply (unfold HTTgen_def) 

45 
apply blast 

46 
done 

47 

48 
lemma HTTXH: 

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

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

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

52 
apply blast 

53 
done 

54 

55 

56 
subsection {* Introduction Rules for HTT *} 

57 

58 
lemma HTT_bot: "~ bot : HTT" 

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

60 

61 
lemma HTT_true: "true : HTT" 

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

63 

64 
lemma HTT_false: "false : HTT" 

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

66 

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

68 
apply (rule HTTXH [THEN iff_trans]) 

69 
apply blast 

70 
done 

71 

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

73 
apply (rule HTTXH [THEN iff_trans]) 

74 
apply auto 

75 
done 

76 

77 
lemmas HTT_rews1 = HTT_bot HTT_true HTT_false HTT_pair HTT_lam 

78 

79 
lemma HTT_rews2: 

80 
"one : HTT" 

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

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

83 
"zero : HTT" 

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

85 
"[] : HTT" 

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

87 
by (simp_all add: data_defs HTT_rews1) 

88 

89 
lemmas HTT_rews = HTT_rews1 HTT_rews2 

90 

91 

92 
subsection {* Coinduction for HTT *} 

93 

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

95 
apply (erule HTT_def [THEN def_coinduct]) 

96 
apply assumption 

97 
done 

98 

99 
ML {* 

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

103 
lemma HTT_coinduct3: 

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

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

106 
apply assumption 

107 
done 

108 

109 
ML {* 

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

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

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

115 
val HTTgenIs = 

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

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

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

121 
"one : HTTgen(R)", 

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

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

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

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

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

127 
"[ 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))"] 

128 
*} 

129 

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

131 

132 

133 
subsection {* Formation Rules for Types *} 

134 

135 
lemma UnitF: "Unit <= HTT" 

136 
by (simp add: subsetXH UnitXH HTT_rews) 

137 

138 
lemma BoolF: "Bool <= HTT" 

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

140 

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

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

143 

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

145 
by (fastsimp simp: subsetXH SgXH HTT_rews) 

146 

147 

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

149 
(*** exhaution rule for typeformer ***) 

150 

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

152 
lemma "Nat <= HTT" 

153 
apply (simp add: subsetXH) 

154 
apply clarify 

155 
apply (erule Nat_ind) 

156 
apply (fastsimp iff: HTT_rews)+ 

157 
done 

158 

159 
lemma NatF: "Nat <= HTT" 

160 
apply clarify 

161 
apply (erule HTT_coinduct3) 

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

163 
done 

164 

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

166 
apply clarify 

167 
apply (erule HTT_coinduct3) 

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

169 
subsetD [THEN HTTgen_mono [THEN ci3_AI]] 

170 
dest: ListXH [THEN iffD1]) 

171 
done 

172 

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

174 
apply clarify 

175 
apply (erule HTT_coinduct3) 

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

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

178 
done 

179 

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

181 
apply clarify 

182 
apply (erule HTT_coinduct3) 

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

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

185 
done 

186 

187 
end 