equal
deleted
inserted
replaced
539 |
539 |
540 text {* A completely unspecified non-empty subset of @{typ "'a"}: *} |
540 text {* A completely unspecified non-empty subset of @{typ "'a"}: *} |
541 |
541 |
542 definition "myTdef = insert (undefined::'a) (undefined::'a set)" |
542 definition "myTdef = insert (undefined::'a) (undefined::'a set)" |
543 |
543 |
544 typedef (open) 'a myTdef = "myTdef :: 'a set" |
544 typedef 'a myTdef = "myTdef :: 'a set" |
545 unfolding myTdef_def by auto |
545 unfolding myTdef_def by auto |
546 |
546 |
547 lemma "(x\<Colon>'a myTdef) = y" |
547 lemma "(x\<Colon>'a myTdef) = y" |
548 nitpick [expect = genuine] |
548 nitpick [expect = genuine] |
549 oops |
549 oops |
550 |
550 |
551 typedecl myTdecl |
551 typedecl myTdecl |
552 |
552 |
553 definition "T_bij = {(f::'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}" |
553 definition "T_bij = {(f::'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}" |
554 |
554 |
555 typedef (open) 'a T_bij = "T_bij :: ('a \<Rightarrow> 'a) set" |
555 typedef 'a T_bij = "T_bij :: ('a \<Rightarrow> 'a) set" |
556 unfolding T_bij_def by auto |
556 unfolding T_bij_def by auto |
557 |
557 |
558 lemma "P (f\<Colon>(myTdecl myTdef) T_bij)" |
558 lemma "P (f\<Colon>(myTdecl myTdef) T_bij)" |
559 nitpick [expect = genuine] |
559 nitpick [expect = genuine] |
560 oops |
560 oops |