theory QuotMain

imports QuotScript QuotList

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) = a"

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:

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

apply(subst thm11)

apply(simp add: thm10 thm11)

apply(subst thm11)

apply(simp add: thm10 thm11)

done

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

end

section {* type definition for the quotient type *}

ML {*

Variable.variant_frees

*}

ML {*

(* constructs the term \<lambda>(c::ty \<Rightarrow> bool). \<exists>x. c = rel x *)

fun typedef_term rel ty lthy =

let 

  val [x, c] = [("x", ty), ("c", ty --> @{typ bool})] 

               |> Variable.variant_frees lthy [rel]

               |> map Free

in

  lambda c 

    (HOLogic.mk_exists 

       ("x", ty, HOLogic.mk_eq (c, (rel $ x))))

end

*}

ML {*

 typedef_term @{term R} @{typ "nat"} @{context} 

  |> Syntax.string_of_term @{context}

  |> writeln

*}

ML {*

val typedef_tac =  

  EVERY1 [rewrite_goal_tac @{thms mem_def},

          rtac @{thm exI}, rtac @{thm exI}, rtac @{thm refl}]

*}

ML {*

(* makes the new type definitions *)

fun typedef_make (qty_name, rel, ty) lthy =

  LocalTheory.theory_result

  (Typedef.add_typedef false NONE 

     (qty_name, map fst (Term.add_tfreesT ty []), NoSyn)

       (typedef_term rel ty lthy)

         NONE typedef_tac) lthy

*}

text {* proves the QUOT_TYPE theorem for the new type *}

ML {*

fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = 

let

  val rep_thm = #Rep typedef_info

  val rep_inv = #Rep_inverse typedef_info

  val abs_inv = #Abs_inverse typedef_info

  val rep_inj = #Rep_inject typedef_info

  val ss = HOL_basic_ss addsimps @{thms mem_def}

  val rep_thm_simpd = Simplifier.asm_full_simplify ss rep_thm

  val abs_inv_simpd = Simplifier.asm_full_simplify ss abs_inv

in

  EVERY1 [rtac @{thm QUOT_TYPE.intro},

          rtac equiv_thm, 

          rtac rep_thm_simpd, 

          rtac rep_inv, 

          rtac abs_inv_simpd, rtac @{thm exI}, rtac @{thm refl},

          rtac rep_inj]

end

*}

term QUOT_TYPE

ML {* HOLogic.mk_Trueprop *}

ML {* Goal.prove *}

ML {* Syntax.check_term *}

ML {* 

fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =

let

  val quot_type_const = Const (@{const_name "QUOT_TYPE"}, dummyT)

  val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)

             |> Syntax.check_term lthy

in

  Goal.prove lthy [] [] goal

    (fn _ => typedef_quot_type_tac equiv_thm typedef_info)

end

*}

ML {*

fun typedef_quotient_thm_tac defs quot_type_thm =

  EVERY1 [K (rewrite_goals_tac defs), 

          rtac @{thm QUOT_TYPE.QUOTIENT}, 

          rtac quot_type_thm]

*}

ML {* 

fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy =

let

  val quotient_const = Const (@{const_name "QUOTIENT"}, dummyT)

  val goal = HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep)

             |> Syntax.check_term lthy

in

  Goal.prove lthy [] [] goal

    (fn _ => typedef_quotient_thm_tac [abs_def, rep_def] quot_type_thm)

end

*}

text {* two wrappers for define and note *}

ML {* 

fun make_def (name, mx, trm) lthy =

let   

  val ((trm, (_ , thm)), lthy') = 

     LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, trm)) lthy

in

  ((trm, thm), lthy')

end

*}

ML {*

fun reg_thm (name, thm) lthy = 

let

  val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy 

in

  (thm',lthy')

end

*}

ML {* 

fun typedef_main (qty_name, rel, ty, equiv_thm) lthy =

let 

  (* generates typedef *)

  val ((_,typedef_info), lthy') = typedef_make (qty_name, rel, ty) lthy

  (* abs and rep functions *)

  val abs_ty = #abs_type typedef_info

  val rep_ty = #rep_type typedef_info

  val abs_name = #Abs_name typedef_info

  val rep_name = #Rep_name typedef_info

  val abs = Const (abs_name, rep_ty --> abs_ty)

  val rep = Const (rep_name, abs_ty --> rep_ty)

  (* ABS and REP definitions *)

  val ABS_const = Const (@{const_name "QUOT_TYPE.ABS"}, dummyT )

  val REP_const = Const (@{const_name "QUOT_TYPE.REP"}, dummyT )

  val ABS_trm = Syntax.check_term lthy' (ABS_const $ rel $ abs) 

  val REP_trm = Syntax.check_term lthy' (REP_const $ rep) 

  val ABS_name = Binding.prefix_name "ABS_" qty_name

  val REP_name = Binding.prefix_name "REP_" qty_name  

  val (((ABS, ABS_def), (REP, REP_def)), lthy'') = 

         lthy' |> make_def (ABS_name, NoSyn, ABS_trm)

               ||>> make_def (REP_name, NoSyn, REP_trm)

  (* quot_type theorem *)

  val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy''

  val quot_thm_name = Binding.prefix_name "QUOT_TYPE_" qty_name

  (* quotient theorem *)

  val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy''

  val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name

in

  lthy'' 

  |> reg_thm (quot_thm_name, quot_thm)  

  ||>> reg_thm (quotient_thm_name, quotient_thm)

end

*}

section {* various tests for quotient types*}

datatype trm =

  var  "nat" 

| app  "trm" "trm"

| lam  "nat" "trm"

consts R :: "trm \<Rightarrow> trm \<Rightarrow> bool"

axioms r_eq: "EQUIV R"

ML {*

  typedef_main 

*}

local_setup {*

  typedef_main (@{binding "qtrm"}, @{term "R"}, @{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

thm Rep_qtrm

text {* another test *}

datatype 'a my = foo

consts Rmy :: "'a my \<Rightarrow> 'a my \<Rightarrow> bool"

axioms rmy_eq: "EQUIV Rmy"

term "\<lambda>(c::'a my\<Rightarrow>bool). \<exists>x. c = Rmy x"

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'"}, @{term "R'"}, @{typ "'a trm'"}, @{thm r_eq'}) #> snd

*}

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"}, @{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 = GenericDataFun

  (type T = typ_info Symtab.table

   val empty = Symtab.empty

   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 {*

    Context.theory_map (update @{type_name "list"} {mapfun = @{const_name "map"}})

 #> Context.theory_map (update @{type_name "*"} {mapfun = @{const_name "prod_fun"}})

 #> Context.theory_map (update @{type_name "fun"}  {mapfun = @{const_name "fun_map"}})

*}

ML {* lookup (Context.Proof @{context}) @{type_name list} *}

ML {*

datatype abs_or_rep = abs | rep

fun get_fun abs_or_rep 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 (Context.Proof 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 abs = (Const ("QuotMain.ABS_" ^ qty_name, rty --> qty), (rty, qty))

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

in

  if ty = qty

  then (get_const abs_or_rep)

  else (case ty of

          TFree _ => (Abs ("x", ty, Bound 0), (ty, ty))

        | Type (_, []) => (Abs ("x", ty, Bound 0), (ty, ty))

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

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

       )

end

*}

ML {*

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

  |> fst

  |> Syntax.string_of_term @{context}

  |> writeln

*}

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 rep rty qty lthy) arg_tys

  val abs_fn  = (fst o get_fun abs 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_name oconst mx rty qty lthy = 

let

  val oconst_ty = fastype_of oconst

  val nconst_ty = exchange_ty rty qty oconst_ty

  val nconst = Const (nconst_name, nconst_ty)

  val def_trm = get_const_def nconst oconst rty qty lthy

in

  make_def (Binding.name nconst_name, mx, def_trm) lthy

end  

*}

local_setup {*

  make_const_def "VR" @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd

*}

local_setup {*

  make_const_def "AP" @{term "ap"} NoSyn @{typ "t"} @{typ "qt"} #> snd

*}

local_setup {*

  make_const_def "LM" @{term "lm"} NoSyn @{typ "t"} @{typ "qt"} #> snd

*}

thm VR_def

thm AP_def

thm 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'"}, @{term "Rt'"}, @{typ "'a t'"}, @{thm t_eq'}) #> snd

*}

local_setup {*

  make_const_def "VR'" @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd

*}

local_setup {*

  make_const_def "AP'" @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd

*}

local_setup {*

  make_const_def "LM'" @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd

*}

thm VR'_def

thm AP'_def

thm LM'_def

term LM' 

term VR'

term AP'

text {* finite set example *}

inductive 

  list_eq ("_ \<approx> _")

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_sym:

  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_sym)

done

local_setup {*

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

*}

typ "'a fset"

thm "Rep_fset"

local_setup {*

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

*}

term Nil 

term EMPTY

thm EMPTY_def

local_setup {*

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

*}

term Cons 

term INSERT

thm INSERT_def