1.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Thu Jul 24 11:54:15 2014 +0200
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Thu Jul 24 13:01:49 2014 +0200
     1.3 @@ -39,6 +39,20 @@
     1.4        handle ERROR _ => NONE
     1.5    end
     1.6  
     1.7 +fun try_prove_refl_rel ctxt rel =
     1.8 +  let
     1.9 +    fun mk_ge_eq x =
    1.10 +      let
    1.11 +        val T = fastype_of x
    1.12 +      in
    1.13 +        Const (@{const_name "less_eq"}, T --> T --> HOLogic.boolT) $ 
    1.14 +          (Const (@{const_name HOL.eq}, T)) $ x
    1.15 +      end;
    1.16 +    val goal = HOLogic.mk_Trueprop (mk_ge_eq rel);
    1.17 +  in
    1.18 +     mono_eq_prover ctxt goal
    1.19 +  end;
    1.20 +
    1.21  fun try_prove_reflexivity ctxt prop =
    1.22    let
    1.23      val thy = Proof_Context.theory_of ctxt
    1.24 @@ -178,6 +192,9 @@
    1.25      get_body_type_by_rel S (U, V)
    1.26    | get_body_type_by_rel _ (U, V)  = (U, V)
    1.27  
    1.28 +fun get_binder_rels (Const (@{const_name "rel_fun"}, _) $ R $ S) = R :: get_binder_rels S
    1.29 +  | get_binder_rels _ = []
    1.30 +
    1.31  fun force_rty_type ctxt rty rhs = 
    1.32    let
    1.33      val thy = Proof_Context.theory_of ctxt
    1.34 @@ -319,11 +336,11 @@
    1.35          |> (fn x => x RS (@{thm Quotient_rel_abs2} OF [quot_ret_thm]))
    1.36        end
    1.37      
    1.38 -    val prems = prems_of abs_eq_with_assms
    1.39 -    val indexed_prems = map_index (apfst (fn x => x + 1)) prems
    1.40 -    val indexed_assms = map (apsnd (try_prove_reflexivity ctxt)) indexed_prems
    1.41 -    val proved_assms = map (apsnd the) (filter (is_some o snd) indexed_assms)
    1.42 -    val abs_eq = fold_rev (fn (i, assms) => fn thm => assms RSN (i, thm)) proved_assms abs_eq_with_assms
    1.43 +    val prem_rels = get_binder_rels (quot_thm_rel quot_thm);
    1.44 +    val proved_assms = prem_rels |> map (try_prove_refl_rel ctxt) 
    1.45 +      |> map_index (apfst (fn x => x + 1)) |> filter (is_some o snd) |> map (apsnd the) 
    1.46 +      |> map (apsnd (fn assm => assm RS @{thm ge_eq_refl}))
    1.47 +    val abs_eq = fold_rev (fn (i, assm) => fn thm => assm RSN (i, thm)) proved_assms abs_eq_with_assms
    1.48    in
    1.49      simplify_code_eq ctxt abs_eq
    1.50    end