default abstypes and default abstract equations make technical (no_code) annotation superfluous
authorhaftmann
Fri Feb 06 17:57:03 2015 +0100 (2015-02-06)
changeset 59487adaa430fc0f7
parent 59486 2025a17bb20f
child 59488 8a183caa424d
child 59493 e088f1b2f2fc
child 59497 0c5cd369a643
default abstypes and default abstract equations make technical (no_code) annotation superfluous
src/Doc/Isar_Ref/HOL_Specific.thy
src/HOL/Code_Numeral.thy
src/HOL/Library/AList_Mapping.thy
src/HOL/Library/Float.thy
src/HOL/Library/Polynomial.thy
src/HOL/Tools/Lifting/lifting_setup.ML
src/HOL/Tools/Quotient/quotient_type.ML
src/HOL/Word/Word.thy
     1.1 --- a/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Feb 06 19:17:17 2015 +0100
     1.2 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Feb 06 17:57:03 2015 +0100
     1.3 @@ -1592,7 +1592,7 @@
     1.4    \end{matharray}
     1.5  
     1.6    @{rail \<open>
     1.7 -    @@{command (HOL) setup_lifting} ('(' 'no_code' ')')? \<newline>
     1.8 +    @@{command (HOL) setup_lifting} \<newline>
     1.9        @{syntax thmref} @{syntax thmref}? (@'parametric' @{syntax thmref})?;
    1.10    \<close>}
    1.11  
    1.12 @@ -1645,9 +1645,6 @@
    1.13      The command @{command (HOL) "setup_lifting"} also sets up the code generator
    1.14      for the new type. Later on, when a new constant is defined by @{command (HOL) "lift_definition"},
    1.15      the Lifting package proves and registers a code equation (if there is one) for the new constant.
    1.16 -    If the option @{text "no_code"} is specified, the Lifting package does not set up the code
    1.17 -    generator and as a consequence no code equations involving an abstract type are registered
    1.18 -    by @{command (HOL) "lift_definition"}.
    1.19  
    1.20    \item @{command (HOL) "lift_definition"} @{text "f :: \<tau>"} @{keyword (HOL) "is"} @{text t}
    1.21      Defines a new function @{text f} with an abstract type @{text \<tau>}
     2.1 --- a/src/HOL/Code_Numeral.thy	Fri Feb 06 19:17:17 2015 +0100
     2.2 +++ b/src/HOL/Code_Numeral.thy	Fri Feb 06 17:57:03 2015 +0100
     2.3 @@ -13,7 +13,7 @@
     2.4  typedef integer = "UNIV \<Colon> int set"
     2.5    morphisms int_of_integer integer_of_int ..
     2.6  
     2.7 -setup_lifting (no_code) type_definition_integer
     2.8 +setup_lifting type_definition_integer
     2.9  
    2.10  lemma integer_eq_iff:
    2.11    "k = l \<longleftrightarrow> int_of_integer k = int_of_integer l"
    2.12 @@ -620,7 +620,7 @@
    2.13  typedef natural = "UNIV \<Colon> nat set"
    2.14    morphisms nat_of_natural natural_of_nat ..
    2.15  
    2.16 -setup_lifting (no_code) type_definition_natural
    2.17 +setup_lifting type_definition_natural
    2.18  
    2.19  lemma natural_eq_iff [termination_simp]:
    2.20    "m = n \<longleftrightarrow> nat_of_natural m = nat_of_natural n"
     3.1 --- a/src/HOL/Library/AList_Mapping.thy	Fri Feb 06 19:17:17 2015 +0100
     3.2 +++ b/src/HOL/Library/AList_Mapping.thy	Fri Feb 06 17:57:03 2015 +0100
     3.3 @@ -66,5 +66,6 @@
     3.4  lemma [code nbe]:
     3.5    "HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True"
     3.6    by (fact equal_refl)
     3.7 -  
     3.8 +
     3.9  end
    3.10 +
     4.1 --- a/src/HOL/Library/Float.thy	Fri Feb 06 19:17:17 2015 +0100
     4.2 +++ b/src/HOL/Library/Float.thy	Fri Feb 06 17:57:03 2015 +0100
     4.3 @@ -27,7 +27,7 @@
     4.4  lemma type_definition_float': "type_definition real float_of float"
     4.5    using type_definition_float unfolding real_of_float_def .
     4.6  
     4.7 -setup_lifting (no_code) type_definition_float'
     4.8 +setup_lifting type_definition_float'
     4.9  
    4.10  lemmas float_of_inject[simp]
    4.11  
     5.1 --- a/src/HOL/Library/Polynomial.thy	Fri Feb 06 19:17:17 2015 +0100
     5.2 +++ b/src/HOL/Library/Polynomial.thy	Fri Feb 06 17:57:03 2015 +0100
     5.3 @@ -93,7 +93,7 @@
     5.4    morphisms coeff Abs_poly
     5.5    unfolding almost_everywhere_zero_def by auto
     5.6  
     5.7 -setup_lifting (no_code) type_definition_poly
     5.8 +setup_lifting type_definition_poly
     5.9  
    5.10  lemma poly_eq_iff: "p = q \<longleftrightarrow> (\<forall>n. coeff p n = coeff q n)"
    5.11    by (simp add: coeff_inject [symmetric] fun_eq_iff)
     6.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Fri Feb 06 19:17:17 2015 +0100
     6.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Fri Feb 06 17:57:03 2015 +0100
     6.3 @@ -8,9 +8,9 @@
     6.4  sig
     6.5    exception SETUP_LIFTING_INFR of string
     6.6  
     6.7 -  val setup_by_quotient: bool -> thm -> thm option -> thm option -> local_theory -> local_theory
     6.8 +  val setup_by_quotient: thm -> thm option -> thm option -> local_theory -> local_theory
     6.9  
    6.10 -  val setup_by_typedef_thm: bool -> thm -> local_theory -> local_theory
    6.11 +  val setup_by_typedef_thm: thm -> local_theory -> local_theory
    6.12  
    6.13    val lifting_restore: Lifting_Info.quotient -> Context.generic -> Context.generic
    6.14  end
    6.15 @@ -138,22 +138,22 @@
    6.16    end
    6.17  end
    6.18  
    6.19 -fun define_code_constr gen_code quot_thm lthy =
    6.20 +fun define_code_constr quot_thm lthy =
    6.21    let
    6.22      val abs = quot_thm_abs quot_thm
    6.23    in
    6.24 -    if gen_code andalso is_Const abs then
    6.25 +    if is_Const abs then
    6.26        let
    6.27 -        val (fixed_abs, lthy') = yield_singleton(Variable.importT_terms) abs lthy
    6.28 +        val (fixed_abs, lthy') = yield_singleton Variable.importT_terms abs lthy
    6.29        in  
    6.30 -         Local_Theory.background_theory(Code.add_datatype [dest_Const fixed_abs]) lthy'
    6.31 +         Local_Theory.background_theory (Code.add_datatype [dest_Const fixed_abs]) lthy'
    6.32        end
    6.33      else
    6.34        lthy
    6.35    end
    6.36  
    6.37 -fun define_abs_type gen_code quot_thm lthy =
    6.38 -  if gen_code andalso Lifting_Def.can_generate_code_cert quot_thm then
    6.39 +fun define_abs_type quot_thm lthy =
    6.40 +  if Lifting_Def.can_generate_code_cert quot_thm then
    6.41      let
    6.42        val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep}
    6.43        val add_abstype_attribute = 
    6.44 @@ -232,7 +232,7 @@
    6.45        |> Bundle.bundle ((binding, [restore_lifting_att])) []
    6.46    end
    6.47  
    6.48 -fun setup_lifting_infr gen_code quot_thm opt_reflp_thm lthy =
    6.49 +fun setup_lifting_infr quot_thm opt_reflp_thm lthy =
    6.50    let
    6.51      val _ = quot_thm_sanity_check lthy quot_thm
    6.52      val (_, qty) = quot_thm_rty_qty quot_thm
    6.53 @@ -254,17 +254,14 @@
    6.54        SOME reflp_thm => lthy
    6.55          |> (snd oo Local_Theory.note) ((Binding.empty, [reflexivity_rule_attr]),
    6.56                [reflp_thm RS @{thm reflp_ge_eq}])
    6.57 -        |> define_code_constr gen_code quot_thm
    6.58 +        |> define_code_constr quot_thm
    6.59        | NONE => lthy
    6.60 -        |> define_abs_type gen_code quot_thm
    6.61 -    fun declare_no_code qty =  Local_Theory.declaration {syntax = false, pervasive = true}
    6.62 -        (fn phi => Lifting_Info.add_no_code_type (Morphism.typ phi qty |> Tname))
    6.63 +        |> define_abs_type quot_thm
    6.64    in
    6.65      lthy
    6.66        |> Local_Theory.declaration {syntax = false, pervasive = true}
    6.67          (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi))
    6.68        |> lifting_bundle qty_full_name quotients
    6.69 -      |> (if not gen_code then declare_no_code qty else I)
    6.70    end
    6.71  
    6.72  local
    6.73 @@ -476,15 +473,13 @@
    6.74  (*
    6.75    Sets up the Lifting package by a quotient theorem.
    6.76  
    6.77 -  gen_code - flag if an abstract type given by quot_thm should be registred 
    6.78 -    as an abstract type in the code generator
    6.79    quot_thm - a quotient theorem (Quotient R Abs Rep T)
    6.80    opt_reflp_thm - a theorem saying that a relation from quot_thm is reflexive
    6.81      (in the form "reflp R")
    6.82    opt_par_thm - a parametricity theorem for R
    6.83  *)
    6.84  
    6.85 -fun setup_by_quotient gen_code quot_thm opt_reflp_thm opt_par_thm lthy =
    6.86 +fun setup_by_quotient quot_thm opt_reflp_thm opt_par_thm lthy =
    6.87    let
    6.88      (**)
    6.89      val quot_thm = Morphism.thm (Local_Theory.target_morphism lthy) quot_thm
    6.90 @@ -612,7 +607,7 @@
    6.91                                                       else setup_transfer_rules_nonpar lthy
    6.92    in
    6.93      lthy
    6.94 -      |> setup_lifting_infr gen_code quot_thm opt_reflp_thm
    6.95 +      |> setup_lifting_infr quot_thm opt_reflp_thm
    6.96        |> setup_transfer_rules
    6.97    end
    6.98  
    6.99 @@ -624,7 +619,7 @@
   6.100    typedef_thm - a typedef theorem (type_definition Rep Abs S)
   6.101  *)
   6.102  
   6.103 -fun setup_by_typedef_thm gen_code typedef_thm lthy =
   6.104 +fun setup_by_typedef_thm typedef_thm lthy =
   6.105    let
   6.106      val transfer_attr = Attrib.internal (K Transfer.transfer_add)
   6.107      val transfer_domain_attr = Attrib.internal (K Transfer.transfer_domain_add)
   6.108 @@ -737,11 +732,11 @@
   6.109      lthy
   6.110        |> (snd oo Local_Theory.note) ((Binding.prefix_name "Quotient_" qty_name, []), 
   6.111              [quot_thm])
   6.112 -      |> setup_lifting_infr gen_code quot_thm opt_reflp_thm
   6.113 +      |> setup_lifting_infr quot_thm opt_reflp_thm
   6.114        |> setup_transfer_rules
   6.115    end
   6.116  
   6.117 -fun setup_lifting_cmd gen_code xthm opt_reflp_xthm opt_par_xthm lthy =
   6.118 +fun setup_lifting_cmd xthm opt_reflp_xthm opt_par_xthm lthy =
   6.119    let 
   6.120      val input_thm = singleton (Attrib.eval_thms lthy) xthm
   6.121      val input_term = (HOLogic.dest_Trueprop o prop_of) input_thm
   6.122 @@ -768,7 +763,7 @@
   6.123          val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_par_xthm
   6.124          val _ = check_qty (snd (quot_thm_rty_qty input_thm))
   6.125        in
   6.126 -        setup_by_quotient gen_code input_thm opt_reflp_thm opt_par_thm lthy
   6.127 +        setup_by_quotient input_thm opt_reflp_thm opt_par_thm lthy
   6.128        end
   6.129  
   6.130      fun setup_typedef () = 
   6.131 @@ -781,7 +776,7 @@
   6.132            | NONE => (
   6.133              case opt_par_xthm of
   6.134                SOME _ => error "The parametricity theorem cannot be specified if the type_definition theorem is used."
   6.135 -              | NONE => setup_by_typedef_thm gen_code input_thm lthy
   6.136 +              | NONE => setup_by_typedef_thm input_thm lthy
   6.137            )
   6.138        end
   6.139    in
   6.140 @@ -791,16 +786,13 @@
   6.141        | _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported."
   6.142    end
   6.143  
   6.144 -val opt_gen_code =
   6.145 -  Scan.optional (@{keyword "("} |-- Parse.!!! ((Parse.reserved "no_code" >> K false) --| @{keyword ")"})) true
   6.146 -
   6.147  val _ = 
   6.148    Outer_Syntax.local_theory @{command_spec "setup_lifting"}
   6.149      "setup lifting infrastructure" 
   6.150 -      (opt_gen_code -- Parse.xthm -- Scan.option Parse.xthm 
   6.151 +      (Parse.xthm -- Scan.option Parse.xthm 
   6.152        -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm) >> 
   6.153 -        (fn (((gen_code, xthm), opt_reflp_xthm), opt_par_xthm) => 
   6.154 -          setup_lifting_cmd gen_code xthm opt_reflp_xthm opt_par_xthm))
   6.155 +        (fn ((xthm, opt_reflp_xthm), opt_par_xthm) => 
   6.156 +          setup_lifting_cmd xthm opt_reflp_xthm opt_par_xthm))
   6.157  
   6.158  (* restoring lifting infrastructure *)
   6.159  
     7.1 --- a/src/HOL/Tools/Quotient/quotient_type.ML	Fri Feb 06 19:17:17 2015 +0100
     7.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML	Fri Feb 06 17:57:03 2015 +0100
     7.3 @@ -7,12 +7,12 @@
     7.4  signature QUOTIENT_TYPE =
     7.5  sig
     7.6    val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * 
     7.7 -    ((binding * binding) option * bool * thm option)) * thm -> local_theory -> Quotient_Info.quotients * local_theory
     7.8 +    ((binding * binding) option * thm option)) * thm -> local_theory -> Quotient_Info.quotients * local_theory
     7.9  
    7.10    val quotient_type: (string list * binding * mixfix) * (typ * term * bool) * 
    7.11 -    ((binding * binding) option * bool * thm option) -> Proof.context -> Proof.state
    7.12 +    ((binding * binding) option * thm option) -> Proof.context -> Proof.state
    7.13  
    7.14 -  val quotient_type_cmd: ((((((bool * string list) * binding) * mixfix) * string) * (bool * string)) *
    7.15 +  val quotient_type_cmd: (((((string list * binding) * mixfix) * string) * (bool * string)) *
    7.16      (binding * binding) option) * (Facts.ref * Token.src list) option -> Proof.context -> Proof.state
    7.17  end;
    7.18  
    7.19 @@ -110,7 +110,7 @@
    7.20      (def_thm, lthy'')
    7.21    end;
    7.22  
    7.23 -fun setup_lifting_package gen_code quot3_thm equiv_thm opt_par_thm lthy =
    7.24 +fun setup_lifting_package quot3_thm equiv_thm opt_par_thm lthy =
    7.25    let
    7.26      val (_ $ _ $ abs_fun $ _) = (HOLogic.dest_Trueprop o prop_of) quot3_thm
    7.27      val (T_def, lthy') = define_cr_rel equiv_thm abs_fun lthy
    7.28 @@ -128,11 +128,11 @@
    7.29        )
    7.30    in
    7.31      lthy'
    7.32 -      |> Lifting_Setup.setup_by_quotient gen_code quot_thm reflp_thm opt_par_thm
    7.33 +      |> Lifting_Setup.setup_by_quotient quot_thm reflp_thm opt_par_thm
    7.34        |> (snd oo Local_Theory.note) ((quotient_thm_name, []), [quot_thm])
    7.35    end
    7.36  
    7.37 -fun init_quotient_infr gen_code quot_thm equiv_thm opt_par_thm lthy =
    7.38 +fun init_quotient_infr quot_thm equiv_thm opt_par_thm lthy =
    7.39    let
    7.40      val (_ $ rel $ abs $ rep) = (HOLogic.dest_Trueprop o prop_of) quot_thm
    7.41      val (qtyp, rtyp) = (dest_funT o fastype_of) rep
    7.42 @@ -147,11 +147,11 @@
    7.43        |> Local_Theory.declaration {syntax = false, pervasive = true}
    7.44          (fn phi => Quotient_Info.update_quotients (qty_full_name, quot_info phi)
    7.45            #> Quotient_Info.update_abs_rep (qty_full_name, abs_rep_info phi))
    7.46 -      |> setup_lifting_package gen_code quot_thm equiv_thm opt_par_thm
    7.47 +      |> setup_lifting_package quot_thm equiv_thm opt_par_thm
    7.48    end
    7.49  
    7.50  (* main function for constructing a quotient type *)
    7.51 -fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, gen_code, opt_par_thm)), equiv_thm) lthy =
    7.52 +fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, opt_par_thm)), equiv_thm) lthy =
    7.53    let
    7.54      val part_equiv =
    7.55        if partial
    7.56 @@ -203,7 +203,7 @@
    7.57        quot_thm = quotient_thm}
    7.58  
    7.59      val lthy4 = lthy3
    7.60 -      |> init_quotient_infr gen_code quotient_thm equiv_thm opt_par_thm
    7.61 +      |> init_quotient_infr quotient_thm equiv_thm opt_par_thm
    7.62        |> (snd oo Local_Theory.note)
    7.63          ((equiv_thm_name,
    7.64            if partial then [] else @{attributes [quot_equiv]}),
    7.65 @@ -313,7 +313,7 @@
    7.66  
    7.67  fun quotient_type_cmd spec lthy =
    7.68    let
    7.69 -    fun parse_spec (((((((gen_code, vs), qty_name), mx), rty_str), (partial, rel_str)), opt_morphs), opt_par_xthm) lthy =
    7.70 +    fun parse_spec ((((((vs, qty_name), mx), rty_str), (partial, rel_str)), opt_morphs), opt_par_xthm) lthy =
    7.71        let
    7.72          val rty = Syntax.read_typ lthy rty_str
    7.73          val tmp_lthy1 = Variable.declare_typ rty lthy
    7.74 @@ -324,7 +324,7 @@
    7.75          val tmp_lthy2 = Variable.declare_term rel tmp_lthy1
    7.76          val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_par_xthm
    7.77        in
    7.78 -        (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, gen_code, opt_par_thm)), tmp_lthy2)
    7.79 +        (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, opt_par_thm)), tmp_lthy2)
    7.80        end
    7.81  
    7.82      val (spec', _) = parse_spec spec lthy
    7.83 @@ -332,13 +332,10 @@
    7.84      quotient_type spec' lthy
    7.85    end
    7.86  
    7.87 -val opt_gen_code =
    7.88 -  Scan.optional (@{keyword "("} |-- (Parse.reserved "no_code" >> K false) --| Parse.!!! @{keyword ")"}) true
    7.89 -
    7.90  val partial = Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false
    7.91  
    7.92  val quotspec_parser =
    7.93 -     (opt_gen_code -- Parse.type_args -- Parse.binding) --
    7.94 +     (Parse.type_args -- Parse.binding) --
    7.95        (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *)
    7.96        Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --
    7.97          (@{keyword "/"} |-- (partial -- Parse.term))  --
     8.1 --- a/src/HOL/Word/Word.thy	Fri Feb 06 19:17:17 2015 +0100
     8.2 +++ b/src/HOL/Word/Word.thy	Fri Feb 06 17:57:03 2015 +0100
     8.3 @@ -187,7 +187,7 @@
     8.4    "reflp (\<lambda>x y. bintrunc (len_of TYPE('a::len0)) x = bintrunc (len_of TYPE('a)) y)"
     8.5    by (simp add: reflp_def)
     8.6  
     8.7 -setup_lifting (no_code) Quotient_word reflp_word
     8.8 +setup_lifting Quotient_word reflp_word
     8.9  
    8.10  text {* TODO: The next lemma could be generated automatically. *}
    8.11