--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/QuotTest.thy	Fri Oct 23 16:34:20 2009 +0200
@@ -0,0 +1,189 @@
+theory QuotTest
+imports QuotMain
+begin
+
+section {* various tests for quotient types*}
+datatype trm =
+  var  "nat"
+| app  "trm" "trm"
+| lam  "nat" "trm"
+
+axiomatization
+  RR :: "trm ⇒ trm ⇒ bool"
+where
+  r_eq: "EQUIV RR"
+
+ML {* print_quotdata @{context} *}
+
+quotient qtrm = trm / "RR"
+  apply(rule r_eq)
+  done
+
+ML {* print_quotdata @{context} *}
+
+typ qtrm
+term Rep_qtrm
+term REP_qtrm
+term Abs_qtrm
+term ABS_qtrm
+thm QUOT_TYPE_qtrm
+thm QUOTIENT_qtrm
+thm REP_qtrm_def
+
+(* Test interpretation *)
+thm QUOT_TYPE_I_qtrm.thm11
+thm QUOT_TYPE.thm11
+
+print_theorems
+
+thm Rep_qtrm
+
+text {* another test *}
+datatype 'a trm' =
+  var'  "'a"
+| app'  "'a trm'" "'a trm'"
+| lam'  "'a" "'a trm'"
+
+consts R' :: "'a trm' ⇒ 'a trm' ⇒ bool"
+axioms r_eq': "EQUIV R'"
+
+quotient qtrm' = "'a trm'" / "R'"
+  apply(rule r_eq')
+  done
+
+print_theorems
+
+term ABS_qtrm'
+term REP_qtrm'
+thm QUOT_TYPE_qtrm'
+thm QUOTIENT_qtrm'
+thm Rep_qtrm'
+
+
+text {* a test with lists of terms *}
+datatype t =
+  vr "string"
+| ap "t list"
+| lm "string" "t"
+
+consts Rt :: "t ⇒ t ⇒ bool"
+axioms t_eq: "EQUIV Rt"
+
+quotient qt = "t" / "Rt"
+  by (rule t_eq)
+
+
+ML {*
+  get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt ⇒ qt) ⇒ qt) ⇒ qt) list) * nat"}
+  |> fst
+  |> Syntax.string_of_term @{context}
+  |> writeln
+*}
+
+ML {*
+  get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt * nat"}
+  |> fst
+  |> Syntax.string_of_term @{context}
+  |> writeln
+*}
+
+ML {*
+  get_fun absF @{typ t} @{typ qt} @{context} @{typ "(qt ⇒ qt) ⇒ qt"}
+  |> fst
+  |> Syntax.pretty_term @{context}
+  |> Pretty.string_of
+  |> writeln
+*}
+
+(* A test whether get_fun works properly
+consts bla :: "(t ⇒ t) ⇒ t"
+local_setup {*
+  fn lthy => (Toplevel.program (fn () =>
+    make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy
+  )) |> snd
+*}
+*)
+
+local_setup {*
+  make_const_def @{binding VR} @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd #>
+  make_const_def @{binding AP} @{term "ap"} NoSyn @{typ "t"} @{typ "qt"} #> snd #>
+  make_const_def @{binding LM} @{term "lm"} NoSyn @{typ "t"} @{typ "qt"} #> snd
+*}
+
+term vr
+term ap
+term lm
+thm VR_def AP_def LM_def
+term LM
+term VR
+term AP
+
+text {* a test with functions *}
+datatype 'a t' =
+  vr' "string"
+| ap' "('a t') * ('a t')"
+| lm' "'a" "string ⇒ ('a t')"
+
+consts Rt' :: "('a t') ⇒ ('a t') ⇒ bool"
+axioms t_eq': "EQUIV Rt'"
+
+quotient qt' = "'a t'" / "Rt'"
+  apply(rule t_eq')
+  done
+
+print_theorems
+
+local_setup {*
+  make_const_def @{binding VR'} @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #>
+  make_const_def @{binding AP'} @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #>
+  make_const_def @{binding LM'} @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
+*}
+
+term vr'
+term ap'
+term ap'
+thm VR'_def AP'_def LM'_def
+term LM'
+term VR'
+term AP'
+
+text {* Tests of regularise *}
+ML {*
+  cterm_of @{theory} (regularise @{term "λx :: int. x"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (regularise @{term "λx :: trm. x"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (regularise @{term "∀x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (regularise @{term "∃x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (regularise @{term "All (P :: trm ⇒ bool)"} @{typ "trm"} @{term "RR"} @{context});
+*}
+
+ML {*
+  cterm_of @{theory} (regularise @{term "∃(y::trm). P (λ(x::trm). y)"} @{typ "trm"}
+     @{term "RR"} @{context});
+  cterm_of @{theory} (my_reg @{term "RR"} @{term "∃(y::trm). P (λ(x::trm). y)"})
+*}
+
+ML {*
+  cterm_of @{theory} (regularise @{term "λx::trm. x"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (my_reg @{term "RR"} @{term "λx::trm. x"})
+*}
+
+ML {*
+  cterm_of @{theory} (regularise @{term "∀(x::trm) (y::trm). P x y"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (my_reg @{term "RR"} @{term "∀(x::trm) (y::trm). P x y"})
+*}
+
+ML {*
+  cterm_of @{theory} (regularise @{term "∀x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (my_reg @{term "RR"} @{term "∀x::trm. P x"})
+*}
+
+ML {*
+  cterm_of @{theory} (regularise @{term "∃x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (my_reg @{term "RR"} @{term "∃x::trm. P x"})
+*}
+
+(* my version is not eta-expanded, but that should be OK *)
+ML {*
+  cterm_of @{theory} (regularise @{term "All (P::trm ⇒ bool)"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (my_reg @{term "RR"} @{term "All (P::trm ⇒ bool)"})
+*}