# HG changeset patch # User huffman # Date 1321588595 -3600 # Node ID 3eb6319febfed77a4827f29dca043ccd073d7d70 # Parent 3e2722d661694f00de89c5eb5563bb3c5fd7adfb# Parent 1fffa81b9b83af43af217312270697b180dac63c merged diff -r 3e2722d66169 -r 3eb6319febfe src/HOL/IsaMakefile --- 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 diff -r 3e2722d66169 -r 3eb6319febfe src/HOL/Quotient_Examples/Lift_Set.thy --- /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 diff -r 3e2722d66169 -r 3eb6319febfe src/HOL/Quotient_Examples/Quotient_Message.thy --- 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*} diff -r 3e2722d66169 -r 3eb6319febfe src/HOL/Quotient_Examples/ROOT.ML --- 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"]; diff -r 3e2722d66169 -r 3eb6319febfe src/HOL/Tools/Quotient/quotient_info.ML --- 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} diff -r 3e2722d66169 -r 3eb6319febfe src/HOL/Tools/Quotient/quotient_term.ML --- 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) diff -r 3e2722d66169 -r 3eb6319febfe src/HOL/Tools/Quotient/quotient_typ.ML --- 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)]), diff -r 3e2722d66169 -r 3eb6319febfe src/HOL/Word/Misc_Typedef.thy --- 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 \ A ==> y \ 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 diff -r 3e2722d66169 -r 3eb6319febfe src/HOL/Word/Word.thy --- 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 @@ "(\h i. h i \ 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))) \ diff -r 3e2722d66169 -r 3eb6319febfe src/Pure/Isar/attrib.ML --- 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;