src/HOL/Tools/Lifting/lifting_def.ML
changeset 60231 0daab758e087
parent 60230 4857d553c52c
child 60239 755e11e2e15d
     1.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Mon Apr 13 15:27:34 2015 +0200
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Sat May 02 13:58:06 2015 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4      (binding * mixfix -> typ -> term -> thm -> thm list -> Proof.context -> 
     1.5        lift_def * local_theory) -> 
     1.6      binding * mixfix -> typ -> term -> thm list -> local_theory -> 
     1.7 -    term option * (thm list list -> Proof.context -> lift_def * local_theory)
     1.8 +    term option * (thm -> Proof.context -> lift_def * local_theory)
     1.9  
    1.10    val gen_lift_def:
    1.11      (binding * mixfix -> typ -> term -> thm -> thm list -> local_theory -> 
    1.12 @@ -616,112 +616,6 @@
    1.13        ||> Local_Theory.restore
    1.14    end
    1.15  
    1.16 -local
    1.17 -  val eq_onp_assms_tac_fixed_rules = map (Transfer.prep_transfer_domain_thm @{context})
    1.18 -    [@{thm pcr_Domainp_total}, @{thm pcr_Domainp_par_left_total}, @{thm pcr_Domainp_par}, 
    1.19 -      @{thm pcr_Domainp}]
    1.20 -in
    1.21 -fun mk_readable_rsp_thm_eq tm lthy =
    1.22 -  let
    1.23 -    val ctm = Thm.cterm_of lthy tm
    1.24 -    
    1.25 -    fun assms_rewr_conv tactic rule ct =
    1.26 -      let
    1.27 -        fun prove_extra_assms thm =
    1.28 -          let
    1.29 -            val assms = cprems_of thm
    1.30 -            fun finish thm = if Thm.no_prems thm then SOME (Goal.conclude thm) else NONE
    1.31 -            fun prove ctm = Option.mapPartial finish (SINGLE tactic (Goal.init ctm))
    1.32 -          in
    1.33 -            map_interrupt prove assms
    1.34 -          end
    1.35 -    
    1.36 -        fun cconl_of thm = Drule.strip_imp_concl (Thm.cprop_of thm)
    1.37 -        fun lhs_of thm = fst (Thm.dest_equals (cconl_of thm))
    1.38 -        fun rhs_of thm = snd (Thm.dest_equals (cconl_of thm))
    1.39 -        val rule1 = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) rule;
    1.40 -        val lhs = lhs_of rule1;
    1.41 -        val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1;
    1.42 -        val rule3 =
    1.43 -          Thm.instantiate (Thm.match (lhs, ct)) rule2
    1.44 -            handle Pattern.MATCH => raise CTERM ("assms_rewr_conv", [lhs, ct]);
    1.45 -        val proved_assms = prove_extra_assms rule3
    1.46 -      in
    1.47 -        case proved_assms of
    1.48 -          SOME proved_assms =>
    1.49 -            let
    1.50 -              val rule3 = proved_assms MRSL rule3
    1.51 -              val rule4 =
    1.52 -                if lhs_of rule3 aconvc ct then rule3
    1.53 -                else
    1.54 -                  let val ceq = Thm.dest_fun2 (Thm.cprop_of rule3)
    1.55 -                  in rule3 COMP Thm.trivial (Thm.mk_binop ceq ct (rhs_of rule3)) end
    1.56 -            in Thm.transitive rule4 (Thm.beta_conversion true (rhs_of rule4)) end
    1.57 -          | NONE => Conv.no_conv ct
    1.58 -      end
    1.59 -
    1.60 -    fun assms_rewrs_conv tactic rules = Conv.first_conv (map (assms_rewr_conv tactic) rules)
    1.61 -
    1.62 -    fun simp_arrows_conv ctm =
    1.63 -      let
    1.64 -        val unfold_conv = Conv.rewrs_conv 
    1.65 -          [@{thm rel_fun_eq_eq_onp[THEN eq_reflection]}, 
    1.66 -            @{thm rel_fun_eq_onp_rel[THEN eq_reflection]},
    1.67 -            @{thm rel_fun_eq[THEN eq_reflection]},
    1.68 -            @{thm rel_fun_eq_rel[THEN eq_reflection]}, 
    1.69 -            @{thm rel_fun_def[THEN eq_reflection]}]
    1.70 -        fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
    1.71 -        val eq_onp_assms_tac_rules = @{thm left_unique_OO} :: 
    1.72 -            eq_onp_assms_tac_fixed_rules @ (Transfer.get_transfer_raw lthy)
    1.73 -        val intro_top_rule = @{thm eq_onp_top_eq_eq[symmetric, THEN eq_reflection]}
    1.74 -        val kill_tops = Transfer.top_sweep_rewr_conv [@{thm eq_onp_top_eq_eq[THEN eq_reflection]}]
    1.75 -        val eq_onp_assms_tac = (CONVERSION kill_tops THEN' 
    1.76 -          TRY o REPEAT_ALL_NEW (resolve_tac lthy eq_onp_assms_tac_rules) 
    1.77 -          THEN_ALL_NEW (DETERM o Transfer.eq_tac lthy)) 1
    1.78 -        val relator_eq_onp_conv = Conv.bottom_conv
    1.79 -          (K (Conv.try_conv (assms_rewrs_conv eq_onp_assms_tac
    1.80 -            (intro_top_rule :: Lifting_Info.get_relator_eq_onp_rules lthy)))) lthy
    1.81 -          then_conv kill_tops
    1.82 -        val relator_eq_conv = Conv.bottom_conv
    1.83 -          (K (Conv.try_conv (Conv.rewrs_conv (Transfer.get_relator_eq lthy)))) lthy
    1.84 -      in
    1.85 -        case (Thm.term_of ctm) of
    1.86 -          Const (@{const_name "rel_fun"}, _) $ _ $ _ => 
    1.87 -            (binop_conv2 simp_arrows_conv simp_arrows_conv then_conv unfold_conv) ctm
    1.88 -          | _ => (relator_eq_onp_conv then_conv relator_eq_conv) ctm
    1.89 -      end
    1.90 -    
    1.91 -    val unfold_ret_val_invs = Conv.bottom_conv 
    1.92 -      (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args[THEN eq_reflection]}))) lthy
    1.93 -    val unfold_inv_conv = 
    1.94 -      Conv.top_sweep_conv (K (Conv.rewr_conv @{thm eq_onp_def[THEN eq_reflection]})) lthy
    1.95 -    val simp_conv = HOLogic.Trueprop_conv (Conv.fun2_conv simp_arrows_conv)
    1.96 -    val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]}
    1.97 -    val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy
    1.98 -    val beta_conv = Thm.beta_conversion true
    1.99 -    val eq_thm = 
   1.100 -      (simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs
   1.101 -         then_conv unfold_inv_conv) ctm
   1.102 -  in
   1.103 -    Object_Logic.rulify lthy (eq_thm RS Drule.equal_elim_rule2)
   1.104 -  end
   1.105 -end
   1.106 -
   1.107 -fun rename_to_tnames ctxt term =
   1.108 -  let
   1.109 -    fun all_typs (Const (@{const_name Pure.all}, _) $ Abs (_, T, t)) = T :: all_typs t
   1.110 -      | all_typs _ = []
   1.111 -
   1.112 -    fun rename (Const (@{const_name Pure.all}, T1) $ Abs (_, T2, t)) (new_name :: names) = 
   1.113 -        (Const (@{const_name Pure.all}, T1) $ Abs (new_name, T2, rename t names)) 
   1.114 -      | rename t _ = t
   1.115 -
   1.116 -    val (fixed_def_t, _) = yield_singleton (Variable.importT_terms) term ctxt
   1.117 -    val new_names = Old_Datatype_Prop.make_tnames (all_typs fixed_def_t)
   1.118 -  in
   1.119 -    rename term new_names
   1.120 -  end
   1.121 -
   1.122  (* This is not very cheap way of getting the rules but we have only few active
   1.123    liftings in the current setting *)
   1.124  fun get_cr_pcr_eqs ctxt =
   1.125 @@ -756,23 +650,7 @@
   1.126    in
   1.127      case opt_proven_rsp_thm of
   1.128        SOME thm => (NONE, K (after_qed thm))
   1.129 -      | NONE =>  
   1.130 -        let
   1.131 -          val readable_rsp_thm_eq = mk_readable_rsp_thm_eq prsp_tm lthy
   1.132 -          val (readable_rsp_tm, _) = Logic.dest_implies (Thm.prop_of readable_rsp_thm_eq)
   1.133 -          val readable_rsp_tm_tnames = rename_to_tnames lthy readable_rsp_tm
   1.134 -      
   1.135 -          fun after_qed' thm_list lthy = 
   1.136 -            let
   1.137 -              val internal_rsp_thm = Goal.prove lthy [] [] prsp_tm 
   1.138 -                  (fn {context = ctxt, ...} =>
   1.139 -                    rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac ctxt (hd thm_list) 1)
   1.140 -            in
   1.141 -              after_qed internal_rsp_thm lthy
   1.142 -            end
   1.143 -        in
   1.144 -          (SOME readable_rsp_tm_tnames, after_qed')
   1.145 -        end 
   1.146 +      | NONE => (SOME prsp_tm, after_qed) 
   1.147    end
   1.148  
   1.149  fun gen_lift_def add_lift_def var qty rhs tac par_thms lthy =
   1.150 @@ -785,9 +663,9 @@
   1.151            val rsp_thm = Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => tac ctxt)
   1.152              |> Thm.close_derivation
   1.153          in
   1.154 -          after_qed [[rsp_thm]] lthy
   1.155 +          after_qed rsp_thm lthy
   1.156          end
   1.157 -      | NONE => after_qed [[Drule.dummy_thm]] lthy
   1.158 +      | NONE => after_qed Drule.dummy_thm lthy
   1.159    end
   1.160  
   1.161  fun lift_def config var qty rhs tac par_thms lthy = gen_lift_def (add_lift_def config)