Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
QuotTest.thy
changeset 177 bdfe4388955d
parent 163 3da18bf6886c
child 180 fcacca9588b4
equal deleted inserted replaced
176:3a8978c335f0 177:bdfe4388955d 
     7   var  "nat"
 
     7   var  "nat"
 
     8 | app  "trm" "trm"
 
     8 | app  "trm" "trm"
 
     9 | lam  "nat" "trm"
 
     9 | lam  "nat" "trm"
 
    10 
    10 
    11 axiomatization
 
    11 axiomatization
 
    12   RR :: "trm ⇒ trm ⇒ bool"
 
    12   RR :: "trm \<Rightarrow> trm \<Rightarrow> bool"
 
    13 where
 
    13 where
 
    14   r_eq: "EQUIV RR"
 
    14   r_eq: "EQUIV RR"
 
    15 
    15 
    16 ML {* print_quotdata @{context} *}
 
    16 ML {* print_quotdata @{context} *}
 
    17 
    17 
    42 datatype 'a trm' =
 
    42 datatype 'a trm' =
 
    43   var'  "'a"
 
    43   var'  "'a"
 
    44 | app'  "'a trm'" "'a trm'"
 
    44 | app'  "'a trm'" "'a trm'"
 
    45 | lam'  "'a" "'a trm'"
 
    45 | lam'  "'a" "'a trm'"
 
    46 
    46 
    47 consts R' :: "'a trm' ⇒ 'a trm' ⇒ bool"
 
    47 consts R' :: "'a trm' \<Rightarrow> 'a trm' \<Rightarrow> bool"
 
    48 axioms r_eq': "EQUIV R'"
 
    48 axioms r_eq': "EQUIV R'"
 
    49 
    49 
    50 quotient qtrm' = "'a trm'" / "R'"
 
    50 quotient qtrm' = "'a trm'" / "R'"
 
    51   apply(rule r_eq')
 
    51   apply(rule r_eq')
 
    52   done
 
    52   done
 
    64 datatype t =
 
    64 datatype t =
 
    65   vr "string"
 
    65   vr "string"
 
    66 | ap "t list"
 
    66 | ap "t list"
 
    67 | lm "string" "t"
 
    67 | lm "string" "t"
 
    68 
    68 
    69 consts Rt :: "t ⇒ t ⇒ bool"
 
    69 consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool"
 
    70 axioms t_eq: "EQUIV Rt"
 
    70 axioms t_eq: "EQUIV Rt"
 
    71 
    71 
    72 quotient qt = "t" / "Rt"
 
    72 quotient qt = "t" / "Rt"
 
    73   by (rule t_eq)
 
    73   by (rule t_eq)
 
    74 
    74 
    75 
    75 
    76 ML {*
 
    76 ML {*
 
    77   get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt ⇒ qt) ⇒ qt) ⇒ qt) list) * nat"}
 
    77   get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"}
 
    78   |> fst
 
    78   |> fst
 
    79   |> Syntax.string_of_term @{context}
 
    79   |> Syntax.string_of_term @{context}
 
    80   |> writeln
 
    80   |> writeln
 
    81 *}
 
    81 *}
 
    82 
    82 
    86   |> Syntax.string_of_term @{context}
 
    86   |> Syntax.string_of_term @{context}
 
    87   |> writeln
 
    87   |> writeln
 
    88 *}
 
    88 *}
 
    89 
    89 
    90 ML {*
 
    90 ML {*
 
    91   get_fun absF @{typ t} @{typ qt} @{context} @{typ "(qt ⇒ qt) ⇒ qt"}
 
    91   get_fun absF @{typ t} @{typ qt} @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"}
 
    92   |> fst
 
    92   |> fst
 
    93   |> Syntax.pretty_term @{context}
 
    93   |> Syntax.pretty_term @{context}
 
    94   |> Pretty.string_of
 
    94   |> Pretty.string_of
 
    95   |> writeln
 
    95   |> writeln
 
    96 *}
 
    96 *}
 
    97 
    97 
    98 (* A test whether get_fun works properly
 
    98 (* A test whether get_fun works properly
 
    99 consts bla :: "(t ⇒ t) ⇒ t"
 
    99 consts bla :: "(t \<Rightarrow> t) \<Rightarrow> t"
 
   100 local_setup {*
 
   100 local_setup {*
 
   101   fn lthy => (Toplevel.program (fn () =>
 
   101   fn lthy => (Toplevel.program (fn () =>
 
   102     make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy
 
   102     make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy
 
   103   )) |> snd
 
   103   )) |> snd
 
   104 *}
 
   104 *}
 
   120 
   120 
   121 text {* a test with functions *}
 
   121 text {* a test with functions *}
 
   122 datatype 'a t' =
 
   122 datatype 'a t' =
 
   123   vr' "string"
 
   123   vr' "string"
 
   124 | ap' "('a t') * ('a t')"
 
   124 | ap' "('a t') * ('a t')"
 
   125 | lm' "'a" "string ⇒ ('a t')"
 
   125 | lm' "'a" "string \<Rightarrow> ('a t')"
 
   126 
   126 
   127 consts Rt' :: "('a t') ⇒ ('a t') ⇒ bool"
 
   127 consts Rt' :: "('a t') \<Rightarrow> ('a t') \<Rightarrow> bool"
 
   128 axioms t_eq': "EQUIV Rt'"
 
   128 axioms t_eq': "EQUIV Rt'"
 
   129 
   129 
   130 quotient qt' = "'a t'" / "Rt'"
 
   130 quotient qt' = "'a t'" / "Rt'"
 
   131   apply(rule t_eq')
 
   131   apply(rule t_eq')
 
   132   done
 
   132   done
 
   147 term VR'
 
   147 term VR'
 
   148 term AP'
 
   148 term AP'
 
   149 
   149 
   150 text {* Tests of regularise *}
 
   150 text {* Tests of regularise *}
 
   151 ML {*
 
   151 ML {*
 
   152   cterm_of @{theory} (regularise @{term "λx :: int. x"} @{typ "trm"} @{term "RR"} @{context});
 
   152   cterm_of @{theory} (regularise @{term "\<lambda>x :: int. x"} @{typ "trm"} @{term "RR"} @{context});
 
   153   cterm_of @{theory} (regularise @{term "λx :: trm. x"} @{typ "trm"} @{term "RR"} @{context});
 
   153   cterm_of @{theory} (regularise @{term "\<lambda>x :: trm. x"} @{typ "trm"} @{term "RR"} @{context});
 
   154   cterm_of @{theory} (regularise @{term "∀x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
 
   154   cterm_of @{theory} (regularise @{term "\<forall>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
 
   155   cterm_of @{theory} (regularise @{term "∃x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
 
   155   cterm_of @{theory} (regularise @{term "\<exists>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
 
   156   cterm_of @{theory} (regularise @{term "All (P :: trm ⇒ bool)"} @{typ "trm"} @{term "RR"} @{context});
 
   156   cterm_of @{theory} (regularise @{term "All (P :: trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context});
 
   157 *}
 
   157 *}
 
   158 
   158 
   159 ML {*
 
   159 ML {*
 
   160   cterm_of @{theory} (regularise @{term "∃(y::trm). P (λ(x::trm). y)"} @{typ "trm"}
 
   160   cterm_of @{theory} (regularise @{term "\<exists>(y::trm). P (\<lambda>(x::trm). y)"} @{typ "trm"}
 
   161      @{term "RR"} @{context});
 
   161      @{term "RR"} @{context});
 
   162   cterm_of @{theory} (my_reg @{term "RR"} @{term "∃(y::trm). P (λ(x::trm). y)"})
 
   162   cterm_of @{theory} (my_reg @{term "RR"} @{term "\<exists>(y::trm). P (\<lambda>(x::trm). y)"})
 
   163 *}
 
   163 *}
 
   164 
   164 
   165 ML {*
 
   165 ML {*
 
   166   cterm_of @{theory} (regularise @{term "λx::trm. x"} @{typ "trm"} @{term "RR"} @{context});
 
   166   cterm_of @{theory} (regularise @{term "\<lambda>x::trm. x"} @{typ "trm"} @{term "RR"} @{context});
 
   167   cterm_of @{theory} (my_reg @{term "RR"} @{term "λx::trm. x"})
 
   167   cterm_of @{theory} (my_reg @{term "RR"} @{term "\<lambda>x::trm. x"})
 
   168 *}
 
   168 *}
 
   169 
   169 
   170 ML {*
 
   170 ML {*
 
   171   cterm_of @{theory} (regularise @{term "∀(x::trm) (y::trm). P x y"} @{typ "trm"} @{term "RR"} @{context});
 
   171   cterm_of @{theory} (regularise @{term "\<forall>(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"})
 
   172   cterm_of @{theory} (my_reg @{term "RR"} @{term "\<forall>(x::trm) (y::trm). P x y"})
 
   173 *}
 
   173 *}
 
   174 
   174 
   175 ML {*
 
   175 ML {*
 
   176   cterm_of @{theory} (regularise @{term "∀x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});
 
   176   cterm_of @{theory} (regularise @{term "\<forall>x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});
 
   177   cterm_of @{theory} (my_reg @{term "RR"} @{term "∀x::trm. P x"})
 
   177   cterm_of @{theory} (my_reg @{term "RR"} @{term "\<forall>x::trm. P x"})
 
   178 *}
 
   178 *}
 
   179 
   179 
   180 ML {*
 
   180 ML {*
 
   181   cterm_of @{theory} (regularise @{term "∃x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});
 
   181   cterm_of @{theory} (regularise @{term "\<exists>x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});
 
   182   cterm_of @{theory} (my_reg @{term "RR"} @{term "∃x::trm. P x"})
 
   182   cterm_of @{theory} (my_reg @{term "RR"} @{term "\<exists>x::trm. P x"})
 
   183 *}
 
   183 *}
 
   184 
   184 
   185 (* my version is not eta-expanded, but that should be OK *)
 
   185 (* my version is not eta-expanded, but that should be OK *)
 
   186 ML {*
 
   186 ML {*
 
   187   cterm_of @{theory} (regularise @{term "All (P::trm ⇒ bool)"} @{typ "trm"} @{term "RR"} @{context});
 
   187   cterm_of @{theory} (regularise @{term "All (P::trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context});
 
   188   cterm_of @{theory} (my_reg @{term "RR"} @{term "All (P::trm ⇒ bool)"})
 
   188   cterm_of @{theory} (my_reg @{term "RR"} @{term "All (P::trm \<Rightarrow> bool)"})
 
   189 *}
 
   189 *}
nominal2