# HG changeset patch # User kuncar # Date 1334761443 -7200 # Node ID a2850a16e30f3a3a9d956c486f1b8d1f844f2d5d # Parent e455cdaac4790b0315db8fd761cc11ac7f500f20 Lifting: generate more thms & note them & tuned diff -r e455cdaac479 -r a2850a16e30f src/HOL/Lifting.thy --- a/src/HOL/Lifting.thy Wed Apr 18 15:48:32 2012 +0200 +++ b/src/HOL/Lifting.thy Wed Apr 18 17:04:03 2012 +0200 @@ -353,39 +353,27 @@ unfolding bi_unique_def T_def by (simp add: type_definition.Rep_inject [OF type]) -lemma typedef_right_total: "right_total T" - unfolding right_total_def T_def by simp - lemma typedef_rep_transfer: "(T ===> op =) (\x. x) Rep" unfolding fun_rel_def T_def by simp -lemma typedef_transfer_All: "((T ===> op =) ===> op =) (Ball A) All" - unfolding T_def fun_rel_def - by (metis type_definition.Rep [OF type] - type_definition.Abs_inverse [OF type]) - -lemma typedef_transfer_Ex: "((T ===> op =) ===> op =) (Bex A) Ex" +lemma typedef_All_transfer: "((T ===> op =) ===> op =) (Ball A) All" unfolding T_def fun_rel_def by (metis type_definition.Rep [OF type] type_definition.Abs_inverse [OF type]) -lemma typedef_transfer_bforall: +lemma typedef_Ex_transfer: "((T ===> op =) ===> op =) (Bex A) Ex" + unfolding T_def fun_rel_def + by (metis type_definition.Rep [OF type] + type_definition.Abs_inverse [OF type]) + +lemma typedef_forall_transfer: "((T ===> op =) ===> op =) (transfer_bforall (\x. x \ A)) transfer_forall" unfolding transfer_bforall_def transfer_forall_def Ball_def [symmetric] - by (rule typedef_transfer_All) + by (rule typedef_All_transfer) end -text {* Generating transfer rules for a type copy. *} - -lemma copy_type_bi_total: - assumes type: "type_definition Rep Abs UNIV" - assumes T_def: "T \ (\x y. x = Rep y)" - shows "bi_total T" - unfolding bi_total_def T_def - by (metis type_definition.Abs_inverse [OF type] UNIV_I) - text {* Generating the correspondence rule for a constant defined with @{text "lift_definition"}. *} diff -r e455cdaac479 -r a2850a16e30f src/HOL/Tools/Lifting/lifting_def.ML --- a/src/HOL/Tools/Lifting/lifting_def.ML Wed Apr 18 15:48:32 2012 +0200 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Wed Apr 18 17:04:03 2012 +0200 @@ -180,10 +180,9 @@ val transfer_thm = [quotient_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer} |> Raw_Simplifier.rewrite_rule (Transfer.get_relator_eq lthy') - fun qualify defname suffix = Binding.name suffix - |> Binding.qualify true defname + fun qualify defname suffix = Binding.qualified true suffix defname - val lhs_name = Binding.name_of (#1 var) + val lhs_name = (#1 var) val rsp_thm_name = qualify lhs_name "rsp" val code_eqn_thm_name = qualify lhs_name "rep_eq" val transfer_thm_name = qualify lhs_name "transfer" diff -r e455cdaac479 -r a2850a16e30f src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Wed Apr 18 15:48:32 2012 +0200 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Wed Apr 18 17:04:03 2012 +0200 @@ -59,19 +59,19 @@ val rty_tfreesT = Term.add_tfree_namesT rty [] val qty_tfreesT = Term.add_tfree_namesT qty [] val extra_rty_tfrees = - (case subtract (op =) qty_tfreesT rty_tfreesT of + case subtract (op =) qty_tfreesT rty_tfreesT of [] => [] | extras => [Pretty.block ([Pretty.str "Extra variables in the raw type:", Pretty.brk 1] @ ((Pretty.commas o map (Pretty.str o quote)) extras) @ - [Pretty.str "."])]) + [Pretty.str "."])] val not_type_constr = - (case qty of + case qty of Type _ => [] | _ => [Pretty.block [Pretty.str "The quotient type ", Pretty.quote (Syntax.pretty_typ ctxt' qty), Pretty.brk 1, - Pretty.str "is not a type constructor."]]) + Pretty.str "is not a type constructor."]] val errs = extra_rty_tfrees @ not_type_constr in if null errs then () else error (cat_lines (["Sanity check of the quotient theorem failed:",""] @@ -95,20 +95,29 @@ fun setup_by_quotient quot_thm maybe_reflp_thm lthy = let val transfer_attr = Attrib.internal (K Transfer.transfer_add) + val (_, qty) = Lifting_Term.quot_thm_rty_qty quot_thm + val qty_name = (Binding.name o fst o dest_Type) qty + fun qualify suffix = Binding.qualified true suffix qty_name val lthy' = case maybe_reflp_thm of SOME reflp_thm => lthy - |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), + |> (snd oo Local_Theory.note) ((qualify "bi_total", [transfer_attr]), [[quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}]) - |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), + |> (snd oo Local_Theory.note) ((qualify "id_abs_transfer", [transfer_attr]), [[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}]) | NONE => lthy + |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]), + [quot_thm RS @{thm Quotient_All_transfer}]) + |> (snd oo Local_Theory.note) ((qualify "Ex_transfer", [transfer_attr]), + [quot_thm RS @{thm Quotient_Ex_transfer}]) + |> (snd oo Local_Theory.note) ((qualify "forall_transfer", [transfer_attr]), + [quot_thm RS @{thm Quotient_forall_transfer}]) in lthy' - |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), + |> (snd oo Local_Theory.note) ((qualify "right_unique", [transfer_attr]), [quot_thm RS @{thm Quotient_right_unique}]) - |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), + |> (snd oo Local_Theory.note) ((qualify "right_total", [transfer_attr]), [quot_thm RS @{thm Quotient_right_total}]) - |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), + |> (snd oo Local_Theory.note) ((qualify "rel_eq_transfer", [transfer_attr]), [quot_thm RS @{thm Quotient_rel_eq_transfer}]) |> setup_lifting_infr quot_thm end @@ -118,33 +127,48 @@ 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 + + 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}) + [typedef_thm, T_def] MRSL @{thm typedef_to_Quotient} + + val (_, qty) = Lifting_Term.quot_thm_rty_qty quot_thm + val qty_name = (Binding.name o fst o dest_Type) qty + fun qualify suffix = Binding.qualified true suffix qty_name - 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') + val lthy'' = case typedef_set of + Const ("Orderings.top_class.top", _) => + let + val equivp_thm = typedef_thm RS @{thm UNIV_typedef_to_equivp} + val reflp_thm = equivp_thm RS @{thm equivp_reflp2} + in + lthy' + |> (snd oo Local_Theory.note) ((qualify "bi_total", [transfer_attr]), + [[quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}]) + |> (snd oo Local_Theory.note) ((qualify "id_abs_transfer", [transfer_attr]), + [[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}]) + end + | _ => lthy' + |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]), + [[typedef_thm, T_def] MRSL @{thm typedef_All_transfer}]) + |> (snd oo Local_Theory.note) ((qualify "Ex_transfer", [transfer_attr]), + [[typedef_thm, T_def] MRSL @{thm typedef_Ex_transfer}]) + |> (snd oo Local_Theory.note) ((qualify "forall_transfer", [transfer_attr]), + [[typedef_thm, T_def] MRSL @{thm typedef_forall_transfer}]) in lthy'' - |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), + |> (snd oo Local_Theory.note) ((qualify "bi_unique", [transfer_attr]), [[typedef_thm, T_def] MRSL @{thm typedef_bi_unique}]) - |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), - [[typedef_thm, T_def] MRSL @{thm typedef_right_total}]) - |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), + |> (snd oo Local_Theory.note) ((qualify "rep_transfer", [transfer_attr]), [[typedef_thm, T_def] MRSL @{thm typedef_rep_transfer}]) - |> (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}]) + |> (snd oo Local_Theory.note) ((qualify "right_unique", [transfer_attr]), + [[quot_thm] MRSL @{thm Quotient_right_unique}]) + |> (snd oo Local_Theory.note) ((qualify "right_total", [transfer_attr]), + [[quot_thm] MRSL @{thm Quotient_right_total}]) |> setup_lifting_infr quot_thm end