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 

     5 

     6 

     8 

     7 locale QUOT_TYPE =

     9 locale QUOT_TYPE =

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

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

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

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

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

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

   174 axiomatization

   176 axiomatization

   175   RR :: "trm \<Rightarrow> trm \<Rightarrow> bool"

   177   RR :: "trm \<Rightarrow> trm \<Rightarrow> bool"

   176 where

   178 where

   177   r_eq: "EQUIV RR"

   179   r_eq: "EQUIV RR"

   178 

   180 

   179 quotient qtrm = trm / "RR"

   183 quotient qtrm = trm / "RR"

   180   apply(rule r_eq)

   184   apply(rule r_eq)

   181   done

   185   done

   182 

   188 

   183 typ qtrm

   189 typ qtrm

   184 term Rep_qtrm

   190 term Rep_qtrm

   185 term REP_qtrm

   191 term REP_qtrm

   186 term Abs_qtrm

   192 term Abs_qtrm

  1416 | OBJ1 "(string * (string \<Rightarrow> obj1)) list"

  1422 | OBJ1 "(string * (string \<Rightarrow> obj1)) list"

  1417 | INVOKE1 "obj1 \<Rightarrow> string"

  1423 | INVOKE1 "obj1 \<Rightarrow> string"

  1418 | UPDATE1 "obj1 \<Rightarrow> string \<Rightarrow> (string \<Rightarrow> obj1)"

  1424 | UPDATE1 "obj1 \<Rightarrow> string \<Rightarrow> (string \<Rightarrow> obj1)"

  1419 *)

  1425 *)

  1420 

  1426 

  1421 end

  1430 end

  1422  

  1431