# HG changeset patch # User Cezary Kaliszyk # Date 1256652015 -3600 # Node ID 18d7d9dc75cbf07c7a8b204e1e89c859fbdeba4d # Parent 1e227c9ee915550a78b2ddaece1e049571b5a7a8# Parent 2a803a1556d54838da43961b28e3025995fde75c Merged diff -r 1e227c9ee915 -r 18d7d9dc75cb LamEx.thy --- a/LamEx.thy Tue Oct 27 14:59:00 2009 +0100 +++ b/LamEx.thy Tue Oct 27 15:00:15 2009 +0100 @@ -17,8 +17,11 @@ | a3: "\t \ ([(a,b)]\s); a\s\ \ rLam a t \ rLam b s" quotient lam = rlam / alpha +apply - sorry +print_quotients + local_setup {* make_const_def @{binding Var} @{term "rVar"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #> make_const_def @{binding App} @{term "rApp"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #> diff -r 1e227c9ee915 -r 18d7d9dc75cb QuotMain.thy --- a/QuotMain.thy Tue Oct 27 14:59:00 2009 +0100 +++ b/QuotMain.thy Tue Oct 27 15:00:15 2009 +0100 @@ -137,6 +137,8 @@ section {* type definition for the quotient type *} +ML {* Proof.theorem_i NONE *} + use "quotient.ML" declare [[map list = (map, LIST_REL)]] @@ -150,7 +152,7 @@ ML {* val quot_def_parser = (OuterParse.$$$ "(" |-- OuterParse.$$$ "with" |-- - ((OuterParse.list1 OuterParse.binding) --| OuterParse.$$$ ")")) -- + ((OuterParse.list1 OuterParse.typ) --| OuterParse.$$$ ")")) -- (OuterParse.binding -- Scan.option (OuterParse.$$$ "::" |-- OuterParse.typ) -- OuterParse.mixfix --| OuterParse.where_ -- SpecParse.spec) diff -r 1e227c9ee915 -r 18d7d9dc75cb quotient.ML --- a/quotient.ML Tue Oct 27 14:59:00 2009 +0100 +++ b/quotient.ML Tue Oct 27 15:00:15 2009 +0100 @@ -1,7 +1,7 @@ signature QUOTIENT = sig type maps_info = {mapfun: string, relfun: string} - type quotient_info = {qtyp: typ, rtyp: typ, rel: term} + type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} val mk_quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state val mk_quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory @@ -11,8 +11,8 @@ val maps_update: string -> maps_info -> Proof.context -> Proof.context val print_quotdata: Proof.context -> unit val quotdata_lookup: theory -> quotient_info list - val quotdata_update_thy: (typ * typ * term) -> theory -> theory - val quotdata_update: (typ * typ * term) -> Proof.context -> Proof.context + val quotdata_update_thy: (typ * typ * term * thm) -> theory -> theory + val quotdata_update: (typ * typ * term * thm) -> Proof.context -> Proof.context end; structure Quotient: QUOTIENT = @@ -61,7 +61,7 @@ (* info about the quotient types *) -type quotient_info = {qtyp: typ, rtyp: typ, rel: term} +type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} structure QuotData = TheoryDataFun (type T = quotient_info list @@ -72,22 +72,24 @@ val quotdata_lookup = QuotData.get -fun quotdata_update_thy (qty, rty, rel) thy = - QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel}::ls) thy +fun quotdata_update_thy (qty, rty, rel, equiv_thm) thy = + QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm}::ls) thy -fun quotdata_update (qty, rty, rel) ctxt = - ProofContext.theory (quotdata_update_thy (qty, rty, rel)) ctxt +fun quotdata_update (qty, rty, rel, equiv_thm) ctxt = + ProofContext.theory (quotdata_update_thy (qty, rty, rel, equiv_thm)) ctxt fun print_quotdata ctxt = let - fun prt_quot {qtyp, rtyp, rel} = + fun prt_quot {qtyp, rtyp, rel, equiv_thm} = Pretty.block (Library.separate (Pretty.brk 2) [Pretty.str ("quotient type:"), Syntax.pretty_typ ctxt qtyp, Pretty.str ("raw type:"), Syntax.pretty_typ ctxt rtyp, Pretty.str ("relation:"), - Syntax.pretty_term ctxt rel]) + Syntax.pretty_term ctxt rel, + Pretty.str ("equiv. thm:"), + Syntax.pretty_term ctxt (prop_of equiv_thm)]) in QuotData.get (ProofContext.theory_of ctxt) |> map prt_quot @@ -101,7 +103,7 @@ -(* wrappers for define and note *) +(* wrappers for define, note and theorem_i *) fun define (name, mx, rhs) lthy = let val ((rhs, (_ , thm)), lthy') = @@ -117,6 +119,13 @@ (thm', lthy') end +fun theorem after_qed goals ctxt = +let + val goals' = map (rpair []) goals + fun after_qed' thms = after_qed (the_single thms) +in + Proof.theorem_i NONE after_qed' [goals'] ctxt +end (* definition of the quotient type *) @@ -154,7 +163,7 @@ (* tactic to prove the QUOT_TYPE theorem for the new type *) fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = let - val unfold_mem = MetaSimplifier.rewrite_rule @{thms mem_def} + val unfold_mem = MetaSimplifier.rewrite_rule [@{thm mem_def}] val rep_thm = #Rep typedef_info |> unfold_mem val rep_inv = #Rep_inverse typedef_info val abs_inv = #Abs_inverse typedef_info |> unfold_mem @@ -231,7 +240,7 @@ val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name (* storing the quot-info *) - val lthy3 = quotdata_update (abs_ty, rty, rel) lthy2 + val lthy3 = quotdata_update (abs_ty, rty, rel, equiv_thm) lthy2 (* interpretation *) val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) @@ -281,15 +290,29 @@ let val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} in - (HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel), []) + HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel) end val goals = map (mk_goal o snd) quot_list fun after_qed thms lthy = - fold_map mk_typedef_main (quot_list ~~ (flat thms)) lthy |> snd + fold_map mk_typedef_main (quot_list ~~ thms) lthy |> snd in - Proof.theorem_i NONE after_qed [goals] lthy + theorem after_qed goals lthy +end + +fun mk_quotient_type_cmd spec lthy = +let + fun parse_spec (((qty_str, mx), rty_str), rel_str) = + let + val qty_name = Binding.name qty_str + val rty = Syntax.parse_typ lthy rty_str |> Syntax.check_typ lthy + val rel = Syntax.parse_term lthy rel_str |> Syntax.check_term lthy + in + ((qty_name, mx), (rty, rel)) + end +in + mk_quotient_type (map parse_spec spec) lthy end val quotspec_parser = @@ -297,21 +320,6 @@ (OuterParse.short_ident -- OuterParse.opt_infix -- (OuterParse.$$$ "=" |-- OuterParse.typ) -- (OuterParse.$$$ "/" |-- OuterParse.term)) - -fun mk_quotient_type_cmd spec lthy = -let - fun parse_spec (((qty_str, mx), rty_str), rel_str) = - let - val qty_name = Binding.name qty_str - val rty = Syntax.parse_typ lthy rty_str - val rel = Syntax.parse_term lthy rel_str - |> Syntax.check_term lthy - in - ((qty_name, mx), (rty, rel)) - end -in - mk_quotient_type (map parse_spec spec) lthy -end val _ = OuterKeyword.keyword "/"