1 theory QuotMain

     2 imports QuotScript QuotList

     3 begin

     4 

     5 locale QUOT_TYPE =

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

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

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

     9   assumes equiv: "EQUIV R"

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

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

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

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

    14 begin 

    15 

    16 definition

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

    18 

    19 definition

    20   "REP a = Eps (Rep a)"

    21 

    22 lemma lem9: 

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

    24 proof -

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

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

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

    28     using equiv unfolding EQUIV_def by simp

    29 qed

    30 

    31 theorem thm10:

    32   shows "ABS (REP a) = a"

    33 unfolding ABS_def REP_def

    34 proof -

    35   from rep_prop 

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

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

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

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

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

    41   finally

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

    43 qed

    44 

    45 lemma REP_refl: 

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

    47 unfolding REP_def

    48 by (simp add: equiv[simplified EQUIV_def])

    49 

    50 lemma lem7:

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

    52 apply(rule iffI)

    53 apply(simp)

    54 apply(drule rep_inject[THEN iffD2])

    55 apply(simp add: abs_inverse)

    56 done

    57   

    58 theorem thm11:

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

    60 unfolding ABS_def

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

    62 

    63 lemma QUOTIENT:

    64   "QUOTIENT R ABS REP"

    65 apply(unfold QUOTIENT_def)

    66 apply(simp add: thm10)

    67 apply(simp add: REP_refl)

    68 apply(subst thm11[symmetric])

    69 apply(simp add: equiv[simplified EQUIV_def])

    70 done

    71 

    72 end

    73 

    74 ML {*

    75   Variable.variant_frees

    76 *}

    77 

    78 

    79 section {* type definition for the quotient type *}

    80 

    81 ML {*

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

    83 fun typedef_term rel ty lthy =

    84 let 

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

    86                |> Variable.variant_frees lthy [rel]

    87                |> map Free

    88 in

    89   lambda c  

    90     ((HOLogic.exists_const ty) $ 

    91       (lambda x (HOLogic.mk_eq (c, (rel $ x)))))

    92 end

    93 *}

    94 

    95 ML {*

    96 val typedef_tac =  

    97   EVERY1 [rewrite_goal_tac @{thms mem_def},

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

    99 *}

   100 

   101 ML {*

   102 (* makes the new type definitions *)

   103 fun typedef_make (qty_name, rel, ty) lthy =

   104   LocalTheory.theory_result

   105   (TypedefPackage.add_typedef false NONE 

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

   107        (typedef_term rel ty lthy)

   108          NONE typedef_tac) lthy

   109 *}

   110 

   111 text {* proves the QUOTIENT theorem for the new type *}

   112 ML {*

   113 fun typedef_quot_type_tac equiv_thm (typedef_info: TypedefPackage.info) = 

   114 let

   115   val rep_thm = #Rep typedef_info

   116   val rep_inv = #Rep_inverse typedef_info

   117   val abs_inv = #Abs_inverse typedef_info

   118   val rep_inj = #Rep_inject typedef_info

   119 

   120   val ss = HOL_basic_ss addsimps @{thms mem_def}

   121   val rep_thm_simpd = Simplifier.asm_full_simplify ss rep_thm

   122   val abs_inv_simpd = Simplifier.asm_full_simplify ss abs_inv

   123 in

   124   EVERY1 [rtac @{thm QUOT_TYPE.intro},

   125           rtac equiv_thm, 

   126           rtac rep_thm_simpd, 

   127           rtac rep_inv, 

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

   129           rtac rep_inj]

   130 end

   131 *}

   132 

   133 ML {* 

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

   135 let

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

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

   138              |> Syntax.check_term lthy

   139 in

   140   Goal.prove lthy [] [] goal

   141     (fn _ => typedef_quot_type_tac equiv_thm typedef_info)

   142 end

   143 *}

   144 

   145 ML {*

   146 fun typedef_quotient_thm_tac defs quot_type_thm =

   147   EVERY1 [K (rewrite_goals_tac defs), 

   148           rtac @{thm QUOT_TYPE.QUOTIENT}, 

   149           rtac quot_type_thm]

   150 *}

   151 

   152 ML {* 

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

   154 let

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

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

   157              |> Syntax.check_term lthy

   158 in

   159   Goal.prove lthy [] [] goal

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

   161 end

   162 *}

   163 

   164 text {* two wrappers for define and note *}

   165 ML {* 

   166 fun make_def (name, mx, trm) lthy =

   167 let   

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

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

   170 in

   171   ((trm, thm), lthy')

   172 end

   173 *}

   174 

   175 ML {*

   176 fun reg_thm (name, thm) lthy = 

   177 let

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

   179 in

   180   (thm',lthy')

   181 end

   182 *}

   183 

   184 ML {* 

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

   186 let 

   187   (* generates typedef *)

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

   189 

   190   (* abs and rep functions *)

   191   val abs_ty = #abs_type typedef_info

   192   val rep_ty = #rep_type typedef_info

   193   val abs_name = #Abs_name typedef_info

   194   val rep_name = #Rep_name typedef_info

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

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

   197 

   198   (* ABS and REP definitions *)

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

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

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

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

   203   val ABS_name = Binding.prefix_name "ABS_" qty_name

   204   val REP_name = Binding.prefix_name "REP_" qty_name  

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

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

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

   208 

   209   (* quot_type theorem *)

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

   211   val quot_thm_name = Binding.prefix_name "QUOT_TYPE_" qty_name

   212 

   213   (* quotient theorem *)

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

   215   val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name

   216 

   217 in

   218   lthy'' 

   219   |> reg_thm (quot_thm_name, quot_thm)  

   220   ||>> reg_thm (quotient_thm_name, quotient_thm)

   221 end

   222 *}

   223 

   224 section {* various tests for quotient types*}

   225 datatype trm =

   226   var  "nat" 

   227 | app  "trm" "trm"

   228 | lam  "nat" "trm"

   229   

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

   231 axioms r_eq: "EQUIV R"

   232 

   233 local_setup {*

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

   235 *}

   236 

   237 term Rep_qtrm

   238 term Abs_qtrm

   239 term ABS_qtrm

   240 term REP_qtrm

   241 thm QUOT_TYPE_qtrm

   242 thm QUOTIENT_qtrm

   243 thm Rep_qtrm

   244 

   245 text {* another test *}

   246 datatype 'a my = foo

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

   248 axioms rmy_eq: "EQUIV Rmy"

   249 

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

   251 

   252 datatype 'a trm' =

   253   var'  "'a" 

   254 | app'  "'a trm'" "'a trm'"

   255 | lam'  "'a" "'a trm'"

   256   

   257 consts R' :: "'a trm' \<Rightarrow> 'a trm' \<Rightarrow> bool"

   258 axioms r_eq': "EQUIV R'"

   259 

   260 local_setup {*

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

   262 *}

   263 

   264 term ABS_qtrm'

   265 term REP_qtrm'

   266 thm QUOT_TYPE_qtrm'

   267 thm QUOTIENT_qtrm'

   268 thm Rep_qtrm'

   269 

   270 text {* a test with lists of terms *}

   271 datatype t =

   272   vr "string"

   273 | ap "t list"

   274 | lm "string" "t"

   275 

   276 consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool"

   277 axioms t_eq: "EQUIV Rt"

   278 

   279 local_setup {*

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

   281 *}

   282 

   283 section {* lifting of constants *}

   284 

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

   286 ML {*

   287 type typ_info = {mapfun: string}

   288 

   289 local

   290   structure Data = GenericDataFun

   291   (type T = typ_info Symtab.table

   292    val empty = Symtab.empty

   293    val extend = I

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

   295 in

   296  val lookup = Symtab.lookup o Data.get

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

   298 end

   299 *}

   300 

   301 (* mapfuns for some standard types *)

   302 setup {*

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

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

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

   306 *}

   307 

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

   309 

   310 ML {*

   311 datatype abs_or_rep = abs | rep

   312 

   313 fun get_fun abs_or_rep rty qty lthy ty = 

   314 let

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

   316   

   317   fun get_fun_aux s fs_tys =

   318   let

   319     val (fs, tys) = split_list fs_tys

   320     val (otys, ntys) = split_list tys 

   321     val oty = Type (s, otys)

   322     val nty = Type (s, ntys)

   323     val ftys = map (op -->) tys

   324   in

   325    (case (lookup (Context.Proof lthy) s) of 

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

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

   328   end

   329 

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

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

   332 in

   333   if ty = qty

   334   then (get_const abs_or_rep)

   335   else (case ty of

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

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

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

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

   340        )

   341 end

   342 *}

   343 

   344 ML {*

   345 fun get_const_def nconst oconst rty qty lthy =

   346 let

   347   val ty = fastype_of nconst

   348   val (arg_tys, res_ty) = strip_type ty

   349  

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

   351                            |> Variable.variant_frees lthy [nconst, oconst] 

   352                            |> map Free

   353 

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

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

   356 

   357 in

   358   map (op $) (rep_fns ~~ fresh_args)

   359   |> curry list_comb oconst

   360   |> curry (op $) abs_fn

   361   |> fold_rev lambda fresh_args

   362 end

   363 *}

   364 

   365 ML {*

   366 fun exchange_ty rty qty ty = 

   367   if ty = rty then qty

   368   else 

   369     (case ty of

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

   371       | _ => ty)

   372 *}

   373 

   374 ML {*

   375 fun make_const_def nconst_name oconst mx rty qty lthy = 

   376 let

   377   val oconst_ty = fastype_of oconst

   378   val nconst_ty = exchange_ty rty qty oconst_ty

   379   val nconst = Const (nconst_name, nconst_ty)

   380   val def_trm = get_const_def nconst oconst rty qty lthy

   381 in

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

   383 end  

   384 *}

   385 

   386 text {* a test with functions *}

   387 datatype 'a t' =

   388   vr' "string"

   389 | ap' "('a t') * ('a t')"

   390 | lm' "'a" "string \<Rightarrow> ('a t')"

   391 

   392 consts Rt' :: "('a t') \<Rightarrow> ('a t') \<Rightarrow> bool"

   393 axioms t_eq': "EQUIV Rt'"

   394 

   395 local_setup {*

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

   397 *}

   398 

   399 local_setup {*

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

   401 *}

   402 

   403 local_setup {*

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

   405 *}

   406 

   407 local_setup {*

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

   409 *}

   410 

   411 thm VR'_def

   412 thm AP'_def

   413 thm LM'_def

   414 term LM' 

   415 term VR'

   416 term AP'

   417 

   418 text {* finite set example *}

   419 

   420 inductive 

   421   list_eq ("_ \<approx> _")

   422 where

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

   424 | "[] \<approx> []"

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

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

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

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

   429 

   430 lemma list_eq_sym:

   431   shows "xs \<approx> xs"

   432 apply(induct xs)

   433 apply(auto intro: list_eq.intros)

   434 done

   435 

   436 lemma equiv_list_eq:

   437   shows "EQUIV list_eq"

   438 unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def

   439 apply(auto intro: list_eq.intros list_eq_sym)

   440 done

   441 

   442 local_setup {*

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

   444 *}

   445 

   446 typ "'a fset"

   447 thm "Rep_fset"

   448 

   449 local_setup {*

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

   451 *}

   452 

   453 term Nil 

   454 term EMPTY

   455 

   456 local_setup {*

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

   458 *}

   459 

   460 term Cons 

   461 term INSERT

   462 

   463 local_setup {*

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

   465 *}

   466 

   467 term append 

   468 term UNION

   469 thm QUOTIENT_fset

   470 thm Insert_def

   471 

   472 fun 

   473   membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" ("_ memb _")

   474 where

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

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

   477 

   478 

   479 local_setup {*

   480   make_const_def "IN" @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd

   481 *}

   482 

   483 term membship

   484 term IN

   485 

   486 lemma

   487   shows "IN x EMPTY = False"

   488 unfolding IN_def EMPTY_def

   489 apply(auto)

   490 thm Rep_fset_inverse

   491 

   492 

   493 

   494 

   495 

   496 

   497 

   498 

   499 

   500 

   501 text {* old stuff *}

   502 

   503 

   504 lemma QUOT_TYPE_qtrm_old:

   505   "QUOT_TYPE R Abs_qtrm Rep_qtrm"

   506 apply(rule QUOT_TYPE.intro)

   507 apply(rule r_eq)

   508 apply(rule Rep_qtrm[simplified mem_def])

   509 apply(rule Rep_qtrm_inverse)

   510 apply(rule Abs_qtrm_inverse[simplified mem_def])

   511 apply(rule exI)

   512 apply(rule refl)

   513 apply(rule Rep_qtrm_inject)

   514 done

   515 

   516 definition

   517   "ABS_qtrm_old \<equiv> QUOT_TYPE.ABS R Abs_qtrm"

   518 

   519 definition

   520   "REP_qtrm_old \<equiv> QUOT_TYPE.REP Rep_qtrm"

   521 

   522 lemma 

   523   "QUOTIENT R (ABS_qtrm) (REP_qtrm)"

   524 apply(simp add: ABS_qtrm_def REP_qtrm_def)

   525 apply(rule QUOT_TYPE.QUOTIENT)

   526 apply(rule QUOT_TYPE_qtrm)

   527 done

   528 

   529 term "var"

   530 term "app"

   531 term "lam"

   532 

   533 definition

   534   "VAR x \<equiv> ABS_qtrm (var x)"

   535 

   536 definition

   537   "APP t1 t2 \<equiv> ABS_qtrm (app (REP_qtrm t1) (REP_qtrm t2))"

   538 

   539 definition

   540   "LAM x t \<equiv> ABS_qtrm (lam x (REP_qtrm t))"

   541 

   542 

   543 

   544 

   545 definition

   546   "VR x \<equiv> ABS_qt (vr x)"

   547 

   548 definition

   549   "AP ts \<equiv> ABS_qt (ap (map REP_qt ts))"

   550 

   551 definition

   552   "LM x t \<equiv> ABS_qt (lm x (REP_qt t))"

   553 

   554 (* for printing types *)

   555 ML {*

   556 fun setmp_show_all_types f =

   557   setmp show_all_types

   558   (! show_types orelse ! show_sorts orelse ! show_all_types) f

   559 *}