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 {*
Toplevel.context_of;
Toplevel.keep
*}

ML {*
  get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> 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 \<Rightarrow> qt) \<Rightarrow> qt"}
  |> fst
  |> Syntax.pretty_term @{context}
  |> Pretty.string_of
  |> writeln
*}

(* A test whether get_fun works properly
consts bla :: "(t \<Rightarrow> t) \<Rightarrow> 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 \<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

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 "\<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)"})
*}