author  wenzelm 
Mon, 07 Oct 2013 21:24:44 +0200  
changeset 54313  da2e6282a4f5 
parent 47966  b8a94ed1646e 
child 58889  5b7a9633cfa8 
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 

42156  18 
definition HTTgen :: "i set => i set" where 
19 
"HTTgen(R) == 

20 
{t. t=true  t=false  (EX a b. t= <a, b> & a : R & b : R)  

21 
(EX f. t = lam x. f(x) & (ALL x. f(x) : R))}" 

0  22 

42156  23 
definition HTT :: "i set" 
24 
where "HTT == gfp(HTTgen)" 

17456  25 

20140  26 

27 
subsection {* Hereditary Termination *} 

28 

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

30 
apply (unfold HTTgen_def) 

31 
apply (rule monoI) 

32 
apply blast 

33 
done 

34 

35 
lemma HTTgenXH: 

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

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

38 
apply (unfold HTTgen_def) 

39 
apply blast 

40 
done 

41 

42 
lemma HTTXH: 

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

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

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

46 
apply blast 

47 
done 

48 

49 

50 
subsection {* Introduction Rules for HTT *} 

51 

52 
lemma HTT_bot: "~ bot : HTT" 

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

54 

55 
lemma HTT_true: "true : HTT" 

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

57 

58 
lemma HTT_false: "false : HTT" 

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

60 

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

62 
apply (rule HTTXH [THEN iff_trans]) 

63 
apply blast 

64 
done 

65 

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

67 
apply (rule HTTXH [THEN iff_trans]) 

68 
apply auto 

69 
done 

70 

71 
lemmas HTT_rews1 = HTT_bot HTT_true HTT_false HTT_pair HTT_lam 

72 

73 
lemma HTT_rews2: 

74 
"one : HTT" 

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

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

77 
"zero : HTT" 

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

79 
"[] : HTT" 

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

81 
by (simp_all add: data_defs HTT_rews1) 

82 

83 
lemmas HTT_rews = HTT_rews1 HTT_rews2 

84 

85 

86 
subsection {* Coinduction for HTT *} 

87 

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

89 
apply (erule HTT_def [THEN def_coinduct]) 

90 
apply assumption 

91 
done 

92 

93 
lemma HTT_coinduct3: 

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

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

96 
apply assumption 

97 
done 

98 

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

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

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

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

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

103 
"!!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

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

105 
"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

106 
"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

107 
"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

108 
"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

109 
"[] : 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

110 
"[ 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

111 
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

112 
unfolding data_defs by (genIs HTTgenXH HTTgen_mono)+ 
20140  113 

114 

115 
subsection {* Formation Rules for Types *} 

116 

117 
lemma UnitF: "Unit <= HTT" 

118 
by (simp add: subsetXH UnitXH HTT_rews) 

119 

120 
lemma BoolF: "Bool <= HTT" 

47966  121 
by (fastforce simp: subsetXH BoolXH iff: HTT_rews) 
20140  122 

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

47966  124 
by (fastforce simp: subsetXH PlusXH iff: HTT_rews) 
20140  125 

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

47966  127 
by (fastforce simp: subsetXH SgXH HTT_rews) 
20140  128 

129 

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

131 
(*** exhaution rule for typeformer ***) 

132 

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

134 
lemma "Nat <= HTT" 

135 
apply (simp add: subsetXH) 

136 
apply clarify 

137 
apply (erule Nat_ind) 

47966  138 
apply (fastforce iff: HTT_rews)+ 
20140  139 
done 
140 

141 
lemma NatF: "Nat <= HTT" 

142 
apply clarify 

143 
apply (erule HTT_coinduct3) 

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

145 
done 

146 

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

148 
apply clarify 

149 
apply (erule HTT_coinduct3) 

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

151 
subsetD [THEN HTTgen_mono [THEN ci3_AI]] 

152 
dest: ListXH [THEN iffD1]) 

153 
done 

154 

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

156 
apply clarify 

157 
apply (erule HTT_coinduct3) 

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

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

160 
done 

161 

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

163 
apply clarify 

164 
apply (erule HTT_coinduct3) 

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

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

167 
done 

168 

169 
end 