author  wenzelm 
Sat, 25 May 2013 17:40:44 +0200  
changeset 52147  9943f8067f11 
parent 52143  36ffe23b25f8 
child 56199  8e8d28ed7529 
permissions  rwrr 
17456  1 
(* Title: CCL/Term.thy 
1474  2 
Author: Martin Coen 
0  3 
Copyright 1993 University of Cambridge 
4 
*) 

5 

17456  6 
header {* Definitions of usual program constructs in CCL *} 
7 

8 
theory Term 

9 
imports CCL 

10 
begin 

0  11 

12 
consts 

13 

998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

14 
one :: "i" 
0  15 

19796  16 
"if" :: "[i,i,i]=>i" ("(3if _/ then _/ else _)" [0,0,60] 60) 
0  17 

17456  18 
inl :: "i=>i" 
19 
inr :: "i=>i" 

20 
when :: "[i,i=>i,i=>i]=>i" 

0  21 

998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

22 
split :: "[i,[i,i]=>i]=>i" 
17456  23 
fst :: "i=>i" 
24 
snd :: "i=>i" 

998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

25 
thd :: "i=>i" 
0  26 

998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

27 
zero :: "i" 
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

28 
succ :: "i=>i" 
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

29 
ncase :: "[i,i,i=>i]=>i" 
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

30 
nrec :: "[i,i,[i,i]=>i]=>i" 
0  31 

998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

32 
nil :: "i" ("([])") 
24825  33 
cons :: "[i,i]=>i" (infixr "$" 80) 
998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

34 
lcase :: "[i,i,[i,i]=>i]=>i" 
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

35 
lrec :: "[i,i,[i,i,i]=>i]=>i" 
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

36 

17456  37 
"let" :: "[i,i=>i]=>i" 
998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

38 
letrec :: "[[i,i=>i]=>i,(i=>i)=>i]=>i" 
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

39 
letrec2 :: "[[i,i,i=>i=>i]=>i,(i=>i=>i)=>i]=>i" 
17456  40 
letrec3 :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i" 
0  41 

14765  42 
syntax 
42051
dbdd4790da34
let syntax: reverted to plain "id", since translations cannot cope with constraints (notably position information);
wenzelm
parents:
35113
diff
changeset

43 
"_let" :: "[id,i,i]=>i" ("(3let _ be _/ in _)" 
1474  44 
[0,0,60] 60) 
998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

45 

42051
dbdd4790da34
let syntax: reverted to plain "id", since translations cannot cope with constraints (notably position information);
wenzelm
parents:
35113
diff
changeset

46 
"_letrec" :: "[id,id,i,i]=>i" ("(3letrec _ _ be _/ in _)" 
1474  47 
[0,0,0,60] 60) 
0  48 

42051
dbdd4790da34
let syntax: reverted to plain "id", since translations cannot cope with constraints (notably position information);
wenzelm
parents:
35113
diff
changeset

49 
"_letrec2" :: "[id,id,id,i,i]=>i" ("(3letrec _ _ _ be _/ in _)" 
1474  50 
[0,0,0,0,60] 60) 
0  51 

42051
dbdd4790da34
let syntax: reverted to plain "id", since translations cannot cope with constraints (notably position information);
wenzelm
parents:
35113
diff
changeset

52 
"_letrec3" :: "[id,id,id,id,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)" 
1474  53 
[0,0,0,0,0,60] 60) 
998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

54 

17456  55 
ML {* 
0  56 
(** Quantifier translations: variable binding **) 
57 

17781  58 
(* FIXME does not handle "_idtdummy" *) 
49660
de49d9b4d7bc
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents:
44241
diff
changeset

59 
(* FIXME should use Syntax_Trans.mark_bound, Syntax_Trans.variant_abs' *) 
2709  60 

44241  61 
fun let_tr [Free x, a, b] = Const(@{const_syntax let},dummyT) $ a $ absfree x b; 
0  62 
fun let_tr' [a,Abs(id,T,b)] = 
42284  63 
let val (id',b') = Syntax_Trans.variant_abs(id,T,b) 
35113  64 
in Const(@{syntax_const "_let"},dummyT) $ Free(id',T) $ a $ b' end; 
0  65 

44241  66 
fun letrec_tr [Free f, Free x, a, b] = 
67 
Const(@{const_syntax letrec}, dummyT) $ absfree x (absfree f a) $ absfree f b; 

68 
fun letrec2_tr [Free f, Free x, Free y, a, b] = 

69 
Const(@{const_syntax letrec2}, dummyT) $ absfree x (absfree y (absfree f a)) $ absfree f b; 

70 
fun letrec3_tr [Free f, Free x, Free y, Free z, a, b] = 

71 
Const(@{const_syntax letrec3}, dummyT) $ 

72 
absfree x (absfree y (absfree z (absfree f a))) $ absfree f b; 

0  73 

74 
fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] = 

42284  75 
let val (f',b') = Syntax_Trans.variant_abs(ff,SS,b) 
76 
val (_,a'') = Syntax_Trans.variant_abs(f,S,a) 

77 
val (x',a') = Syntax_Trans.variant_abs(x,T,a'') 

35113  78 
in Const(@{syntax_const "_letrec"},dummyT) $ Free(f',SS) $ Free(x',T) $ a' $ b' end; 
0  79 
fun letrec2_tr' [Abs(x,T,Abs(y,U,Abs(f,S,a))),Abs(ff,SS,b)] = 
42284  80 
let val (f',b') = Syntax_Trans.variant_abs(ff,SS,b) 
81 
val ( _,a1) = Syntax_Trans.variant_abs(f,S,a) 

82 
val (y',a2) = Syntax_Trans.variant_abs(y,U,a1) 

83 
val (x',a') = Syntax_Trans.variant_abs(x,T,a2) 

35113  84 
in Const(@{syntax_const "_letrec2"},dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ a' $ b' 
0  85 
end; 
86 
fun letrec3_tr' [Abs(x,T,Abs(y,U,Abs(z,V,Abs(f,S,a)))),Abs(ff,SS,b)] = 

42284  87 
let val (f',b') = Syntax_Trans.variant_abs(ff,SS,b) 
88 
val ( _,a1) = Syntax_Trans.variant_abs(f,S,a) 

89 
val (z',a2) = Syntax_Trans.variant_abs(z,V,a1) 

90 
val (y',a3) = Syntax_Trans.variant_abs(y,U,a2) 

91 
val (x',a') = Syntax_Trans.variant_abs(x,T,a3) 

35113  92 
in Const(@{syntax_const "_letrec3"},dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b' 
0  93 
end; 
94 

17456  95 
*} 
96 

97 
parse_translation {* 

52143  98 
[(@{syntax_const "_let"}, K let_tr), 
99 
(@{syntax_const "_letrec"}, K letrec_tr), 

100 
(@{syntax_const "_letrec2"}, K letrec2_tr), 

101 
(@{syntax_const "_letrec3"}, K letrec3_tr)] 

35113  102 
*} 
17456  103 

104 
print_translation {* 

52143  105 
[(@{const_syntax let}, K let_tr'), 
106 
(@{const_syntax letrec}, K letrec_tr'), 

107 
(@{const_syntax letrec2}, K letrec2_tr'), 

108 
(@{const_syntax letrec3}, K letrec3_tr')] 

35113  109 
*} 
17456  110 

111 
consts 

112 
napply :: "[i=>i,i,i]=>i" ("(_ ^ _ ` _)" [56,56,56] 56) 

113 

42156  114 
defs 
17456  115 
one_def: "one == true" 
116 
if_def: "if b then t else u == case(b,t,u,% x y. bot,%v. bot)" 

117 
inl_def: "inl(a) == <true,a>" 

118 
inr_def: "inr(b) == <false,b>" 

119 
when_def: "when(t,f,g) == split(t,%b x. if b then f(x) else g(x))" 

120 
split_def: "split(t,f) == case(t,bot,bot,f,%u. bot)" 

121 
fst_def: "fst(t) == split(t,%x y. x)" 

122 
snd_def: "snd(t) == split(t,%x y. y)" 

123 
thd_def: "thd(t) == split(t,%x p. split(p,%y z. z))" 

124 
zero_def: "zero == inl(one)" 

125 
succ_def: "succ(n) == inr(n)" 

126 
ncase_def: "ncase(n,b,c) == when(n,%x. b,%y. c(y))" 

127 
nrec_def: " nrec(n,b,c) == letrec g x be ncase(x,b,%y. c(y,g(y))) in g(n)" 

128 
nil_def: "[] == inl(one)" 

129 
cons_def: "h$t == inr(<h,t>)" 

130 
lcase_def: "lcase(l,b,c) == when(l,%x. b,%y. split(y,c))" 

131 
lrec_def: "lrec(l,b,c) == letrec g x be lcase(x,b,%h t. c(h,t,g(t))) in g(l)" 

132 

133 
let_def: "let x be t in f(x) == case(t,f(true),f(false),%x y. f(<x,y>),%u. f(lam x. u(x)))" 

134 
letrec_def: 

135 
"letrec g x be h(x,g) in b(g) == b(%x. fix(%f. lam x. h(x,%y. f`y))`x)" 

136 

137 
letrec2_def: "letrec g x y be h(x,y,g) in f(g)== 

138 
letrec g' p be split(p,%x y. h(x,y,%u v. g'(<u,v>))) 

139 
in f(%x y. g'(<x,y>))" 

140 

141 
letrec3_def: "letrec g x y z be h(x,y,z,g) in f(g) == 

142 
letrec g' p be split(p,%x xs. split(xs,%y z. h(x,y,z,%u v w. g'(<u,<v,w>>)))) 

143 
in f(%x y z. g'(<x,<y,z>>))" 

144 

145 
napply_def: "f ^n` a == nrec(n,a,%x g. f(g))" 

146 

20140  147 

148 
lemmas simp_can_defs = one_def inl_def inr_def 

149 
and simp_ncan_defs = if_def when_def split_def fst_def snd_def thd_def 

150 
lemmas simp_defs = simp_can_defs simp_ncan_defs 

151 

152 
lemmas ind_can_defs = zero_def succ_def nil_def cons_def 

153 
and ind_ncan_defs = ncase_def nrec_def lcase_def lrec_def 

154 
lemmas ind_defs = ind_can_defs ind_ncan_defs 

155 

156 
lemmas data_defs = simp_defs ind_defs napply_def 

157 
and genrec_defs = letrec_def letrec2_def letrec3_def 

158 

159 

160 
subsection {* Beta Rules, including strictness *} 

161 

162 
lemma letB: "~ t=bot ==> let x be t in f(x) = f(t)" 

163 
apply (unfold let_def) 

164 
apply (erule rev_mp) 

165 
apply (rule_tac t = "t" in term_case) 

166 
apply (simp_all add: caseBtrue caseBfalse caseBpair caseBlam) 

167 
done 

168 

169 
lemma letBabot: "let x be bot in f(x) = bot" 

170 
apply (unfold let_def) 

171 
apply (rule caseBbot) 

172 
done 

173 

174 
lemma letBbbot: "let x be t in bot = bot" 

175 
apply (unfold let_def) 

176 
apply (rule_tac t = t in term_case) 

177 
apply (rule caseBbot) 

178 
apply (simp_all add: caseBtrue caseBfalse caseBpair caseBlam) 

179 
done 

180 

181 
lemma applyB: "(lam x. b(x)) ` a = b(a)" 

182 
apply (unfold apply_def) 

183 
apply (simp add: caseBtrue caseBfalse caseBpair caseBlam) 

184 
done 

185 

186 
lemma applyBbot: "bot ` a = bot" 

187 
apply (unfold apply_def) 

188 
apply (rule caseBbot) 

189 
done 

190 

191 
lemma fixB: "fix(f) = f(fix(f))" 

192 
apply (unfold fix_def) 

193 
apply (rule applyB [THEN ssubst], rule refl) 

194 
done 

195 

196 
lemma letrecB: 

197 
"letrec g x be h(x,g) in g(a) = h(a,%y. letrec g x be h(x,g) in g(y))" 

198 
apply (unfold letrec_def) 

199 
apply (rule fixB [THEN ssubst], rule applyB [THEN ssubst], rule refl) 

200 
done 

201 

202 
lemmas rawBs = caseBs applyB applyBbot 

203 

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

204 
method_setup beta_rl = {* 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

205 
Scan.succeed (fn ctxt => 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

206 
SIMPLE_METHOD' (CHANGED o 
52037  207 
simp_tac (ctxt addsimps @{thms rawBs} setloop (fn _ => stac @{thm letrecB})))) 
42814  208 
*} 
20140  209 

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

210 
lemma ifBtrue: "if true then t else u = t" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

211 
and ifBfalse: "if false then t else u = u" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

212 
and ifBbot: "if bot then t else u = bot" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

213 
unfolding data_defs by beta_rl+ 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

214 

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

215 
lemma whenBinl: "when(inl(a),t,u) = t(a)" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

216 
and whenBinr: "when(inr(a),t,u) = u(a)" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

217 
and whenBbot: "when(bot,t,u) = bot" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

218 
unfolding data_defs by beta_rl+ 
20140  219 

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

220 
lemma splitB: "split(<a,b>,h) = h(a,b)" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

221 
and splitBbot: "split(bot,h) = bot" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

222 
unfolding data_defs by beta_rl+ 
17456  223 

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

224 
lemma fstB: "fst(<a,b>) = a" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

225 
and fstBbot: "fst(bot) = bot" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

226 
unfolding data_defs by beta_rl+ 
20140  227 

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

228 
lemma sndB: "snd(<a,b>) = b" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

229 
and sndBbot: "snd(bot) = bot" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

230 
unfolding data_defs by beta_rl+ 
20140  231 

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

232 
lemma thdB: "thd(<a,<b,c>>) = c" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

233 
and thdBbot: "thd(bot) = bot" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

234 
unfolding data_defs by beta_rl+ 
20140  235 

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

236 
lemma ncaseBzero: "ncase(zero,t,u) = t" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

237 
and ncaseBsucc: "ncase(succ(n),t,u) = u(n)" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

238 
and ncaseBbot: "ncase(bot,t,u) = bot" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

239 
unfolding data_defs by beta_rl+ 
20140  240 

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

241 
lemma nrecBzero: "nrec(zero,t,u) = t" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

242 
and nrecBsucc: "nrec(succ(n),t,u) = u(n,nrec(n,t,u))" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

243 
and nrecBbot: "nrec(bot,t,u) = bot" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

244 
unfolding data_defs by beta_rl+ 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

245 

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

246 
lemma lcaseBnil: "lcase([],t,u) = t" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

247 
and lcaseBcons: "lcase(x$xs,t,u) = u(x,xs)" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

248 
and lcaseBbot: "lcase(bot,t,u) = bot" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

249 
unfolding data_defs by beta_rl+ 
20140  250 

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

251 
lemma lrecBnil: "lrec([],t,u) = t" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

252 
and lrecBcons: "lrec(x$xs,t,u) = u(x,xs,lrec(xs,t,u))" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

253 
and lrecBbot: "lrec(bot,t,u) = bot" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

254 
unfolding data_defs by beta_rl+ 
20140  255 

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

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

257 
"letrec g x y be h(x,y,g) in g(p,q) = h(p,q,%u v. letrec g x y be h(x,y,g) in g(u,v))" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

258 
unfolding data_defs letrec2_def by beta_rl+ 
20140  259 

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

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

261 
"letrec g x y z be h(x,y,z,g) in g(p,q,r) = 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

262 
h(p,q,r,%u v w. letrec g x y z be h(x,y,z,g) in g(u,v,w))" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

263 
unfolding data_defs letrec3_def by beta_rl+ 
20140  264 

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

265 
lemma napplyBzero: "f^zero`a = a" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

266 
and napplyBsucc: "f^succ(n)`a = f(f^n`a)" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

267 
unfolding data_defs by beta_rl+ 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

268 

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

269 
lemmas termBs = letB applyB applyBbot splitB splitBbot fstB fstBbot 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

270 
sndB sndBbot thdB thdBbot ifBtrue ifBfalse ifBbot whenBinl whenBinr 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

271 
whenBbot ncaseBzero ncaseBsucc ncaseBbot nrecBzero nrecBsucc 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

272 
nrecBbot lcaseBnil lcaseBcons lcaseBbot lrecBnil lrecBcons lrecBbot 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset

273 
napplyBzero napplyBsucc 
20140  274 

275 

276 
subsection {* Constructors are injective *} 

277 

32154  278 
lemma term_injs: 
279 
"(inl(a) = inl(a')) <> (a=a')" 

280 
"(inr(a) = inr(a')) <> (a=a')" 

281 
"(succ(a) = succ(a')) <> (a=a')" 

282 
"(a$b = a'$b') <> (a=a' & b=b')" 

283 
by (inj_rl applyB splitB whenBinl whenBinr ncaseBsucc lcaseBcons) 

20140  284 

285 

286 
subsection {* Constructors are distinct *} 

287 

26480  288 
ML {* 
20140  289 
bind_thms ("term_dstncts", 
51670  290 
mkall_dstnct_thms @{context} @{thms data_defs} (@{thms ccl_injs} @ @{thms term_injs}) 
24825  291 
[["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","cons"]]); 
20140  292 
*} 
293 

294 

295 
subsection {* Rules for preorder @{text "[="} *} 

296 

32154  297 
lemma term_porews: 
298 
"inl(a) [= inl(a') <> a [= a'" 

299 
"inr(b) [= inr(b') <> b [= b'" 

300 
"succ(n) [= succ(n') <> n [= n'" 

301 
"x$xs [= x'$xs' <> x [= x' & xs [= xs'" 

302 
by (simp_all add: data_defs ccl_porews) 

20140  303 

304 

305 
subsection {* Rewriting and Proving *} 

306 

26480  307 
ML {* 
24790  308 
bind_thms ("term_injDs", XH_to_Ds @{thms term_injs}); 
20140  309 
*} 
310 

20917  311 
lemmas term_rews = termBs term_injs term_dstncts ccl_porews term_porews 
312 

20140  313 
lemmas [simp] = term_rews 
20917  314 
lemmas [elim!] = term_dstncts [THEN notE] 
315 
lemmas [dest!] = term_injDs 

20140  316 

317 
end 