# HG changeset patch # User haftmann # Date 1423241823 -3600 # Node ID adaa430fc0f7665a7bb532ad46a178c2fa6c7ad5 # Parent 2025a17bb20fa59c9f86a9ec22f8794526cec2f7 default abstypes and default abstract equations make technical (no_code) annotation superfluous diff -r 2025a17bb20f -r adaa430fc0f7 src/Doc/Isar_Ref/HOL_Specific.thy --- a/src/Doc/Isar_Ref/HOL_Specific.thy Fri Feb 06 19:17:17 2015 +0100 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy Fri Feb 06 17:57:03 2015 +0100 @@ -1592,7 +1592,7 @@ \end{matharray} @{rail \ - @@{command (HOL) setup_lifting} ('(' 'no_code' ')')? \ + @@{command (HOL) setup_lifting} \ @{syntax thmref} @{syntax thmref}? (@'parametric' @{syntax thmref})?; \} @@ -1645,9 +1645,6 @@ The command @{command (HOL) "setup_lifting"} also sets up the code generator for the new type. Later on, when a new constant is defined by @{command (HOL) "lift_definition"}, the Lifting package proves and registers a code equation (if there is one) for the new constant. - If the option @{text "no_code"} is specified, the Lifting package does not set up the code - generator and as a consequence no code equations involving an abstract type are registered - by @{command (HOL) "lift_definition"}. \item @{command (HOL) "lift_definition"} @{text "f :: \"} @{keyword (HOL) "is"} @{text t} Defines a new function @{text f} with an abstract type @{text \} diff -r 2025a17bb20f -r adaa430fc0f7 src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Fri Feb 06 19:17:17 2015 +0100 +++ b/src/HOL/Code_Numeral.thy Fri Feb 06 17:57:03 2015 +0100 @@ -13,7 +13,7 @@ typedef integer = "UNIV \ int set" morphisms int_of_integer integer_of_int .. -setup_lifting (no_code) type_definition_integer +setup_lifting type_definition_integer lemma integer_eq_iff: "k = l \ int_of_integer k = int_of_integer l" @@ -620,7 +620,7 @@ typedef natural = "UNIV \ nat set" morphisms nat_of_natural natural_of_nat .. -setup_lifting (no_code) type_definition_natural +setup_lifting type_definition_natural lemma natural_eq_iff [termination_simp]: "m = n \ nat_of_natural m = nat_of_natural n" diff -r 2025a17bb20f -r adaa430fc0f7 src/HOL/Library/AList_Mapping.thy --- a/src/HOL/Library/AList_Mapping.thy Fri Feb 06 19:17:17 2015 +0100 +++ b/src/HOL/Library/AList_Mapping.thy Fri Feb 06 17:57:03 2015 +0100 @@ -66,5 +66,6 @@ lemma [code nbe]: "HOL.equal (x :: ('a, 'b) mapping) x \ True" by (fact equal_refl) - + end + diff -r 2025a17bb20f -r adaa430fc0f7 src/HOL/Library/Float.thy --- a/src/HOL/Library/Float.thy Fri Feb 06 19:17:17 2015 +0100 +++ b/src/HOL/Library/Float.thy Fri Feb 06 17:57:03 2015 +0100 @@ -27,7 +27,7 @@ lemma type_definition_float': "type_definition real float_of float" using type_definition_float unfolding real_of_float_def . -setup_lifting (no_code) type_definition_float' +setup_lifting type_definition_float' lemmas float_of_inject[simp] diff -r 2025a17bb20f -r adaa430fc0f7 src/HOL/Library/Polynomial.thy --- a/src/HOL/Library/Polynomial.thy Fri Feb 06 19:17:17 2015 +0100 +++ b/src/HOL/Library/Polynomial.thy Fri Feb 06 17:57:03 2015 +0100 @@ -93,7 +93,7 @@ morphisms coeff Abs_poly unfolding almost_everywhere_zero_def by auto -setup_lifting (no_code) type_definition_poly +setup_lifting type_definition_poly lemma poly_eq_iff: "p = q \ (\n. coeff p n = coeff q n)" by (simp add: coeff_inject [symmetric] fun_eq_iff) diff -r 2025a17bb20f -r adaa430fc0f7 src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Fri Feb 06 19:17:17 2015 +0100 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Fri Feb 06 17:57:03 2015 +0100 @@ -8,9 +8,9 @@ sig exception SETUP_LIFTING_INFR of string - val setup_by_quotient: bool -> thm -> thm option -> thm option -> local_theory -> local_theory + val setup_by_quotient: thm -> thm option -> thm option -> local_theory -> local_theory - val setup_by_typedef_thm: bool -> thm -> local_theory -> local_theory + val setup_by_typedef_thm: thm -> local_theory -> local_theory val lifting_restore: Lifting_Info.quotient -> Context.generic -> Context.generic end @@ -138,22 +138,22 @@ end end -fun define_code_constr gen_code quot_thm lthy = +fun define_code_constr quot_thm lthy = let val abs = quot_thm_abs quot_thm in - if gen_code andalso is_Const abs then + if is_Const abs then let - val (fixed_abs, lthy') = yield_singleton(Variable.importT_terms) abs lthy + val (fixed_abs, lthy') = yield_singleton Variable.importT_terms abs lthy in - Local_Theory.background_theory(Code.add_datatype [dest_Const fixed_abs]) lthy' + Local_Theory.background_theory (Code.add_datatype [dest_Const fixed_abs]) lthy' end else lthy end -fun define_abs_type gen_code quot_thm lthy = - if gen_code andalso Lifting_Def.can_generate_code_cert quot_thm then +fun define_abs_type quot_thm lthy = + if Lifting_Def.can_generate_code_cert quot_thm then let val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep} val add_abstype_attribute = @@ -232,7 +232,7 @@ |> Bundle.bundle ((binding, [restore_lifting_att])) [] end -fun setup_lifting_infr gen_code quot_thm opt_reflp_thm lthy = +fun setup_lifting_infr quot_thm opt_reflp_thm lthy = let val _ = quot_thm_sanity_check lthy quot_thm val (_, qty) = quot_thm_rty_qty quot_thm @@ -254,17 +254,14 @@ SOME reflp_thm => lthy |> (snd oo Local_Theory.note) ((Binding.empty, [reflexivity_rule_attr]), [reflp_thm RS @{thm reflp_ge_eq}]) - |> define_code_constr gen_code quot_thm + |> define_code_constr quot_thm | NONE => lthy - |> define_abs_type gen_code quot_thm - fun declare_no_code qty = Local_Theory.declaration {syntax = false, pervasive = true} - (fn phi => Lifting_Info.add_no_code_type (Morphism.typ phi qty |> Tname)) + |> define_abs_type quot_thm in lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi)) |> lifting_bundle qty_full_name quotients - |> (if not gen_code then declare_no_code qty else I) end local @@ -476,15 +473,13 @@ (* Sets up the Lifting package by a quotient theorem. - gen_code - flag if an abstract type given by quot_thm should be registred - as an abstract type in the code generator quot_thm - a quotient theorem (Quotient R Abs Rep T) opt_reflp_thm - a theorem saying that a relation from quot_thm is reflexive (in the form "reflp R") opt_par_thm - a parametricity theorem for R *) -fun setup_by_quotient gen_code quot_thm opt_reflp_thm opt_par_thm lthy = +fun setup_by_quotient quot_thm opt_reflp_thm opt_par_thm lthy = let (**) val quot_thm = Morphism.thm (Local_Theory.target_morphism lthy) quot_thm @@ -612,7 +607,7 @@ else setup_transfer_rules_nonpar lthy in lthy - |> setup_lifting_infr gen_code quot_thm opt_reflp_thm + |> setup_lifting_infr quot_thm opt_reflp_thm |> setup_transfer_rules end @@ -624,7 +619,7 @@ typedef_thm - a typedef theorem (type_definition Rep Abs S) *) -fun setup_by_typedef_thm gen_code typedef_thm lthy = +fun setup_by_typedef_thm typedef_thm lthy = let val transfer_attr = Attrib.internal (K Transfer.transfer_add) val transfer_domain_attr = Attrib.internal (K Transfer.transfer_domain_add) @@ -737,11 +732,11 @@ lthy |> (snd oo Local_Theory.note) ((Binding.prefix_name "Quotient_" qty_name, []), [quot_thm]) - |> setup_lifting_infr gen_code quot_thm opt_reflp_thm + |> setup_lifting_infr quot_thm opt_reflp_thm |> setup_transfer_rules end -fun setup_lifting_cmd gen_code xthm opt_reflp_xthm opt_par_xthm lthy = +fun setup_lifting_cmd xthm opt_reflp_xthm opt_par_xthm lthy = let val input_thm = singleton (Attrib.eval_thms lthy) xthm val input_term = (HOLogic.dest_Trueprop o prop_of) input_thm @@ -768,7 +763,7 @@ val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_par_xthm val _ = check_qty (snd (quot_thm_rty_qty input_thm)) in - setup_by_quotient gen_code input_thm opt_reflp_thm opt_par_thm lthy + setup_by_quotient input_thm opt_reflp_thm opt_par_thm lthy end fun setup_typedef () = @@ -781,7 +776,7 @@ | NONE => ( case opt_par_xthm of SOME _ => error "The parametricity theorem cannot be specified if the type_definition theorem is used." - | NONE => setup_by_typedef_thm gen_code input_thm lthy + | NONE => setup_by_typedef_thm input_thm lthy ) end in @@ -791,16 +786,13 @@ | _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported." end -val opt_gen_code = - Scan.optional (@{keyword "("} |-- Parse.!!! ((Parse.reserved "no_code" >> K false) --| @{keyword ")"})) true - val _ = Outer_Syntax.local_theory @{command_spec "setup_lifting"} "setup lifting infrastructure" - (opt_gen_code -- Parse.xthm -- Scan.option Parse.xthm + (Parse.xthm -- Scan.option Parse.xthm -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm) >> - (fn (((gen_code, xthm), opt_reflp_xthm), opt_par_xthm) => - setup_lifting_cmd gen_code xthm opt_reflp_xthm opt_par_xthm)) + (fn ((xthm, opt_reflp_xthm), opt_par_xthm) => + setup_lifting_cmd xthm opt_reflp_xthm opt_par_xthm)) (* restoring lifting infrastructure *) diff -r 2025a17bb20f -r adaa430fc0f7 src/HOL/Tools/Quotient/quotient_type.ML --- a/src/HOL/Tools/Quotient/quotient_type.ML Fri Feb 06 19:17:17 2015 +0100 +++ b/src/HOL/Tools/Quotient/quotient_type.ML Fri Feb 06 17:57:03 2015 +0100 @@ -7,12 +7,12 @@ signature QUOTIENT_TYPE = sig val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * - ((binding * binding) option * bool * thm option)) * thm -> local_theory -> Quotient_Info.quotients * local_theory + ((binding * binding) option * thm option)) * thm -> local_theory -> Quotient_Info.quotients * local_theory val quotient_type: (string list * binding * mixfix) * (typ * term * bool) * - ((binding * binding) option * bool * thm option) -> Proof.context -> Proof.state + ((binding * binding) option * thm option) -> Proof.context -> Proof.state - val quotient_type_cmd: ((((((bool * string list) * binding) * mixfix) * string) * (bool * string)) * + val quotient_type_cmd: (((((string list * binding) * mixfix) * string) * (bool * string)) * (binding * binding) option) * (Facts.ref * Token.src list) option -> Proof.context -> Proof.state end; @@ -110,7 +110,7 @@ (def_thm, lthy'') end; -fun setup_lifting_package gen_code quot3_thm equiv_thm opt_par_thm lthy = +fun setup_lifting_package quot3_thm equiv_thm opt_par_thm lthy = let val (_ $ _ $ abs_fun $ _) = (HOLogic.dest_Trueprop o prop_of) quot3_thm val (T_def, lthy') = define_cr_rel equiv_thm abs_fun lthy @@ -128,11 +128,11 @@ ) in lthy' - |> Lifting_Setup.setup_by_quotient gen_code quot_thm reflp_thm opt_par_thm + |> Lifting_Setup.setup_by_quotient quot_thm reflp_thm opt_par_thm |> (snd oo Local_Theory.note) ((quotient_thm_name, []), [quot_thm]) end -fun init_quotient_infr gen_code quot_thm equiv_thm opt_par_thm lthy = +fun init_quotient_infr quot_thm equiv_thm opt_par_thm lthy = let val (_ $ rel $ abs $ rep) = (HOLogic.dest_Trueprop o prop_of) quot_thm val (qtyp, rtyp) = (dest_funT o fastype_of) rep @@ -147,11 +147,11 @@ |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Quotient_Info.update_quotients (qty_full_name, quot_info phi) #> Quotient_Info.update_abs_rep (qty_full_name, abs_rep_info phi)) - |> setup_lifting_package gen_code quot_thm equiv_thm opt_par_thm + |> setup_lifting_package quot_thm equiv_thm opt_par_thm end (* main function for constructing a quotient type *) -fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, gen_code, opt_par_thm)), equiv_thm) lthy = +fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, opt_par_thm)), equiv_thm) lthy = let val part_equiv = if partial @@ -203,7 +203,7 @@ quot_thm = quotient_thm} val lthy4 = lthy3 - |> init_quotient_infr gen_code quotient_thm equiv_thm opt_par_thm + |> init_quotient_infr quotient_thm equiv_thm opt_par_thm |> (snd oo Local_Theory.note) ((equiv_thm_name, if partial then [] else @{attributes [quot_equiv]}), @@ -313,7 +313,7 @@ fun quotient_type_cmd spec lthy = let - fun parse_spec (((((((gen_code, vs), qty_name), mx), rty_str), (partial, rel_str)), opt_morphs), opt_par_xthm) lthy = + fun parse_spec ((((((vs, qty_name), mx), rty_str), (partial, rel_str)), opt_morphs), opt_par_xthm) lthy = let val rty = Syntax.read_typ lthy rty_str val tmp_lthy1 = Variable.declare_typ rty lthy @@ -324,7 +324,7 @@ val tmp_lthy2 = Variable.declare_term rel tmp_lthy1 val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_par_xthm in - (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, gen_code, opt_par_thm)), tmp_lthy2) + (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, opt_par_thm)), tmp_lthy2) end val (spec', _) = parse_spec spec lthy @@ -332,13 +332,10 @@ quotient_type spec' lthy end -val opt_gen_code = - Scan.optional (@{keyword "("} |-- (Parse.reserved "no_code" >> K false) --| Parse.!!! @{keyword ")"}) true - val partial = Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false val quotspec_parser = - (opt_gen_code -- Parse.type_args -- Parse.binding) -- + (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)) -- diff -r 2025a17bb20f -r adaa430fc0f7 src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Fri Feb 06 19:17:17 2015 +0100 +++ b/src/HOL/Word/Word.thy Fri Feb 06 17:57:03 2015 +0100 @@ -187,7 +187,7 @@ "reflp (\x y. bintrunc (len_of TYPE('a::len0)) x = bintrunc (len_of TYPE('a)) y)" by (simp add: reflp_def) -setup_lifting (no_code) Quotient_word reflp_word +setup_lifting Quotient_word reflp_word text {* TODO: The next lemma could be generated automatically. *}