theory QuotMain

imports QuotScript QuotList Prove

uses ("quotient.ML")

begin

locale QUOT_TYPE =

  fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

  and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"

  and   Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"

  assumes equiv: "EQUIV R"

  and     rep_prop: "\<And>y. \<exists>x. Rep y = R x"

  and     rep_inverse: "\<And>x. Abs (Rep x) = x"

  and     abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"

  and     rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"

begin

definition

  "ABS x \<equiv> Abs (R x)"

definition

  "REP a = Eps (Rep a)"

lemma lem9:

  shows "R (Eps (R x)) = R x"

proof -

  have a: "R x x" using equiv by (simp add: EQUIV_REFL_SYM_TRANS REFL_def)

  then have "R x (Eps (R x))" by (rule someI)

  then show "R (Eps (R x)) = R x"

    using equiv unfolding EQUIV_def by simp

qed

theorem thm10:

  shows "ABS (REP a) \<equiv> a"

  apply  (rule eq_reflection)

  unfolding ABS_def REP_def

proof -

  from rep_prop

  obtain x where eq: "Rep a = R x" by auto

  have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp

  also have "\<dots> = Abs (R x)" using lem9 by simp

  also have "\<dots> = Abs (Rep a)" using eq by simp

  also have "\<dots> = a" using rep_inverse by simp

  finally

  show "Abs (R (Eps (Rep a))) = a" by simp

qed

lemma REP_refl:

  shows "R (REP a) (REP a)"

unfolding REP_def

by (simp add: equiv[simplified EQUIV_def])

lemma lem7:

  shows "(R x = R y) = (Abs (R x) = Abs (R y))"

apply(rule iffI)

apply(simp)

apply(drule rep_inject[THEN iffD2])

apply(simp add: abs_inverse)

done

theorem thm11:

  shows "R r r' = (ABS r = ABS r')"

unfolding ABS_def

by (simp only: equiv[simplified EQUIV_def] lem7)

lemma REP_ABS_rsp:

  shows "R f (REP (ABS g)) = R f g"

  and   "R (REP (ABS g)) f = R g f"

by (simp_all add: thm10 thm11)

lemma QUOTIENT:

  "QUOTIENT R ABS REP"

apply(unfold QUOTIENT_def)

apply(simp add: thm10)

apply(simp add: REP_refl)

apply(subst thm11[symmetric])

apply(simp add: equiv[simplified EQUIV_def])

done

lemma R_trans:

  assumes ab: "R a b"

  and     bc: "R b c"

  shows "R a c"

proof -

  have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp

  moreover have ab: "R a b" by fact

  moreover have bc: "R b c" by fact

  ultimately show "R a c" unfolding TRANS_def by blast

qed

lemma R_sym:

  assumes ab: "R a b"

  shows "R b a"

proof -

  have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp

  then show "R b a" using ab unfolding SYM_def by blast

qed

lemma R_trans2:

  assumes ac: "R a c"

  and     bd: "R b d"

  shows "R a b = R c d"

proof

  assume "R a b"

  then have "R b a" using R_sym by blast

  then have "R b c" using ac R_trans by blast

  then have "R c b" using R_sym by blast

  then show "R c d" using bd R_trans by blast

next

  assume "R c d"

  then have "R a d" using ac R_trans by blast

  then have "R d a" using R_sym by blast

  then have "R b a" using bd R_trans by blast

  then show "R a b" using R_sym by blast

qed

lemma REPS_same:

  shows "R (REP a) (REP b) \<equiv> (a = b)"

proof -

  have "R (REP a) (REP b) = (a = b)"

  proof

    assume as: "R (REP a) (REP b)"

    from rep_prop

    obtain x y

      where eqs: "Rep a = R x" "Rep b = R y" by blast

    from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp

    then have "R x (Eps (R y))" using lem9 by simp

    then have "R (Eps (R y)) x" using R_sym by blast

    then have "R y x" using lem9 by simp

    then have "R x y" using R_sym by blast

    then have "ABS x = ABS y" using thm11 by simp

    then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp

    then show "a = b" using rep_inverse by simp

  next

    assume ab: "a = b"

    have "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp

    then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto

  qed

  then show "R (REP a) (REP b) \<equiv> (a = b)" by simp

qed

end

section {* type definition for the quotient type *}

use "quotient.ML"

ML {*

val no_vars = Thm.rule_attribute (fn context => fn th =>

  let

    val ctxt = Variable.set_body false (Context.proof_of context);

    val ((_, [th']), _) = Variable.import true [th] ctxt;

  in th' end);

*}

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"

local_setup {*

  typedef_main (@{binding "qtrm"}, NoSyn, @{term "RR"}, @{typ trm}, @{thm r_eq}) #> snd

*}

term Rep_qtrm

term REP_qtrm

term Abs_qtrm

term ABS_qtrm

thm QUOT_TYPE_qtrm

thm QUOTIENT_qtrm

(* 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'"

local_setup {*

  typedef_main (@{binding "qtrm'"}, NoSyn, @{term "R'"}, @{typ "'a trm'"}, @{thm r_eq'}) #> snd

*}

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"

local_setup {*

  typedef_main (@{binding "qt"}, NoSyn, @{term "Rt"}, @{typ "t"}, @{thm t_eq}) #> snd

*}

section {* lifting of constants *}

text {* information about map-functions for type-constructor *}

ML {*

type typ_info = {mapfun: string}

local

  structure Data = TheoryDataFun

  (type T = typ_info Symtab.table

   val empty = Symtab.empty

   val copy = I

   val extend = I

   fun merge _ = Symtab.merge (K true))

in

  val lookup = Symtab.lookup o Data.get

  fun update k v = Data.map (Symtab.update (k, v))

end

*}

(* mapfuns for some standard types *)

setup {*

  update @{type_name "list"} {mapfun = @{const_name "map"}} #> 

  update @{type_name "*"}    {mapfun = @{const_name "prod_fun"}} #> 

  update @{type_name "fun"}  {mapfun = @{const_name "fun_map"}}

*}

ML {* lookup @{theory} @{type_name list} *}

ML {*

datatype flag = absF | repF

fun get_fun flag rty qty lthy ty =

let

  val qty_name = Long_Name.base_name (fst (dest_Type qty))

  fun get_fun_aux s fs_tys =

  let

    val (fs, tys) = split_list fs_tys

    val (otys, ntys) = split_list tys

    val oty = Type (s, otys)

    val nty = Type (s, ntys)

    val ftys = map (op -->) tys

  in

   (case (lookup (ProofContext.theory_of lthy) s) of

      SOME info => (list_comb (Const (#mapfun info, ftys ---> oty --> nty), fs), (oty, nty))

    | NONE      => raise ERROR ("no map association for type " ^ s))

  end

  fun get_const absF = (Const ("QuotMain.ABS_" ^ qty_name, rty --> qty), (rty, qty))

    | get_const repF = (Const ("QuotMain.REP_" ^ qty_name, qty --> rty), (qty, rty))

  fun mk_identity ty = Abs ("", ty, Bound 0)

in

  if ty = qty

  then (get_const flag)

  else (case ty of

          TFree _ => (mk_identity ty, (ty, ty))

        | Type (_, []) => (mk_identity ty, (ty, ty))

        | Type (s, tys) => get_fun_aux s (map (get_fun flag rty qty lthy) tys)

        | _ => raise ERROR ("no type variables")

       )

end

*}

ML {*

  get_fun repF @{typ t} @{typ qt} @{context} @{typ "t * nat"}

  |> fst

  |> Syntax.string_of_term @{context}

  |> writeln

*}

ML {*

  get_fun absF @{typ t} @{typ qt} @{context} @{typ "t * nat"}

  |> fst

  |> Syntax.string_of_term @{context}

  |> writeln

*}

text {* produces the definition for a lifted constant *}

ML {*

fun get_const_def nconst oconst rty qty lthy =

let

  val ty = fastype_of nconst

  val (arg_tys, res_ty) = strip_type ty

  val fresh_args = arg_tys |> map (pair "x")

                           |> Variable.variant_frees lthy [nconst, oconst]

                           |> map Free

  val rep_fns = map (fst o get_fun repF rty qty lthy) arg_tys

  val abs_fn  = (fst o get_fun absF rty qty lthy) res_ty

in

  map (op $) (rep_fns ~~ fresh_args)

  |> curry list_comb oconst

  |> curry (op $) abs_fn

  |> fold_rev lambda fresh_args

end

*}

ML {*

fun exchange_ty rty qty ty =

  if ty = rty

  then qty

  else

    (case ty of

       Type (s, tys) => Type (s, map (exchange_ty rty qty) tys)

      | _ => ty

    )

*}

ML {*

fun make_const_def nconst_bname oconst mx rty qty lthy =

let

  val oconst_ty = fastype_of oconst

  val nconst_ty = exchange_ty rty qty oconst_ty

  val nconst = Const (Binding.name_of nconst_bname, nconst_ty)

  val def_trm = get_const_def nconst oconst rty qty lthy

in

  make_def (nconst_bname, mx, def_trm) lthy

end

*}

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'"

local_setup {*

  typedef_main (@{binding "qt'"}, NoSyn, @{term "Rt'"}, @{typ "'a t'"}, @{thm t_eq'}) #> snd

*}

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 {* finite set example *}

print_syntax

inductive

  list_eq (infix "\<approx>" 50)

where

  "a#b#xs \<approx> b#a#xs"

| "[] \<approx> []"

| "xs \<approx> ys \<Longrightarrow> ys \<approx> xs"

| "a#a#xs \<approx> a#xs"

| "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys"

| "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3"

lemma list_eq_refl:

  shows "xs \<approx> xs"

  apply (induct xs)

   apply (auto intro: list_eq.intros)

  done

lemma equiv_list_eq:

  shows "EQUIV list_eq"

  unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def

  apply(auto intro: list_eq.intros list_eq_refl)

  done

local_setup {*

  typedef_main (@{binding "fset"}, NoSyn, @{term "list_eq"}, @{typ "'a list"}, @{thm "equiv_list_eq"}) #> snd

*}

print_theorems

typ "'a fset"

thm "Rep_fset"

local_setup {*

  make_const_def @{binding EMPTY} @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd

*}

term Nil

term EMPTY

thm EMPTY_def

local_setup {*

  make_const_def @{binding INSERT} @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd

*}

term Cons

term INSERT

thm INSERT_def

local_setup {*

  make_const_def @{binding UNION} @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd

*}

term append

term UNION

thm UNION_def

thm QUOTIENT_fset

thm QUOT_TYPE_I_fset.thm11

fun

  membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infix "memb" 100)

where

  m1: "(x memb []) = False"

| m2: "(x memb (y#xs)) = ((x=y) \<or> (x memb xs))"

lemma mem_respects:

  fixes z

  assumes a: "list_eq x y"

  shows "(z memb x) = (z memb y)"

  using a by induct auto

fun

  card1 :: "'a list \<Rightarrow> nat"

where

  card1_nil: "(card1 []) = 0"

| card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))"

local_setup {*

  make_const_def @{binding card} @{term "card1"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd

*}

term card1

term card

thm card_def

(* text {*

 Maybe make_const_def should require a theorem that says that the particular lifted function

 respects the relation. With it such a definition would be impossible:

 make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd

*}*)

lemma card1_rsp:

  fixes a b :: "'a list"

  assumes e: "a \<approx> b"

  shows "card1 a = card1 b"

  using e apply induct

  apply (simp_all add:mem_respects)

  done

lemma card1_0:

  fixes a :: "'a list"