1.1 --- a/src/HOL/Lifting.thy Wed Apr 18 15:48:32 2012 +0200
1.2 +++ b/src/HOL/Lifting.thy Wed Apr 18 17:04:03 2012 +0200
1.3 @@ -353,39 +353,27 @@
1.4 unfolding bi_unique_def T_def
1.5 by (simp add: type_definition.Rep_inject [OF type])
1.6
1.7 -lemma typedef_right_total: "right_total T"
1.8 - unfolding right_total_def T_def by simp
1.9 -
1.10 lemma typedef_rep_transfer: "(T ===> op =) (\<lambda>x. x) Rep"
1.11 unfolding fun_rel_def T_def by simp
1.12
1.13 -lemma typedef_transfer_All: "((T ===> op =) ===> op =) (Ball A) All"
1.14 +lemma typedef_All_transfer: "((T ===> op =) ===> op =) (Ball A) All"
1.15 unfolding T_def fun_rel_def
1.16 by (metis type_definition.Rep [OF type]
1.17 type_definition.Abs_inverse [OF type])
1.18
1.19 -lemma typedef_transfer_Ex: "((T ===> op =) ===> op =) (Bex A) Ex"
1.20 +lemma typedef_Ex_transfer: "((T ===> op =) ===> op =) (Bex A) Ex"
1.21 unfolding T_def fun_rel_def
1.22 by (metis type_definition.Rep [OF type]
1.23 type_definition.Abs_inverse [OF type])
1.24
1.25 -lemma typedef_transfer_bforall:
1.26 +lemma typedef_forall_transfer:
1.27 "((T ===> op =) ===> op =)
1.28 (transfer_bforall (\<lambda>x. x \<in> A)) transfer_forall"
1.29 unfolding transfer_bforall_def transfer_forall_def Ball_def [symmetric]
1.30 - by (rule typedef_transfer_All)
1.31 + by (rule typedef_All_transfer)
1.32
1.33 end
1.34
1.35 -text {* Generating transfer rules for a type copy. *}
1.36 -
1.37 -lemma copy_type_bi_total:
1.38 - assumes type: "type_definition Rep Abs UNIV"
1.39 - assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
1.40 - shows "bi_total T"
1.41 - unfolding bi_total_def T_def
1.42 - by (metis type_definition.Abs_inverse [OF type] UNIV_I)
1.43 -
1.44 text {* Generating the correspondence rule for a constant defined with
1.45 @{text "lift_definition"}. *}
1.46
2.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML Wed Apr 18 15:48:32 2012 +0200
2.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Wed Apr 18 17:04:03 2012 +0200
2.3 @@ -180,10 +180,9 @@
2.4 val transfer_thm = [quotient_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer}
2.5 |> Raw_Simplifier.rewrite_rule (Transfer.get_relator_eq lthy')
2.6
2.7 - fun qualify defname suffix = Binding.name suffix
2.8 - |> Binding.qualify true defname
2.9 + fun qualify defname suffix = Binding.qualified true suffix defname
2.10
2.11 - val lhs_name = Binding.name_of (#1 var)
2.12 + val lhs_name = (#1 var)
2.13 val rsp_thm_name = qualify lhs_name "rsp"
2.14 val code_eqn_thm_name = qualify lhs_name "rep_eq"
2.15 val transfer_thm_name = qualify lhs_name "transfer"
3.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML Wed Apr 18 15:48:32 2012 +0200
3.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Wed Apr 18 17:04:03 2012 +0200
3.3 @@ -59,19 +59,19 @@
3.4 val rty_tfreesT = Term.add_tfree_namesT rty []
3.5 val qty_tfreesT = Term.add_tfree_namesT qty []
3.6 val extra_rty_tfrees =
3.7 - (case subtract (op =) qty_tfreesT rty_tfreesT of
3.8 + case subtract (op =) qty_tfreesT rty_tfreesT of
3.9 [] => []
3.10 | extras => [Pretty.block ([Pretty.str "Extra variables in the raw type:",
3.11 Pretty.brk 1] @
3.12 ((Pretty.commas o map (Pretty.str o quote)) extras) @
3.13 - [Pretty.str "."])])
3.14 + [Pretty.str "."])]
3.15 val not_type_constr =
3.16 - (case qty of
3.17 + case qty of
3.18 Type _ => []
3.19 | _ => [Pretty.block [Pretty.str "The quotient type ",
3.20 Pretty.quote (Syntax.pretty_typ ctxt' qty),
3.21 Pretty.brk 1,
3.22 - Pretty.str "is not a type constructor."]])
3.23 + Pretty.str "is not a type constructor."]]
3.24 val errs = extra_rty_tfrees @ not_type_constr
3.25 in
3.26 if null errs then () else error (cat_lines (["Sanity check of the quotient theorem failed:",""]
3.27 @@ -95,20 +95,29 @@
3.28 fun setup_by_quotient quot_thm maybe_reflp_thm lthy =
3.29 let
3.30 val transfer_attr = Attrib.internal (K Transfer.transfer_add)
3.31 + val (_, qty) = Lifting_Term.quot_thm_rty_qty quot_thm
3.32 + val qty_name = (Binding.name o fst o dest_Type) qty
3.33 + fun qualify suffix = Binding.qualified true suffix qty_name
3.34 val lthy' = case maybe_reflp_thm of
3.35 SOME reflp_thm => lthy
3.36 - |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
3.37 + |> (snd oo Local_Theory.note) ((qualify "bi_total", [transfer_attr]),
3.38 [[quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}])
3.39 - |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
3.40 + |> (snd oo Local_Theory.note) ((qualify "id_abs_transfer", [transfer_attr]),
3.41 [[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}])
3.42 | NONE => lthy
3.43 + |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]),
3.44 + [quot_thm RS @{thm Quotient_All_transfer}])
3.45 + |> (snd oo Local_Theory.note) ((qualify "Ex_transfer", [transfer_attr]),
3.46 + [quot_thm RS @{thm Quotient_Ex_transfer}])
3.47 + |> (snd oo Local_Theory.note) ((qualify "forall_transfer", [transfer_attr]),
3.48 + [quot_thm RS @{thm Quotient_forall_transfer}])
3.49 in
3.50 lthy'
3.51 - |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
3.52 + |> (snd oo Local_Theory.note) ((qualify "right_unique", [transfer_attr]),
3.53 [quot_thm RS @{thm Quotient_right_unique}])
3.54 - |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
3.55 + |> (snd oo Local_Theory.note) ((qualify "right_total", [transfer_attr]),
3.56 [quot_thm RS @{thm Quotient_right_total}])
3.57 - |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
3.58 + |> (snd oo Local_Theory.note) ((qualify "rel_eq_transfer", [transfer_attr]),
3.59 [quot_thm RS @{thm Quotient_rel_eq_transfer}])
3.60 |> setup_lifting_infr quot_thm
3.61 end
3.62 @@ -118,33 +127,48 @@
3.63 val transfer_attr = Attrib.internal (K Transfer.transfer_add)
3.64 val (_ $ rep_fun $ _ $ typedef_set) = (HOLogic.dest_Trueprop o prop_of) typedef_thm
3.65 val (T_def, lthy') = define_cr_rel rep_fun lthy
3.66 -
3.67 - val quot_thm = (case typedef_set of
3.68 +
3.69 + val quot_thm = case typedef_set of
3.70 Const ("Orderings.top_class.top", _) =>
3.71 [typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient}
3.72 | Const (@{const_name "Collect"}, _) $ Abs (_, _, _) =>
3.73 [typedef_thm, T_def] MRSL @{thm open_typedef_to_Quotient}
3.74 | _ =>
3.75 - [typedef_thm, T_def] MRSL @{thm typedef_to_Quotient})
3.76 + [typedef_thm, T_def] MRSL @{thm typedef_to_Quotient}
3.77
3.78 - val lthy'' = (case typedef_set of
3.79 - Const ("Orderings.top_class.top", _) => (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
3.80 - [[typedef_thm,T_def] MRSL @{thm copy_type_bi_total}]) lthy'
3.81 - | _ => lthy')
3.82 + val (_, qty) = Lifting_Term.quot_thm_rty_qty quot_thm
3.83 + val qty_name = (Binding.name o fst o dest_Type) qty
3.84 + fun qualify suffix = Binding.qualified true suffix qty_name
3.85 +
3.86 + val lthy'' = case typedef_set of
3.87 + Const ("Orderings.top_class.top", _) =>
3.88 + let
3.89 + val equivp_thm = typedef_thm RS @{thm UNIV_typedef_to_equivp}
3.90 + val reflp_thm = equivp_thm RS @{thm equivp_reflp2}
3.91 + in
3.92 + lthy'
3.93 + |> (snd oo Local_Theory.note) ((qualify "bi_total", [transfer_attr]),
3.94 + [[quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}])
3.95 + |> (snd oo Local_Theory.note) ((qualify "id_abs_transfer", [transfer_attr]),
3.96 + [[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}])
3.97 + end
3.98 + | _ => lthy'
3.99 + |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]),
3.100 + [[typedef_thm, T_def] MRSL @{thm typedef_All_transfer}])
3.101 + |> (snd oo Local_Theory.note) ((qualify "Ex_transfer", [transfer_attr]),
3.102 + [[typedef_thm, T_def] MRSL @{thm typedef_Ex_transfer}])
3.103 + |> (snd oo Local_Theory.note) ((qualify "forall_transfer", [transfer_attr]),
3.104 + [[typedef_thm, T_def] MRSL @{thm typedef_forall_transfer}])
3.105 in
3.106 lthy''
3.107 - |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
3.108 + |> (snd oo Local_Theory.note) ((qualify "bi_unique", [transfer_attr]),
3.109 [[typedef_thm, T_def] MRSL @{thm typedef_bi_unique}])
3.110 - |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
3.111 - [[typedef_thm, T_def] MRSL @{thm typedef_right_total}])
3.112 - |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
3.113 + |> (snd oo Local_Theory.note) ((qualify "rep_transfer", [transfer_attr]),
3.114 [[typedef_thm, T_def] MRSL @{thm typedef_rep_transfer}])
3.115 - |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
3.116 - [[typedef_thm, T_def] MRSL @{thm typedef_transfer_All}])
3.117 - |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
3.118 - [[typedef_thm, T_def] MRSL @{thm typedef_transfer_Ex}])
3.119 - |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
3.120 - [[typedef_thm, T_def] MRSL @{thm typedef_transfer_bforall}])
3.121 + |> (snd oo Local_Theory.note) ((qualify "right_unique", [transfer_attr]),
3.122 + [[quot_thm] MRSL @{thm Quotient_right_unique}])
3.123 + |> (snd oo Local_Theory.note) ((qualify "right_total", [transfer_attr]),
3.124 + [[quot_thm] MRSL @{thm Quotient_right_total}])
3.125 |> setup_lifting_infr quot_thm
3.126 end
3.127