1 theory QuotMain

     1 theory QuotMain

     2 imports QuotScript QuotList Prove

     2 imports QuotScript QuotList Prove

     3 uses ("quotient.ML")

     3 uses ("quotient.ML")

     4 begin

     4 begin

     5 

     6 

     6 locale QUOT_TYPE =

     7 locale QUOT_TYPE =

     7   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

     8   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

     8   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"

     9   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"

     9   and   Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"

    10   and   Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"

   139   then show "R (REP a) (REP b) \<equiv> (a = b)" by simp

   140   then show "R (REP a) (REP b) \<equiv> (a = b)" by simp

   140 qed

   141 qed

   141 

   142 

   142 end

   143 end

   143 

   144 

   144 section {* type definition for the quotient type *}

   146 section {* type definition for the quotient type *}

   145 

   147 

   146 use "quotient.ML"

   148 use "quotient.ML"

   147 

   149 

   148 term EQUIV

   150 term EQUIV

   247   update @{type_name "fun"}  {mapfun = @{const_name "fun_map"},  relfun = @{const_name "FUN_REL"}}

   249   update @{type_name "fun"}  {mapfun = @{const_name "fun_map"},  relfun = @{const_name "FUN_REL"}}

   248 *}

   250 *}

   249 

   251 

   250 

   252 

   251 ML {* lookup @{theory} @{type_name list} *}

   253 ML {* lookup @{theory} @{type_name list} *}

   253 

   254 

   254 ML {*

   255 ML {*

   255 (* calculates the aggregate abs and rep functions for a given type; 

   256 (* calculates the aggregate abs and rep functions for a given type; 

   256    repF is for constants' arguments; absF is for constants;

   257    repF is for constants' arguments; absF is for constants;

   257    function types need to be treated specially, since repF and absF

   258    function types need to be treated specially, since repF and absF