1.1 --- a/src/HOL/IntDiv.thy Fri Mar 13 10:14:47 2009 -0700
1.2 +++ b/src/HOL/IntDiv.thy Fri Mar 13 19:18:07 2009 +0100
1.3 @@ -512,15 +512,12 @@
1.4 (* simprocs adapted from HOL/ex/Binary.thy *)
1.5 ML {*
1.6 local
1.7 - infix ==;
1.8 - val op == = Logic.mk_equals;
1.9 - fun plus m n = @{term "plus :: int \<Rightarrow> int \<Rightarrow> int"} $ m $ n;
1.10 - fun mult m n = @{term "times :: int \<Rightarrow> int \<Rightarrow> int"} $ m $ n;
1.11 -
1.12 - val binary_ss = HOL_basic_ss addsimps @{thms arithmetic_simps};
1.13 - fun prove ctxt prop =
1.14 - Goal.prove ctxt [] [] prop (fn _ => ALLGOALS (full_simp_tac binary_ss));
1.15 -
1.16 + val mk_number = HOLogic.mk_number HOLogic.intT;
1.17 + fun mk_cert u k l = @{term "plus :: int \<Rightarrow> int \<Rightarrow> int"} $
1.18 + (@{term "times :: int \<Rightarrow> int \<Rightarrow> int"} $ u $ mk_number k) $
1.19 + mk_number l;
1.20 + fun prove ctxt prop = Goal.prove ctxt [] [] prop
1.21 + (K (ALLGOALS (full_simp_tac (HOL_basic_ss addsimps @{thms arithmetic_simps}))));
1.22 fun binary_proc proc ss ct =
1.23 (case Thm.term_of ct of
1.24 _ $ t $ u =>
1.25 @@ -529,16 +526,11 @@
1.26 | NONE => NONE)
1.27 | _ => NONE);
1.28 in
1.29 -
1.30 -fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
1.31 - if n = 0 then NONE
1.32 - else
1.33 - let val (k, l) = Integer.div_mod m n;
1.34 - fun mk_num x = HOLogic.mk_number HOLogic.intT x;
1.35 - in SOME (rule OF [prove ctxt (t == plus (mult u (mk_num k)) (mk_num l))])
1.36 - end);
1.37 -
1.38 -end;
1.39 + fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
1.40 + if n = 0 then NONE
1.41 + else let val (k, l) = Integer.div_mod m n;
1.42 + in SOME (rule OF [prove ctxt (Logic.mk_equals (t, mk_cert u k l))]) end);
1.43 +end
1.44 *}
1.45
1.46 simproc_setup binary_int_div ("number_of m div number_of n :: int") =
2.1 --- a/src/HOL/Tools/arith_data.ML Fri Mar 13 10:14:47 2009 -0700
2.2 +++ b/src/HOL/Tools/arith_data.ML Fri Mar 13 19:18:07 2009 +0100
2.3 @@ -10,6 +10,8 @@
2.4 val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
2.5 val prove_conv2: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
2.6 val simp_all_tac: thm list -> simpset -> tactic
2.7 + val simplify_meta_eq: thm list -> simpset -> thm -> thm
2.8 + val trans_tac: thm option -> tactic
2.9 val prep_simproc: string * string list * (theory -> simpset -> term -> thm option)
2.10 -> simproc
2.11 end;
2.12 @@ -33,6 +35,13 @@
2.13 let val ss0 = HOL_ss addsimps rules
2.14 in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
2.15
2.16 +fun simplify_meta_eq rules =
2.17 + let val ss0 = HOL_basic_ss addeqcongs [eq_cong2] addsimps rules
2.18 + in fn ss => simplify (Simplifier.inherit_context ss ss0) o mk_meta_eq end
2.19 +
2.20 +fun trans_tac NONE = all_tac
2.21 + | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
2.22 +
2.23 fun prep_simproc (name, pats, proc) = (*FIXME avoid the_context*)
2.24 Simplifier.simproc (the_context ()) name pats proc;
2.25
3.1 --- a/src/HOL/Tools/int_arith.ML Fri Mar 13 10:14:47 2009 -0700
3.2 +++ b/src/HOL/Tools/int_arith.ML Fri Mar 13 19:18:07 2009 +0100
3.3 @@ -29,41 +29,6 @@
3.4 (*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*)
3.5 val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym];
3.6
3.7 -(** New term ordering so that AC-rewriting brings numerals to the front **)
3.8 -
3.9 -(*Order integers by absolute value and then by sign. The standard integer
3.10 - ordering is not well-founded.*)
3.11 -fun num_ord (i,j) =
3.12 - (case int_ord (abs i, abs j) of
3.13 - EQUAL => int_ord (Int.sign i, Int.sign j)
3.14 - | ord => ord);
3.15 -
3.16 -(*This resembles TermOrd.term_ord, but it puts binary numerals before other
3.17 - non-atomic terms.*)
3.18 -local open Term
3.19 -in
3.20 -fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) =
3.21 - (case numterm_ord (t, u) of EQUAL => TermOrd.typ_ord (T, U) | ord => ord)
3.22 - | numterm_ord
3.23 - (Const(@{const_name Int.number_of}, _) $ v, Const(@{const_name Int.number_of}, _) $ w) =
3.24 - num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w)
3.25 - | numterm_ord (Const(@{const_name Int.number_of}, _) $ _, _) = LESS
3.26 - | numterm_ord (_, Const(@{const_name Int.number_of}, _) $ _) = GREATER
3.27 - | numterm_ord (t, u) =
3.28 - (case int_ord (size_of_term t, size_of_term u) of
3.29 - EQUAL =>
3.30 - let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
3.31 - (case TermOrd.hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)
3.32 - end
3.33 - | ord => ord)
3.34 -and numterms_ord (ts, us) = list_ord numterm_ord (ts, us)
3.35 -end;
3.36 -
3.37 -fun numtermless tu = (numterm_ord tu = LESS);
3.38 -
3.39 -(*Defined in this file, but perhaps needed only for Int_Numeral_Simprocs of type nat.*)
3.40 -val num_ss = HOL_ss settermless numtermless;
3.41 -
3.42
3.43 (** Utilities **)
3.44
3.45 @@ -177,6 +142,41 @@
3.46 in (mk_frac (p, 1), mk_divide (t', one_of T)) end;
3.47
3.48
3.49 +(** New term ordering so that AC-rewriting brings numerals to the front **)
3.50 +
3.51 +(*Order integers by absolute value and then by sign. The standard integer
3.52 + ordering is not well-founded.*)
3.53 +fun num_ord (i,j) =
3.54 + (case int_ord (abs i, abs j) of
3.55 + EQUAL => int_ord (Int.sign i, Int.sign j)
3.56 + | ord => ord);
3.57 +
3.58 +(*This resembles TermOrd.term_ord, but it puts binary numerals before other
3.59 + non-atomic terms.*)
3.60 +local open Term
3.61 +in
3.62 +fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) =
3.63 + (case numterm_ord (t, u) of EQUAL => TermOrd.typ_ord (T, U) | ord => ord)
3.64 + | numterm_ord
3.65 + (Const(@{const_name Int.number_of}, _) $ v, Const(@{const_name Int.number_of}, _) $ w) =
3.66 + num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w)
3.67 + | numterm_ord (Const(@{const_name Int.number_of}, _) $ _, _) = LESS
3.68 + | numterm_ord (_, Const(@{const_name Int.number_of}, _) $ _) = GREATER
3.69 + | numterm_ord (t, u) =
3.70 + (case int_ord (size_of_term t, size_of_term u) of
3.71 + EQUAL =>
3.72 + let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
3.73 + (case TermOrd.hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)
3.74 + end
3.75 + | ord => ord)
3.76 +and numterms_ord (ts, us) = list_ord numterm_ord (ts, us)
3.77 +end;
3.78 +
3.79 +fun numtermless tu = (numterm_ord tu = LESS);
3.80 +
3.81 +val num_ss = HOL_ss settermless numtermless;
3.82 +
3.83 +
3.84 (*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *)
3.85 val add_0s = thms "add_0s";
3.86 val mult_1s = thms "mult_1s" @ [thm"mult_1_left", thm"mult_1_right", thm"divide_1"];
3.87 @@ -218,14 +218,6 @@
3.88 val mult_minus_simps =
3.89 [@{thm mult_assoc}, @{thm minus_mult_left}, minus_mult_eq_1_to_2];
3.90
3.91 -(*Apply the given rewrite (if present) just once*)
3.92 -fun trans_tac NONE = all_tac
3.93 - | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
3.94 -
3.95 -fun simplify_meta_eq rules =
3.96 - let val ss0 = HOL_basic_ss addeqcongs [eq_cong2] addsimps rules
3.97 - in fn ss => simplify (Simplifier.inherit_context ss ss0) o mk_meta_eq end
3.98 -
3.99 structure CancelNumeralsCommon =
3.100 struct
3.101 val mk_sum = mk_sum
3.102 @@ -233,7 +225,7 @@
3.103 val mk_coeff = mk_coeff
3.104 val dest_coeff = dest_coeff 1
3.105 val find_first_coeff = find_first_coeff []
3.106 - val trans_tac = fn _ => trans_tac
3.107 + val trans_tac = K Arith_Data.trans_tac
3.108
3.109 val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
3.110 diff_simps @ minus_simps @ @{thms add_ac}
3.111 @@ -246,7 +238,7 @@
3.112
3.113 val numeral_simp_ss = HOL_ss addsimps add_0s @ simps
3.114 fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
3.115 - val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
3.116 + val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s)
3.117 end;
3.118
3.119
3.120 @@ -316,7 +308,7 @@
3.121 val dest_coeff = dest_coeff 1
3.122 val left_distrib = @{thm combine_common_factor} RS trans
3.123 val prove_conv = Arith_Data.prove_conv_nohyps
3.124 - val trans_tac = fn _ => trans_tac
3.125 + val trans_tac = K Arith_Data.trans_tac
3.126
3.127 val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
3.128 diff_simps @ minus_simps @ @{thms add_ac}
3.129 @@ -329,7 +321,7 @@
3.130
3.131 val numeral_simp_ss = HOL_ss addsimps add_0s @ simps
3.132 fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
3.133 - val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
3.134 + val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s)
3.135 end;
3.136
3.137 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
3.138 @@ -346,7 +338,7 @@
3.139 val dest_coeff = dest_fcoeff 1
3.140 val left_distrib = @{thm combine_common_factor} RS trans
3.141 val prove_conv = Arith_Data.prove_conv_nohyps
3.142 - val trans_tac = fn _ => trans_tac
3.143 + val trans_tac = K Arith_Data.trans_tac
3.144
3.145 val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
3.146 inverse_1s @ divide_simps @ diff_simps @ minus_simps @ @{thms add_ac}
3.147 @@ -359,7 +351,7 @@
3.148
3.149 val numeral_simp_ss = HOL_ss addsimps add_0s @ simps @ [@{thm add_frac_eq}]
3.150 fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
3.151 - val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s @ divide_1s)
3.152 + val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s @ divide_1s)
3.153 end;
3.154
3.155 structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData);
4.1 --- a/src/HOL/Tools/int_factor_simprocs.ML Fri Mar 13 10:14:47 2009 -0700
4.2 +++ b/src/HOL/Tools/int_factor_simprocs.ML Fri Mar 13 19:18:07 2009 +0100
4.3 @@ -29,7 +29,7 @@
4.4 struct
4.5 val mk_coeff = mk_coeff
4.6 val dest_coeff = dest_coeff 1
4.7 - val trans_tac = fn _ => trans_tac
4.8 + val trans_tac = K Arith_Data.trans_tac
4.9
4.10 val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s
4.11 val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps
4.12 @@ -41,7 +41,7 @@
4.13
4.14 val numeral_simp_ss = HOL_ss addsimps rel_number_of @ simps
4.15 fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
4.16 - val simplify_meta_eq = Int_Numeral_Simprocs.simplify_meta_eq
4.17 + val simplify_meta_eq = Arith_Data.simplify_meta_eq
4.18 [@{thm add_0}, @{thm add_0_right}, @{thm mult_zero_left},
4.19 @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right}];
4.20 end
4.21 @@ -215,7 +215,7 @@
4.22 handle TERM _ => find_first_t (t::past) u terms;
4.23
4.24 (** Final simplification for the CancelFactor simprocs **)
4.25 -val simplify_one = Int_Numeral_Simprocs.simplify_meta_eq
4.26 +val simplify_one = Arith_Data.simplify_meta_eq
4.27 [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_1_eq_1}];
4.28
4.29 fun cancel_simplify_meta_eq cancel_th ss th =
4.30 @@ -228,7 +228,7 @@
4.31 val mk_coeff = mk_coeff
4.32 val dest_coeff = dest_coeff
4.33 val find_first = find_first_t []
4.34 - val trans_tac = fn _ => trans_tac
4.35 + val trans_tac = K Arith_Data.trans_tac
4.36 val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
4.37 fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
4.38 end;
5.1 --- a/src/HOL/Tools/nat_simprocs.ML Fri Mar 13 10:14:47 2009 -0700
5.2 +++ b/src/HOL/Tools/nat_simprocs.ML Fri Mar 13 19:18:07 2009 +0100
5.3 @@ -41,8 +41,6 @@
5.4
5.5 (** Other simproc items **)
5.6
5.7 -val trans_tac = Int_Numeral_Simprocs.trans_tac;
5.8 -
5.9 val bin_simps =
5.10 [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym,
5.11 @{thm add_nat_number_of}, @{thm nat_number_of_add_left},
5.12 @@ -130,15 +128,11 @@
5.13 @{thm Suc_not_Zero}, @{thm le_0_eq}];
5.14
5.15 val simplify_meta_eq =
5.16 - Int_Numeral_Simprocs.simplify_meta_eq
5.17 + Arith_Data.simplify_meta_eq
5.18 ([@{thm nat_numeral_0_eq_0}, @{thm numeral_1_eq_Suc_0}, @{thm add_0}, @{thm add_0_right},
5.19 @{thm mult_0}, @{thm mult_0_right}, @{thm mult_1}, @{thm mult_1_right}] @ contra_rules);
5.20
5.21
5.22 -(*Like HOL_ss but with an ordering that brings numerals to the front
5.23 - under AC-rewriting.*)
5.24 -val num_ss = Int_Numeral_Simprocs.num_ss;
5.25 -
5.26 (*** Applying CancelNumeralsFun ***)
5.27
5.28 structure CancelNumeralsCommon =
5.29 @@ -148,11 +142,11 @@
5.30 val mk_coeff = mk_coeff
5.31 val dest_coeff = dest_coeff
5.32 val find_first_coeff = find_first_coeff []
5.33 - val trans_tac = fn _ => trans_tac
5.34 + val trans_tac = K Arith_Data.trans_tac
5.35
5.36 - val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
5.37 + val norm_ss1 = Int_Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @
5.38 [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
5.39 - val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
5.40 + val norm_ss2 = Int_Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
5.41 fun norm_tac ss =
5.42 ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
5.43 THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
5.44 @@ -237,10 +231,10 @@
5.45 val dest_coeff = dest_coeff
5.46 val left_distrib = @{thm left_add_mult_distrib} RS trans
5.47 val prove_conv = Arith_Data.prove_conv_nohyps
5.48 - val trans_tac = fn _ => trans_tac
5.49 + val trans_tac = K Arith_Data.trans_tac
5.50
5.51 - val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac}
5.52 - val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
5.53 + val norm_ss1 = Int_Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac}
5.54 + val norm_ss2 = Int_Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
5.55 fun norm_tac ss =
5.56 ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
5.57 THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
5.58 @@ -262,11 +256,11 @@
5.59 struct
5.60 val mk_coeff = mk_coeff
5.61 val dest_coeff = dest_coeff
5.62 - val trans_tac = fn _ => trans_tac
5.63 + val trans_tac = K Arith_Data.trans_tac
5.64
5.65 - val norm_ss1 = num_ss addsimps
5.66 + val norm_ss1 = Int_Numeral_Simprocs.num_ss addsimps
5.67 numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
5.68 - val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
5.69 + val norm_ss2 = Int_Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
5.70 fun norm_tac ss =
5.71 ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
5.72 THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
5.73 @@ -355,7 +349,7 @@
5.74 handle TERM _ => find_first_t (t::past) u terms;
5.75
5.76 (** Final simplification for the CancelFactor simprocs **)
5.77 -val simplify_one = Int_Numeral_Simprocs.simplify_meta_eq
5.78 +val simplify_one = Arith_Data.simplify_meta_eq
5.79 [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_1}, @{thm numeral_1_eq_Suc_0}];
5.80
5.81 fun cancel_simplify_meta_eq cancel_th ss th =
5.82 @@ -368,7 +362,7 @@
5.83 val mk_coeff = mk_coeff
5.84 val dest_coeff = dest_coeff
5.85 val find_first = find_first_t []
5.86 - val trans_tac = fn _ => trans_tac
5.87 + val trans_tac = K Arith_Data.trans_tac
5.88 val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
5.89 fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
5.90 end;
6.1 --- a/src/Pure/Isar/class_target.ML Fri Mar 13 10:14:47 2009 -0700
6.2 +++ b/src/Pure/Isar/class_target.ML Fri Mar 13 19:18:07 2009 +0100
6.3 @@ -43,8 +43,8 @@
6.4 val prove_instantiation_exit_result: (morphism -> 'a -> 'b)
6.5 -> (Proof.context -> 'b -> tactic) -> 'a -> local_theory -> 'b * theory
6.6 val conclude_instantiation: local_theory -> local_theory
6.7 - val instantiation_param: local_theory -> string -> string option
6.8 - val confirm_declaration: string -> local_theory -> local_theory
6.9 + val instantiation_param: local_theory -> binding -> string option
6.10 + val confirm_declaration: binding -> local_theory -> local_theory
6.11 val pretty_instantiation: local_theory -> Pretty.T
6.12 val type_name: string -> string
6.13
6.14 @@ -430,8 +430,8 @@
6.15
6.16 val instantiation_params = #params o get_instantiation;
6.17
6.18 -fun instantiation_param lthy v = instantiation_params lthy
6.19 - |> find_first (fn (_, (v', _)) => v = v')
6.20 +fun instantiation_param lthy b = instantiation_params lthy
6.21 + |> find_first (fn (_, (v, _)) => Binding.name_of b = v)
6.22 |> Option.map (fst o fst);
6.23
6.24
6.25 @@ -530,8 +530,8 @@
6.26 |> synchronize_inst_syntax
6.27 end;
6.28
6.29 -fun confirm_declaration c = (map_instantiation o apsnd)
6.30 - (filter_out (fn (_, (c', _)) => c' = c))
6.31 +fun confirm_declaration b = (map_instantiation o apsnd)
6.32 + (filter_out (fn (_, (c', _)) => c' = Binding.name_of b))
6.33 #> LocalTheory.target synchronize_inst_syntax
6.34
6.35 fun gen_instantiation_instance do_proof after_qed lthy =
7.1 --- a/src/Pure/Isar/overloading.ML Fri Mar 13 10:14:47 2009 -0700
7.2 +++ b/src/Pure/Isar/overloading.ML Fri Mar 13 19:18:07 2009 +0100
7.3 @@ -9,9 +9,9 @@
7.4 val init: (string * (string * typ) * bool) list -> theory -> local_theory
7.5 val conclude: local_theory -> local_theory
7.6 val declare: string * typ -> theory -> term * theory
7.7 - val confirm: string -> local_theory -> local_theory
7.8 - val define: bool -> string -> string * term -> theory -> thm * theory
7.9 - val operation: Proof.context -> string -> (string * bool) option
7.10 + val confirm: binding -> local_theory -> local_theory
7.11 + val define: bool -> binding -> string * term -> theory -> thm * theory
7.12 + val operation: Proof.context -> binding -> (string * bool) option
7.13 val pretty: Proof.context -> Pretty.T
7.14
7.15 type improvable_syntax
7.16 @@ -123,18 +123,19 @@
7.17 val get_overloading = OverloadingData.get o LocalTheory.target_of;
7.18 val map_overloading = LocalTheory.target o OverloadingData.map;
7.19
7.20 -fun operation lthy v = get_overloading lthy
7.21 - |> get_first (fn ((c, _), (v', checked)) => if v = v' then SOME (c, checked) else NONE);
7.22 +fun operation lthy b = get_overloading lthy
7.23 + |> get_first (fn ((c, _), (v, checked)) =>
7.24 + if Binding.name_of b = v then SOME (c, checked) else NONE);
7.25
7.26 -fun confirm c = map_overloading (filter_out (fn (_, (c', _)) => c' = c));
7.27 +fun confirm b = map_overloading (filter_out (fn (_, (c', _)) => c' = Binding.name_of b));
7.28
7.29
7.30 (* overloaded declarations and definitions *)
7.31
7.32 fun declare c_ty = pair (Const c_ty);
7.33
7.34 -fun define checked name (c, t) = Thm.add_def (not checked) true (Binding.name name,
7.35 - Logic.mk_equals (Const (c, Term.fastype_of t), t));
7.36 +fun define checked b (c, t) = Thm.add_def (not checked) true
7.37 + (b, Logic.mk_equals (Const (c, Term.fastype_of t), t));
7.38
7.39
7.40 (* target *)
8.1 --- a/src/Pure/Isar/theory_target.ML Fri Mar 13 10:14:47 2009 -0700
8.2 +++ b/src/Pure/Isar/theory_target.ML Fri Mar 13 19:18:07 2009 +0100
8.3 @@ -188,10 +188,7 @@
8.4 in
8.5 not (is_class andalso (similar_body orelse class_global)) ?
8.6 (Context.mapping_result
8.7 - (fn thy => thy
8.8 - |> Sign.no_base_names
8.9 - |> Sign.add_abbrev PrintMode.internal tags legacy_arg
8.10 - ||> Sign.restore_naming thy)
8.11 + (Sign.add_abbrev PrintMode.internal tags legacy_arg)
8.12 (ProofContext.add_abbrev PrintMode.internal tags arg)
8.13 #-> (fn (lhs' as Const (d, _), _) =>
8.14 similar_body ?
8.15 @@ -203,23 +200,22 @@
8.16
8.17 fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
8.18 let
8.19 - val c = Binding.qualified_name_of b;
8.20 val tags = LocalTheory.group_position_of lthy;
8.21 val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
8.22 val U = map #2 xs ---> T;
8.23 val (mx1, mx2, mx3) = fork_mixfix ta mx;
8.24 val declare_const =
8.25 - (case Class_Target.instantiation_param lthy c of
8.26 + (case Class_Target.instantiation_param lthy b of
8.27 SOME c' =>
8.28 if mx3 <> NoSyn then syntax_error c'
8.29 else LocalTheory.theory_result (AxClass.declare_overloaded (c', U))
8.30 - ##> Class_Target.confirm_declaration c
8.31 + ##> Class_Target.confirm_declaration b
8.32 | NONE =>
8.33 - (case Overloading.operation lthy c of
8.34 + (case Overloading.operation lthy b of
8.35 SOME (c', _) =>
8.36 if mx3 <> NoSyn then syntax_error c'
8.37 else LocalTheory.theory_result (Overloading.declare (c', U))
8.38 - ##> Overloading.confirm c
8.39 + ##> Overloading.confirm b
8.40 | NONE => LocalTheory.theory_result (Sign.declare_const tags ((b, U), mx3))));
8.41 val (const, lthy') = lthy |> declare_const;
8.42 val t = Term.list_comb (const, map Free xs);
8.43 @@ -282,17 +278,14 @@
8.44 val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def);
8.45
8.46 (*def*)
8.47 - val c = Binding.qualified_name_of b;
8.48 - val define_const =
8.49 - (case Overloading.operation lthy c of
8.50 - SOME (_, checked) =>
8.51 - (fn name => fn (Const (c, _), rhs) => Overloading.define checked name (c, rhs))
8.52 - | NONE =>
8.53 - if is_none (Class_Target.instantiation_param lthy c)
8.54 - then (fn name => fn eq => Thm.add_def false false (Binding.name name, Logic.mk_equals eq))
8.55 - else (fn name => fn (Const (c, _), rhs) => AxClass.define_overloaded name (c, rhs)));
8.56 val (global_def, lthy3) = lthy2
8.57 - |> LocalTheory.theory_result (define_const (Binding.name_of name') (lhs', rhs'));
8.58 + |> LocalTheory.theory_result (case Overloading.operation lthy b of
8.59 + SOME (_, checked) =>
8.60 + Overloading.define checked name' ((fst o dest_Const) lhs', rhs')
8.61 + | NONE =>
8.62 + if is_none (Class_Target.instantiation_param lthy b)
8.63 + then Thm.add_def false false (name', Logic.mk_equals (lhs', rhs'))
8.64 + else AxClass.define_overloaded name' ((fst o dest_Const) lhs', rhs'));
8.65 val def = LocalDefs.trans_terms lthy3
8.66 [(*c == global.c xs*) local_def,
8.67 (*global.c xs == rhs'*) global_def,
9.1 --- a/src/Pure/axclass.ML Fri Mar 13 10:14:47 2009 -0700
9.2 +++ b/src/Pure/axclass.ML Fri Mar 13 19:18:07 2009 +0100
9.3 @@ -27,7 +27,7 @@
9.4 val axiomatize_arity_cmd: xstring * string list * string -> theory -> theory
9.5 val instance_name: string * class -> string
9.6 val declare_overloaded: string * typ -> theory -> term * theory
9.7 - val define_overloaded: string -> string * term -> theory -> thm * theory
9.8 + val define_overloaded: binding -> string * term -> theory -> thm * theory
9.9 val inst_tyco_of: theory -> string * typ -> string option
9.10 val unoverload: theory -> thm -> thm
9.11 val overload: theory -> thm -> thm
9.12 @@ -383,16 +383,17 @@
9.13 #> pair (Const (c, T))))
9.14 end;
9.15
9.16 -fun define_overloaded name (c, t) thy =
9.17 +fun define_overloaded b (c, t) thy =
9.18 let
9.19 val T = Term.fastype_of t;
9.20 val SOME tyco = inst_tyco_of thy (c, T);
9.21 val (c', eq) = get_inst_param thy (c, tyco);
9.22 val prop = Logic.mk_equals (Const (c', T), t);
9.23 - val name' = Thm.def_name_optional (Long_Name.base_name c ^ "_" ^ Long_Name.base_name tyco) name;
9.24 + val b' = Thm.def_binding_optional
9.25 + (Binding.name (Long_Name.base_name c ^ "_" ^ Long_Name.base_name tyco)) b;
9.26 in
9.27 thy
9.28 - |> Thm.add_def false false (Binding.name name', prop)
9.29 + |> Thm.add_def false false (b', prop)
9.30 |>> (fn thm => Drule.transitive_thm OF [eq, thm])
9.31 end;
9.32