# HG changeset patch # User kuncar # Date 1393336939 -3600 # Node ID 66df76dd26400348af6c0cb1472f2a5e8a49d4cb # Parent 97ff9276e12db43c26f8d58b77f70304e42cba52 rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user diff -r 97ff9276e12d -r 66df76dd2640 src/HOL/Lifting.thy --- a/src/HOL/Lifting.thy Mon Feb 24 23:17:55 2014 +0000 +++ b/src/HOL/Lifting.thy Tue Feb 25 15:02:19 2014 +0100 @@ -591,6 +591,21 @@ subsection {* Domains *} +lemma composed_equiv_rel_invariant: + assumes "left_unique R" + assumes "(R ===> op=) P P'" + assumes "Domainp R = P''" + shows "(R OO Lifting.invariant P' OO R\\) = Lifting.invariant (inf P'' P)" +using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def fun_rel_def invariant_def +fun_eq_iff by blast + +lemma composed_equiv_rel_eq_invariant: + assumes "left_unique R" + assumes "Domainp R = P" + shows "(R OO op= OO R\\) = Lifting.invariant P" +using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def invariant_def +fun_eq_iff is_equality_def by metis + lemma pcr_Domainp_par_left_total: assumes "Domainp B = P" assumes "left_total A" diff -r 97ff9276e12d -r 66df76dd2640 src/HOL/Tools/Lifting/lifting_def.ML --- a/src/HOL/Tools/Lifting/lifting_def.ML Mon Feb 24 23:17:55 2014 +0000 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Tue Feb 25 15:02:19 2014 +0100 @@ -443,10 +443,65 @@ |> register_code_eq abs_eq_thm opt_rep_eq_thm (rty_forced, qty) end +local + val invariant_assms_tac_fixed_rules = map (Transfer.prep_transfer_domain_thm @{context}) + [@{thm pcr_Domainp_total}, @{thm pcr_Domainp_par_left_total}, @{thm pcr_Domainp_par}, + @{thm pcr_Domainp}] +in fun mk_readable_rsp_thm_eq tm lthy = let val ctm = cterm_of (Proof_Context.theory_of lthy) tm + (* This is not very cheap way of getting the rules but we have only few active + liftings in the current setting *) + fun get_cr_pcr_eqs ctxt = + let + fun collect (data : Lifting_Info.quotient) l = + if is_some (#pcr_info data) + then ((Thm.symmetric o safe_mk_meta_eq o #pcr_cr_eq o the o #pcr_info) data :: l) + else l + val table = Lifting_Info.get_quotients ctxt + in + Symtab.fold (fn (_, data) => fn l => collect data l) table [] + end + + fun assms_rewr_conv tactic rule ct = + let + fun prove_extra_assms thm = + let + val assms = cprems_of thm + fun finish thm = if Thm.no_prems thm then SOME (Goal.conclude thm) else NONE + fun prove ctm = Option.mapPartial finish (SINGLE tactic (Goal.init ctm)) + in + map_interrupt prove assms + end + + fun cconl_of thm = Drule.strip_imp_concl (cprop_of thm) + fun lhs_of thm = fst (Thm.dest_equals (cconl_of thm)) + fun rhs_of thm = snd (Thm.dest_equals (cconl_of thm)) + val rule1 = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) rule; + val lhs = lhs_of rule1; + val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1; + val rule3 = + Thm.instantiate (Thm.match (lhs, ct)) rule2 + handle Pattern.MATCH => raise CTERM ("assms_rewr_conv", [lhs, ct]); + val proved_assms = prove_extra_assms rule3 + in + case proved_assms of + SOME proved_assms => + let + val rule3 = proved_assms MRSL rule3 + val rule4 = + if lhs_of rule3 aconvc ct then rule3 + else + let val ceq = Thm.dest_fun2 (Thm.cprop_of rule3) + in rule3 COMP Thm.trivial (Thm.mk_binop ceq ct (rhs_of rule3)) end + in Thm.transitive rule4 (Thm.beta_conversion true (rhs_of rule4)) end + | NONE => Conv.no_conv ct + end + + fun assms_rewrs_conv tactic rules = Conv.first_conv (map (assms_rewr_conv tactic) rules) + fun simp_arrows_conv ctm = let val unfold_conv = Conv.rewrs_conv @@ -455,8 +510,13 @@ @{thm fun_rel_eq_rel[THEN eq_reflection]}, @{thm fun_rel_def[THEN eq_reflection]}] fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2 + val invariant_assms_tac_rules = @{thm left_unique_composition} :: + invariant_assms_tac_fixed_rules @ (Transfer.get_transfer_raw lthy) + val invariant_assms_tac = (TRY o REPEAT_ALL_NEW (resolve_tac invariant_assms_tac_rules) + THEN_ALL_NEW (DETERM o Transfer.eq_tac lthy)) 1 val invariant_commute_conv = Conv.bottom_conv - (K (Conv.try_conv (Conv.rewrs_conv (Lifting_Info.get_invariant_commute_rules lthy)))) lthy + (K (Conv.try_conv (assms_rewrs_conv invariant_assms_tac + (Lifting_Info.get_invariant_commute_rules lthy)))) lthy val relator_eq_conv = Conv.bottom_conv (K (Conv.try_conv (Conv.rewrs_conv (Transfer.get_relator_eq lthy)))) lthy in @@ -467,8 +527,9 @@ end val unfold_ret_val_invs = Conv.bottom_conv - (K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy - val simp_conv = HOLogic.Trueprop_conv (Conv.fun2_conv simp_arrows_conv) + (K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy + val cr_to_pcr_conv = Raw_Simplifier.rewrite lthy false (get_cr_pcr_eqs lthy) + val simp_conv = HOLogic.Trueprop_conv (Conv.fun2_conv (cr_to_pcr_conv then_conv simp_arrows_conv)) val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]} val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy val beta_conv = Thm.beta_conversion true @@ -477,6 +538,7 @@ in Object_Logic.rulify lthy (eq_thm RS Drule.equal_elim_rule2) end +end fun rename_to_tnames ctxt term = let diff -r 97ff9276e12d -r 66df76dd2640 src/HOL/Tools/Lifting/lifting_info.ML --- a/src/HOL/Tools/Lifting/lifting_info.ML Mon Feb 24 23:17:55 2014 +0000 +++ b/src/HOL/Tools/Lifting/lifting_info.ML Tue Feb 25 15:02:19 2014 +0100 @@ -516,6 +516,11 @@ #> relfexivity_rule_setup #> relator_distr_attribute_setup +(* setup fixed invariant rules *) + +val _ = Context.>> (fold (Invariant_Commute.add_thm o Transfer.prep_transfer_domain_thm @{context}) + [@{thm composed_equiv_rel_invariant}, @{thm composed_equiv_rel_eq_invariant}]) + (* outer syntax commands *) val _ = diff -r 97ff9276e12d -r 66df76dd2640 src/HOL/Tools/Lifting/lifting_term.ML --- a/src/HOL/Tools/Lifting/lifting_term.ML Mon Feb 24 23:17:55 2014 +0000 +++ b/src/HOL/Tools/Lifting/lifting_term.ML Tue Feb 25 15:02:19 2014 +0100 @@ -447,16 +447,6 @@ end fun rewrs_imp rules = first_imp (map rewr_imp rules) - - fun map_interrupt f l = - let - fun map_interrupt' _ [] l = SOME (rev l) - | map_interrupt' f (x::xs) l = (case f x of - NONE => NONE - | SOME v => map_interrupt' f xs (v::l)) - in - map_interrupt' f l [] - end in (* diff -r 97ff9276e12d -r 66df76dd2640 src/HOL/Tools/Lifting/lifting_util.ML --- a/src/HOL/Tools/Lifting/lifting_util.ML Mon Feb 24 23:17:55 2014 +0000 +++ b/src/HOL/Tools/Lifting/lifting_util.ML Tue Feb 25 15:02:19 2014 +0100 @@ -31,6 +31,7 @@ val relation_types: typ -> typ * typ val mk_HOL_eq: thm -> thm val safe_HOL_meta_eq: thm -> thm + val map_interrupt: ('a -> 'b option) -> 'a list -> 'b list option end @@ -121,4 +122,14 @@ fun safe_HOL_meta_eq r = mk_HOL_eq r handle Thm.THM _ => r +fun map_interrupt f l = + let + fun map_interrupt' _ [] l = SOME (rev l) + | map_interrupt' f (x::xs) l = (case f x of + NONE => NONE + | SOME v => map_interrupt' f xs (v::l)) + in + map_interrupt' f l [] + end + end diff -r 97ff9276e12d -r 66df76dd2640 src/HOL/Tools/transfer.ML --- a/src/HOL/Tools/transfer.ML Mon Feb 24 23:17:55 2014 +0000 +++ b/src/HOL/Tools/transfer.ML Tue Feb 25 15:02:19 2014 +0100 @@ -25,10 +25,13 @@ val transfer_raw_del: thm -> Context.generic -> Context.generic val transferred_attribute: thm list -> attribute val untransferred_attribute: thm list -> attribute + val prep_transfer_domain_thm: Proof.context -> thm -> thm val transfer_domain_add: attribute val transfer_domain_del: attribute val transfer_rule_of_term: Proof.context -> bool -> term -> thm val transfer_rule_of_lhs: Proof.context -> term -> thm + val eq_tac: Proof.context -> int -> tactic + val transfer_step_tac: Proof.context -> int -> tactic val transfer_tac: bool -> Proof.context -> int -> tactic val transfer_prover_tac: Proof.context -> int -> tactic val gen_frees_tac: (string * typ) list -> Proof.context -> int -> tactic @@ -346,11 +349,14 @@ (** Adding transfer domain rules **) -fun add_transfer_domain_thm thm ctxt = - (add_transfer_thm o abstract_equalities_domain (Context.proof_of ctxt) o detect_transfer_rules) thm ctxt +fun prep_transfer_domain_thm ctxt thm = + (abstract_equalities_domain ctxt o detect_transfer_rules) thm -fun del_transfer_domain_thm thm ctxt = - (del_transfer_thm o abstract_equalities_domain (Context.proof_of ctxt) o detect_transfer_rules) thm ctxt +fun add_transfer_domain_thm thm ctxt = (add_transfer_thm o + prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt + +fun del_transfer_domain_thm thm ctxt = (del_transfer_thm o + prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt (** Transfer proof method **) @@ -571,7 +577,13 @@ |> Thm.instantiate (map tinst binsts, map inst binsts) end -fun eq_tac eq_rules = TRY o REPEAT_ALL_NEW (resolve_tac eq_rules) THEN_ALL_NEW rtac @{thm is_equality_eq} +fun eq_rules_tac eq_rules = TRY o REPEAT_ALL_NEW (resolve_tac eq_rules) + THEN_ALL_NEW rtac @{thm is_equality_eq} + +fun eq_tac ctxt = eq_rules_tac (get_relator_eq_raw ctxt) + +fun transfer_step_tac ctxt = (REPEAT_ALL_NEW (resolve_tac (get_transfer_raw ctxt)) + THEN_ALL_NEW (DETERM o eq_rules_tac (get_relator_eq_raw ctxt))) fun transfer_tac equiv ctxt i = let @@ -587,7 +599,7 @@ rtac start_rule i THEN (rtac (transfer_rule_of_term ctxt equiv (HOLogic.dest_Trueprop t)) THEN_ALL_NEW - (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_tac eq_rules)) + (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)) ORELSE' end_tac)) (i + 1) handle TERM (_, ts) => raise TERM (err_msg, ts) in @@ -612,7 +624,7 @@ rtac @{thm transfer_prover_start} i, ((rtac rule1 ORELSE' (CONVERSION expand_eq_in_rel THEN' rtac rule1)) THEN_ALL_NEW - (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_tac eq_rules))) (i+1), + (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules))) (i+1), rtac @{thm refl} i] end) @@ -640,7 +652,7 @@ (rtac rule THEN_ALL_NEW (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules) - THEN_ALL_NEW (DETERM o eq_tac eq_rules)))) 1 + THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)))) 1 handle TERM (_, ts) => raise TERM (err_msg, ts) val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac) val tnames = map (fst o dest_TFree o snd) instT @@ -676,7 +688,7 @@ (rtac rule THEN_ALL_NEW (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules) - THEN_ALL_NEW (DETERM o eq_tac eq_rules)))) 1 + THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)))) 1 handle TERM (_, ts) => raise TERM (err_msg, ts) val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac) val tnames = map (fst o dest_TFree o snd) instT