1 theory QuotTest

     2 imports QuotMain

     3 begin

     4 

     5 section {* various tests for quotient types*}

     6 datatype trm =

     7   var  "nat"

     8 | app  "trm" "trm"

     9 | lam  "nat" "trm"

    10 

    11 axiomatization

    12   RR :: "trm ⇒ trm ⇒ bool"

    13 where

    14   r_eq: "EQUIV RR"

    15 

    16 ML {* print_quotdata @{context} *}

    17 

    18 quotient qtrm = trm / "RR"

    19   apply(rule r_eq)

    20   done

    21 

    22 ML {* print_quotdata @{context} *}

    23 

    24 typ qtrm

    25 term Rep_qtrm

    26 term REP_qtrm

    27 term Abs_qtrm

    28 term ABS_qtrm

    29 thm QUOT_TYPE_qtrm

    30 thm QUOTIENT_qtrm

    31 thm REP_qtrm_def

    32 

    33 (* Test interpretation *)

    34 thm QUOT_TYPE_I_qtrm.thm11

    35 thm QUOT_TYPE.thm11

    36 

    37 print_theorems

    38 

    39 thm Rep_qtrm

    40 

    41 text {* another test *}

    42 datatype 'a trm' =

    43   var'  "'a"

    44 | app'  "'a trm'" "'a trm'"

    45 | lam'  "'a" "'a trm'"

    46 

    47 consts R' :: "'a trm' ⇒ 'a trm' ⇒ bool"

    48 axioms r_eq': "EQUIV R'"

    49 

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

    51   apply(rule r_eq')

    52   done

    53 

    54 print_theorems

    55 

    56 term ABS_qtrm'

    57 term REP_qtrm'

    58 thm QUOT_TYPE_qtrm'

    59 thm QUOTIENT_qtrm'

    60 thm Rep_qtrm'

    61 

    62 

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

    64 datatype t =

    65   vr "string"

    66 | ap "t list"

    67 | lm "string" "t"

    68 

    69 consts Rt :: "t ⇒ t ⇒ bool"

    70 axioms t_eq: "EQUIV Rt"

    71 

    72 quotient qt = "t" / "Rt"

    73   by (rule t_eq)

    74 

    75 

    76 ML {*

    77   get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt ⇒ qt) ⇒ qt) ⇒ qt) list) * nat"}

    78   |> fst

    79   |> Syntax.string_of_term @{context}

    80   |> writeln

    81 *}

    82 

    83 ML {*

    84   get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt * nat"}

    85   |> fst

    86   |> Syntax.string_of_term @{context}

    87   |> writeln

    88 *}

    89 

    90 ML {*

    91   get_fun absF @{typ t} @{typ qt} @{context} @{typ "(qt ⇒ qt) ⇒ qt"}

    92   |> fst

    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 ⇒ t) ⇒ t"

   100 local_setup {*

   101   fn lthy => (Toplevel.program (fn () =>

   102     make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy

   103   )) |> snd

   104 *}

   105 *)

   106 

   107 local_setup {*

   108   make_const_def @{binding VR} @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd #>

   109   make_const_def @{binding AP} @{term "ap"} NoSyn @{typ "t"} @{typ "qt"} #> snd #>

   110   make_const_def @{binding LM} @{term "lm"} NoSyn @{typ "t"} @{typ "qt"} #> snd

   111 *}

   112 

   113 term vr

   114 term ap

   115 term lm

   116 thm VR_def AP_def LM_def

   117 term LM

   118 term VR

   119 term AP

   120 

   121 text {* a test with functions *}

   122 datatype 'a t' =

   123   vr' "string"

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

   125 | lm' "'a" "string ⇒ ('a t')"

   126 

   127 consts Rt' :: "('a t') ⇒ ('a t') ⇒ bool"

   128 axioms t_eq': "EQUIV Rt'"

   129 

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

   131   apply(rule t_eq')

   132   done

   133 

   134 print_theorems

   135 

   136 local_setup {*

   137   make_const_def @{binding VR'} @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #>

   138   make_const_def @{binding AP'} @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #>

   139   make_const_def @{binding LM'} @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd

   140 *}

   141 

   142 term vr'

   143 term ap'

   144 term ap'

   145 thm VR'_def AP'_def LM'_def

   146 term LM'

   147 term VR'

   148 term AP'

   149 

   150 text {* Tests of regularise *}

   151 ML {*

   152   cterm_of @{theory} (regularise @{term "λx :: int. x"} @{typ "trm"} @{term "RR"} @{context});

   153   cterm_of @{theory} (regularise @{term "λx :: trm. x"} @{typ "trm"} @{term "RR"} @{context});

   154   cterm_of @{theory} (regularise @{term "∀x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});

   155   cterm_of @{theory} (regularise @{term "∃x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});

   156   cterm_of @{theory} (regularise @{term "All (P :: trm ⇒ bool)"} @{typ "trm"} @{term "RR"} @{context});

   157 *}

   158 

   159 ML {*

   160   cterm_of @{theory} (regularise @{term "∃(y::trm). P (λ(x::trm). y)"} @{typ "trm"}

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

   162   cterm_of @{theory} (my_reg @{term "RR"} @{term "∃(y::trm). P (λ(x::trm). y)"})

   163 *}

   164 

   165 ML {*

   166   cterm_of @{theory} (regularise @{term "λx::trm. x"} @{typ "trm"} @{term "RR"} @{context});

   167   cterm_of @{theory} (my_reg @{term "RR"} @{term "λx::trm. x"})

   168 *}

   169 

   170 ML {*

   171   cterm_of @{theory} (regularise @{term "∀(x::trm) (y::trm). P x y"} @{typ "trm"} @{term "RR"} @{context});

   172   cterm_of @{theory} (my_reg @{term "RR"} @{term "∀(x::trm) (y::trm). P x y"})

   173 *}

   174 

   175 ML {*

   176   cterm_of @{theory} (regularise @{term "∀x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});

   177   cterm_of @{theory} (my_reg @{term "RR"} @{term "∀x::trm. P x"})

   178 *}

   179 

   180 ML {*

   181   cterm_of @{theory} (regularise @{term "∃x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});

   182   cterm_of @{theory} (my_reg @{term "RR"} @{term "∃x::trm. P x"})

   183 *}

   184 

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

   186 ML {*

   187   cterm_of @{theory} (regularise @{term "All (P::trm ⇒ bool)"} @{typ "trm"} @{term "RR"} @{context});

   188   cterm_of @{theory} (my_reg @{term "RR"} @{term "All (P::trm ⇒ bool)"})

   189 *}