293 |
293 |
294 text {* It seems to be more elegant to have an overloaded injection like the |
294 text {* It seems to be more elegant to have an overloaded injection like the |
295 following. |
295 following. |
296 *} |
296 *} |
297 |
297 |
298 axclass inj_term < "type" |
298 class inj_term = |
299 consts inj_term:: "'a::inj_term \<Rightarrow> term" ("\<langle>_\<rangle>" 1000) |
299 fixes inj_term:: "'a \<Rightarrow> term" ("\<langle>_\<rangle>" 1000) |
300 |
300 |
301 text {* How this overloaded injections work can be seen in the theory |
301 text {* How this overloaded injections work can be seen in the theory |
302 @{text DefiniteAssignment}. Other big inductive relations on |
302 @{text DefiniteAssignment}. Other big inductive relations on |
303 terms defined in theories @{text WellType}, @{text Eval}, @{text Evaln} and |
303 terms defined in theories @{text WellType}, @{text Eval}, @{text Evaln} and |
304 @{text AxSem} don't follow this convention right now, but introduce subtle |
304 @{text AxSem} don't follow this convention right now, but introduce subtle |
306 expressions, statements and so on. So unfortunately you will encounter a |
306 expressions, statements and so on. So unfortunately you will encounter a |
307 mixture of dealing with these injections. The abbreviations above are used |
307 mixture of dealing with these injections. The abbreviations above are used |
308 as bridge between the different conventions. |
308 as bridge between the different conventions. |
309 *} |
309 *} |
310 |
310 |
311 instance stmt::inj_term .. |
311 instantiation stmt :: inj_term |
312 |
312 begin |
313 defs (overloaded) |
313 |
314 stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c" |
314 definition |
|
315 stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c" |
|
316 |
|
317 instance .. |
|
318 |
|
319 end |
315 |
320 |
316 lemma stmt_inj_term_simp: "\<langle>c::stmt\<rangle> = In1r c" |
321 lemma stmt_inj_term_simp: "\<langle>c::stmt\<rangle> = In1r c" |
317 by (simp add: stmt_inj_term_def) |
322 by (simp add: stmt_inj_term_def) |
318 |
323 |
319 lemma stmt_inj_term [iff]: "\<langle>x::stmt\<rangle> = \<langle>y\<rangle> \<equiv> x = y" |
324 lemma stmt_inj_term [iff]: "\<langle>x::stmt\<rangle> = \<langle>y\<rangle> \<equiv> x = y" |
320 by (simp add: stmt_inj_term_simp) |
325 by (simp add: stmt_inj_term_simp) |
321 |
326 |
322 instance expr::inj_term .. |
327 instantiation expr :: inj_term |
323 |
328 begin |
324 defs (overloaded) |
329 |
325 expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e" |
330 definition |
|
331 expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e" |
|
332 |
|
333 instance .. |
|
334 |
|
335 end |
326 |
336 |
327 lemma expr_inj_term_simp: "\<langle>e::expr\<rangle> = In1l e" |
337 lemma expr_inj_term_simp: "\<langle>e::expr\<rangle> = In1l e" |
328 by (simp add: expr_inj_term_def) |
338 by (simp add: expr_inj_term_def) |
329 |
339 |
330 lemma expr_inj_term [iff]: "\<langle>x::expr\<rangle> = \<langle>y\<rangle> \<equiv> x = y" |
340 lemma expr_inj_term [iff]: "\<langle>x::expr\<rangle> = \<langle>y\<rangle> \<equiv> x = y" |
331 by (simp add: expr_inj_term_simp) |
341 by (simp add: expr_inj_term_simp) |
332 |
342 |
333 instance var::inj_term .. |
343 instantiation var :: inj_term |
334 |
344 begin |
335 defs (overloaded) |
345 |
336 var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v" |
346 definition |
|
347 var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v" |
|
348 |
|
349 instance .. |
|
350 |
|
351 end |
337 |
352 |
338 lemma var_inj_term_simp: "\<langle>v::var\<rangle> = In2 v" |
353 lemma var_inj_term_simp: "\<langle>v::var\<rangle> = In2 v" |
339 by (simp add: var_inj_term_def) |
354 by (simp add: var_inj_term_def) |
340 |
355 |
341 lemma var_inj_term [iff]: "\<langle>x::var\<rangle> = \<langle>y\<rangle> \<equiv> x = y" |
356 lemma var_inj_term [iff]: "\<langle>x::var\<rangle> = \<langle>y\<rangle> \<equiv> x = y" |
342 by (simp add: var_inj_term_simp) |
357 by (simp add: var_inj_term_simp) |
343 |
358 |
344 instance "list":: (type) inj_term .. |
359 class expr_of = |
345 |
360 fixes expr_of :: "'a \<Rightarrow> expr" |
346 defs (overloaded) |
361 |
347 expr_list_inj_term_def: "\<langle>es::expr list\<rangle> \<equiv> In3 es" |
362 instantiation expr :: expr_of |
|
363 begin |
|
364 |
|
365 definition |
|
366 "expr_of = (\<lambda>(e::expr). e)" |
|
367 |
|
368 instance .. |
|
369 |
|
370 end |
|
371 |
|
372 instantiation list :: (expr_of) inj_term |
|
373 begin |
|
374 |
|
375 definition |
|
376 "\<langle>es::'a list\<rangle> \<equiv> In3 (map expr_of es)" |
|
377 |
|
378 instance .. |
|
379 |
|
380 end |
|
381 |
|
382 lemma expr_list_inj_term_def: |
|
383 "\<langle>es::expr list\<rangle> \<equiv> In3 es" |
|
384 by (simp add: inj_term_list_def expr_of_expr_def) |
348 |
385 |
349 lemma expr_list_inj_term_simp: "\<langle>es::expr list\<rangle> = In3 es" |
386 lemma expr_list_inj_term_simp: "\<langle>es::expr list\<rangle> = In3 es" |
350 by (simp add: expr_list_inj_term_def) |
387 by (simp add: expr_list_inj_term_def) |
351 |
388 |
352 lemma expr_list_inj_term [iff]: "\<langle>x::expr list\<rangle> = \<langle>y\<rangle> \<equiv> x = y" |
389 lemma expr_list_inj_term [iff]: "\<langle>x::expr list\<rangle> = \<langle>y\<rangle> \<equiv> x = y" |