1.1 --- a/src/HOL/Library/Float.thy	Wed May 16 19:15:45 2012 +0200
     1.2 +++ b/src/HOL/Library/Float.thy	Wed May 16 19:17:20 2012 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4  lemma type_definition_float': "type_definition real float_of float"
     1.5    using type_definition_float unfolding real_of_float_def .
     1.6  
     1.7 -setup_lifting (no_abs_code) type_definition_float'
     1.8 +setup_lifting (no_code) type_definition_float'
     1.9  
    1.10  lemmas float_of_inject[simp]
    1.11  

     2.1 --- a/src/HOL/Lifting.thy	Wed May 16 19:15:45 2012 +0200
     2.2 +++ b/src/HOL/Lifting.thy	Wed May 16 19:17:20 2012 +0200
     2.3 @@ -82,10 +82,31 @@
     2.4    using a unfolding Quotient_def
     2.5    by blast
     2.6  
     2.7 +lemma Quotient_rep_abs_fold_unmap: 
     2.8 +  assumes "x' \<equiv> Abs x" and "R x x" and "Rep x' \<equiv> Rep' x'" 
     2.9 +  shows "R (Rep' x') x"
    2.10 +proof -
    2.11 +  have "R (Rep x') x" using assms(1-2) Quotient_rep_abs by auto
    2.12 +  then show ?thesis using assms(3) by simp
    2.13 +qed
    2.14 +
    2.15 +lemma Quotient_Rep_eq:
    2.16 +  assumes "x' \<equiv> Abs x" 
    2.17 +  shows "Rep x' \<equiv> Rep x'"
    2.18 +by simp
    2.19 +
    2.20  lemma Quotient_rel_abs: "R r s \<Longrightarrow> Abs r = Abs s"
    2.21    using a unfolding Quotient_def
    2.22    by blast
    2.23  
    2.24 +lemma Quotient_rel_abs2:
    2.25 +  assumes "R (Rep x) y"
    2.26 +  shows "x = Abs y"
    2.27 +proof -
    2.28 +  from assms have "Abs (Rep x) = Abs y" by (auto intro: Quotient_rel_abs)
    2.29 +  then show ?thesis using assms(1) by (simp add: Quotient_abs_rep)
    2.30 +qed
    2.31 +
    2.32  lemma Quotient_symp: "symp R"
    2.33    using a unfolding Quotient_def using sympI by (metis (full_types))
    2.34  

     3.1 --- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Wed May 16 19:15:45 2012 +0200
     3.2 +++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Wed May 16 19:17:20 2012 +0200
     3.3 @@ -81,6 +81,10 @@
     3.4      done
     3.5  qed
     3.6  
     3.7 +text {* We can export code: *}
     3.8 +
     3.9 +export_code fnil fcons fappend fmap ffilter fset in SML
    3.10 +
    3.11  text {* Note that the generated transfer rule contains a composition
    3.12    of relations. The transfer rule is not yet very useful in this form. *}
    3.13  

     4.1 --- a/src/HOL/Relation.thy	Wed May 16 19:15:45 2012 +0200
     4.2 +++ b/src/HOL/Relation.thy	Wed May 16 19:17:20 2012 +0200
     4.3 @@ -173,6 +173,11 @@
     4.4    obtains "r x x"
     4.5    using assms by (auto dest: refl_onD simp add: reflp_def)
     4.6  
     4.7 +lemma reflpD:
     4.8 +  assumes "reflp r"
     4.9 +  shows "r x x"
    4.10 +  using assms by (auto elim: reflpE)
    4.11 +
    4.12  lemma refl_on_Int: "refl_on A r ==> refl_on B s ==> refl_on (A \<inter> B) (r \<inter> s)"
    4.13    by (unfold refl_on_def) blast
    4.14  

     5.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Wed May 16 19:15:45 2012 +0200
     5.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Wed May 16 19:17:20 2012 +0200
     5.3 @@ -30,6 +30,14 @@
     5.4  fun get_binder_types (Type ("fun", [T, U]), Type ("fun", [V, W])) = (T, V) :: get_binder_types (U, W)
     5.5    | get_binder_types _ = []
     5.6  
     5.7 +fun get_binder_types_by_rel (Const (@{const_name "fun_rel"}, _) $ _ $ S) (Type ("fun", [T, U]), Type ("fun", [V, W])) = 
     5.8 +    (T, V) :: get_binder_types_by_rel S (U, W)
     5.9 +  | get_binder_types_by_rel _ _ = []
    5.10 +
    5.11 +fun get_body_type_by_rel (Const (@{const_name "fun_rel"}, _) $ _ $ S) (Type ("fun", [_, U]), Type ("fun", [_, V])) = 
    5.12 +    get_body_type_by_rel S (U, V)
    5.13 +  | get_body_type_by_rel _ (U, V)  = (U, V)
    5.14 +
    5.15  fun force_rty_type ctxt rty rhs = 
    5.16    let
    5.17      val thy = Proof_Context.theory_of ctxt
    5.18 @@ -75,9 +83,14 @@
    5.19          Const (@{const_name "map_fun"}, _) $ _ $ _ => 
    5.20            (Conv.arg_conv unfold_conv then_conv Conv.rewr_conv map_fun_unfolded) ctm
    5.21          | _ => Conv.all_conv ctm
    5.22 -    val try_beta_conv = Conv.try_conv (Thm.beta_conversion false)
    5.23    in
    5.24 -    (Conv.arg_conv (Conv.fun_conv unfold_conv then_conv try_beta_conv)) ctm
    5.25 +    (Conv.fun_conv unfold_conv) ctm
    5.26 +  end
    5.27 +
    5.28 +fun unfold_fun_maps_beta ctm =
    5.29 +  let val try_beta_conv = Conv.try_conv (Thm.beta_conversion false)
    5.30 +  in 
    5.31 +    (unfold_fun_maps then_conv try_beta_conv) ctm 
    5.32    end
    5.33  
    5.34  fun prove_rel ctxt rsp_thm (rty, qty) =
    5.35 @@ -121,7 +134,7 @@
    5.36          Const (@{const_name HOL.eq}, _) $ _ $ _ => abs_rep_thm
    5.37          | Const (@{const_name invariant}, _) $ _ $ _ $ _ => abs_rep_thm RS @{thm invariant_to_eq}
    5.38          | _ => raise CODE_CERT_GEN "relation is neither equality nor invariant"
    5.39 -    val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm
    5.40 +    val unfolded_def = Conv.fconv_rule (Conv.arg_conv unfold_fun_maps_beta) def_thm
    5.41      val unabs_def = unabs_all_def ctxt unfolded_def
    5.42      val rep = (cterm_of thy o Lifting_Term.quot_thm_rep) quot_thm
    5.43      val rep_refl = Thm.reflexive rep RS @{thm meta_eq_to_obj_eq}
    5.44 @@ -131,53 +144,150 @@
    5.45      simplify_code_eq ctxt code_cert
    5.46    end
    5.47  
    5.48 -fun is_abstype ctxt typ =
    5.49 +fun generate_trivial_rep_eq ctxt def_thm =
    5.50    let
    5.51 -    val thy = Proof_Context.theory_of ctxt
    5.52 -    val type_name = (fst o dest_Type) typ
    5.53 +    val unfolded_def = Conv.fconv_rule (Conv.arg_conv unfold_fun_maps_beta) def_thm
    5.54 +    val code_eq = unabs_all_def ctxt unfolded_def
    5.55 +    val simp_code_eq = simplify_code_eq ctxt code_eq
    5.56    in
    5.57 -    (snd oo Code.get_type) thy type_name
    5.58 +    simp_code_eq
    5.59    end
    5.60 +
    5.61 +fun generate_rep_eq ctxt def_thm rsp_thm (rty, qty) =
    5.62 +  if body_type rty = body_type qty then 
    5.63 +    SOME (generate_trivial_rep_eq ctxt def_thm)
    5.64 +  else 
    5.65 +    let
    5.66 +      val (rty_body, qty_body) = get_body_types (rty, qty)
    5.67 +      val quot_thm = Lifting_Term.prove_quot_thm ctxt (rty_body, qty_body)
    5.68 +    in
    5.69 +      if can_generate_code_cert quot_thm then
    5.70 +        SOME (generate_code_cert ctxt def_thm rsp_thm (rty, qty))
    5.71 +      else 
    5.72 +        NONE
    5.73 +    end
    5.74 +
    5.75 +fun generate_abs_eq ctxt def_thm rsp_thm quot_thm =
    5.76 +  let
    5.77 +    fun refl_tac ctxt =
    5.78 +      let
    5.79 +        fun intro_reflp_tac (t, i) = 
    5.80 +        let
    5.81 +          val concl_pat = Drule.strip_imp_concl (cprop_of @{thm reflpD})
    5.82 +          val insts = Thm.first_order_match (concl_pat, t)
    5.83 +        in
    5.84 +          rtac (Drule.instantiate_normalize insts @{thm reflpD}) i
    5.85 +        end
    5.86 +        handle Pattern.MATCH => no_tac
    5.87 +        
    5.88 +        val fun_rel_meta_eq = mk_meta_eq @{thm fun_rel_eq}
    5.89 +        val conv = Conv.bottom_conv (K (Conv.try_conv (Conv.rewr_conv fun_rel_meta_eq))) ctxt
    5.90 +        val rules = Lifting_Info.get_reflp_preserve_rules ctxt
    5.91 +      in
    5.92 +        EVERY' [CSUBGOAL intro_reflp_tac, 
    5.93 +                CONVERSION conv,
    5.94 +                REPEAT_ALL_NEW (resolve_tac rules)]
    5.95 +      end
    5.96 +    
    5.97 +    fun try_prove_prem ctxt prop =
    5.98 +      SOME (Goal.prove ctxt [] [] prop (fn {context, ...} => refl_tac context 1))
    5.99 +        handle ERROR _ => NONE
   5.100 +
   5.101 +    val abs_eq_with_assms =
   5.102 +      let
   5.103 +        val (rty, qty) = Lifting_Term.quot_thm_rty_qty quot_thm
   5.104 +        val rel = Lifting_Term.quot_thm_rel quot_thm
   5.105 +        val ty_args = get_binder_types_by_rel rel (rty, qty)
   5.106 +        val body_type = get_body_type_by_rel rel (rty, qty)
   5.107 +        val quot_ret_thm = Lifting_Term.prove_quot_thm ctxt body_type
   5.108 +        
   5.109 +        val rep_abs_folded_unmapped_thm = 
   5.110 +          let
   5.111 +            val rep_id = [quot_thm, def_thm] MRSL @{thm Quotient_Rep_eq}
   5.112 +            val ctm = Thm.dest_equals_lhs (cprop_of rep_id)
   5.113 +            val unfolded_maps_eq = unfold_fun_maps ctm
   5.114 +            val t1 = [quot_thm, def_thm, rsp_thm] MRSL @{thm Quotient_rep_abs_fold_unmap}
   5.115 +            val prems_pat = (hd o Drule.cprems_of) t1
   5.116 +            val insts = Thm.first_order_match (prems_pat, cprop_of unfolded_maps_eq)
   5.117 +          in
   5.118 +            unfolded_maps_eq RS (Drule.instantiate_normalize insts t1)
   5.119 +          end
   5.120 +      in
   5.121 +        rep_abs_folded_unmapped_thm
   5.122 +        |> fold (fn _ => fn thm => thm RS @{thm fun_relD2}) ty_args
   5.123 +        |> (fn x => x RS (@{thm Quotient_rel_abs2} OF [quot_ret_thm]))
   5.124 +      end
   5.125 +    
   5.126 +    val prems = prems_of abs_eq_with_assms
   5.127 +    val indexed_prems = map_index (apfst (fn x => x + 1)) prems
   5.128 +    val indexed_assms = map (apsnd (try_prove_prem ctxt)) indexed_prems
   5.129 +    val proved_assms = map (apsnd the) (filter (is_some o snd) indexed_assms)
   5.130 +    val abs_eq = fold_rev (fn (i, assms) => fn thm => assms RSN (i, thm)) proved_assms abs_eq_with_assms
   5.131 +  in
   5.132 +    simplify_code_eq ctxt abs_eq
   5.133 +  end
   5.134 +
   5.135 +fun define_code_using_abs_eq abs_eq_thm lthy =
   5.136 +  if null (Logic.strip_imp_prems(prop_of abs_eq_thm)) then
   5.137 +    (snd oo Local_Theory.note) ((Binding.empty, [Code.add_default_eqn_attrib]), [abs_eq_thm]) lthy
   5.138 +  else
   5.139 +    lthy
   5.140    
   5.141 -
   5.142 -fun define_code_cert code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy = 
   5.143 -  let
   5.144 -    val (rty_body, qty_body) = get_body_types (rty, qty)
   5.145 -    val quot_thm = Lifting_Term.prove_quot_thm lthy (rty_body, qty_body)
   5.146 -  in
   5.147 -    if can_generate_code_cert quot_thm then
   5.148 +fun define_code_using_rep_eq maybe_rep_eq_thm lthy = 
   5.149 +  case maybe_rep_eq_thm of
   5.150 +    SOME rep_eq_thm =>   
   5.151        let
   5.152 -        val code_cert = generate_code_cert lthy def_thm rsp_thm (rty, qty)
   5.153          val add_abs_eqn_attribute = 
   5.154            Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abs_eqn thm) I)
   5.155          val add_abs_eqn_attrib = Attrib.internal (K add_abs_eqn_attribute);
   5.156 -        val lthy' = 
   5.157 -          (snd oo Local_Theory.note) ((code_eqn_thm_name, []), [code_cert]) lthy
   5.158        in
   5.159 -        if is_abstype lthy qty_body then
   5.160 -          (snd oo Local_Theory.note) ((Binding.empty, [add_abs_eqn_attrib]), [code_cert]) lthy'
   5.161 -        else
   5.162 -          lthy'
   5.163 +        (snd oo Local_Theory.note) ((Binding.empty, [add_abs_eqn_attrib]), [rep_eq_thm]) lthy
   5.164        end
   5.165 +    | NONE => lthy
   5.166 +
   5.167 +fun has_constr ctxt quot_thm =
   5.168 +  let
   5.169 +    val thy = Proof_Context.theory_of ctxt
   5.170 +    val abs_fun = Lifting_Term.quot_thm_abs quot_thm
   5.171 +  in
   5.172 +    if is_Const abs_fun then
   5.173 +      Code.is_constr thy ((fst o dest_Const) abs_fun)
   5.174      else
   5.175 -      lthy
   5.176 +      false
   5.177    end
   5.178  
   5.179 -fun define_code_eq code_eqn_thm_name def_thm lthy =
   5.180 +fun has_abstr ctxt quot_thm =
   5.181    let
   5.182 -    val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm
   5.183 -    val code_eq = unabs_all_def lthy unfolded_def
   5.184 -    val simp_code_eq = simplify_code_eq lthy code_eq
   5.185 +    val thy = Proof_Context.theory_of ctxt
   5.186 +    val abs_fun = Lifting_Term.quot_thm_abs quot_thm
   5.187    in
   5.188 -    lthy
   5.189 -      |> (snd oo Local_Theory.note) ((code_eqn_thm_name, [Code.add_default_eqn_attrib]), [simp_code_eq])
   5.190 +    if is_Const abs_fun then
   5.191 +      Code.is_abstr thy ((fst o dest_Const) abs_fun)
   5.192 +    else
   5.193 +      false
   5.194    end
   5.195  
   5.196 -fun define_code code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy =
   5.197 -  if body_type rty = body_type qty then 
   5.198 -    define_code_eq code_eqn_thm_name def_thm lthy
   5.199 -  else 
   5.200 -    define_code_cert code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy
   5.201 +fun define_code abs_eq_thm maybe_rep_eq_thm (rty, qty) lthy =
   5.202 +  let
   5.203 +    val (rty_body, qty_body) = get_body_types (rty, qty)
   5.204 +  in
   5.205 +    if rty_body = qty_body then
   5.206 +      if null (Logic.strip_imp_prems(prop_of abs_eq_thm)) then
   5.207 +        (snd oo Local_Theory.note) ((Binding.empty, [Code.add_default_eqn_attrib]), [abs_eq_thm]) lthy
   5.208 +      else
   5.209 +        (snd oo Local_Theory.note) ((Binding.empty, [Code.add_default_eqn_attrib]), [the maybe_rep_eq_thm]) lthy
   5.210 +    else
   5.211 +      let 
   5.212 +        val body_quot_thm = Lifting_Term.prove_quot_thm lthy (rty_body, qty_body)
   5.213 +      in
   5.214 +        if has_constr lthy body_quot_thm then
   5.215 +          define_code_using_abs_eq abs_eq_thm lthy
   5.216 +        else if has_abstr lthy body_quot_thm then
   5.217 +          define_code_using_rep_eq maybe_rep_eq_thm lthy
   5.218 +        else
   5.219 +          lthy
   5.220 +      end
   5.221 +  end
   5.222  
   5.223  (*
   5.224    Defines an operation on an abstract type in terms of a corresponding operation 
   5.225 @@ -186,15 +296,15 @@
   5.226    var - a binding and a mixfix of the new constant being defined
   5.227    qty - an abstract type of the new constant
   5.228    rhs - a term representing the new constant on the raw level
   5.229 -  rsp_thm - a respectfulness theorem in the internal form (like (R ===> R ===> R) f f),
   5.230 +  rsp_thm - a respectfulness theorem in the internal tagged form (like '(R ===> R ===> R) f f'),
   5.231      i.e. "(Lifting_Term.equiv_relation (fastype_of rhs, qty)) $ rhs $ rhs"
   5.232  *)
   5.233  
   5.234  fun add_lift_def var qty rhs rsp_thm lthy =
   5.235    let
   5.236      val rty = fastype_of rhs
   5.237 -    val quotient_thm = Lifting_Term.prove_quot_thm lthy (rty, qty)
   5.238 -    val absrep_trm =  Lifting_Term.quot_thm_abs quotient_thm
   5.239 +    val quot_thm = Lifting_Term.prove_quot_thm lthy (rty, qty)
   5.240 +    val absrep_trm =  Lifting_Term.quot_thm_abs quot_thm
   5.241      val rty_forced = (domain_type o fastype_of) absrep_trm
   5.242      val forced_rhs = force_rty_type lthy rty_forced rhs
   5.243      val lhs = Free (Binding.print (#1 var), qty)
   5.244 @@ -205,21 +315,29 @@
   5.245      val ((_, (_ , def_thm)), lthy') = 
   5.246        Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy
   5.247  
   5.248 -    val transfer_thm = ([quotient_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer})
   5.249 +    val transfer_thm = ([quot_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer})
   5.250          |> Raw_Simplifier.rewrite_rule (Transfer.get_relator_eq lthy')
   5.251 +     
   5.252 +    val abs_eq_thm = generate_abs_eq lthy' def_thm rsp_thm quot_thm
   5.253 +    val maybe_rep_eq_thm = generate_rep_eq lthy' def_thm rsp_thm (rty_forced, qty)
   5.254  
   5.255      fun qualify defname suffix = Binding.qualified true suffix defname
   5.256  
   5.257      val lhs_name = (#1 var)
   5.258      val rsp_thm_name = qualify lhs_name "rsp"
   5.259 -    val code_eqn_thm_name = qualify lhs_name "rep_eq"
   5.260 +    val abs_eq_thm_name = qualify lhs_name "abs_eq"
   5.261 +    val rep_eq_thm_name = qualify lhs_name "rep_eq"
   5.262      val transfer_thm_name = qualify lhs_name "transfer"
   5.263      val transfer_attr = Attrib.internal (K Transfer.transfer_add)
   5.264    in
   5.265      lthy'
   5.266        |> (snd oo Local_Theory.note) ((rsp_thm_name, []), [rsp_thm])
   5.267        |> (snd oo Local_Theory.note) ((transfer_thm_name, [transfer_attr]), [transfer_thm])
   5.268 -      |> define_code code_eqn_thm_name def_thm rsp_thm (rty_forced, qty)
   5.269 +      |> (snd oo Local_Theory.note) ((abs_eq_thm_name, []), [abs_eq_thm])
   5.270 +      |> (case maybe_rep_eq_thm of 
   5.271 +            SOME rep_eq_thm => (snd oo Local_Theory.note) ((rep_eq_thm_name, []), [rep_eq_thm])
   5.272 +            | NONE => I)
   5.273 +      |> define_code abs_eq_thm maybe_rep_eq_thm (rty_forced, qty)
   5.274    end
   5.275  
   5.276  fun mk_readable_rsp_thm_eq tm lthy =
   5.277 @@ -253,7 +371,7 @@
   5.278              (binop_conv2  left_conv simp_arrows_conv then_conv unfold_conv) ctm
   5.279            | _ => invariant_commute_conv ctm
   5.280        end
   5.281 -
   5.282 +    
   5.283      val unfold_ret_val_invs = Conv.bottom_conv 
   5.284        (K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy 
   5.285      val simp_conv = Trueprop_conv (Conv.fun2_conv simp_arrows_conv)

     6.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Wed May 16 19:15:45 2012 +0200
     6.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Wed May 16 19:17:20 2012 +0200
     6.3 @@ -36,8 +36,26 @@
     6.4      (def_thm, lthy'')
     6.5    end
     6.6  
     6.7 -fun define_abs_type gen_abs_code quot_thm lthy =
     6.8 -  if gen_abs_code andalso Lifting_Def.can_generate_code_cert quot_thm then
     6.9 +fun define_code_constr gen_code quot_thm lthy =
    6.10 +  let
    6.11 +    val abs = Lifting_Term.quot_thm_abs quot_thm
    6.12 +    val abs_background = Morphism.term (Local_Theory.target_morphism lthy) abs
    6.13 +  in
    6.14 +    if gen_code andalso is_Const abs_background then
    6.15 +      let
    6.16 +        val (const_name, typ) = dest_Const abs_background
    6.17 +        val fake_term = Logic.mk_type typ
    6.18 +        val (fixed_fake_term, lthy') = yield_singleton(Variable.importT_terms) fake_term lthy
    6.19 +        val fixed_type = Logic.dest_type fixed_fake_term
    6.20 +      in  
    6.21 +         Local_Theory.background_theory(Code.add_datatype [(const_name, fixed_type)]) lthy'
    6.22 +      end
    6.23 +    else
    6.24 +      lthy
    6.25 +  end
    6.26 +
    6.27 +fun define_abs_type gen_code quot_thm lthy =
    6.28 +  if gen_code andalso Lifting_Def.can_generate_code_cert quot_thm then
    6.29      let
    6.30        val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep}
    6.31        val add_abstype_attribute = 
    6.32 @@ -76,31 +94,37 @@
    6.33                                                  @ (map Pretty.string_of errs)))
    6.34    end
    6.35  
    6.36 -fun setup_lifting_infr gen_abs_code quot_thm lthy =
    6.37 +fun setup_lifting_infr gen_code quot_thm maybe_reflp_thm lthy =
    6.38    let
    6.39      val _ = quot_thm_sanity_check lthy quot_thm
    6.40      val (_, qtyp) = Lifting_Term.quot_thm_rty_qty quot_thm
    6.41      val qty_full_name = (fst o dest_Type) qtyp
    6.42      val quotients = { quot_thm = quot_thm }
    6.43      fun quot_info phi = Lifting_Info.transform_quotients phi quotients
    6.44 +    val lthy' = case maybe_reflp_thm of
    6.45 +      SOME reflp_thm => lthy
    6.46 +        |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflp_preserve_rule_attrib]),
    6.47 +              [reflp_thm])
    6.48 +        |> define_code_constr gen_code quot_thm
    6.49 +      | NONE => lthy
    6.50 +        |> define_abs_type gen_code quot_thm
    6.51    in
    6.52 -    lthy
    6.53 +    lthy'
    6.54        |> Local_Theory.declaration {syntax = false, pervasive = true}
    6.55          (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi))
    6.56 -      |> define_abs_type gen_abs_code quot_thm
    6.57    end
    6.58  
    6.59  (*
    6.60    Sets up the Lifting package by a quotient theorem.
    6.61  
    6.62 -  gen_abs_code - flag if an abstract type given by quot_thm should be registred 
    6.63 +  gen_code - flag if an abstract type given by quot_thm should be registred 
    6.64      as an abstract type in the code generator
    6.65    quot_thm - a quotient theorem (Quotient R Abs Rep T)
    6.66    maybe_reflp_thm - a theorem saying that a relation from quot_thm is reflexive
    6.67      (in the form "reflp R")
    6.68  *)
    6.69  
    6.70 -fun setup_by_quotient gen_abs_code quot_thm maybe_reflp_thm lthy =
    6.71 +fun setup_by_quotient gen_code quot_thm maybe_reflp_thm lthy =
    6.72    let
    6.73      val transfer_attr = Attrib.internal (K Transfer.transfer_add)
    6.74      val (_, qty) = Lifting_Term.quot_thm_rty_qty quot_thm
    6.75 @@ -117,8 +141,6 @@
    6.76            [[quot_thm, reflp_thm] MRSL @{thm Quotient_total_abs_induct}])
    6.77          |> (snd oo Local_Theory.note) ((qualify "abs_eq_iff", []),
    6.78            [[quot_thm, reflp_thm] MRSL @{thm Quotient_total_abs_eq_iff}])
    6.79 -        |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflp_preserve_rule_attrib]),
    6.80 -          [reflp_thm])
    6.81        | NONE => lthy
    6.82          |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]), 
    6.83            [quot_thm RS @{thm Quotient_All_transfer}])
    6.84 @@ -136,18 +158,18 @@
    6.85          [quot_thm RS @{thm Quotient_right_total}])
    6.86        |> (snd oo Local_Theory.note) ((qualify "rel_eq_transfer", [transfer_attr]), 
    6.87          [quot_thm RS @{thm Quotient_rel_eq_transfer}])
    6.88 -      |> setup_lifting_infr gen_abs_code quot_thm
    6.89 +      |> setup_lifting_infr gen_code quot_thm maybe_reflp_thm
    6.90    end
    6.91  
    6.92  (*
    6.93    Sets up the Lifting package by a typedef theorem.
    6.94  
    6.95 -  gen_abs_code - flag if an abstract type given by typedef_thm should be registred 
    6.96 +  gen_code - flag if an abstract type given by typedef_thm should be registred 
    6.97      as an abstract type in the code generator
    6.98    typedef_thm - a typedef theorem (type_definition Rep Abs S)
    6.99  *)
   6.100  
   6.101 -fun setup_by_typedef_thm gen_abs_code typedef_thm lthy =
   6.102 +fun setup_by_typedef_thm gen_code typedef_thm lthy =
   6.103    let
   6.104      val transfer_attr = Attrib.internal (K Transfer.transfer_add)
   6.105      val (_ $ rep_fun $ _ $ typedef_set) = (HOLogic.dest_Trueprop o prop_of) typedef_thm
   6.106 @@ -166,7 +188,7 @@
   6.107      fun qualify suffix = Binding.qualified true suffix qty_name
   6.108      val simplify = Raw_Simplifier.rewrite_rule [mk_meta_eq @{thm mem_Collect_eq}]
   6.109  
   6.110 -    val lthy'' = case typedef_set of
   6.111 +    val (maybe_reflp_thm, lthy'') = case typedef_set of
   6.112        Const ("Orderings.top_class.top", _) => 
   6.113          let
   6.114            val equivp_thm = typedef_thm RS @{thm UNIV_typedef_to_equivp}
   6.115 @@ -177,8 +199,7 @@
   6.116                [[quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}])
   6.117              |> (snd oo Local_Theory.note) ((qualify "id_abs_transfer", [transfer_attr]), 
   6.118                [[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}])
   6.119 -            |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflp_preserve_rule_attrib]),
   6.120 -              [reflp_thm])
   6.121 +            |> pair (SOME reflp_thm)
   6.122          end
   6.123        | _ => lthy'
   6.124          |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]), 
   6.125 @@ -187,6 +208,7 @@
   6.126            [[typedef_thm, T_def] MRSL @{thm typedef_Ex_transfer}])
   6.127          |> (snd oo Local_Theory.note) ((qualify "forall_transfer", [transfer_attr]), 
   6.128            [simplify ([typedef_thm, T_def] MRSL @{thm typedef_forall_transfer})])
   6.129 +        |> pair NONE
   6.130    in
   6.131      lthy''
   6.132        |> (snd oo Local_Theory.note) ((qualify "bi_unique", [transfer_attr]), 
   6.133 @@ -197,10 +219,10 @@
   6.134          [[quot_thm] MRSL @{thm Quotient_right_unique}])
   6.135        |> (snd oo Local_Theory.note) ((qualify "right_total", [transfer_attr]), 
   6.136          [[quot_thm] MRSL @{thm Quotient_right_total}])
   6.137 -      |> setup_lifting_infr gen_abs_code quot_thm
   6.138 +      |> setup_lifting_infr gen_code quot_thm maybe_reflp_thm
   6.139    end
   6.140  
   6.141 -fun setup_lifting_cmd gen_abs_code xthm opt_reflp_xthm lthy =
   6.142 +fun setup_lifting_cmd gen_code xthm opt_reflp_xthm lthy =
   6.143    let 
   6.144      val input_thm = singleton (Attrib.eval_thms lthy) xthm
   6.145      val input_term = (HOLogic.dest_Trueprop o prop_of) input_thm
   6.146 @@ -223,14 +245,14 @@
   6.147              val reflp_thm = singleton (Attrib.eval_thms lthy) reflp_xthm
   6.148              val _ = sanity_check_reflp_thm reflp_thm
   6.149            in
   6.150 -            setup_by_quotient gen_abs_code input_thm (SOME reflp_thm) lthy
   6.151 +            setup_by_quotient gen_code input_thm (SOME reflp_thm) lthy
   6.152            end
   6.153 -        | NONE => setup_by_quotient gen_abs_code input_thm NONE lthy
   6.154 +        | NONE => setup_by_quotient gen_code input_thm NONE lthy
   6.155  
   6.156      fun setup_typedef () = 
   6.157        case opt_reflp_xthm of
   6.158          SOME _ => error "The reflexivity theorem cannot be specified if the type_definition theorem is used."
   6.159 -        | NONE => setup_by_typedef_thm gen_abs_code input_thm lthy
   6.160 +        | NONE => setup_by_typedef_thm gen_code input_thm lthy
   6.161    in
   6.162      case input_term of
   6.163        (Const (@{const_name Quotient}, _) $ _ $ _ $ _ $ _) => setup_quotient ()
   6.164 @@ -238,12 +260,12 @@
   6.165        | _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported."
   6.166    end
   6.167  
   6.168 -val opt_gen_abs_code =
   6.169 -  Scan.optional (@{keyword "("} |-- Parse.!!! ((Parse.reserved "no_abs_code" >> K false) --| @{keyword ")"})) true
   6.170 +val opt_gen_code =
   6.171 +  Scan.optional (@{keyword "("} |-- Parse.!!! ((Parse.reserved "no_code" >> K false) --| @{keyword ")"})) true
   6.172  
   6.173  val _ = 
   6.174    Outer_Syntax.local_theory @{command_spec "setup_lifting"}
   6.175      "Setup lifting infrastructure" 
   6.176 -      (opt_gen_abs_code -- Parse_Spec.xthm -- Scan.option Parse_Spec.xthm >> 
   6.177 -        (fn ((gen_abs_code, xthm), opt_reflp_xthm) => setup_lifting_cmd gen_abs_code xthm opt_reflp_xthm))
   6.178 +      (opt_gen_code -- Parse_Spec.xthm -- Scan.option Parse_Spec.xthm >> 
   6.179 +        (fn ((gen_code, xthm), opt_reflp_xthm) => setup_lifting_cmd gen_code xthm opt_reflp_xthm))
   6.180  end;

     7.1 --- a/src/HOL/Tools/Quotient/quotient_type.ML	Wed May 16 19:15:45 2012 +0200
     7.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML	Wed May 16 19:17:20 2012 +0200
     7.3 @@ -9,12 +9,12 @@
     7.4    val can_generate_code_cert: thm -> bool
     7.5    
     7.6    val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * 
     7.7 -    ((binding * binding) option)) * thm -> local_theory -> Quotient_Info.quotients * local_theory
     7.8 +    ((binding * binding) option * bool)) * 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)) list -> Proof.context -> Proof.state
    7.12 +    ((binding * binding) option * bool)) list -> Proof.context -> Proof.state
    7.13  
    7.14 -  val quotient_type_cmd: (((((string list * binding) * mixfix) * string) * (bool * string)) *
    7.15 +  val quotient_type_cmd: ((((((bool * string list) * binding) * mixfix) * string) * (bool * string)) *
    7.16      (binding * binding) option) list -> Proof.context -> Proof.state
    7.17  end;
    7.18  
    7.19 @@ -132,7 +132,7 @@
    7.20      (def_thm, lthy'')
    7.21    end;
    7.22  
    7.23 -fun setup_lifting_package quot3_thm equiv_thm lthy =
    7.24 +fun setup_lifting_package gen_code quot3_thm equiv_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 @@ -150,11 +150,11 @@
    7.29        )
    7.30    in
    7.31      lthy'
    7.32 -      |> Lifting_Setup.setup_by_quotient false quot_thm reflp_thm
    7.33 +      |> Lifting_Setup.setup_by_quotient gen_code quot_thm reflp_thm
    7.34        |> (snd oo Local_Theory.note) ((quotient_thm_name, []), [quot_thm])
    7.35    end
    7.36  
    7.37 -fun init_quotient_infr quot_thm equiv_thm lthy =
    7.38 +fun init_quotient_infr gen_code quot_thm equiv_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 @@ -170,11 +170,11 @@
    7.43          (fn phi => Quotient_Info.update_quotients qty_full_name (quot_info phi)
    7.44            #> Quotient_Info.update_abs_rep qty_full_name (abs_rep_info phi))
    7.45        |> define_abs_type quot_thm
    7.46 -      |> setup_lifting_package quot_thm equiv_thm
    7.47 +      |> setup_lifting_package gen_code quot_thm equiv_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), equiv_thm) lthy =
    7.52 +fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, gen_code)), equiv_thm) lthy =
    7.53    let
    7.54      val part_equiv =
    7.55        if partial
    7.56 @@ -226,7 +226,7 @@
    7.57        quot_thm = quotient_thm}
    7.58  
    7.59      val lthy4 = lthy3
    7.60 -      |> init_quotient_infr quotient_thm equiv_thm
    7.61 +      |> init_quotient_infr gen_code quotient_thm equiv_thm
    7.62        |> (snd oo Local_Theory.note)
    7.63          ((equiv_thm_name,
    7.64            if partial then [] else [Attrib.internal (K Quotient_Info.equiv_rules_add)]),
    7.65 @@ -307,6 +307,7 @@
    7.66   - the partial flag (a boolean)
    7.67   - the relation according to which the type is quotient
    7.68   - optional names of morphisms (rep/abs)
    7.69 + - flag if code should be generated by Lifting package
    7.70  
    7.71   it opens a proof-state in which one has to show that the
    7.72   relations are equivalence relations
    7.73 @@ -336,7 +337,7 @@
    7.74  
    7.75  fun quotient_type_cmd specs lthy =
    7.76    let
    7.77 -    fun parse_spec (((((vs, qty_name), mx), rty_str), (partial, rel_str)), opt_morphs) lthy =
    7.78 +    fun parse_spec ((((((gen_code, vs), qty_name), mx), rty_str), (partial, rel_str)), opt_morphs) lthy =
    7.79        let
    7.80          val rty = Syntax.read_typ lthy rty_str
    7.81          val tmp_lthy1 = Variable.declare_typ rty lthy
    7.82 @@ -346,7 +347,7 @@
    7.83            |> Syntax.check_term tmp_lthy1
    7.84          val tmp_lthy2 = Variable.declare_term rel tmp_lthy1
    7.85        in
    7.86 -        (((vs, qty_name, mx), (rty, rel, partial), opt_morphs), tmp_lthy2)
    7.87 +        (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, gen_code)), tmp_lthy2)
    7.88        end
    7.89  
    7.90      val (spec', _) = fold_map parse_spec specs lthy
    7.91 @@ -354,11 +355,14 @@
    7.92      quotient_type spec' lthy
    7.93    end
    7.94  
    7.95 +val opt_gen_code =
    7.96 +  Scan.optional (@{keyword "("} |-- (Parse.reserved "no_code" >> K false) --| Parse.!!! @{keyword ")"}) true
    7.97 +
    7.98  val partial = Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false
    7.99  
   7.100  val quotspec_parser =
   7.101    Parse.and_list1
   7.102 -    ((Parse.type_args -- Parse.binding) --
   7.103 +    ((opt_gen_code -- Parse.type_args -- Parse.binding) --
   7.104        (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *)
   7.105        Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --
   7.106          (@{keyword "/"} |-- (partial -- Parse.term))  --

     8.1 --- a/src/HOL/Transfer.thy	Wed May 16 19:15:45 2012 +0200
     8.2 +++ b/src/HOL/Transfer.thy	Wed May 16 19:17:20 2012 +0200
     8.3 @@ -26,6 +26,11 @@
     8.4    shows "B (f x) (g y)"
     8.5    using assms by (simp add: fun_rel_def)
     8.6  
     8.7 +lemma fun_relD2:
     8.8 +  assumes "(A ===> B) f g" and "A x x"
     8.9 +  shows "B (f x) (g x)"
    8.10 +  using assms unfolding fun_rel_def by auto
    8.11 +
    8.12  lemma fun_relE:
    8.13    assumes "(A ===> B) f g" and "A x y"
    8.14    obtains "B (f x) (g y)"