src/HOL/Tools/Lifting/lifting_def.ML
changeset 56518 beb3b6851665
parent 56245 84fc7dfa3cd4
child 56519 c1048f5bbb45
     1.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Thu Apr 10 17:48:13 2014 +0200
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Thu Apr 10 17:48:14 2014 +0200
     1.3 @@ -29,12 +29,18 @@
     1.4  
     1.5  fun mono_eq_prover ctxt prop =
     1.6    let
     1.7 -    val rules = Lifting_Info.get_reflexivity_rules ctxt
     1.8 +    val refl_rules = Lifting_Info.get_reflexivity_rules ctxt
     1.9 +    val transfer_rules = Transfer.get_transfer_raw ctxt
    1.10 +    
    1.11 +    fun main_tac (t, i) =
    1.12 +      case HOLogic.dest_Trueprop t of 
    1.13 +        Const (@{const_name "less_eq"}, _) $ _ $ _ => REPEAT_ALL_NEW (resolve_tac refl_rules) i
    1.14 +        |  _ => REPEAT_ALL_NEW (resolve_tac transfer_rules) i
    1.15    in
    1.16 -    SOME (Goal.prove ctxt [] [] prop (K (REPEAT_ALL_NEW (resolve_tac rules) 1)))
    1.17 +    SOME (Goal.prove ctxt [] [] prop (K (SUBGOAL main_tac 1)))
    1.18        handle ERROR _ => NONE
    1.19    end
    1.20 -   
    1.21 +
    1.22  fun try_prove_reflexivity ctxt prop =
    1.23    let
    1.24      val thy = Proof_Context.theory_of ctxt
    1.25 @@ -511,7 +517,7 @@
    1.26              @{thm rel_fun_eq_rel[THEN eq_reflection]}, 
    1.27              @{thm rel_fun_def[THEN eq_reflection]}]
    1.28          fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
    1.29 -        val invariant_assms_tac_rules = @{thm left_unique_composition} :: 
    1.30 +        val invariant_assms_tac_rules = @{thm left_unique_OO} :: 
    1.31              invariant_assms_tac_fixed_rules @ (Transfer.get_transfer_raw lthy)
    1.32          val invariant_assms_tac = (TRY o REPEAT_ALL_NEW (resolve_tac invariant_assms_tac_rules) 
    1.33            THEN_ALL_NEW (DETERM o Transfer.eq_tac lthy)) 1