equal
deleted
inserted
replaced
110 |
110 |
111 eq_reflection: "(x=y) ==> (x==y)" |
111 eq_reflection: "(x=y) ==> (x==y)" |
112 iff_reflection: "(P<->Q) ==> (P==Q)" |
112 iff_reflection: "(P<->Q) ==> (P==Q)" |
113 |
113 |
114 |
114 |
|
115 |
115 subsection {* Lemmas and proof tools *} |
116 subsection {* Lemmas and proof tools *} |
116 |
117 |
117 setup Simplifier.setup |
118 setup Simplifier.setup |
118 use "IFOL_lemmas.ML" |
119 use "IFOL_lemmas.ML" |
119 |
120 |
242 back_subst |
243 back_subst |
243 rev_mp |
244 rev_mp |
244 mp |
245 mp |
245 trans |
246 trans |
246 |
247 |
|
248 |
|
249 |
|
250 subsection {* ``Let'' declarations *} |
|
251 |
|
252 nonterminals letbinds letbind |
|
253 |
|
254 constdefs |
|
255 Let :: "['a::logic, 'a => 'b] => ('b::logic)" |
|
256 "Let(s, f) == f(s)" |
|
257 |
|
258 syntax |
|
259 "_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10) |
|
260 "" :: "letbind => letbinds" ("_") |
|
261 "_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _") |
|
262 "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10) |
|
263 |
|
264 translations |
|
265 "_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))" |
|
266 "let x = a in e" == "Let(a, %x. e)" |
|
267 |
|
268 |
|
269 lemma LetI: |
|
270 assumes prem: "(!!x. x=t ==> P(u(x)))" |
|
271 shows "P(let x=t in u(x))" |
|
272 apply (unfold Let_def) |
|
273 apply (rule refl [THEN prem]) |
|
274 done |
|
275 |
|
276 ML |
|
277 {* |
|
278 val Let_def = thm "Let_def"; |
|
279 val LetI = thm "LetI"; |
|
280 *} |
|
281 |
247 end |
282 end |