refactoring; generate rep_eq always, not only when it would be accepted by the code generator
authorkuncar
Thu Feb 20 16:56:33 2014 +0100 (2014-02-20)
changeset 556109066b603dff6
parent 55609 69ac773a467f
child 55637 79a43f8e18a3
refactoring; generate rep_eq always, not only when it would be accepted by the code generator
src/HOL/Lifting.thy
src/HOL/Tools/Lifting/lifting_def.ML
     1.1 --- a/src/HOL/Lifting.thy	Thu Feb 20 16:56:32 2014 +0100
     1.2 +++ b/src/HOL/Lifting.thy	Thu Feb 20 16:56:33 2014 +0100
     1.3 @@ -155,6 +155,10 @@
     1.4    using a unfolding Quotient_def
     1.5    by blast
     1.6  
     1.7 +lemma Quotient_rep_abs_eq: "R t t \<Longrightarrow> R \<le> op= \<Longrightarrow> Rep (Abs t) = t"
     1.8 +  using a unfolding Quotient_def
     1.9 +  by blast
    1.10 +
    1.11  lemma Quotient_rep_abs_fold_unmap: 
    1.12    assumes "x' \<equiv> Abs x" and "R x x" and "Rep x' \<equiv> Rep' x'" 
    1.13    shows "R (Rep' x') x"
     2.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Thu Feb 20 16:56:32 2014 +0100
     2.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Thu Feb 20 16:56:33 2014 +0100
     2.3 @@ -46,7 +46,7 @@
     2.4      val prop = hd (prems_of rule)
     2.5    in
     2.6      case mono_eq_prover ctxt prop of
     2.7 -      SOME thm => SOME (rule OF [thm])
     2.8 +      SOME thm => SOME (thm RS rule)
     2.9        | NONE => NONE
    2.10    end
    2.11  
    2.12 @@ -259,50 +259,35 @@
    2.13      | Const (@{const_name invariant}, _) $ _  => true
    2.14      | _ => false
    2.15  
    2.16 -fun generate_code_cert ctxt def_thm rsp_thm (rty, qty) =
    2.17 +fun generate_rep_eq ctxt def_thm rsp_thm (rty, qty) =
    2.18    let
    2.19 -    val thy = Proof_Context.theory_of ctxt
    2.20 -    val quot_thm = Lifting_Term.prove_quot_thm ctxt (get_body_types (rty, qty))
    2.21 -    val fun_rel = prove_rel ctxt rsp_thm (rty, qty)
    2.22 -    val abs_rep_thm = [quot_thm, fun_rel] MRSL @{thm Quotient_rep_abs}
    2.23 -    val abs_rep_eq = 
    2.24 -      case (HOLogic.dest_Trueprop o prop_of) fun_rel of
    2.25 -        Const (@{const_name HOL.eq}, _) $ _ $ _ => abs_rep_thm
    2.26 -        | Const (@{const_name invariant}, _) $ _ $ _ $ _ => abs_rep_thm RS @{thm invariant_to_eq}
    2.27 -        | _ => raise CODE_CERT_GEN "relation is neither equality nor invariant"
    2.28      val unfolded_def = Conv.fconv_rule (Conv.arg_conv unfold_fun_maps_beta) def_thm
    2.29      val unabs_def = unabs_all_def ctxt unfolded_def
    2.30 -    val rep = (cterm_of thy o quot_thm_rep) quot_thm
    2.31 -    val rep_refl = Thm.reflexive rep RS @{thm meta_eq_to_obj_eq}
    2.32 -    val repped_eq = [rep_refl, unabs_def RS @{thm meta_eq_to_obj_eq}] MRSL @{thm cong}
    2.33 -    val code_cert = [repped_eq, abs_rep_eq] MRSL @{thm trans}
    2.34 -  in
    2.35 -    simplify_code_eq ctxt code_cert
    2.36 +  in  
    2.37 +    if body_type rty = body_type qty then 
    2.38 +      SOME (simplify_code_eq ctxt unabs_def)
    2.39 +    else 
    2.40 +      let
    2.41 +        val thy = Proof_Context.theory_of ctxt
    2.42 +        val quot_thm = Lifting_Term.prove_quot_thm ctxt (get_body_types (rty, qty))
    2.43 +        val fun_rel = prove_rel ctxt rsp_thm (rty, qty)
    2.44 +        val rep_abs_thm = [quot_thm, fun_rel] MRSL @{thm Quotient_rep_abs_eq}
    2.45 +      in
    2.46 +        case mono_eq_prover ctxt (hd(prems_of rep_abs_thm)) of
    2.47 +          SOME mono_eq_thm =>
    2.48 +            let
    2.49 +              val rep_abs_eq = mono_eq_thm RS rep_abs_thm
    2.50 +              val rep = (cterm_of thy o quot_thm_rep) quot_thm
    2.51 +              val rep_refl = Thm.reflexive rep RS @{thm meta_eq_to_obj_eq}
    2.52 +              val repped_eq = [rep_refl, unabs_def RS @{thm meta_eq_to_obj_eq}] MRSL @{thm cong}
    2.53 +              val code_cert = [repped_eq, rep_abs_eq] MRSL trans
    2.54 +            in
    2.55 +              SOME (simplify_code_eq ctxt code_cert)
    2.56 +            end
    2.57 +          | NONE => NONE
    2.58 +      end
    2.59    end
    2.60  
    2.61 -fun generate_trivial_rep_eq ctxt def_thm =
    2.62 -  let
    2.63 -    val unfolded_def = Conv.fconv_rule (Conv.arg_conv unfold_fun_maps_beta) def_thm
    2.64 -    val code_eq = unabs_all_def ctxt unfolded_def
    2.65 -    val simp_code_eq = simplify_code_eq ctxt code_eq
    2.66 -  in
    2.67 -    simp_code_eq
    2.68 -  end
    2.69 -
    2.70 -fun generate_rep_eq ctxt def_thm rsp_thm (rty, qty) =
    2.71 -  if body_type rty = body_type qty then 
    2.72 -    SOME (generate_trivial_rep_eq ctxt def_thm)
    2.73 -  else 
    2.74 -    let
    2.75 -      val (rty_body, qty_body) = get_body_types (rty, qty)
    2.76 -      val quot_thm = Lifting_Term.prove_quot_thm ctxt (rty_body, qty_body)
    2.77 -    in
    2.78 -      if can_generate_code_cert quot_thm then
    2.79 -        SOME (generate_code_cert ctxt def_thm rsp_thm (rty, qty))
    2.80 -      else 
    2.81 -        NONE
    2.82 -    end
    2.83 -
    2.84  fun generate_abs_eq ctxt def_thm rsp_thm quot_thm =
    2.85    let
    2.86      val abs_eq_with_assms =