author  wenzelm 
Thu, 23 Jul 2009 22:20:37 +0200  
changeset 32154  9721e8e4d48c 
parent 32153  a0e57fb1b930 
child 42156  df219e736a5d 
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 
lemma HTT_coinduct3: 

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

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

101 
apply assumption 

102 
done 

103 

32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

104 
lemma HTTgenIs: 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

105 
"true : HTTgen(R)" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

106 
"false : HTTgen(R)" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

107 
"[ a : R; b : R ] ==> <a,b> : HTTgen(R)" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

108 
"!!b. [ !!x. b(x) : R ] ==> lam x. b(x) : HTTgen(R)" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

109 
"one : HTTgen(R)" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

110 
"a : lfp(%x. HTTgen(x) Un R Un HTT) ==> inl(a) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

111 
"b : lfp(%x. HTTgen(x) Un R Un HTT) ==> inr(b) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

112 
"zero : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

113 
"n : lfp(%x. HTTgen(x) Un R Un HTT) ==> succ(n) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

114 
"[] : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

115 
"[ h : lfp(%x. HTTgen(x) Un R Un HTT); t : lfp(%x. HTTgen(x) Un R Un HTT) ] ==> 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

116 
h$t : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

117 
unfolding data_defs by (genIs HTTgenXH HTTgen_mono)+ 
20140  118 

119 

120 
subsection {* Formation Rules for Types *} 

121 

122 
lemma UnitF: "Unit <= HTT" 

123 
by (simp add: subsetXH UnitXH HTT_rews) 

124 

125 
lemma BoolF: "Bool <= HTT" 

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

127 

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

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

130 

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

132 
by (fastsimp simp: subsetXH SgXH HTT_rews) 

133 

134 

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

136 
(*** exhaution rule for typeformer ***) 

137 

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

139 
lemma "Nat <= HTT" 

140 
apply (simp add: subsetXH) 

141 
apply clarify 

142 
apply (erule Nat_ind) 

143 
apply (fastsimp iff: HTT_rews)+ 

144 
done 

145 

146 
lemma NatF: "Nat <= HTT" 

147 
apply clarify 

148 
apply (erule HTT_coinduct3) 

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

150 
done 

151 

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

153 
apply clarify 

154 
apply (erule HTT_coinduct3) 

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

156 
subsetD [THEN HTTgen_mono [THEN ci3_AI]] 

157 
dest: ListXH [THEN iffD1]) 

158 
done 

159 

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

161 
apply clarify 

162 
apply (erule HTT_coinduct3) 

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

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

165 
done 

166 

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

168 
apply clarify 

169 
apply (erule HTT_coinduct3) 

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

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

172 
done 

173 

174 
end 