1 theory QuotTest

     2 imports QuotMain

     3 begin

     4 

     5 

     6 section {* various tests for quotient types*}

     7 datatype trm =

     8   var  "nat"

     9 | app  "trm" "trm"

    10 | lam  "nat" "trm"

    11 

    12 axiomatization

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

    14 where

    15   r_eq: "EQUIV RR"

    16 

    17 print_quotients

    18 

    19 quotient qtrm = trm / "RR"

    20   apply(rule r_eq)

    21   done

    22 

    23 print_quotients

    24 

    25 typ qtrm

    26 term Rep_qtrm

    27 term REP_qtrm

    28 term Abs_qtrm

    29 term ABS_qtrm

    30 thm QUOT_TYPE_qtrm

    31 thm QUOTIENT_qtrm

    32 thm REP_qtrm_def

    33 

    34 (* Test interpretation *)

    35 thm QUOT_TYPE_I_qtrm.thm11

    36 thm QUOT_TYPE.thm11

    37 

    38 print_theorems

    39 

    40 thm Rep_qtrm

    41 

    42 text {* another test *}

    43 datatype 'a trm' =

    44   var'  "'a"

    45 | app'  "'a trm'" "'a trm'"

    46 | lam'  "'a" "'a trm'"

    47 

    48 consts R' :: "'a trm' \<Rightarrow> 'a trm' \<Rightarrow> bool"

    49 axioms r_eq': "EQUIV R'"

    50 

    51 quotient qtrm' = "'a trm'" / "R'"

    52   apply(rule r_eq')

    53   done

    54 

    55 print_quotients

    56 print_theorems

    57 

    58 term ABS_qtrm'

    59 term REP_qtrm'

    60 thm QUOT_TYPE_qtrm'

    61 thm QUOTIENT_qtrm'

    62 thm Rep_qtrm'

    63 

    64 

    65 text {* a test with lists of terms *}

    66 datatype t =

    67   vr "string"

    68 | ap "t list"

    69 | lm "string" "t"

    70 

    71 consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool"

    72 axioms t_eq: "EQUIV Rt"

    73 

    74 quotient qt = "t" / "Rt"

    75   by (rule t_eq)

    76 

    77 print_quotients

    78 

    79 ML {*

    80   get_fun repF [(@{typ qt}, @{typ qt})] @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"}

    81   |> Syntax.string_of_term @{context}

    82   |> writeln

    83 *}

    84 

    85 ML {*

    86   get_fun absF [(@{typ qt}, @{typ t})] @{context} @{typ "qt * nat"}

    87   |> Syntax.string_of_term @{context}

    88   |> writeln

    89 *}

    90 

    91 ML {*

    92   get_fun absF [(@{typ qt}, @{typ t})] @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"}

    93   |> Syntax.pretty_term @{context}

    94   |> Pretty.string_of

    95   |> writeln

    96 *}

    97 

    98 (* A test whether get_fun works properly

    99 consts bla :: "(t \<Rightarrow> t) \<Rightarrow> t"

   100 local_setup {*

   101     make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy |> snd

   102 *}

   103 *)

   104 

   105 consts Rl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"

   106 axioms Rl_eq: "EQUIV Rl"

   107 

   108 quotient ql = "'a list" / "Rl"

   109   by (rule Rl_eq)

   110 

   111 ML {* val al = snd (dest_Free (term_of @{cpat "f :: ?'a list"})) *}

   112 ML {* val aq = snd (dest_Free (term_of @{cpat "f :: ?'a ql"})) *}

   113 ML {* val ttt = snd (dest_Free (term_of @{cpat "f :: ?'a ql \<Rightarrow> ?'a ql"})) *}

   114 

   115 ML {*

   116   fst (get_fun absF [(aq, al)] @{context} ttt)

   117   |> cterm_of @{theory}

   118 *}

   119 

   120 ML {* val ttt2 = snd (dest_Free (term_of @{cpat "f :: nat ql \<Rightarrow> bool ql \<Rightarrow> 'a ql"})) *}

   121 

   122 ML {*

   123   fst (get_fun absF [(aq, al), (@{typ "nat ql"}, @{typ "nat list"}), (@{typ "bool ql"}, @{typ "bool list"})] @{context} ttt2)

   124   |> cterm_of @{theory}

   125 *}

   126 

   127 quotient_def (for qt)

   128   VR ::"string \<Rightarrow> qt"

   129 where

   130   "VR \<equiv> vr"

   131 

   132 quotient_def (for qt)

   133   AP ::"qt list \<Rightarrow> qt"

   134 where

   135   "AP \<equiv> ap"

   136 

   137 quotient_def (for qt)

   138   LM ::"string \<Rightarrow> qt \<Rightarrow> qt"

   139 where

   140   "LM \<equiv> lm"

   141 

   142 term vr

   143 term ap

   144 term lm

   145 thm VR_def AP_def LM_def

   146 term LM

   147 term VR

   148 term AP

   149 

   150 text {* a test with functions *}

   151 datatype 'a t' =

   152   vr' "string"

   153 | ap' "('a t') * ('a t')"

   154 | lm' "'a" "string \<Rightarrow> ('a t')"

   155 

   156 consts Rt' :: "('a t') \<Rightarrow> ('a t') \<Rightarrow> bool"

   157 axioms t_eq': "EQUIV Rt'"

   158 

   159 quotient qt' = "'a t'" / "Rt'"

   160   apply(rule t_eq')

   161   done

   162 

   163 print_quotients

   164 print_theorems

   165 

   166 

   167 quotient_def (for "'a qt'")

   168   VR' ::"string \<Rightarrow> 'a qt"

   169 where

   170   "VR' \<equiv> vr'"

   171 

   172 quotient_def (for "'a qt'")

   173   AP' ::"('a qt') * ('a qt') \<Rightarrow> 'a qt"

   174 where

   175   "AP' \<equiv> ap'"

   176 

   177 quotient_def (for "'a qt'")

   178   LM' ::"'a \<Rightarrow> string \<Rightarrow> 'a qt'"

   179 where

   180   "LM' \<equiv> lm'"

   181 

   182 term vr'

   183 term ap'

   184 term ap'

   185 thm VR'_def AP'_def LM'_def

   186 term LM'

   187 term VR'

   188 term AP'

   189 

   190 text {* Tests of regularise *}

   191 ML {*

   192   cterm_of @{theory} (regularise @{term "\<lambda>x :: int. x"} @{typ "trm"} @{term "RR"} @{context});

   193   cterm_of @{theory} (regularise @{term "\<lambda>x :: trm. x"} @{typ "trm"} @{term "RR"} @{context});

   194   cterm_of @{theory} (regularise @{term "\<forall>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});

   195   cterm_of @{theory} (regularise @{term "\<exists>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});

   196   cterm_of @{theory} (regularise @{term "All (P :: trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context});

   197 *}

   198 

   199 ML {*

   200   cterm_of @{theory} (regularise @{term "\<exists>(y::trm). P (\<lambda>(x::trm). y)"} @{typ "trm"}

   201      @{term "RR"} @{context});

   202   cterm_of @{theory} (my_reg @{term "RR"} @{term "\<exists>(y::trm). P (\<lambda>(x::trm). y)"})

   203 *}

   204 

   205 ML {*

   206   cterm_of @{theory} (regularise @{term "\<lambda>x::trm. x"} @{typ "trm"} @{term "RR"} @{context});

   207   cterm_of @{theory} (my_reg @{term "RR"} @{term "\<lambda>x::trm. x"})

   208 *}

   209 

   210 ML {*

   211   cterm_of @{theory} (regularise @{term "\<forall>(x::trm) (y::trm). P x y"} @{typ "trm"} @{term "RR"} @{context});

   212   cterm_of @{theory} (my_reg @{term "RR"} @{term "\<forall>(x::trm) (y::trm). P x y"})

   213 *}

   214 

   215 ML {*

   216   cterm_of @{theory} (regularise @{term "\<forall>x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});

   217   cterm_of @{theory} (my_reg @{term "RR"} @{term "\<forall>x::trm. P x"})

   218 *}

   219 

   220 ML {*

   221   cterm_of @{theory} (regularise @{term "\<exists>x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});

   222   cterm_of @{theory} (my_reg @{term "RR"} @{term "\<exists>x::trm. P x"})

   223 *}

   224 

   225 (* my version is not eta-expanded, but that should be OK *)

   226 ML {*

   227   cterm_of @{theory} (regularise @{term "All (P::trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context});

   228   cterm_of @{theory} (my_reg @{term "RR"} @{term "All (P::trm \<Rightarrow> bool)"})

   229 *}