# HG changeset patch # User wenzelm # Date 1436204010 -7200 # Node ID 0e745bd11c5523b362a5449b9108480e22f529ef # Parent 5d281c5fe712d19d493fb781b641a7052fd6c2f9 tuned; diff -r 5d281c5fe712 -r 0e745bd11c55 src/HOL/Tools/Lifting/lifting_def_code_dt.ML --- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Mon Jul 06 19:12:33 2015 +0200 +++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Mon Jul 06 19:33:30 2015 +0200 @@ -801,16 +801,17 @@ val parse_param = Parse.name val parse_params = Scan.optional (Args.parens (Parse.list parse_param)) []; -(* parser and command *) -val liftdef_parser = - parse_params -- - (((Parse.binding -- (@{keyword "::"} |-- (Parse.typ >> SOME) -- Parse.opt_mixfix') >> Parse.triple2) - --| @{keyword "is"} -- Parse.term -- - Scan.optional (@{keyword "parametric"} |-- Parse.!!! Parse.xthms1) []) >> Parse.triple1) + +(* command syntax *) val _ = Outer_Syntax.local_theory_to_proof @{command_keyword "lift_definition"} "definition for constants over the quotient type" - (liftdef_parser >> lift_def_cmd_with_err_handling) + (parse_params -- + (((Parse.binding -- (@{keyword "::"} |-- (Parse.typ >> SOME) -- Parse.opt_mixfix') + >> Parse.triple2) -- + (@{keyword "is"} |-- Parse.term) -- + Scan.optional (@{keyword "parametric"} |-- Parse.!!! Parse.xthms1) []) >> Parse.triple1) + >> lift_def_cmd_with_err_handling); end diff -r 5d281c5fe712 -r 0e745bd11c55 src/HOL/Tools/Quotient/quotient_def.ML --- a/src/HOL/Tools/Quotient/quotient_def.ML Mon Jul 06 19:12:33 2015 +0200 +++ b/src/HOL/Tools/Quotient/quotient_def.ML Mon Jul 06 19:33:30 2015 +0200 @@ -203,15 +203,13 @@ val quotient_def_cmd = gen_quotient_def Proof_Context.read_var Syntax.parse_term -(* parser and command *) -val quotdef_parser = - Scan.option Parse_Spec.constdecl -- - Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| @{keyword "is"} -- Parse.term)) +(* command syntax *) val _ = Outer_Syntax.local_theory_to_proof @{command_keyword quotient_definition} "definition for constants over the quotient type" - (quotdef_parser >> quotient_def_cmd) + (Scan.option Parse_Spec.constdecl -- + Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term -- (@{keyword "is"} |-- Parse.term))) + >> quotient_def_cmd); - -end; (* structure *) +end; diff -r 5d281c5fe712 -r 0e745bd11c55 src/HOL/Tools/Quotient/quotient_type.ML --- a/src/HOL/Tools/Quotient/quotient_type.ML Mon Jul 06 19:12:33 2015 +0200 +++ b/src/HOL/Tools/Quotient/quotient_type.ML Mon Jul 06 19:33:30 2015 +0200 @@ -6,10 +6,10 @@ signature QUOTIENT_TYPE = sig - val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * + val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * ((binding * binding) option * thm option)) * thm -> local_theory -> Quotient_Info.quotients * local_theory - val quotient_type: (string list * binding * mixfix) * (typ * term * bool) * + val quotient_type: (string list * binding * mixfix) * (typ * term * bool) * ((binding * binding) option * thm option) -> Proof.context -> Proof.state val quotient_type_cmd: (((((string list * binding) * mixfix) * string) * (bool * string)) * @@ -22,8 +22,8 @@ (*** definition of quotient types ***) -val mem_def1 = @{lemma "y : Collect S ==> S y" by simp} -val mem_def2 = @{lemma "S y ==> y : Collect S" by simp} +val mem_def1 = @{lemma "y \ Collect S \ S y" by simp} +val mem_def2 = @{lemma "S y \ y \ Collect S" by simp} (* constructs the term {c. EX (x::rty). rel x x \ c = Collect (rel x)} *) fun typedef_term rel rty lthy = @@ -76,7 +76,7 @@ Goal.prove lthy [] [] goal (fn {context = ctxt, ...} => typedef_quot_type_tac ctxt equiv_thm typedef_info) end - + open Lifting_Util infix 0 MRSL @@ -91,12 +91,12 @@ in Envir.subst_term_types ty_inst rel end - + val (rty, qty) = (dest_funT o fastype_of) abs_fun val abs_fun_graph = HOLogic.mk_eq(abs_fun $ Bound 1, Bound 0) val Abs_body = (case (HOLogic.dest_Trueprop o Thm.prop_of) equiv_thm of Const (@{const_name equivp}, _) $ _ => abs_fun_graph - | Const (@{const_name part_equivp}, _) $ rel => + | Const (@{const_name part_equivp}, _) $ rel => HOLogic.mk_conj (force_type_of_rel rel rty $ Bound 1 $ Bound 1, abs_fun_graph) | _ => error "unsupported equivalence theorem" ) @@ -138,7 +138,7 @@ val (_ $ rel $ abs $ rep) = (HOLogic.dest_Trueprop o Thm.prop_of) quot_thm val (qtyp, rtyp) = (dest_funT o fastype_of) rep val qty_full_name = (fst o dest_Type) qtyp - val quotients = {qtyp = qtyp, rtyp = rtyp, equiv_rel = rel, equiv_thm = equiv_thm, + val quotients = {qtyp = qtyp, rtyp = rtyp, equiv_rel = rel, equiv_thm = equiv_thm, quot_thm = quot_thm } fun quot_info phi = Quotient_Info.transform_quotients phi quotients val abs_rep = {abs = abs, rep = rep} @@ -200,7 +200,7 @@ val equiv_thm_name = Binding.suffix_name "_equivp" qty_name (* storing the quotients *) - val quotients = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm, + val quotients = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm, quot_thm = quotient_thm} val lthy4 = lthy3 @@ -333,20 +333,18 @@ quotient_type spec' lthy end -val partial = Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false -val quotspec_parser = - (Parse.type_args -- Parse.binding) -- - (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *) - Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) -- - (@{keyword "/"} |-- (partial -- Parse.term)) -- - Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)) - -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm) +(* command syntax *) val _ = Outer_Syntax.local_theory_to_proof @{command_keyword quotient_type} "quotient type definitions (require equivalence proofs)" - (quotspec_parser >> quotient_type_cmd) + (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *) + (Parse.type_args -- Parse.binding -- + Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) -- (@{keyword "/"} |-- + Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false -- Parse.term) -- + Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)) -- + Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm) + >> quotient_type_cmd) - -end; +end