--- a/src/HOL/Datatype.thy Tue Dec 21 08:43:39 2010 -0800
+++ b/src/HOL/Datatype.thy Tue Dec 21 17:52:35 2010 +0100
@@ -15,7 +15,7 @@
subsection {* Prelude: lifting over function space *}
-type_lifting map_fun
+type_lifting map_fun: map_fun
by (simp_all add: fun_eq_iff)
--- a/src/HOL/Library/Cset.thy Tue Dec 21 08:43:39 2010 -0800
+++ b/src/HOL/Library/Cset.thy Tue Dec 21 17:52:35 2010 +0100
@@ -188,8 +188,8 @@
"map f (Cset.set xs) = Cset.set (remdups (List.map f xs))"
by (simp add: set_def)
-type_lifting map
- by (simp_all add: image_image)
+type_lifting map: map
+ by (simp_all add: fun_eq_iff image_compose)
definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
[simp]: "filter P A = Set (More_Set.project P (member A))"
--- a/src/HOL/Library/Dlist.thy Tue Dec 21 08:43:39 2010 -0800
+++ b/src/HOL/Library/Dlist.thy Tue Dec 21 17:52:35 2010 +0100
@@ -175,8 +175,8 @@
section {* Functorial structure *}
-type_lifting map
- by (auto intro: dlist_eqI simp add: remdups_map_remdups comp_def)
+type_lifting map: map
+ by (simp_all add: List.map.id remdups_map_remdups fun_eq_iff dlist_eq_iff)
section {* Implementation of sets by distinct lists -- canonical! *}
--- a/src/HOL/Library/Mapping.thy Tue Dec 21 08:43:39 2010 -0800
+++ b/src/HOL/Library/Mapping.thy Tue Dec 21 17:52:35 2010 +0100
@@ -50,8 +50,8 @@
"lookup (map f g m) = Option.map g \<circ> lookup m \<circ> f"
by (simp add: map_def)
-type_lifting map
- by (auto intro!: mapping_eqI ext simp add: Option.map.compositionality Option.map.identity)
+type_lifting map: map
+ by (simp_all add: mapping_eq_iff fun_eq_iff Option.map.compositionality Option.map.id)
subsection {* Derived operations *}
--- a/src/HOL/Library/Multiset.thy Tue Dec 21 08:43:39 2010 -0800
+++ b/src/HOL/Library/Multiset.thy Tue Dec 21 17:52:35 2010 +0100
@@ -1643,12 +1643,21 @@
@{term "{#x+x|x:#M. x<c#}"}.
*}
-type_lifting image_mset proof -
- fix f g A show "image_mset f (image_mset g A) = image_mset (\<lambda>x. f (g x)) A"
- by (induct A) simp_all
+type_lifting image_mset: image_mset proof -
+ fix f g
+ show "image_mset f \<circ> image_mset g = image_mset (f \<circ> g)"
+ proof
+ fix A
+ show "(image_mset f \<circ> image_mset g) A = image_mset (f \<circ> g) A"
+ by (induct A) simp_all
+ qed
next
- fix A show "image_mset (\<lambda>x. x) A = A"
- by (induct A) simp_all
+ show "image_mset id = id"
+ proof
+ fix A
+ show "image_mset id A = id A"
+ by (induct A) simp_all
+ qed
qed
--- a/src/HOL/Library/Quotient_Option.thy Tue Dec 21 08:43:39 2010 -0800
+++ b/src/HOL/Library/Quotient_Option.thy Tue Dec 21 17:52:35 2010 +0100
@@ -60,7 +60,7 @@
assumes "Quotient R Abs Rep"
shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)"
apply (rule QuotientI)
- apply (simp_all add: Option.map.compositionality Option.map.identity option_rel_eq option_rel_map1 option_rel_map2 Quotient_abs_rep [OF assms] Quotient_rel_rep [OF assms])
+ apply (simp_all add: Option.map.compositionality comp_def Option.map.identity option_rel_eq option_rel_map1 option_rel_map2 Quotient_abs_rep [OF assms] Quotient_rel_rep [OF assms])
using Quotient_rel [OF assms]
apply (simp add: option_rel_unfold split: option.split)
done
--- a/src/HOL/Library/Quotient_Product.thy Tue Dec 21 08:43:39 2010 -0800
+++ b/src/HOL/Library/Quotient_Product.thy Tue Dec 21 17:52:35 2010 +0100
@@ -38,7 +38,7 @@
assumes "Quotient R2 Abs2 Rep2"
shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)"
apply (rule QuotientI)
- apply (simp add: map_pair.compositionality map_pair.identity
+ apply (simp add: map_pair.compositionality comp_def map_pair.identity
Quotient_abs_rep [OF assms(1)] Quotient_abs_rep [OF assms(2)])
apply (simp add: split_paired_all Quotient_rel_rep [OF assms(1)] Quotient_rel_rep [OF assms(2)])
using Quotient_rel [OF assms(1)] Quotient_rel [OF assms(2)]
--- a/src/HOL/Library/Quotient_Sum.thy Tue Dec 21 08:43:39 2010 -0800
+++ b/src/HOL/Library/Quotient_Sum.thy Tue Dec 21 17:52:35 2010 +0100
@@ -61,10 +61,10 @@
assumes q2: "Quotient R2 Abs2 Rep2"
shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)"
apply (rule QuotientI)
- apply (simp_all add: sum_map.compositionality sum_map.identity sum_rel_eq sum_rel_map1 sum_rel_map2
+ apply (simp_all add: sum_map.compositionality comp_def sum_map.identity sum_rel_eq sum_rel_map1 sum_rel_map2
Quotient_abs_rep [OF q1] Quotient_rel_rep [OF q1] Quotient_abs_rep [OF q2] Quotient_rel_rep [OF q2])
using Quotient_rel [OF q1] Quotient_rel [OF q2]
- apply (simp add: sum_rel_unfold split: sum.split)
+ apply (simp add: sum_rel_unfold comp_def split: sum.split)
done
lemma sum_Inl_rsp [quot_respect]:
--- a/src/HOL/List.thy Tue Dec 21 08:43:39 2010 -0800
+++ b/src/HOL/List.thy Tue Dec 21 17:52:35 2010 +0100
@@ -881,8 +881,8 @@
"length xs = length ys \<Longrightarrow> map snd (zip xs ys) = ys"
by (induct rule:list_induct2, simp_all)
-type_lifting map
- by simp_all
+type_lifting map: map
+ by (simp_all add: fun_eq_iff id_def)
subsubsection {* @{text rev} *}
--- a/src/HOL/Option.thy Tue Dec 21 08:43:39 2010 -0800
+++ b/src/HOL/Option.thy Tue Dec 21 17:52:35 2010 +0100
@@ -81,14 +81,21 @@
"map f o sum_case g h = sum_case (map f o g) (map f o h)"
by (rule ext) (simp split: sum.split)
-type_lifting Option.map proof -
- fix f g x
- show "Option.map f (Option.map g x) = Option.map (\<lambda>x. f (g x)) x"
- by (cases x) simp_all
+type_lifting map: Option.map proof -
+ fix f g
+ show "Option.map f \<circ> Option.map g = Option.map (f \<circ> g)"
+ proof
+ fix x
+ show "(Option.map f \<circ> Option.map g) x= Option.map (f \<circ> g) x"
+ by (cases x) simp_all
+ qed
next
- fix x
- show "Option.map (\<lambda>x. x) x = x"
- by (cases x) simp_all
+ show "Option.map id = id"
+ proof
+ fix x
+ show "Option.map id x = id x"
+ by (cases x) simp_all
+ qed
qed
primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option" where
--- a/src/HOL/Predicate.thy Tue Dec 21 08:43:39 2010 -0800
+++ b/src/HOL/Predicate.thy Tue Dec 21 17:52:35 2010 +0100
@@ -795,8 +795,8 @@
"eval (map f P) = image f (eval P)"
by (auto simp add: map_def)
-type_lifting map
- by (auto intro!: pred_eqI simp add: image_image)
+type_lifting map: map
+ by (auto intro!: pred_eqI simp add: fun_eq_iff image_compose)
subsubsection {* Implementation *}
--- a/src/HOL/Product_Type.thy Tue Dec 21 08:43:39 2010 -0800
+++ b/src/HOL/Product_Type.thy Tue Dec 21 17:52:35 2010 +0100
@@ -834,8 +834,8 @@
"map_pair f g (a, b) = (f a, g b)"
by (simp add: map_pair_def)
-type_lifting map_pair
- by (simp_all add: split_paired_all)
+type_lifting map_pair: map_pair
+ by (auto simp add: split_paired_all intro: ext)
lemma fst_map_pair [simp]:
"fst (map_pair f g x) = f (fst x)"
--- a/src/HOL/Sum_Type.thy Tue Dec 21 08:43:39 2010 -0800
+++ b/src/HOL/Sum_Type.thy Tue Dec 21 17:52:35 2010 +0100
@@ -95,14 +95,22 @@
"sum_map f1 f2 (Inl a) = Inl (f1 a)"
| "sum_map f1 f2 (Inr a) = Inr (f2 a)"
-type_lifting sum_map proof -
- fix f g h i s
- show "sum_map f g (sum_map h i s) = sum_map (\<lambda>x. f (h x)) (\<lambda>x. g (i x)) s"
- by (cases s) simp_all
+type_lifting sum_map: sum_map proof -
+ fix f g h i
+ show "sum_map f g \<circ> sum_map h i = sum_map (f \<circ> h) (g \<circ> i)"
+ proof
+ fix s
+ show "(sum_map f g \<circ> sum_map h i) s = sum_map (f \<circ> h) (g \<circ> i) s"
+ by (cases s) simp_all
+ qed
next
fix s
- show "sum_map (\<lambda>x. x) (\<lambda>x. x) s = s"
- by (cases s) simp_all
+ show "sum_map id id = id"
+ proof
+ fix s
+ show "sum_map id id s = id s"
+ by (cases s) simp_all
+ qed
qed
--- a/src/HOL/Tools/type_lifting.ML Tue Dec 21 08:43:39 2010 -0800
+++ b/src/HOL/Tools/type_lifting.ML Tue Dec 21 17:52:35 2010 +0100
@@ -17,6 +17,8 @@
structure Type_Lifting : TYPE_LIFTING =
struct
+val compN = "comp";
+val idN = "id";
val compositionalityN = "compositionality";
val identityN = "identity";
@@ -25,7 +27,7 @@
(* bookkeeping *)
type entry = { mapper: string, variances: (sort * (bool * bool)) list,
- compositionality: thm, identity: thm };
+ comp: thm, id: thm };
structure Data = Theory_Data(
type T = entry Symtab.table
@@ -74,19 +76,14 @@
(* mapper properties *)
-fun make_compositionality_prop variances (tyco, mapper) =
+fun make_comp_prop ctxt variances (tyco, mapper) =
let
- fun invents n k nctxt =
- let
- val names = Name.invents nctxt n k;
- in (names, fold Name.declare names nctxt) end;
- val (((vs3, vs2), vs1), _) = Name.context
- |> invents Name.aT (length variances)
- ||>> invents Name.aT (length variances)
- ||>> invents Name.aT (length variances);
- fun mk_Ts vs = map2 (fn v => fn (sort, _) => TFree (v, sort))
- vs variances;
- val (Ts1, Ts2, Ts3) = (mk_Ts vs1, mk_Ts vs2, mk_Ts vs3);
+ val sorts = map fst variances
+ val (((vs3, vs2), vs1), _) = ctxt
+ |> Variable.invent_types sorts
+ ||>> Variable.invent_types sorts
+ ||>> Variable.invent_types sorts
+ val (Ts1, Ts2, Ts3) = (map TFree vs1, map TFree vs2, map TFree vs3);
fun mk_argT ((T, T'), (_, (co, contra))) =
(if co then [(T --> T')] else [])
@ (if contra then [(T' --> T)] else []);
@@ -94,40 +91,66 @@
(if co then [false] else []) @ (if contra then [true] else [])) variances;
val Ts21 = maps mk_argT ((Ts2 ~~ Ts1) ~~ variances);
val Ts32 = maps mk_argT ((Ts3 ~~ Ts2) ~~ variances);
- val ((names21, names32), nctxt) = Name.context
+ fun invents n k nctxt =
+ let
+ val names = Name.invents nctxt n k;
+ in (names, fold Name.declare names nctxt) end;
+ val ((names21, names32), nctxt) = Variable.names_of ctxt
|> invents "f" (length Ts21)
||>> invents "f" (length Ts32);
val T1 = Type (tyco, Ts1);
val T2 = Type (tyco, Ts2);
val T3 = Type (tyco, Ts3);
- val x = Free (the_single (Name.invents nctxt (Long_Name.base_name tyco) 1), T3);
val (args21, args32) = (names21 ~~ Ts21, names32 ~~ Ts32);
val args31 = map2 (fn is_contra => fn ((f21, T21), (f32, T32)) =>
if not is_contra then
- Abs ("x", domain_type T32, Free (f21, T21) $ (Free (f32, T32) $ Bound 0))
+ HOLogic.mk_comp (Free (f21, T21), Free (f32, T32))
else
- Abs ("x", domain_type T21, Free (f32, T32) $ (Free (f21, T21) $ Bound 0))
+ HOLogic.mk_comp (Free (f32, T32), Free (f21, T21))
) contras (args21 ~~ args32)
fun mk_mapper T T' args = list_comb (Const (mapper,
map fastype_of args ---> T --> T'), args);
- val lhs = mk_mapper T2 T1 (map Free args21) $
- (mk_mapper T3 T2 (map Free args32) $ x);
- val rhs = mk_mapper T3 T1 args31 $ x;
- in (map Free (args21 @ args32) @ [x], (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, rhs)) end;
+ val lhs = HOLogic.mk_comp (mk_mapper T2 T1 (map Free args21), mk_mapper T3 T2 (map Free args32));
+ val rhs = mk_mapper T3 T1 args31;
+ in fold_rev Logic.all (map Free (args21 @ args32)) ((HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, rhs)) end;
-fun make_identity_prop variances (tyco, mapper) =
+fun make_id_prop ctxt variances (tyco, mapper) =
let
- val vs = Name.invents Name.context Name.aT (length variances);
- val Ts = map2 (fn v => fn (sort, _) => TFree (v, sort)) vs variances;
+ val (vs, ctxt') = Variable.invent_types (map fst variances) ctxt;
+ val Ts = map TFree vs;
fun bool_num b = if b then 1 else 0;
fun mk_argT (T, (_, (co, contra))) =
replicate (bool_num co + bool_num contra) (T --> T)
val Ts' = maps mk_argT (Ts ~~ variances)
val T = Type (tyco, Ts);
- val x = Free (Long_Name.base_name tyco, T);
val lhs = list_comb (Const (mapper, Ts' ---> T --> T),
- map (fn T => Abs ("x", domain_type T, Bound 0)) Ts') $ x;
- in (x, (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, x)) end;
+ map (HOLogic.id_const o domain_type) Ts');
+ in (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, HOLogic.id_const T) end;
+
+val comp_apply = Simpdata.mk_eq @{thm o_apply};
+val id_def = Simpdata.mk_eq @{thm id_def};
+
+fun make_compositionality ctxt thm =
+ let
+ val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt;
+ val thm'' = @{thm fun_cong} OF [thm'];
+ val thm''' =
+ (Conv.fconv_rule o Conv.arg_conv o Conv.arg1_conv o Conv.rewr_conv) comp_apply thm'';
+ in singleton (Variable.export ctxt' ctxt) thm''' end;
+
+fun args_conv k conv =
+ if k <= 0 then Conv.all_conv
+ else Conv.combination_conv (args_conv (k - 1) conv) conv;
+
+fun make_identity ctxt variances thm =
+ let
+ val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt;
+ fun bool_num b = if b then 1 else 0;
+ val num_args = Integer.sum
+ (map (fn (_, (co, contra)) => bool_num co + bool_num contra) variances);
+ val thm'' =
+ (Conv.fconv_rule o Conv.arg_conv o Conv.arg1_conv o args_conv num_args o Conv.rewr_conv) id_def thm';
+ in singleton (Variable.export ctxt' ctxt) thm'' end;
(* analyzing and registering mappers *)
@@ -177,7 +200,6 @@
val (mapper, T) = case prep_term thy raw_t
of Const cT => cT
| t => error ("No constant: " ^ Syntax.string_of_term_global thy t);
- val prfx = the_default (Long_Name.base_name mapper) some_prfx;
val _ = Type.no_tvars T;
fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts
| add_tycos _ = I;
@@ -186,24 +208,29 @@
else case remove (op =) "fun" tycos
of [tyco] => tyco
| _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ_global thy T);
+ val prfx = the_default (Long_Name.base_name tyco) some_prfx;
val variances = analyze_variances thy tyco T;
- val compositionality_prop = uncurry (fold_rev Logic.all)
- (make_compositionality_prop variances (tyco, mapper));
- val identity_prop = uncurry Logic.all
- (make_identity_prop variances (tyco, mapper));
+ val ctxt = ProofContext.init_global thy;
+ val comp_prop = make_comp_prop ctxt variances (tyco, mapper);
+ val id_prop = make_id_prop ctxt variances (tyco, mapper);
val qualify = Binding.qualify true prfx o Binding.name;
- fun after_qed [single_compositionality, single_identity] lthy =
+ fun after_qed [single_comp, single_id] lthy =
lthy
- |> Local_Theory.note ((qualify compositionalityN, []), single_compositionality)
- ||>> Local_Theory.note ((qualify identityN, []), single_identity)
- |-> (fn ((_, [compositionality]), (_, [identity])) =>
- (Local_Theory.background_theory o Data.map)
+ |> Local_Theory.note ((qualify compN, []), single_comp)
+ ||>> Local_Theory.note ((qualify idN, []), single_id)
+ |-> (fn ((_, [comp]), (_, [id])) => fn lthy =>
+ lthy
+ |> Local_Theory.note ((qualify compositionalityN, []), [make_compositionality lthy comp])
+ |> snd
+ |> Local_Theory.note ((qualify identityN, []), [make_identity lthy variances id])
+ |> snd
+ |> (Local_Theory.background_theory o Data.map)
(Symtab.update (tyco, { mapper = mapper, variances = variances,
- compositionality = compositionality, identity = identity })));
+ comp = comp, id = id })));
in
thy
|> Named_Target.theory_init
- |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [compositionality_prop, identity_prop])
+ |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [comp_prop, id_prop])
end
val type_lifting = gen_type_lifting Sign.cert_term;