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

*}