equal
deleted
inserted
replaced
178 end |
178 end |
179 *} |
179 *} |
180 |
180 |
181 text {* two wrappers for define and note *} |
181 text {* two wrappers for define and note *} |
182 ML {* |
182 ML {* |
183 fun make_def (name, mx, trm) lthy = |
183 fun make_def (name, mx, rhs) lthy = |
184 let |
184 let |
185 val ((trm, (_ , thm)), lthy') = |
185 val ((rhs, (_ , thm)), lthy') = |
186 LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, trm)) lthy |
186 LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, rhs)) lthy |
187 in |
187 in |
188 ((trm, thm), lthy') |
188 ((rhs, thm), lthy') |
189 end |
189 end |
190 *} |
190 *} |
191 |
191 |
192 ML {* |
192 ML {* |
193 fun reg_thm (name, thm) lthy = |
193 fun reg_thm (name, thm) lthy = |
444 Type (s, tys) => Type (s, map (exchange_ty rty qty) tys) |
444 Type (s, tys) => Type (s, map (exchange_ty rty qty) tys) |
445 | _ => ty) |
445 | _ => ty) |
446 *} |
446 *} |
447 |
447 |
448 ML {* |
448 ML {* |
449 fun make_const_def nconst_name oconst mx rty qty lthy = |
449 fun make_const_def nconst_bname oconst mx rty qty lthy = |
450 let |
450 let |
451 val oconst_ty = fastype_of oconst |
451 val oconst_ty = fastype_of oconst |
452 val nconst_ty = exchange_ty rty qty oconst_ty |
452 val nconst_ty = exchange_ty rty qty oconst_ty |
453 val nconst = Const (nconst_name, nconst_ty) |
453 val nconst = Const (Binding.name_of nconst_bname, nconst_ty) |
454 val def_trm = get_const_def nconst oconst rty qty lthy |
454 val def_trm = get_const_def nconst oconst rty qty lthy |
455 in |
455 in |
456 make_def (Binding.name nconst_name, mx, def_trm) lthy |
456 make_def (nconst_bname, mx, def_trm) lthy |
457 end |
457 end |
458 *} |
458 *} |
459 |
459 |
460 local_setup {* |
460 local_setup {* |
461 make_const_def "VR" @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd |
461 make_const_def @{binding VR} @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd |
462 *} |
462 *} |
463 |
463 |
464 local_setup {* |
464 local_setup {* |
465 make_const_def "AP" @{term "ap"} NoSyn @{typ "t"} @{typ "qt"} #> snd |
465 make_const_def @{binding AP} @{term "ap"} NoSyn @{typ "t"} @{typ "qt"} #> snd |
466 *} |
466 *} |
467 |
467 |
468 local_setup {* |
468 local_setup {* |
469 make_const_def "LM" @{term "lm"} NoSyn @{typ "t"} @{typ "qt"} #> snd |
469 make_const_def @{binding LM} @{term "lm"} NoSyn @{typ "t"} @{typ "qt"} #> snd |
470 *} |
470 *} |
471 |
471 |
472 thm VR_def |
472 thm VR_def |
473 thm AP_def |
473 thm AP_def |
474 thm LM_def |
474 thm LM_def |
492 *} |
492 *} |
493 |
493 |
494 print_theorems |
494 print_theorems |
495 |
495 |
496 local_setup {* |
496 local_setup {* |
497 make_const_def "VR'" @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd |
497 make_const_def @{binding VR'} @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd |
498 *} |
498 *} |
499 |
499 |
500 local_setup {* |
500 local_setup {* |
501 make_const_def "AP'" @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd |
501 make_const_def @{binding AP'} @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd |
502 *} |
502 *} |
503 |
503 |
504 local_setup {* |
504 local_setup {* |
505 make_const_def "LM'" @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd |
505 make_const_def @{binding LM'} @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd |
506 *} |
506 *} |
507 |
507 |
508 thm VR'_def |
508 thm VR'_def |
509 thm AP'_def |
509 thm AP'_def |
510 thm LM'_def |
510 thm LM'_def |
545 |
545 |
546 typ "'a fset" |
546 typ "'a fset" |
547 thm "Rep_fset" |
547 thm "Rep_fset" |
548 |
548 |
549 local_setup {* |
549 local_setup {* |
550 make_const_def "EMPTY" @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
550 make_const_def @{binding EMPTY} @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
551 *} |
551 *} |
552 |
552 |
553 term Nil |
553 term Nil |
554 term EMPTY |
554 term EMPTY |
555 thm EMPTY_def |
555 thm EMPTY_def |
556 |
556 |
557 |
557 |
558 local_setup {* |
558 local_setup {* |
559 make_const_def "INSERT" @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
559 make_const_def @{binding INSERT} @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
560 *} |
560 *} |
561 |
561 |
562 term Cons |
562 term Cons |
563 term INSERT |
563 term INSERT |
564 thm INSERT_def |
564 thm INSERT_def |
565 |
565 |
566 local_setup {* |
566 local_setup {* |
567 make_const_def "UNION" @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
567 make_const_def @{binding UNION} @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
568 *} |
568 *} |
569 |
569 |
570 term append |
570 term append |
571 term UNION |
571 term UNION |
572 thm UNION_def |
572 thm UNION_def |
573 |
573 |
574 local_setup {* |
574 local_setup {* |
575 make_const_def "CARD" @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
575 make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
576 *} |
576 *} |
577 |
577 |
578 term length |
578 term length |
579 term CARD |
579 term CARD |
580 thm CARD_def |
580 thm CARD_def |
618 | NONE => singleton (ProofContext.export ctxt orig_ctxt) t) |
618 | NONE => singleton (ProofContext.export ctxt orig_ctxt) t) |
619 end |
619 end |
620 *} |
620 *} |
621 |
621 |
622 local_setup {* |
622 local_setup {* |
623 make_const_def "IN" @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
623 make_const_def @{binding IN} @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
624 *} |
624 *} |
625 |
625 |
626 term membship |
626 term membship |
627 term IN |
627 term IN |
628 thm IN_def |
628 thm IN_def |