1.1 --- a/src/HOL/IsaMakefile Thu Nov 17 18:31:00 2011 +0100
1.2 +++ b/src/HOL/IsaMakefile Fri Nov 18 04:56:35 2011 +0100
1.3 @@ -1507,7 +1507,8 @@
1.4 $(LOG)/HOL-Quotient_Examples.gz: $(OUT)/HOL \
1.5 Quotient_Examples/DList.thy Quotient_Examples/Quotient_Cset.thy \
1.6 Quotient_Examples/FSet.thy Quotient_Examples/List_Quotient_Cset.thy \
1.7 - Quotient_Examples/Quotient_Int.thy Quotient_Examples/Quotient_Message.thy
1.8 + Quotient_Examples/Quotient_Int.thy Quotient_Examples/Quotient_Message.thy \
1.9 + Quotient_Examples/Lift_Set.thy
1.10 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples
1.11
1.12
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/HOL/Quotient_Examples/Lift_Set.thy Fri Nov 18 04:56:35 2011 +0100
2.3 @@ -0,0 +1,43 @@
2.4 +(* Title: HOL/Quotient.thy
2.5 + Author: Lukas Bulwahn and Ondrey Kuncar
2.6 +*)
2.7 +
2.8 +header {* Example of lifting definitions with the quotient infrastructure *}
2.9 +
2.10 +theory Lift_Set
2.11 +imports Main
2.12 +begin
2.13 +
2.14 +typedef 'a set = "(UNIV :: ('a => bool) => bool)"
2.15 +morphisms member Set by auto
2.16 +
2.17 +text {* Here is some ML setup that should eventually be incorporated in the typedef command. *}
2.18 +
2.19 +local_setup {* fn lthy =>
2.20 +let
2.21 + val quotients = {qtyp = @{typ "'a set"}, rtyp = @{typ "'a => bool"}, equiv_rel = @{term "dummy"}, equiv_thm = @{thm refl}}
2.22 + val qty_full_name = @{type_name "set"}
2.23 +
2.24 + fun qinfo phi = Quotient_Info.transform_quotients phi quotients
2.25 + in lthy
2.26 + |> Local_Theory.declaration {syntax = false, pervasive = true}
2.27 + (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi)
2.28 + #> Quotient_Info.update_abs_rep qty_full_name (Quotient_Info.transform_abs_rep phi {abs = @{term "Set"}, rep = @{term "member"}}))
2.29 + end
2.30 +*}
2.31 +
2.32 +text {* Now, we can employ quotient_definition to lift definitions. *}
2.33 +
2.34 +quotient_definition empty where "empty :: 'a set"
2.35 +is "Set.empty"
2.36 +
2.37 +term "Lift_Set.empty"
2.38 +thm Lift_Set.empty_def
2.39 +
2.40 +quotient_definition insert where "insert :: 'a => 'a set => 'a set"
2.41 +is "Set.insert"
2.42 +
2.43 +term "Lift_Set.insert"
2.44 +thm Lift_Set.insert_def
2.45 +
2.46 +end
3.1 --- a/src/HOL/Quotient_Examples/Quotient_Message.thy Thu Nov 17 18:31:00 2011 +0100
3.2 +++ b/src/HOL/Quotient_Examples/Quotient_Message.thy Fri Nov 18 04:56:35 2011 +0100
3.3 @@ -5,7 +5,7 @@
3.4 *)
3.5
3.6 theory Quotient_Message
3.7 -imports Main Quotient_Syntax
3.8 +imports Main "~~/src/HOL/Library/Quotient_Syntax"
3.9 begin
3.10
3.11 subsection{*Defining the Free Algebra*}
4.1 --- a/src/HOL/Quotient_Examples/ROOT.ML Thu Nov 17 18:31:00 2011 +0100
4.2 +++ b/src/HOL/Quotient_Examples/ROOT.ML Fri Nov 18 04:56:35 2011 +0100
4.3 @@ -4,5 +4,5 @@
4.4 Testing the quotient package.
4.5 *)
4.6
4.7 -use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Quotient_Cset", "List_Quotient_Cset"];
4.8 +use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Quotient_Cset", "List_Quotient_Cset", "Lift_Set"];
4.9
5.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML Thu Nov 17 18:31:00 2011 +0100
5.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML Fri Nov 18 04:56:35 2011 +0100
5.3 @@ -11,6 +11,13 @@
5.4 val lookup_quotmaps_global: theory -> string -> quotmaps option
5.5 val print_quotmaps: Proof.context -> unit
5.6
5.7 + type abs_rep = {abs : term, rep : term}
5.8 + val transform_abs_rep: morphism -> abs_rep -> abs_rep
5.9 + val lookup_abs_rep: Proof.context -> string -> abs_rep option
5.10 + val lookup_abs_rep_global: theory -> string -> abs_rep option
5.11 + val update_abs_rep: string -> abs_rep -> Context.generic -> Context.generic
5.12 + val print_abs_rep: Proof.context -> unit
5.13 +
5.14 type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
5.15 val transform_quotients: morphism -> quotients -> quotients
5.16 val lookup_quotients: Proof.context -> string -> quotients option
5.17 @@ -86,6 +93,39 @@
5.18 |> Pretty.writeln
5.19 end
5.20
5.21 +(* info about abs/rep terms *)
5.22 +type abs_rep = {abs : term, rep : term}
5.23 +
5.24 +structure Abs_Rep = Generic_Data
5.25 +(
5.26 + type T = abs_rep Symtab.table
5.27 + val empty = Symtab.empty
5.28 + val extend = I
5.29 + fun merge data = Symtab.merge (K true) data
5.30 +)
5.31 +
5.32 +fun transform_abs_rep phi {abs, rep} = {abs = Morphism.term phi abs, rep = Morphism.term phi rep}
5.33 +
5.34 +val lookup_abs_rep = Symtab.lookup o Abs_Rep.get o Context.Proof
5.35 +val lookup_abs_rep_global = Symtab.lookup o Abs_Rep.get o Context.Theory
5.36 +
5.37 +fun update_abs_rep str data = Abs_Rep.map (Symtab.update (str, data))
5.38 +
5.39 +fun print_abs_rep ctxt =
5.40 + let
5.41 + fun prt_abs_rep (s, {abs, rep}) =
5.42 + Pretty.block (separate (Pretty.brk 2)
5.43 + [Pretty.str "type constructor:",
5.44 + Pretty.str s,
5.45 + Pretty.str "abs term:",
5.46 + Syntax.pretty_term ctxt abs,
5.47 + Pretty.str "rep term:",
5.48 + Syntax.pretty_term ctxt rep])
5.49 + in
5.50 + map prt_abs_rep (Symtab.dest (Abs_Rep.get (Context.Proof ctxt)))
5.51 + |> Pretty.big_list "abs/rep terms:"
5.52 + |> Pretty.writeln
5.53 + end
5.54
5.55 (* info about quotient types *)
5.56 type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
6.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML Thu Nov 17 18:31:00 2011 +0100
6.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML Fri Nov 18 04:56:35 2011 +0100
6.3 @@ -123,14 +123,18 @@
6.4 (* produces the rep or abs constant for a qty *)
6.5 fun absrep_const flag ctxt qty_str =
6.6 let
6.7 - val qty_name = Long_Name.base_name qty_str
6.8 - val qualifier = Long_Name.qualifier qty_str
6.9 + (* FIXME *)
6.10 + fun mk_dummyT (Const (c, _)) = Const (c, dummyT)
6.11 + | mk_dummyT _ = error "Expecting abs/rep term to be a constant"
6.12 in
6.13 - case flag of
6.14 - AbsF => Const (Long_Name.qualify qualifier ("abs_" ^ qty_name), dummyT)
6.15 - | RepF => Const (Long_Name.qualify qualifier ("rep_" ^ qty_name), dummyT)
6.16 + case Quotient_Info.lookup_abs_rep ctxt qty_str of
6.17 + SOME abs_rep =>
6.18 + mk_dummyT (case flag of
6.19 + AbsF => #abs abs_rep
6.20 + | RepF => #rep abs_rep)
6.21 + | NONE => error ("No abs/rep terms for " ^ quote qty_str)
6.22 end
6.23 -
6.24 +
6.25 (* Lets Nitpick represent elements of quotient types as elements of the raw type *)
6.26 fun absrep_const_chk flag ctxt qty_str =
6.27 Syntax.check_term ctxt (absrep_const flag ctxt qty_str)
7.1 --- a/src/HOL/Tools/Quotient/quotient_typ.ML Thu Nov 17 18:31:00 2011 +0100
7.2 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML Fri Nov 18 04:56:35 2011 +0100
7.3 @@ -116,9 +116,9 @@
7.4 val abs_name = Binding.prefix_name "abs_" qty_name
7.5 val rep_name = Binding.prefix_name "rep_" qty_name
7.6
7.7 - val ((_, (_, abs_def)), lthy2) = lthy1
7.8 + val ((abs_t, (_, abs_def)), lthy2) = lthy1
7.9 |> Local_Theory.define ((abs_name, NoSyn), (Attrib.empty_binding, abs_trm))
7.10 - val ((_, (_, rep_def)), lthy3) = lthy2
7.11 + val ((rep_t, (_, rep_def)), lthy3) = lthy2
7.12 |> Local_Theory.define ((rep_name, NoSyn), (Attrib.empty_binding, rep_trm))
7.13
7.14 (* quot_type theorem *)
7.15 @@ -137,10 +137,12 @@
7.16 val quotients = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
7.17
7.18 fun qinfo phi = Quotient_Info.transform_quotients phi quotients
7.19 + fun abs_rep phi = Quotient_Info.transform_abs_rep phi {abs = abs_t, rep = rep_t}
7.20
7.21 val lthy4 = lthy3
7.22 |> Local_Theory.declaration {syntax = false, pervasive = true}
7.23 - (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi))
7.24 + (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi)
7.25 + #> Quotient_Info.update_abs_rep qty_full_name (abs_rep phi))
7.26 |> (snd oo Local_Theory.note)
7.27 ((equiv_thm_name,
7.28 if partial then [] else [Attrib.internal (K Quotient_Info.equiv_rules_add)]),
8.1 --- a/src/HOL/Word/Misc_Typedef.thy Thu Nov 17 18:31:00 2011 +0100
8.2 +++ b/src/HOL/Word/Misc_Typedef.thy Fri Nov 18 04:56:35 2011 +0100
8.3 @@ -25,9 +25,7 @@
8.4 context type_definition
8.5 begin
8.6
8.7 -lemmas Rep' [iff] = Rep [simplified] (* if A is given as Collect .. *)
8.8 -
8.9 -declare Rep_inverse [simp] Rep_inject [simp]
8.10 +declare Rep [iff] Rep_inverse [simp] Rep_inject [simp]
8.11
8.12 lemma Abs_eqD: "Abs x = Abs y ==> x \<in> A ==> y \<in> A ==> x = y"
8.13 by (simp add: Abs_inject)
8.14 @@ -38,7 +36,7 @@
8.15
8.16 lemma Rep_comp_inverse:
8.17 "Rep o f = g ==> Abs o g = f"
8.18 - using Rep_inverse by (auto intro: ext)
8.19 + using Rep_inverse by auto
8.20
8.21 lemma Rep_eqD [elim!]: "Rep x = Rep y ==> x = y"
8.22 by simp
8.23 @@ -48,7 +46,7 @@
8.24
8.25 lemma comp_Abs_inverse:
8.26 "f o Abs = g ==> g o Rep = f"
8.27 - using Rep_inverse by (auto intro: ext)
8.28 + using Rep_inverse by auto
8.29
8.30 lemma set_Rep:
8.31 "A = range Rep"
8.32 @@ -84,7 +82,7 @@
8.33 lemma fns4:
8.34 "Rep o fa o Abs = fr ==>
8.35 Rep o fa = fr o Rep & fa o Abs = Abs o fr"
8.36 - by (auto intro!: ext)
8.37 + by auto
8.38
8.39 end
8.40
8.41 @@ -133,7 +131,7 @@
8.42 by (drule comp_Abs_inverse [symmetric]) simp
8.43
8.44 lemma eq_norm': "Rep o Abs = norm"
8.45 - by (auto simp: eq_norm intro!: ext)
8.46 + by (auto simp: eq_norm)
8.47
8.48 lemma norm_Rep [simp]: "norm (Rep x) = Rep x"
8.49 by (auto simp: eq_norm' intro: td_th)
8.50 @@ -165,7 +163,7 @@
8.51 lemma fns5:
8.52 "Rep o fa o Abs = fr ==>
8.53 fr o norm = fr & norm o fr = fr"
8.54 - by (fold eq_norm') (auto intro!: ext)
8.55 + by (fold eq_norm') auto
8.56
8.57 (* following give conditions for converses to td_fns1
8.58 the condition (norm o fr o norm = fr o norm) says that
9.1 --- a/src/HOL/Word/Word.thy Thu Nov 17 18:31:00 2011 +0100
9.2 +++ b/src/HOL/Word/Word.thy Fri Nov 18 04:56:35 2011 +0100
9.3 @@ -746,6 +746,8 @@
9.4 "{bl. length bl = len_of TYPE('a::len0)}"
9.5 by (rule td_bl)
9.6
9.7 +lemmas word_bl_Rep' = word_bl.Rep [simplified, iff]
9.8 +
9.9 lemma word_size_bl: "size w = size (to_bl w)"
9.10 unfolding word_size by auto
9.11
9.12 @@ -764,7 +766,7 @@
9.13
9.14 lemmas word_rev_gal' = sym [THEN word_rev_gal, symmetric, standard]
9.15
9.16 -lemmas length_bl_gt_0 [iff] = xtr1 [OF word_bl.Rep' len_gt_0, standard]
9.17 +lemmas length_bl_gt_0 [iff] = xtr1 [OF word_bl_Rep' len_gt_0, standard]
9.18 lemmas bl_not_Nil [iff] =
9.19 length_bl_gt_0 [THEN length_greater_0_conv [THEN iffD1], standard]
9.20 lemmas length_bl_neq_0 [iff] = length_bl_gt_0 [THEN gr_implies_not0]
9.21 @@ -914,7 +916,7 @@
9.22 unfolding of_bl_def uint_bl
9.23 by (clarsimp simp add: bl_bin_bl_rtf word_ubin.eq_norm word_size)
9.24
9.25 -lemmas word_rev_tf = refl [THEN word_rev_tf', unfolded word_bl.Rep', standard]
9.26 +lemmas word_rev_tf = refl [THEN word_rev_tf', unfolded word_bl_Rep', standard]
9.27
9.28 lemmas word_rep_drop = word_rev_tf [simplified takefill_alt,
9.29 simplified, simplified rev_take, simplified]
9.30 @@ -2481,9 +2483,6 @@
9.31 "(\<lambda>h i. h i \<and> i < len_of TYPE('a::len0))"
9.32 by (rule td_ext_nth)
9.33
9.34 -declare test_bit.Rep' [simp del]
9.35 -declare test_bit.Rep' [rule del]
9.36 -
9.37 lemmas td_nth = test_bit.td_thm
9.38
9.39 lemma word_set_set_same:
9.40 @@ -3032,7 +3031,7 @@
9.41
9.42 lemmas shiftr_bl_of = refl [THEN shiftr_bl_of', unfolded word_size]
9.43
9.44 -lemmas shiftr_bl = word_bl.Rep' [THEN eq_imp_le, THEN shiftr_bl_of,
9.45 +lemmas shiftr_bl = word_bl_Rep' [THEN eq_imp_le, THEN shiftr_bl_of,
9.46 simplified word_size, simplified, THEN eq_reflection, standard]
9.47
9.48 lemma msb_shift': "msb (w::'a::len word) <-> (w >> (size w - 1)) ~= 0"
9.49 @@ -4062,7 +4061,7 @@
9.50 lemmas blrs0 = rotate_eqs [THEN to_bl_rotl [THEN trans]]
9.51
9.52 lemmas word_rotl_eqs =
9.53 - blrs0 [simplified word_bl.Rep' word_bl.Rep_inject to_bl_rotl [symmetric]]
9.54 + blrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotl [symmetric]]
9.55
9.56 lemma to_bl_rotr:
9.57 "to_bl (word_rotr n w) = rotater n (to_bl w)"
9.58 @@ -4071,7 +4070,7 @@
9.59 lemmas brrs0 = rotater_eqs [THEN to_bl_rotr [THEN trans]]
9.60
9.61 lemmas word_rotr_eqs =
9.62 - brrs0 [simplified word_bl.Rep' word_bl.Rep_inject to_bl_rotr [symmetric]]
9.63 + brrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotr [symmetric]]
9.64
9.65 declare word_rotr_eqs (1) [simp]
9.66 declare word_rotl_eqs (1) [simp]
9.67 @@ -4164,7 +4163,7 @@
9.68
9.69 lemmas blwl_syms [symmetric] = bl_word_not bl_word_and bl_word_or bl_word_xor
9.70
9.71 -lemmas lbl_lbl = trans [OF word_bl.Rep' word_bl.Rep' [symmetric]]
9.72 +lemmas lbl_lbl = trans [OF word_bl_Rep' word_bl_Rep' [symmetric]]
9.73
9.74 lemmas ths_map2 [OF lbl_lbl] = rotate_map2 rotater_map2
9.75
9.76 @@ -4191,10 +4190,10 @@
9.77 lemmas word_rot_logs = word_rotate.word_rot_logs
9.78
9.79 lemmas bl_word_rotl_dt = trans [OF to_bl_rotl rotate_drop_take,
9.80 - simplified word_bl.Rep', standard]
9.81 + simplified word_bl_Rep', standard]
9.82
9.83 lemmas bl_word_rotr_dt = trans [OF to_bl_rotr rotater_drop_take,
9.84 - simplified word_bl.Rep', standard]
9.85 + simplified word_bl_Rep', standard]
9.86
9.87 lemma bl_word_roti_dt':
9.88 "n = nat ((- i) mod int (size (w :: 'a :: len word))) \<Longrightarrow>
10.1 --- a/src/Pure/Isar/attrib.ML Thu Nov 17 18:31:00 2011 +0100
10.2 +++ b/src/Pure/Isar/attrib.ML Fri Nov 18 04:56:35 2011 +0100
10.3 @@ -262,20 +262,21 @@
10.4 fun partial_evaluation ctxt facts =
10.5 let
10.6 val (facts', (decls, _)) =
10.7 - (facts, ([], Context.Proof ctxt)) |-> fold_map (fn ((b, more_atts), fact) => fn res =>
10.8 - let
10.9 - val (fact', res') =
10.10 - (fact, res) |-> fold_map (fn (ths, atts) => fn res1 =>
10.11 - (ths, res1) |-> fold_map (fn th => fn res2 =>
10.12 - let
10.13 - val ((th', dyn'), res3) = fold eval (atts @ more_atts) ((th, NONE), res2);
10.14 - val th_atts' =
10.15 - (case dyn' of
10.16 - NONE => ([th'], [])
10.17 - | SOME (dyn_th', atts') => ([dyn_th'], rev atts'));
10.18 - in (th_atts', res3) end))
10.19 - |>> flat;
10.20 - in (((b, []), fact'), res') end);
10.21 + (facts, ([], Context.Proof (Context_Position.set_visible false ctxt))) |->
10.22 + fold_map (fn ((b, more_atts), fact) => fn res =>
10.23 + let
10.24 + val (fact', res') =
10.25 + (fact, res) |-> fold_map (fn (ths, atts) => fn res1 =>
10.26 + (ths, res1) |-> fold_map (fn th => fn res2 =>
10.27 + let
10.28 + val ((th', dyn'), res3) = fold eval (atts @ more_atts) ((th, NONE), res2);
10.29 + val th_atts' =
10.30 + (case dyn' of
10.31 + NONE => ([th'], [])
10.32 + | SOME (dyn_th', atts') => ([dyn_th'], rev atts'));
10.33 + in (th_atts', res3) end))
10.34 + |>> flat;
10.35 + in (((b, []), fact'), res') end);
10.36 val decl_fact = (empty_binding, rev (map (fn (th, atts) => ([th], rev atts)) decls));
10.37 in decl_fact :: facts' end;
10.38