# HG changeset patch # User huffman # Date 1351097005 -7200 # Node ID faf4afed009fd1b4b67d7ec098579f5838425762 # Parent 791157a4179a3fbe2aea812c6645affe8414b799 transfer package: more flexible handling of equality relations using is_equality predicate diff -r 791157a4179a -r faf4afed009f src/HOL/Library/Mapping.thy --- a/src/HOL/Library/Mapping.thy Wed Oct 24 17:40:56 2012 +0200 +++ b/src/HOL/Library/Mapping.thy Wed Oct 24 18:43:25 2012 +0200 @@ -5,7 +5,7 @@ header {* An abstract view on maps for code generation. *} theory Mapping -imports Main +imports Main Quotient_Option begin subsection {* Type definition and primitive operations *} @@ -61,10 +61,8 @@ | Some v \ m (k \ (f v)))" . lemma map_entry_code [code]: "map_entry k f m = (case lookup m k of None \ m - | Some v \ update k (f v) m)" - apply (cases "lookup m k") - apply simp_all - by (transfer, simp)+ + | Some v \ update k (f v) m)" + by transfer rule definition map_default :: "'a \ 'b \ ('b \ 'b) \ ('a, 'b) mapping \ ('a, 'b) mapping" where "map_default k v f m = map_entry k f (default k v m)" @@ -274,4 +272,4 @@ hide_const (open) empty is_empty rep lookup update delete ordered_keys keys size replace default map_entry map_default tabulate bulkload map -end \ No newline at end of file +end diff -r 791157a4179a -r faf4afed009f src/HOL/Tools/Lifting/lifting_def.ML --- a/src/HOL/Tools/Lifting/lifting_def.ML Wed Oct 24 17:40:56 2012 +0200 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Wed Oct 24 18:43:25 2012 +0200 @@ -316,10 +316,8 @@ Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy fun top_rewr_conv rewrs = Conv.top_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) lthy' - val expand_rel_conv = Trueprop_conv (Conv.fun2_conv(top_rewr_conv (Transfer.get_sym_relator_eq lthy'))) val transfer_thm = ([quot_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer}) - |> Conv.fconv_rule expand_rel_conv - + val abs_eq_thm = generate_abs_eq lthy' def_thm rsp_thm quot_thm val maybe_rep_eq_thm = generate_rep_eq lthy' def_thm rsp_thm (rty_forced, qty) diff -r 791157a4179a -r faf4afed009f src/HOL/Tools/transfer.ML --- a/src/HOL/Tools/transfer.ML Wed Oct 24 17:40:56 2012 +0200 +++ b/src/HOL/Tools/transfer.ML Wed Oct 24 18:43:25 2012 +0200 @@ -85,20 +85,6 @@ fun del_transfer_thm thm = Data.map (map_transfer_raw (Item_Net.remove thm)) -val relator_eq_setup = - let - val name = @{binding relator_eq} - fun add_thm thm = Data.map (map_relator_eq (Item_Net.update thm)) - fun del_thm thm = Data.map (map_relator_eq (Item_Net.remove thm)) - val add = Thm.declaration_attribute add_thm - val del = Thm.declaration_attribute del_thm - val text = "declaration of relator equality rule (used by transfer method)" - val content = Item_Net.content o #relator_eq o Data.get - in - Attrib.setup name (Attrib.add_del add del) text - #> Global_Theory.add_thms_dynamic (name, content) - end - (** Conversions **) val Rel_rule = Thm.symmetric @{thm Rel_def} @@ -125,22 +111,60 @@ else_conv Conv.all_conv) ct -(** Transfer proof method **) +(** Replacing explicit equalities with is_equality premises **) + +fun mk_is_equality t = + Const (@{const_name is_equality}, Term.fastype_of t --> HOLogic.boolT) $ t -fun RelT (Const (@{const_name Rel}, _) $ _ $ _ $ y) = fastype_of y - | RelT t = raise TERM ("RelT", [t]) +val is_equality_lemma = + @{lemma "(!!R. is_equality R ==> PROP (P R)) == PROP (P (op =))" + by (unfold is_equality_def, rule, drule meta_spec, + erule meta_mp, rule refl, simp)} -(* Tactic to correspond a value to itself *) -fun eq_tac ctxt = SUBGOAL (fn (t, i) => +fun gen_abstract_equalities (dest : term -> term * (term -> term)) thm = let - val T = RelT (HOLogic.dest_Trueprop (Logic.strip_assums_concl t)) - val cT = ctyp_of (Proof_Context.theory_of ctxt) T - val rews = get_sym_relator_eq ctxt - val thm1 = Drule.instantiate' [SOME cT] [] @{thm Rel_eq_refl} - val thm2 = Raw_Simplifier.rewrite_rule rews thm1 + val thy = Thm.theory_of_thm thm + val prop = Thm.prop_of thm + val (t, mk_prop') = dest prop + val add_eqs = Term.fold_aterms + (fn t as Const (@{const_name HOL.eq}, _) => insert (op =) t | _ => I) + val eq_consts = rev (add_eqs t []) + val eqTs = map (snd o dest_Const) eq_consts + val used = Term.add_free_names prop [] + val names = map (K "") eqTs |> Name.variant_list used + val frees = map Free (names ~~ eqTs) + val prems = map (HOLogic.mk_Trueprop o mk_is_equality) frees + val prop1 = mk_prop' (Term.subst_atomic (eq_consts ~~ frees) t) + val prop2 = fold Logic.all frees (Logic.list_implies (prems, prop1)) + val cprop = Thm.cterm_of thy prop2 + val equal_thm = Raw_Simplifier.rewrite false [is_equality_lemma] cprop + fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm in - rtac thm2 i - end handle Match => no_tac | TERM _ => no_tac) + forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2})) + end + handle TERM _ => thm + +fun abstract_equalities_transfer thm = + let + fun dest prop = + let + val prems = Logic.strip_imp_prems prop + val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop) + val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl) + in + (rel, fn rel' => + Logic.list_implies (prems, HOLogic.mk_Trueprop (rel' $ x $ y))) + end + in + gen_abstract_equalities dest thm + end + +fun abstract_equalities_relator_eq rel_eq_thm = + gen_abstract_equalities (fn x => (x, I)) + (rel_eq_thm RS @{thm is_equality_def [THEN iffD2]}) + + +(** Transfer proof method **) val post_simps = @{thms transfer_forall_eq [symmetric] @@ -273,7 +297,7 @@ (rtac (transfer_rule_of_term ctxt (HOLogic.dest_Trueprop t)) THEN_ALL_NEW (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)) - ORELSE' eq_tac ctxt ORELSE' end_tac)) (i + 1)) i, + ORELSE' end_tac)) (i + 1)) i, (* FIXME: rewrite_goal_tac does unwanted eta-contraction *) rewrite_goal_tac post_simps i, rtac @{thm _} i] @@ -289,8 +313,7 @@ [CONVERSION prep_conv i, rtac @{thm transfer_prover_start} i, (rtac rule1 THEN_ALL_NEW - REPEAT_ALL_NEW - (resolve_tac rules ORELSE' eq_tac ctxt)) (i+1), + REPEAT_ALL_NEW (resolve_tac rules)) (i+1), rtac @{thm refl} i] end) @@ -311,7 +334,7 @@ (* Attribute for transfer rules *) -val prep_rule = Conv.fconv_rule prep_conv +val prep_rule = abstract_equalities_transfer o Conv.fconv_rule prep_conv val transfer_add = Thm.declaration_attribute (add_transfer_thm o prep_rule) @@ -324,6 +347,22 @@ (* Theory setup *) +val relator_eq_setup = + let + val name = @{binding relator_eq} + fun add_thm thm = Data.map (map_relator_eq (Item_Net.update thm)) + #> add_transfer_thm (abstract_equalities_relator_eq thm) + fun del_thm thm = Data.map (map_relator_eq (Item_Net.remove thm)) + #> del_transfer_thm (abstract_equalities_relator_eq thm) + val add = Thm.declaration_attribute add_thm + val del = Thm.declaration_attribute del_thm + val text = "declaration of relator equality rule (used by transfer method)" + val content = Item_Net.content o #relator_eq o Data.get + in + Attrib.setup name (Attrib.add_del add del) text + #> Global_Theory.add_thms_dynamic (name, content) + end + val setup = relator_eq_setup #> Attrib.setup @{binding transfer_rule} transfer_attribute diff -r 791157a4179a -r faf4afed009f src/HOL/Transfer.thy --- a/src/HOL/Transfer.thy Wed Oct 24 17:40:56 2012 +0200 +++ b/src/HOL/Transfer.thy Wed Oct 24 18:43:25 2012 +0200 @@ -52,6 +52,11 @@ definition Rel :: "('a \ 'b \ bool) \ 'a \ 'b \ bool" where "Rel r \ r" +text {* Handling of equality relations *} + +definition is_equality :: "('a \ 'a \ bool) \ bool" + where "is_equality R \ R = (op =)" + text {* Handling of meta-logic connectives *} definition transfer_forall where @@ -98,6 +103,8 @@ ML_file "Tools/transfer.ML" setup Transfer.setup +declare refl [transfer_rule] + declare fun_rel_eq [relator_eq] hide_const (open) Rel @@ -172,6 +179,9 @@ subsection {* Properties of relators *} +lemma is_equality_eq [transfer_rule]: "is_equality (op =)" + unfolding is_equality_def by simp + lemma right_total_eq [transfer_rule]: "right_total (op =)" unfolding right_total_def by simp