diff -r ae254a6d685c -r 1e07e38ed6c5 QuotTest.thy
--- a/QuotTest.thy	Mon Dec 07 14:12:29 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,229 +0,0 @@
-theory QuotTest
-imports QuotMain
-begin
-
-
-section {* various tests for quotient types*}
-datatype trm =
-  var  "nat"
-| app  "trm" "trm"
-| lam  "nat" "trm"
-
-axiomatization
-  RR :: "trm \<Rightarrow> trm \<Rightarrow> bool"
-where
-  r_eq: "EQUIV RR"
-
-print_quotients
-
-quotient qtrm = trm / "RR"
-  apply(rule r_eq)
-  done
-
-print_quotients
-
-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' \<Rightarrow> 'a trm' \<Rightarrow> bool"
-axioms r_eq': "EQUIV R'"
-
-quotient qtrm' = "'a trm'" / "R'"
-  apply(rule r_eq')
-  done
-
-print_quotients
-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 \<Rightarrow> t \<Rightarrow> bool"
-axioms t_eq: "EQUIV Rt"
-
-quotient qt = "t" / "Rt"
-  by (rule t_eq)
-
-print_quotients
-
-ML {*
-  get_fun repF [(@{typ qt}, @{typ qt})] @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"}
-  |> Syntax.string_of_term @{context}
-  |> writeln
-*}
-
-ML {*
-  get_fun absF [(@{typ qt}, @{typ t})] @{context} @{typ "qt * nat"}
-  |> Syntax.string_of_term @{context}
-  |> writeln
-*}
-
-ML {*
-  get_fun absF [(@{typ qt}, @{typ t})] @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"}
-  |> Syntax.pretty_term @{context}
-  |> Pretty.string_of
-  |> writeln
-*}
-
-(* A test whether get_fun works properly
-consts bla :: "(t \<Rightarrow> t) \<Rightarrow> t"
-local_setup {*
-    make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy |> snd
-*}
-*)
-
-consts Rl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
-axioms Rl_eq: "EQUIV Rl"
-
-quotient ql = "'a list" / "Rl"
-  by (rule Rl_eq)
-
-ML {* val al = snd (dest_Free (term_of @{cpat "f :: ?'a list"})) *}
-ML {* val aq = snd (dest_Free (term_of @{cpat "f :: ?'a ql"})) *}
-ML {* val ttt = snd (dest_Free (term_of @{cpat "f :: ?'a ql \<Rightarrow> ?'a ql"})) *}
-
-ML {*
-  fst (get_fun absF [(aq, al)] @{context} ttt)
-  |> cterm_of @{theory}
-*}
-
-ML {* val ttt2 = snd (dest_Free (term_of @{cpat "f :: nat ql \<Rightarrow> bool ql \<Rightarrow> 'a ql"})) *}
-
-ML {*
-  fst (get_fun absF [(aq, al), (@{typ "nat ql"}, @{typ "nat list"}), (@{typ "bool ql"}, @{typ "bool list"})] @{context} ttt2)
-  |> cterm_of @{theory}
-*}
-
-quotient_def (for qt)
-  VR ::"string \<Rightarrow> qt"
-where
-  "VR \<equiv> vr"
-
-quotient_def (for qt)
-  AP ::"qt list \<Rightarrow> qt"
-where
-  "AP \<equiv> ap"
-
-quotient_def (for qt)
-  LM ::"string \<Rightarrow> qt \<Rightarrow> qt"
-where
-  "LM \<equiv> lm"
-
-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 \<Rightarrow> ('a t')"
-
-consts Rt' :: "('a t') \<Rightarrow> ('a t') \<Rightarrow> bool"
-axioms t_eq': "EQUIV Rt'"
-
-quotient qt' = "'a t'" / "Rt'"
-  apply(rule t_eq')
-  done
-
-print_quotients
-print_theorems
-
-
-quotient_def (for "'a qt'")
-  VR' ::"string \<Rightarrow> 'a qt"
-where
-  "VR' \<equiv> vr'"
-
-quotient_def (for "'a qt'")
-  AP' ::"('a qt') * ('a qt') \<Rightarrow> 'a qt"
-where
-  "AP' \<equiv> ap'"
-
-quotient_def (for "'a qt'")
-  LM' ::"'a \<Rightarrow> string \<Rightarrow> 'a qt'"
-where
-  "LM' \<equiv> lm'"
-
-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 "\<lambda>x :: int. x"} @{typ "trm"} @{term "RR"} @{context});
-  cterm_of @{theory} (regularise @{term "\<lambda>x :: trm. x"} @{typ "trm"} @{term "RR"} @{context});
-  cterm_of @{theory} (regularise @{term "\<forall>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
-  cterm_of @{theory} (regularise @{term "\<exists>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
-  cterm_of @{theory} (regularise @{term "All (P :: trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context});
-*}
-
-ML {*
-  cterm_of @{theory} (regularise @{term "\<exists>(y::trm). P (\<lambda>(x::trm). y)"} @{typ "trm"}
-     @{term "RR"} @{context});
-  cterm_of @{theory} (my_reg @{term "RR"} @{term "\<exists>(y::trm). P (\<lambda>(x::trm). y)"})
-*}
-
-ML {*
-  cterm_of @{theory} (regularise @{term "\<lambda>x::trm. x"} @{typ "trm"} @{term "RR"} @{context});
-  cterm_of @{theory} (my_reg @{term "RR"} @{term "\<lambda>x::trm. x"})
-*}
-
-ML {*
-  cterm_of @{theory} (regularise @{term "\<forall>(x::trm) (y::trm). P x y"} @{typ "trm"} @{term "RR"} @{context});
-  cterm_of @{theory} (my_reg @{term "RR"} @{term "\<forall>(x::trm) (y::trm). P x y"})
-*}
-
-ML {*
-  cterm_of @{theory} (regularise @{term "\<forall>x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});
-  cterm_of @{theory} (my_reg @{term "RR"} @{term "\<forall>x::trm. P x"})
-*}
-
-ML {*
-  cterm_of @{theory} (regularise @{term "\<exists>x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});
-  cterm_of @{theory} (my_reg @{term "RR"} @{term "\<exists>x::trm. P x"})
-*}
-
-(* my version is not eta-expanded, but that should be OK *)
-ML {*
-  cterm_of @{theory} (regularise @{term "All (P::trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context});
-  cterm_of @{theory} (my_reg @{term "RR"} @{term "All (P::trm \<Rightarrow> bool)"})
-*}