rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
authorkuncar
Tue Feb 25 15:02:19 2014 +0100 (2014-02-25)
changeset 5573166df76dd2640
parent 55730 97ff9276e12d
child 55732 07906fc6af7a
rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
src/HOL/Lifting.thy
src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/Lifting/lifting_info.ML
src/HOL/Tools/Lifting/lifting_term.ML
src/HOL/Tools/Lifting/lifting_util.ML
src/HOL/Tools/transfer.ML
     1.1 --- a/src/HOL/Lifting.thy	Mon Feb 24 23:17:55 2014 +0000
     1.2 +++ b/src/HOL/Lifting.thy	Tue Feb 25 15:02:19 2014 +0100
     1.3 @@ -591,6 +591,21 @@
     1.4  
     1.5  subsection {* Domains *}
     1.6  
     1.7 +lemma composed_equiv_rel_invariant:
     1.8 +  assumes "left_unique R"
     1.9 +  assumes "(R ===> op=) P P'"
    1.10 +  assumes "Domainp R = P''"
    1.11 +  shows "(R OO Lifting.invariant P' OO R\<inverse>\<inverse>) = Lifting.invariant (inf P'' P)"
    1.12 +using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def fun_rel_def invariant_def
    1.13 +fun_eq_iff by blast
    1.14 +
    1.15 +lemma composed_equiv_rel_eq_invariant:
    1.16 +  assumes "left_unique R"
    1.17 +  assumes "Domainp R = P"
    1.18 +  shows "(R OO op= OO R\<inverse>\<inverse>) = Lifting.invariant P"
    1.19 +using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def invariant_def
    1.20 +fun_eq_iff is_equality_def by metis
    1.21 +
    1.22  lemma pcr_Domainp_par_left_total:
    1.23    assumes "Domainp B = P"
    1.24    assumes "left_total A"
     2.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Mon Feb 24 23:17:55 2014 +0000
     2.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Tue Feb 25 15:02:19 2014 +0100
     2.3 @@ -443,10 +443,65 @@
     2.4        |> register_code_eq abs_eq_thm opt_rep_eq_thm (rty_forced, qty)
     2.5    end
     2.6  
     2.7 +local
     2.8 +  val invariant_assms_tac_fixed_rules = map (Transfer.prep_transfer_domain_thm @{context})
     2.9 +    [@{thm pcr_Domainp_total}, @{thm pcr_Domainp_par_left_total}, @{thm pcr_Domainp_par}, 
    2.10 +      @{thm pcr_Domainp}]
    2.11 +in
    2.12  fun mk_readable_rsp_thm_eq tm lthy =
    2.13    let
    2.14      val ctm = cterm_of (Proof_Context.theory_of lthy) tm
    2.15      
    2.16 +    (* This is not very cheap way of getting the rules but we have only few active
    2.17 +      liftings in the current setting *)
    2.18 +    fun get_cr_pcr_eqs ctxt =
    2.19 +      let
    2.20 +        fun collect (data : Lifting_Info.quotient) l =
    2.21 +          if is_some (#pcr_info data) 
    2.22 +          then ((Thm.symmetric o safe_mk_meta_eq o #pcr_cr_eq o the o #pcr_info) data :: l) 
    2.23 +          else l
    2.24 +        val table = Lifting_Info.get_quotients ctxt
    2.25 +      in
    2.26 +        Symtab.fold (fn (_, data) => fn l => collect data l) table []
    2.27 +      end
    2.28 +
    2.29 +    fun assms_rewr_conv tactic rule ct =
    2.30 +      let
    2.31 +        fun prove_extra_assms thm =
    2.32 +          let
    2.33 +            val assms = cprems_of thm
    2.34 +            fun finish thm = if Thm.no_prems thm then SOME (Goal.conclude thm) else NONE
    2.35 +            fun prove ctm = Option.mapPartial finish (SINGLE tactic (Goal.init ctm))
    2.36 +          in
    2.37 +            map_interrupt prove assms
    2.38 +          end
    2.39 +    
    2.40 +        fun cconl_of thm = Drule.strip_imp_concl (cprop_of thm)
    2.41 +        fun lhs_of thm = fst (Thm.dest_equals (cconl_of thm))
    2.42 +        fun rhs_of thm = snd (Thm.dest_equals (cconl_of thm))
    2.43 +        val rule1 = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) rule;
    2.44 +        val lhs = lhs_of rule1;
    2.45 +        val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1;
    2.46 +        val rule3 =
    2.47 +          Thm.instantiate (Thm.match (lhs, ct)) rule2
    2.48 +            handle Pattern.MATCH => raise CTERM ("assms_rewr_conv", [lhs, ct]);
    2.49 +        val proved_assms = prove_extra_assms rule3
    2.50 +      in
    2.51 +        case proved_assms of
    2.52 +          SOME proved_assms =>
    2.53 +            let
    2.54 +              val rule3 = proved_assms MRSL rule3
    2.55 +              val rule4 =
    2.56 +                if lhs_of rule3 aconvc ct then rule3
    2.57 +                else
    2.58 +                  let val ceq = Thm.dest_fun2 (Thm.cprop_of rule3)
    2.59 +                  in rule3 COMP Thm.trivial (Thm.mk_binop ceq ct (rhs_of rule3)) end
    2.60 +            in Thm.transitive rule4 (Thm.beta_conversion true (rhs_of rule4)) end
    2.61 +          | NONE => Conv.no_conv ct
    2.62 +      end
    2.63 +
    2.64 +    fun assms_rewrs_conv tactic rules = Conv.first_conv (map (assms_rewr_conv tactic) rules)
    2.65 +
    2.66      fun simp_arrows_conv ctm =
    2.67        let
    2.68          val unfold_conv = Conv.rewrs_conv 
    2.69 @@ -455,8 +510,13 @@
    2.70              @{thm fun_rel_eq_rel[THEN eq_reflection]}, 
    2.71              @{thm fun_rel_def[THEN eq_reflection]}]
    2.72          fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
    2.73 +        val invariant_assms_tac_rules = @{thm left_unique_composition} :: 
    2.74 +            invariant_assms_tac_fixed_rules @ (Transfer.get_transfer_raw lthy)
    2.75 +        val invariant_assms_tac = (TRY o REPEAT_ALL_NEW (resolve_tac invariant_assms_tac_rules) 
    2.76 +          THEN_ALL_NEW (DETERM o Transfer.eq_tac lthy)) 1
    2.77          val invariant_commute_conv = Conv.bottom_conv
    2.78 -          (K (Conv.try_conv (Conv.rewrs_conv (Lifting_Info.get_invariant_commute_rules lthy)))) lthy
    2.79 +          (K (Conv.try_conv (assms_rewrs_conv invariant_assms_tac
    2.80 +            (Lifting_Info.get_invariant_commute_rules lthy)))) lthy
    2.81          val relator_eq_conv = Conv.bottom_conv
    2.82            (K (Conv.try_conv (Conv.rewrs_conv (Transfer.get_relator_eq lthy)))) lthy
    2.83        in
    2.84 @@ -467,8 +527,9 @@
    2.85        end
    2.86      
    2.87      val unfold_ret_val_invs = Conv.bottom_conv 
    2.88 -      (K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy 
    2.89 -    val simp_conv = HOLogic.Trueprop_conv (Conv.fun2_conv simp_arrows_conv)
    2.90 +      (K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy
    2.91 +    val cr_to_pcr_conv = Raw_Simplifier.rewrite lthy false (get_cr_pcr_eqs lthy)
    2.92 +    val simp_conv = HOLogic.Trueprop_conv (Conv.fun2_conv (cr_to_pcr_conv then_conv simp_arrows_conv))
    2.93      val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]}
    2.94      val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy
    2.95      val beta_conv = Thm.beta_conversion true
    2.96 @@ -477,6 +538,7 @@
    2.97    in
    2.98      Object_Logic.rulify lthy (eq_thm RS Drule.equal_elim_rule2)
    2.99    end
   2.100 +end
   2.101  
   2.102  fun rename_to_tnames ctxt term =
   2.103    let
     3.1 --- a/src/HOL/Tools/Lifting/lifting_info.ML	Mon Feb 24 23:17:55 2014 +0000
     3.2 +++ b/src/HOL/Tools/Lifting/lifting_info.ML	Tue Feb 25 15:02:19 2014 +0100
     3.3 @@ -516,6 +516,11 @@
     3.4    #> relfexivity_rule_setup
     3.5    #> relator_distr_attribute_setup
     3.6  
     3.7 +(* setup fixed invariant rules *)
     3.8 +
     3.9 +val _ = Context.>> (fold (Invariant_Commute.add_thm o Transfer.prep_transfer_domain_thm @{context}) 
    3.10 +  [@{thm composed_equiv_rel_invariant}, @{thm composed_equiv_rel_eq_invariant}])
    3.11 +
    3.12  (* outer syntax commands *)
    3.13  
    3.14  val _ =
     4.1 --- a/src/HOL/Tools/Lifting/lifting_term.ML	Mon Feb 24 23:17:55 2014 +0000
     4.2 +++ b/src/HOL/Tools/Lifting/lifting_term.ML	Tue Feb 25 15:02:19 2014 +0100
     4.3 @@ -447,16 +447,6 @@
     4.4     end
     4.5    
     4.6    fun rewrs_imp rules = first_imp (map rewr_imp rules)
     4.7 -
     4.8 -  fun map_interrupt f l =
     4.9 -    let
    4.10 -      fun map_interrupt' _ [] l = SOME (rev l)
    4.11 -       | map_interrupt' f (x::xs) l = (case f x of
    4.12 -        NONE => NONE
    4.13 -        | SOME v => map_interrupt' f xs (v::l))
    4.14 -    in
    4.15 -      map_interrupt' f l []
    4.16 -    end
    4.17  in
    4.18  
    4.19    (*
     5.1 --- a/src/HOL/Tools/Lifting/lifting_util.ML	Mon Feb 24 23:17:55 2014 +0000
     5.2 +++ b/src/HOL/Tools/Lifting/lifting_util.ML	Tue Feb 25 15:02:19 2014 +0100
     5.3 @@ -31,6 +31,7 @@
     5.4    val relation_types: typ -> typ * typ
     5.5    val mk_HOL_eq: thm -> thm
     5.6    val safe_HOL_meta_eq: thm -> thm
     5.7 +  val map_interrupt: ('a -> 'b option) -> 'a list -> 'b list option
     5.8  end
     5.9  
    5.10  
    5.11 @@ -121,4 +122,14 @@
    5.12  
    5.13  fun safe_HOL_meta_eq r = mk_HOL_eq r handle Thm.THM _ => r
    5.14  
    5.15 +fun map_interrupt f l =
    5.16 +  let
    5.17 +    fun map_interrupt' _ [] l = SOME (rev l)
    5.18 +     | map_interrupt' f (x::xs) l = (case f x of
    5.19 +      NONE => NONE
    5.20 +      | SOME v => map_interrupt' f xs (v::l))
    5.21 +  in
    5.22 +    map_interrupt' f l []
    5.23 +  end
    5.24 +
    5.25  end
     6.1 --- a/src/HOL/Tools/transfer.ML	Mon Feb 24 23:17:55 2014 +0000
     6.2 +++ b/src/HOL/Tools/transfer.ML	Tue Feb 25 15:02:19 2014 +0100
     6.3 @@ -25,10 +25,13 @@
     6.4    val transfer_raw_del: thm -> Context.generic -> Context.generic
     6.5    val transferred_attribute: thm list -> attribute
     6.6    val untransferred_attribute: thm list -> attribute
     6.7 +  val prep_transfer_domain_thm: Proof.context -> thm -> thm
     6.8    val transfer_domain_add: attribute
     6.9    val transfer_domain_del: attribute
    6.10    val transfer_rule_of_term: Proof.context -> bool -> term -> thm
    6.11    val transfer_rule_of_lhs: Proof.context -> term -> thm
    6.12 +  val eq_tac: Proof.context -> int -> tactic
    6.13 +  val transfer_step_tac: Proof.context -> int -> tactic
    6.14    val transfer_tac: bool -> Proof.context -> int -> tactic
    6.15    val transfer_prover_tac: Proof.context -> int -> tactic
    6.16    val gen_frees_tac: (string * typ) list -> Proof.context -> int -> tactic
    6.17 @@ -346,11 +349,14 @@
    6.18  
    6.19  (** Adding transfer domain rules **)
    6.20  
    6.21 -fun add_transfer_domain_thm thm ctxt = 
    6.22 -  (add_transfer_thm o abstract_equalities_domain (Context.proof_of ctxt) o detect_transfer_rules) thm ctxt
    6.23 +fun prep_transfer_domain_thm ctxt thm = 
    6.24 +  (abstract_equalities_domain ctxt o detect_transfer_rules) thm 
    6.25  
    6.26 -fun del_transfer_domain_thm thm ctxt = 
    6.27 -  (del_transfer_thm o abstract_equalities_domain (Context.proof_of ctxt) o detect_transfer_rules) thm ctxt
    6.28 +fun add_transfer_domain_thm thm ctxt = (add_transfer_thm o 
    6.29 +  prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt
    6.30 +
    6.31 +fun del_transfer_domain_thm thm ctxt = (del_transfer_thm o 
    6.32 +  prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt
    6.33  
    6.34  (** Transfer proof method **)
    6.35  
    6.36 @@ -571,7 +577,13 @@
    6.37        |> Thm.instantiate (map tinst binsts, map inst binsts)
    6.38    end
    6.39  
    6.40 -fun eq_tac eq_rules = TRY o REPEAT_ALL_NEW (resolve_tac eq_rules) THEN_ALL_NEW rtac @{thm is_equality_eq}
    6.41 +fun eq_rules_tac eq_rules = TRY o REPEAT_ALL_NEW (resolve_tac eq_rules) 
    6.42 +  THEN_ALL_NEW rtac @{thm is_equality_eq}
    6.43 +
    6.44 +fun eq_tac ctxt = eq_rules_tac (get_relator_eq_raw ctxt)
    6.45 +
    6.46 +fun transfer_step_tac ctxt = (REPEAT_ALL_NEW (resolve_tac (get_transfer_raw ctxt)) 
    6.47 +  THEN_ALL_NEW (DETERM o eq_rules_tac (get_relator_eq_raw ctxt)))
    6.48  
    6.49  fun transfer_tac equiv ctxt i =
    6.50    let
    6.51 @@ -587,7 +599,7 @@
    6.52        rtac start_rule i THEN
    6.53        (rtac (transfer_rule_of_term ctxt equiv (HOLogic.dest_Trueprop t))
    6.54          THEN_ALL_NEW
    6.55 -          (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_tac eq_rules))
    6.56 +          (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules))
    6.57              ORELSE' end_tac)) (i + 1)
    6.58          handle TERM (_, ts) => raise TERM (err_msg, ts)
    6.59    in
    6.60 @@ -612,7 +624,7 @@
    6.61         rtac @{thm transfer_prover_start} i,
    6.62         ((rtac rule1 ORELSE' (CONVERSION expand_eq_in_rel THEN' rtac rule1))
    6.63          THEN_ALL_NEW
    6.64 -         (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_tac eq_rules))) (i+1),
    6.65 +         (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules))) (i+1),
    6.66         rtac @{thm refl} i]
    6.67    end)
    6.68  
    6.69 @@ -640,7 +652,7 @@
    6.70        (rtac rule
    6.71          THEN_ALL_NEW
    6.72            (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)
    6.73 -            THEN_ALL_NEW (DETERM o eq_tac eq_rules)))) 1
    6.74 +            THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)))) 1
    6.75          handle TERM (_, ts) => raise TERM (err_msg, ts)
    6.76      val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
    6.77      val tnames = map (fst o dest_TFree o snd) instT
    6.78 @@ -676,7 +688,7 @@
    6.79        (rtac rule
    6.80          THEN_ALL_NEW
    6.81            (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)
    6.82 -            THEN_ALL_NEW (DETERM o eq_tac eq_rules)))) 1
    6.83 +            THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)))) 1
    6.84          handle TERM (_, ts) => raise TERM (err_msg, ts)
    6.85      val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
    6.86      val tnames = map (fst o dest_TFree o snd) instT