src/HOL/Types_To_Sets/Examples/Prerequisites.thy
changeset 64551 79e9587dbcca
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Types_To_Sets/Examples/Prerequisites.thy	Mon Dec 12 11:33:14 2016 +0100
     1.3 @@ -0,0 +1,25 @@
     1.4 +(*  Title:      HOL/Types_To_Sets/Examples/Prerequisites.thy
     1.5 +    Author:     Ondřej Kunčar, TU München
     1.6 +*)
     1.7 +
     1.8 +theory Prerequisites
     1.9 +  imports Main
    1.10 +begin
    1.11 +
    1.12 +context
    1.13 +  fixes Rep Abs A T
    1.14 +  assumes type: "type_definition Rep Abs A"
    1.15 +  assumes T_def: "T \<equiv> (\<lambda>(x::'a) (y::'b). x = Rep y)"
    1.16 +begin
    1.17 +
    1.18 +lemma type_definition_Domainp: "Domainp T = (\<lambda>x. x \<in> A)"
    1.19 +proof -
    1.20 +  interpret type_definition Rep Abs A by(rule type)
    1.21 +  show ?thesis
    1.22 +    unfolding Domainp_iff[abs_def] T_def fun_eq_iff
    1.23 +    by (metis Abs_inverse Rep)
    1.24 +qed
    1.25 +
    1.26 +end
    1.27 +
    1.28 +end