--- a/src/HOL/IsaMakefile Thu Nov 17 18:31:00 2011 +0100
+++ b/src/HOL/IsaMakefile Fri Nov 18 04:56:35 2011 +0100
@@ -1507,7 +1507,8 @@
$(LOG)/HOL-Quotient_Examples.gz: $(OUT)/HOL \
Quotient_Examples/DList.thy Quotient_Examples/Quotient_Cset.thy \
Quotient_Examples/FSet.thy Quotient_Examples/List_Quotient_Cset.thy \
- Quotient_Examples/Quotient_Int.thy Quotient_Examples/Quotient_Message.thy
+ Quotient_Examples/Quotient_Int.thy Quotient_Examples/Quotient_Message.thy \
+ Quotient_Examples/Lift_Set.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quotient_Examples/Lift_Set.thy Fri Nov 18 04:56:35 2011 +0100
@@ -0,0 +1,43 @@
+(* Title: HOL/Quotient.thy
+ Author: Lukas Bulwahn and Ondrey Kuncar
+*)
+
+header {* Example of lifting definitions with the quotient infrastructure *}
+
+theory Lift_Set
+imports Main
+begin
+
+typedef 'a set = "(UNIV :: ('a => bool) => bool)"
+morphisms member Set by auto
+
+text {* Here is some ML setup that should eventually be incorporated in the typedef command. *}
+
+local_setup {* fn lthy =>
+let
+ val quotients = {qtyp = @{typ "'a set"}, rtyp = @{typ "'a => bool"}, equiv_rel = @{term "dummy"}, equiv_thm = @{thm refl}}
+ val qty_full_name = @{type_name "set"}
+
+ fun qinfo phi = Quotient_Info.transform_quotients phi quotients
+ in lthy
+ |> Local_Theory.declaration {syntax = false, pervasive = true}
+ (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi)
+ #> Quotient_Info.update_abs_rep qty_full_name (Quotient_Info.transform_abs_rep phi {abs = @{term "Set"}, rep = @{term "member"}}))
+ end
+*}
+
+text {* Now, we can employ quotient_definition to lift definitions. *}
+
+quotient_definition empty where "empty :: 'a set"
+is "Set.empty"
+
+term "Lift_Set.empty"
+thm Lift_Set.empty_def
+
+quotient_definition insert where "insert :: 'a => 'a set => 'a set"
+is "Set.insert"
+
+term "Lift_Set.insert"
+thm Lift_Set.insert_def
+
+end
--- a/src/HOL/Quotient_Examples/Quotient_Message.thy Thu Nov 17 18:31:00 2011 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Message.thy Fri Nov 18 04:56:35 2011 +0100
@@ -5,7 +5,7 @@
*)
theory Quotient_Message
-imports Main Quotient_Syntax
+imports Main "~~/src/HOL/Library/Quotient_Syntax"
begin
subsection{*Defining the Free Algebra*}
--- a/src/HOL/Quotient_Examples/ROOT.ML Thu Nov 17 18:31:00 2011 +0100
+++ b/src/HOL/Quotient_Examples/ROOT.ML Fri Nov 18 04:56:35 2011 +0100
@@ -4,5 +4,5 @@
Testing the quotient package.
*)
-use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Quotient_Cset", "List_Quotient_Cset"];
+use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Quotient_Cset", "List_Quotient_Cset", "Lift_Set"];
--- a/src/HOL/Tools/Quotient/quotient_info.ML Thu Nov 17 18:31:00 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Fri Nov 18 04:56:35 2011 +0100
@@ -11,6 +11,13 @@
val lookup_quotmaps_global: theory -> string -> quotmaps option
val print_quotmaps: Proof.context -> unit
+ type abs_rep = {abs : term, rep : term}
+ val transform_abs_rep: morphism -> abs_rep -> abs_rep
+ val lookup_abs_rep: Proof.context -> string -> abs_rep option
+ val lookup_abs_rep_global: theory -> string -> abs_rep option
+ val update_abs_rep: string -> abs_rep -> Context.generic -> Context.generic
+ val print_abs_rep: Proof.context -> unit
+
type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
val transform_quotients: morphism -> quotients -> quotients
val lookup_quotients: Proof.context -> string -> quotients option
@@ -86,6 +93,39 @@
|> Pretty.writeln
end
+(* info about abs/rep terms *)
+type abs_rep = {abs : term, rep : term}
+
+structure Abs_Rep = Generic_Data
+(
+ type T = abs_rep Symtab.table
+ val empty = Symtab.empty
+ val extend = I
+ fun merge data = Symtab.merge (K true) data
+)
+
+fun transform_abs_rep phi {abs, rep} = {abs = Morphism.term phi abs, rep = Morphism.term phi rep}
+
+val lookup_abs_rep = Symtab.lookup o Abs_Rep.get o Context.Proof
+val lookup_abs_rep_global = Symtab.lookup o Abs_Rep.get o Context.Theory
+
+fun update_abs_rep str data = Abs_Rep.map (Symtab.update (str, data))
+
+fun print_abs_rep ctxt =
+ let
+ fun prt_abs_rep (s, {abs, rep}) =
+ Pretty.block (separate (Pretty.brk 2)
+ [Pretty.str "type constructor:",
+ Pretty.str s,
+ Pretty.str "abs term:",
+ Syntax.pretty_term ctxt abs,
+ Pretty.str "rep term:",
+ Syntax.pretty_term ctxt rep])
+ in
+ map prt_abs_rep (Symtab.dest (Abs_Rep.get (Context.Proof ctxt)))
+ |> Pretty.big_list "abs/rep terms:"
+ |> Pretty.writeln
+ end
(* info about quotient types *)
type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
--- a/src/HOL/Tools/Quotient/quotient_term.ML Thu Nov 17 18:31:00 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Fri Nov 18 04:56:35 2011 +0100
@@ -123,14 +123,18 @@
(* produces the rep or abs constant for a qty *)
fun absrep_const flag ctxt qty_str =
let
- val qty_name = Long_Name.base_name qty_str
- val qualifier = Long_Name.qualifier qty_str
+ (* FIXME *)
+ fun mk_dummyT (Const (c, _)) = Const (c, dummyT)
+ | mk_dummyT _ = error "Expecting abs/rep term to be a constant"
in
- case flag of
- AbsF => Const (Long_Name.qualify qualifier ("abs_" ^ qty_name), dummyT)
- | RepF => Const (Long_Name.qualify qualifier ("rep_" ^ qty_name), dummyT)
+ case Quotient_Info.lookup_abs_rep ctxt qty_str of
+ SOME abs_rep =>
+ mk_dummyT (case flag of
+ AbsF => #abs abs_rep
+ | RepF => #rep abs_rep)
+ | NONE => error ("No abs/rep terms for " ^ quote qty_str)
end
-
+
(* Lets Nitpick represent elements of quotient types as elements of the raw type *)
fun absrep_const_chk flag ctxt qty_str =
Syntax.check_term ctxt (absrep_const flag ctxt qty_str)
--- a/src/HOL/Tools/Quotient/quotient_typ.ML Thu Nov 17 18:31:00 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML Fri Nov 18 04:56:35 2011 +0100
@@ -116,9 +116,9 @@
val abs_name = Binding.prefix_name "abs_" qty_name
val rep_name = Binding.prefix_name "rep_" qty_name
- val ((_, (_, abs_def)), lthy2) = lthy1
+ val ((abs_t, (_, abs_def)), lthy2) = lthy1
|> Local_Theory.define ((abs_name, NoSyn), (Attrib.empty_binding, abs_trm))
- val ((_, (_, rep_def)), lthy3) = lthy2
+ val ((rep_t, (_, rep_def)), lthy3) = lthy2
|> Local_Theory.define ((rep_name, NoSyn), (Attrib.empty_binding, rep_trm))
(* quot_type theorem *)
@@ -137,10 +137,12 @@
val quotients = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
fun qinfo phi = Quotient_Info.transform_quotients phi quotients
+ fun abs_rep phi = Quotient_Info.transform_abs_rep phi {abs = abs_t, rep = rep_t}
val lthy4 = lthy3
|> Local_Theory.declaration {syntax = false, pervasive = true}
- (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi))
+ (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi)
+ #> Quotient_Info.update_abs_rep qty_full_name (abs_rep phi))
|> (snd oo Local_Theory.note)
((equiv_thm_name,
if partial then [] else [Attrib.internal (K Quotient_Info.equiv_rules_add)]),
--- a/src/HOL/Word/Misc_Typedef.thy Thu Nov 17 18:31:00 2011 +0100
+++ b/src/HOL/Word/Misc_Typedef.thy Fri Nov 18 04:56:35 2011 +0100
@@ -25,9 +25,7 @@
context type_definition
begin
-lemmas Rep' [iff] = Rep [simplified] (* if A is given as Collect .. *)
-
-declare Rep_inverse [simp] Rep_inject [simp]
+declare Rep [iff] Rep_inverse [simp] Rep_inject [simp]
lemma Abs_eqD: "Abs x = Abs y ==> x \<in> A ==> y \<in> A ==> x = y"
by (simp add: Abs_inject)
@@ -38,7 +36,7 @@
lemma Rep_comp_inverse:
"Rep o f = g ==> Abs o g = f"
- using Rep_inverse by (auto intro: ext)
+ using Rep_inverse by auto
lemma Rep_eqD [elim!]: "Rep x = Rep y ==> x = y"
by simp
@@ -48,7 +46,7 @@
lemma comp_Abs_inverse:
"f o Abs = g ==> g o Rep = f"
- using Rep_inverse by (auto intro: ext)
+ using Rep_inverse by auto
lemma set_Rep:
"A = range Rep"
@@ -84,7 +82,7 @@
lemma fns4:
"Rep o fa o Abs = fr ==>
Rep o fa = fr o Rep & fa o Abs = Abs o fr"
- by (auto intro!: ext)
+ by auto
end
@@ -133,7 +131,7 @@
by (drule comp_Abs_inverse [symmetric]) simp
lemma eq_norm': "Rep o Abs = norm"
- by (auto simp: eq_norm intro!: ext)
+ by (auto simp: eq_norm)
lemma norm_Rep [simp]: "norm (Rep x) = Rep x"
by (auto simp: eq_norm' intro: td_th)
@@ -165,7 +163,7 @@
lemma fns5:
"Rep o fa o Abs = fr ==>
fr o norm = fr & norm o fr = fr"
- by (fold eq_norm') (auto intro!: ext)
+ by (fold eq_norm') auto
(* following give conditions for converses to td_fns1
the condition (norm o fr o norm = fr o norm) says that
--- a/src/HOL/Word/Word.thy Thu Nov 17 18:31:00 2011 +0100
+++ b/src/HOL/Word/Word.thy Fri Nov 18 04:56:35 2011 +0100
@@ -746,6 +746,8 @@
"{bl. length bl = len_of TYPE('a::len0)}"
by (rule td_bl)
+lemmas word_bl_Rep' = word_bl.Rep [simplified, iff]
+
lemma word_size_bl: "size w = size (to_bl w)"
unfolding word_size by auto
@@ -764,7 +766,7 @@
lemmas word_rev_gal' = sym [THEN word_rev_gal, symmetric, standard]
-lemmas length_bl_gt_0 [iff] = xtr1 [OF word_bl.Rep' len_gt_0, standard]
+lemmas length_bl_gt_0 [iff] = xtr1 [OF word_bl_Rep' len_gt_0, standard]
lemmas bl_not_Nil [iff] =
length_bl_gt_0 [THEN length_greater_0_conv [THEN iffD1], standard]
lemmas length_bl_neq_0 [iff] = length_bl_gt_0 [THEN gr_implies_not0]
@@ -914,7 +916,7 @@
unfolding of_bl_def uint_bl
by (clarsimp simp add: bl_bin_bl_rtf word_ubin.eq_norm word_size)
-lemmas word_rev_tf = refl [THEN word_rev_tf', unfolded word_bl.Rep', standard]
+lemmas word_rev_tf = refl [THEN word_rev_tf', unfolded word_bl_Rep', standard]
lemmas word_rep_drop = word_rev_tf [simplified takefill_alt,
simplified, simplified rev_take, simplified]
@@ -2481,9 +2483,6 @@
"(\<lambda>h i. h i \<and> i < len_of TYPE('a::len0))"
by (rule td_ext_nth)
-declare test_bit.Rep' [simp del]
-declare test_bit.Rep' [rule del]
-
lemmas td_nth = test_bit.td_thm
lemma word_set_set_same:
@@ -3032,7 +3031,7 @@
lemmas shiftr_bl_of = refl [THEN shiftr_bl_of', unfolded word_size]
-lemmas shiftr_bl = word_bl.Rep' [THEN eq_imp_le, THEN shiftr_bl_of,
+lemmas shiftr_bl = word_bl_Rep' [THEN eq_imp_le, THEN shiftr_bl_of,
simplified word_size, simplified, THEN eq_reflection, standard]
lemma msb_shift': "msb (w::'a::len word) <-> (w >> (size w - 1)) ~= 0"
@@ -4062,7 +4061,7 @@
lemmas blrs0 = rotate_eqs [THEN to_bl_rotl [THEN trans]]
lemmas word_rotl_eqs =
- blrs0 [simplified word_bl.Rep' word_bl.Rep_inject to_bl_rotl [symmetric]]
+ blrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotl [symmetric]]
lemma to_bl_rotr:
"to_bl (word_rotr n w) = rotater n (to_bl w)"
@@ -4071,7 +4070,7 @@
lemmas brrs0 = rotater_eqs [THEN to_bl_rotr [THEN trans]]
lemmas word_rotr_eqs =
- brrs0 [simplified word_bl.Rep' word_bl.Rep_inject to_bl_rotr [symmetric]]
+ brrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotr [symmetric]]
declare word_rotr_eqs (1) [simp]
declare word_rotl_eqs (1) [simp]
@@ -4164,7 +4163,7 @@
lemmas blwl_syms [symmetric] = bl_word_not bl_word_and bl_word_or bl_word_xor
-lemmas lbl_lbl = trans [OF word_bl.Rep' word_bl.Rep' [symmetric]]
+lemmas lbl_lbl = trans [OF word_bl_Rep' word_bl_Rep' [symmetric]]
lemmas ths_map2 [OF lbl_lbl] = rotate_map2 rotater_map2
@@ -4191,10 +4190,10 @@
lemmas word_rot_logs = word_rotate.word_rot_logs
lemmas bl_word_rotl_dt = trans [OF to_bl_rotl rotate_drop_take,
- simplified word_bl.Rep', standard]
+ simplified word_bl_Rep', standard]
lemmas bl_word_rotr_dt = trans [OF to_bl_rotr rotater_drop_take,
- simplified word_bl.Rep', standard]
+ simplified word_bl_Rep', standard]
lemma bl_word_roti_dt':
"n = nat ((- i) mod int (size (w :: 'a :: len word))) \<Longrightarrow>
--- a/src/Pure/Isar/attrib.ML Thu Nov 17 18:31:00 2011 +0100
+++ b/src/Pure/Isar/attrib.ML Fri Nov 18 04:56:35 2011 +0100
@@ -262,20 +262,21 @@
fun partial_evaluation ctxt facts =
let
val (facts', (decls, _)) =
- (facts, ([], Context.Proof ctxt)) |-> fold_map (fn ((b, more_atts), fact) => fn res =>
- let
- val (fact', res') =
- (fact, res) |-> fold_map (fn (ths, atts) => fn res1 =>
- (ths, res1) |-> fold_map (fn th => fn res2 =>
- let
- val ((th', dyn'), res3) = fold eval (atts @ more_atts) ((th, NONE), res2);
- val th_atts' =
- (case dyn' of
- NONE => ([th'], [])
- | SOME (dyn_th', atts') => ([dyn_th'], rev atts'));
- in (th_atts', res3) end))
- |>> flat;
- in (((b, []), fact'), res') end);
+ (facts, ([], Context.Proof (Context_Position.set_visible false ctxt))) |->
+ fold_map (fn ((b, more_atts), fact) => fn res =>
+ let
+ val (fact', res') =
+ (fact, res) |-> fold_map (fn (ths, atts) => fn res1 =>
+ (ths, res1) |-> fold_map (fn th => fn res2 =>
+ let
+ val ((th', dyn'), res3) = fold eval (atts @ more_atts) ((th, NONE), res2);
+ val th_atts' =
+ (case dyn' of
+ NONE => ([th'], [])
+ | SOME (dyn_th', atts') => ([dyn_th'], rev atts'));
+ in (th_atts', res3) end))
+ |>> flat;
+ in (((b, []), fact'), res') end);
val decl_fact = (empty_binding, rev (map (fn (th, atts) => ([th], rev atts)) decls));
in decl_fact :: facts' end;