# HG changeset patch # User kuncar # Date 1334682973 -7200 # Node ID 69f95ac85c3df14bd7c82325f96d23b232672826 # Parent ef2d045203373631c2863649a493816ff0b4eebc tuned the setup of lifting; generate transfer rules for typedef and Quotient thms diff -r ef2d04520337 -r 69f95ac85c3d src/HOL/Lifting.thy --- a/src/HOL/Lifting.thy Tue Apr 17 16:14:07 2012 +0100 +++ b/src/HOL/Lifting.thy Tue Apr 17 19:16:13 2012 +0200 @@ -218,6 +218,10 @@ done qed +lemma equivp_reflp2: + "equivp R \ reflp R" + by (erule equivpE) + subsection {* Invariant *} definition invariant :: "('a \ bool) \ 'a \ 'a \ bool" diff -r ef2d04520337 -r 69f95ac85c3d src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Tue Apr 17 16:14:07 2012 +0100 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Tue Apr 17 19:16:13 2012 +0200 @@ -8,7 +8,9 @@ sig exception SETUP_LIFTING_INFR of string - val setup_lifting_infr: thm -> thm -> local_theory -> local_theory + val setup_lifting_infr: thm -> local_theory -> local_theory + + val setup_by_quotient: thm -> thm option -> local_theory -> local_theory val setup_by_typedef_thm: thm -> local_theory -> local_theory end; @@ -76,7 +78,7 @@ @ (map Pretty.string_of errs))) end -fun setup_lifting_infr quot_thm equiv_thm lthy = +fun setup_lifting_infr quot_thm lthy = let val _ = quot_thm_sanity_check lthy quot_thm val (_, qtyp) = Lifting_Term.quot_thm_rty_qty quot_thm @@ -90,36 +92,73 @@ |> define_abs_type quot_thm end +fun setup_by_quotient quot_thm maybe_reflp_thm lthy = + let + val transfer_attr = Attrib.internal (K Transfer.transfer_add) + val lthy' = case maybe_reflp_thm of + SOME reflp_thm => lthy + |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), + [[quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}]) + |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), + [[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}]) + | NONE => lthy + in + lthy' + |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), + [quot_thm RS @{thm Quotient_right_unique}]) + |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), + [quot_thm RS @{thm Quotient_right_total}]) + |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), + [quot_thm RS @{thm Quotient_rel_eq_transfer}]) + |> setup_lifting_infr quot_thm + end + fun setup_by_typedef_thm typedef_thm lthy = let - fun derive_quot_and_equiv_thm to_quot_thm to_equiv_thm typedef_thm lthy = - let - val (_ $ rep_fun $ _ $ _) = (HOLogic.dest_Trueprop o prop_of) typedef_thm - val equiv_thm = typedef_thm RS to_equiv_thm - val (T_def, lthy') = define_cr_rel rep_fun lthy - val quot_thm = [typedef_thm, T_def] MRSL to_quot_thm - in - (quot_thm, equiv_thm, lthy') - end + val transfer_attr = Attrib.internal (K Transfer.transfer_add) + val (_ $ rep_fun $ _ $ typedef_set) = (HOLogic.dest_Trueprop o prop_of) typedef_thm + val (T_def, lthy') = define_cr_rel rep_fun lthy + + val quot_thm = (case typedef_set of + Const ("Orderings.top_class.top", _) => + [typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient} + | Const (@{const_name "Collect"}, _) $ Abs (_, _, _) => + [typedef_thm, T_def] MRSL @{thm open_typedef_to_Quotient} + | _ => + [typedef_thm, T_def] MRSL @{thm typedef_to_Quotient}) - val typedef_set = (snd o dest_comb o HOLogic.dest_Trueprop o prop_of) typedef_thm - val (quot_thm, equiv_thm, lthy') = (case typedef_set of - Const ("Orderings.top_class.top", _) => - derive_quot_and_equiv_thm @{thm UNIV_typedef_to_Quotient} @{thm UNIV_typedef_to_equivp} - typedef_thm lthy - | Const (@{const_name "Collect"}, _) $ Abs (_, _, _) => - derive_quot_and_equiv_thm @{thm open_typedef_to_Quotient} @{thm open_typedef_to_part_equivp} - typedef_thm lthy - | _ => derive_quot_and_equiv_thm @{thm typedef_to_Quotient} @{thm typedef_to_part_equivp} - typedef_thm lthy) + val lthy'' = (case typedef_set of + Const ("Orderings.top_class.top", _) => (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), + [[typedef_thm,T_def] MRSL @{thm copy_type_bi_total}]) lthy' + | _ => lthy') in - setup_lifting_infr quot_thm equiv_thm lthy' + lthy'' + |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), + [[typedef_thm, T_def] MRSL @{thm typedef_bi_unique}]) + |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), + [T_def RS @{thm typedef_right_total}]) + |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), + [[typedef_thm, T_def] MRSL @{thm typedef_transfer_All}]) + |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), + [[typedef_thm, T_def] MRSL @{thm typedef_transfer_Ex}]) + |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), + [[typedef_thm, T_def] MRSL @{thm typedef_transfer_bforall}]) + |> setup_lifting_infr quot_thm end -fun setup_by_typedef_thm_aux xthm lthy = setup_by_typedef_thm (singleton (Attrib.eval_thms lthy) xthm) lthy +fun setup_lifting_cmd xthm lthy = + let + val input_thm = singleton (Attrib.eval_thms lthy) xthm + val input_term = (HOLogic.dest_Trueprop o prop_of) input_thm + in + case input_term of + (Const (@{const_name Quotient}, _) $ _ $ _ $ _ $ _) => setup_lifting_infr input_thm lthy + | (Const (@{const_name type_definition}, _) $ _ $ _ $ _) => setup_by_typedef_thm input_thm lthy + | _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported." + end val _ = Outer_Syntax.local_theory @{command_spec "setup_lifting"} "Setup lifting infrastructure" - (Parse_Spec.xthm >> (fn xthm => setup_by_typedef_thm_aux xthm)) + (Parse_Spec.xthm >> (fn xthm => setup_lifting_cmd xthm)) end; diff -r ef2d04520337 -r 69f95ac85c3d src/HOL/Tools/Quotient/quotient_type.ML --- a/src/HOL/Tools/Quotient/quotient_type.ML Tue Apr 17 16:14:07 2012 +0100 +++ b/src/HOL/Tools/Quotient/quotient_type.ML Tue Apr 17 19:16:13 2012 +0200 @@ -139,16 +139,18 @@ val (rty, qty) = (dest_funT o fastype_of) abs_fun val qty_name = (fst o dest_Type) qty val quotient_thm_name = Binding.prefix_name "Quotient_" (Binding.qualified_name qty_name) - val quot_thm = (case (HOLogic.dest_Trueprop o prop_of) equiv_thm of - Const (@{const_name equivp}, _) $ _ => - [quot3_thm, T_def, equiv_thm] MRSL @{thm Quotient3_to_Quotient_equivp} - | Const (@{const_name part_equivp}, _) $ _ => - [quot3_thm, T_def] MRSL @{thm Quotient3_to_Quotient} + val (reflp_thm, quot_thm) = (case (HOLogic.dest_Trueprop o prop_of) equiv_thm of + Const (@{const_name equivp}, _) $ _ => + (SOME (equiv_thm RS @{thm equivp_reflp2}), + [quot3_thm, T_def, equiv_thm] MRSL @{thm Quotient3_to_Quotient_equivp}) + | Const (@{const_name part_equivp}, _) $ _ => + (NONE, + [quot3_thm, T_def] MRSL @{thm Quotient3_to_Quotient}) | _ => error "unsupported equivalence theorem" ) in lthy' - |> Lifting_Setup.setup_lifting_infr quot_thm equiv_thm + |> Lifting_Setup.setup_by_quotient quot_thm reflp_thm |> (snd oo Local_Theory.note) ((quotient_thm_name, []), [quot_thm]) end diff -r ef2d04520337 -r 69f95ac85c3d src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Tue Apr 17 16:14:07 2012 +0100 +++ b/src/HOL/Word/Word.thy Tue Apr 17 19:16:13 2012 +0200 @@ -244,26 +244,10 @@ by (simp add: reflp_def) local_setup {* - Lifting_Setup.setup_lifting_infr @{thm Quotient_word} @{thm reflp_word} + Lifting_Setup.setup_by_quotient @{thm Quotient_word} (SOME @{thm reflp_word}) *} -text {* TODO: The next several lemmas could be generated automatically. *} - -lemma bi_total_cr_word [transfer_rule]: "bi_total cr_word" - using Quotient_word reflp_word by (rule Quotient_bi_total) - -lemma right_unique_cr_word [transfer_rule]: "right_unique cr_word" - using Quotient_word by (rule Quotient_right_unique) - -lemma word_eq_transfer [transfer_rule]: - "(fun_rel cr_word (fun_rel cr_word op =)) - (\x y. bintrunc (len_of TYPE('a)) x = bintrunc (len_of TYPE('a)) y) - (op = :: 'a::len0 word \ 'a word \ bool)" - using Quotient_word by (rule Quotient_rel_eq_transfer) - -lemma word_of_int_transfer [transfer_rule]: - "(fun_rel op = cr_word) (\x. x) word_of_int" - using Quotient_word reflp_word by (rule Quotient_id_abs_transfer) +text {* TODO: The next lemma could be generated automatically. *} lemma uint_transfer [transfer_rule]: "(fun_rel cr_word op =) (bintrunc (len_of TYPE('a)))