--- a/src/HOL/FunDef.thy Sun May 06 18:07:06 2007 +0200
+++ b/src/HOL/FunDef.thy Sun May 06 21:49:23 2007 +0200
@@ -100,22 +100,21 @@
setup FundefPackage.setup
-lemma let_cong:
- "M = N ==> (!!x. x = N ==> f x = g x) ==> Let M f = Let N g"
+lemma let_cong [fundef_cong]:
+ "M = N \<Longrightarrow> (\<And>x. x = N \<Longrightarrow> f x = g x) \<Longrightarrow> Let M f = Let N g"
unfolding Let_def by blast
lemmas [fundef_cong] =
- let_cong if_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
-
+ if_cong image_cong INT_cong UN_cong
+ bex_cong ball_cong imp_cong
lemma split_cong [fundef_cong]:
- "\<lbrakk> \<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y; p = q \<rbrakk>
+ "(\<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y) \<Longrightarrow> p = q
\<Longrightarrow> split f p = split g q"
by (auto simp: split_def)
lemma comp_cong [fundef_cong]:
- "f (g x) = f' (g' x')
- ==> (f o g) x = (f' o g') x'"
+ "f (g x) = f' (g' x') \<Longrightarrow> (f o g) x = (f' o g') x'"
unfolding o_apply .
end
--- a/src/HOL/Library/ExecutableRat.thy Sun May 06 18:07:06 2007 +0200
+++ b/src/HOL/Library/ExecutableRat.thy Sun May 06 21:49:23 2007 +0200
@@ -92,7 +92,7 @@
subsubsection {* code lemmas *}
lemma number_of_rat [code unfold]:
- "(number_of k \<Colon> rat) \<equiv> Fract k 1"
+ "(number_of k \<Colon> rat) = Fract k 1"
unfolding Fract_of_int_eq rat_number_of_def by simp
lemma rat_minus [code func]:
--- a/src/HOL/Library/ExecutableSet.thy Sun May 06 18:07:06 2007 +0200
+++ b/src/HOL/Library/ExecutableSet.thy Sun May 06 21:49:23 2007 +0200
@@ -347,7 +347,7 @@
"insert" ("{*insertl*}")
"op Un" ("{*unionl*}")
"op Int" ("{*intersect*}")
- "HOL.minus" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
+ "minus" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
("{*flip subtract*}")
"image" ("{*map_distinct*}")
"Union" ("{*unions*}")
--- a/src/HOL/Product_Type.thy Sun May 06 18:07:06 2007 +0200
+++ b/src/HOL/Product_Type.thy Sun May 06 21:49:23 2007 +0200
@@ -70,7 +70,7 @@
global
typedef (Prod)
- ('a, 'b) "*" (infixr 20)
+ ('a, 'b) "*" (infixr "*" 20)
= "{f. EX a b. f = Pair_Rep (a::'a) (b::'b)}"
proof
fix a b show "Pair_Rep a b : ?Prod"
--- a/src/HOL/Sum_Type.thy Sun May 06 18:07:06 2007 +0200
+++ b/src/HOL/Sum_Type.thy Sun May 06 21:49:23 2007 +0200
@@ -23,7 +23,7 @@
global
typedef (Sum)
- ('a, 'b) "+" (infixr 10)
+ ('a, 'b) "+" (infixr "+" 10)
= "{f. (? a. f = Inl_Rep(a::'a)) | (? b. f = Inr_Rep(b::'b))}"
by auto
--- a/src/HOL/Tools/inductive_package.ML Sun May 06 18:07:06 2007 +0200
+++ b/src/HOL/Tools/inductive_package.ML Sun May 06 21:49:23 2007 +0200
@@ -397,7 +397,9 @@
local
(*delete needless equality assumptions*)
-val refl_thin = prove_goal HOL.thy "!!P. a = a ==> P ==> P" (fn _ => [assume_tac 1]);
+val refl_thin = Goal.prove_global HOL.thy [] []
+ (Sign.read_prop HOL.thy "!!P. a = a ==> P ==> P")
+ (fn _ => assume_tac 1);
val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE];
val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
--- a/src/HOL/arith_data.ML Sun May 06 18:07:06 2007 +0200
+++ b/src/HOL/arith_data.ML Sun May 06 21:49:23 2007 +0200
@@ -51,8 +51,6 @@
(HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
(K (EVERY [expand_tac, norm_tac ss]))));
-val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s"
- (fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]);
(* rewriting *)
@@ -60,9 +58,6 @@
let val ss0 = HOL_ss addsimps rules
in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
-val add_rules = [thm "add_Suc", thm "add_Suc_right", thm "add_0", thm "add_0_right"];
-val mult_rules = [thm "mult_Suc", thm "mult_Suc_right", thm "mult_0", thm "mult_0_right"];
-
fun prep_simproc (name, pats, proc) =
Simplifier.simproc (the_context ()) name pats proc;
@@ -88,13 +83,14 @@
val mk_sum = mk_norm_sum;
val dest_sum = dest_sum;
val prove_conv = prove_conv;
- val norm_tac1 = simp_all_tac add_rules;
+ val norm_tac1 = simp_all_tac [@{thm "add_Suc"}, @{thm "add_Suc_right"},
+ @{thm "add_0"}, @{thm "add_0_right"}];
val norm_tac2 = simp_all_tac @{thms add_ac};
fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
end;
fun gen_uncancel_tac rule ct =
- rtac (instantiate' [] [NONE, SOME ct] (rule RS subst_equals)) 1;
+ rtac (instantiate' [] [NONE, SOME ct] (rule RS @{thm subst_equals})) 1;
(* nat eq *)
@@ -103,7 +99,7 @@
open Sum;
val mk_bal = HOLogic.mk_eq;
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
- val uncancel_tac = gen_uncancel_tac (thm "nat_add_left_cancel");
+ val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel"};
end);
(* nat less *)
@@ -113,7 +109,7 @@
open Sum;
val mk_bal = HOLogic.mk_binrel "Orderings.less";
val dest_bal = HOLogic.dest_bin "Orderings.less" HOLogic.natT;
- val uncancel_tac = gen_uncancel_tac (thm "nat_add_left_cancel_less");
+ val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
end);
(* nat le *)
@@ -123,7 +119,7 @@
open Sum;
val mk_bal = HOLogic.mk_binrel "Orderings.less_eq";
val dest_bal = HOLogic.dest_bin "Orderings.less_eq" HOLogic.natT;
- val uncancel_tac = gen_uncancel_tac (thm "nat_add_left_cancel_le");
+ val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
end);
(* nat diff *)
@@ -133,7 +129,7 @@
open Sum;
val mk_bal = HOLogic.mk_binop "HOL.minus";
val dest_bal = HOLogic.dest_bin "HOL.minus" HOLogic.natT;
- val uncancel_tac = gen_uncancel_tac (thm "diff_cancel");
+ val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"};
end);
(** prepare nat_cancel simprocs **)
@@ -922,61 +918,31 @@
val fast_arith_neq_limit = Fast_Arith.fast_arith_neq_limit;
val fast_arith_split_limit = LA_Data_Ref.fast_arith_split_limit;
-local
-
(* reduce contradictory <= to False.
- Most of the work is done by the cancel tactics.
-*)
-val add_rules =
- [thm "add_zero_left", thm "add_zero_right", thm "Zero_not_Suc", thm "Suc_not_Zero",
- thm "le_0_eq", thm "One_nat_def", thm "order_less_irrefl", thm "zero_neq_one",
- thm "zero_less_one", thm "zero_le_one", thm "zero_neq_one" RS not_sym, thm "not_one_le_zero",
- thm "not_one_less_zero"];
-
-val add_mono_thms_ordered_semiring = map (fn s => prove_goal (the_context ()) s
- (fn prems => [cut_facts_tac prems 1,
- blast_tac (claset() addIs [@{thm add_mono}]) 1]))
-["(i <= j) & (k <= l) ==> i + k <= j + (l::'a::pordered_ab_semigroup_add)",
- "(i = j) & (k <= l) ==> i + k <= j + (l::'a::pordered_ab_semigroup_add)",
- "(i <= j) & (k = l) ==> i + k <= j + (l::'a::pordered_ab_semigroup_add)",
- "(i = j) & (k = l) ==> i + k = j + (l::'a::pordered_ab_semigroup_add)"
-];
-
-val mono_ss = simpset() addsimps
- [@{thm add_mono}, @{thm add_strict_mono},
- @{thm add_less_le_mono}, @{thm add_le_less_mono}];
-
-val add_mono_thms_ordered_field =
- map (fn s => prove_goal (the_context ()) s
- (fn prems => [cut_facts_tac prems 1, asm_simp_tac mono_ss 1]))
- ["(i<j) & (k=l) ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)",
- "(i=j) & (k<l) ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)",
- "(i<j) & (k<=l) ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)",
- "(i<=j) & (k<l) ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)",
- "(i<j) & (k<l) ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)"];
-
-in
+ Most of the work is done by the cancel tactics. *)
val init_lin_arith_data =
Fast_Arith.setup #>
Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
{add_mono_thms = add_mono_thms @
- add_mono_thms_ordered_semiring @ add_mono_thms_ordered_field,
+ @{thms add_mono_thms_ordered_semiring} @ @{thms add_mono_thms_ordered_field},
mult_mono_thms = mult_mono_thms,
inj_thms = inj_thms,
lessD = lessD @ [thm "Suc_leI"],
neqE = [@{thm linorder_neqE_nat},
get_thm (theory "Ring_and_Field") (Name "linorder_neqE_ordered_idom")],
- simpset = HOL_basic_ss addsimps add_rules
- addsimprocs [ab_group_add_cancel.sum_conv,
- ab_group_add_cancel.rel_conv]
- (*abel_cancel helps it work in abstract algebraic domains*)
- addsimprocs nat_cancel_sums_add}) #>
+ simpset = HOL_basic_ss
+ addsimps [@{thm "add_zero_left"}, @{thm "add_zero_right"},
+ @{thm "Zero_not_Suc"}, @{thm "Suc_not_Zero"}, @{thm "le_0_eq"}, @{thm "One_nat_def"},
+ @{thm "order_less_irrefl"}, @{thm "zero_neq_one"}, @{thm "zero_less_one"},
+ @{thm "zero_le_one"}, @{thm "zero_neq_one"} RS not_sym, @{thm "not_one_le_zero"},
+ @{thm "not_one_less_zero"}]
+ addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
+ (*abel_cancel helps it work in abstract algebraic domains*)
+ addsimprocs nat_cancel_sums_add}) #>
ArithTheoryData.init #>
arith_discrete "nat";
-end;
-
val fast_nat_arith_simproc =
Simplifier.simproc (the_context ()) "fast_nat_arith"
["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] Fast_Arith.lin_arith_prover;
--- a/src/HOL/simpdata.ML Sun May 06 18:07:06 2007 +0200
+++ b/src/HOL/simpdata.ML Sun May 06 21:49:23 2007 +0200
@@ -55,6 +55,7 @@
(* Produce theorems of the form
(P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y)
*)
+
fun lift_meta_eq_to_obj_eq i st =
let
fun count_imp (Const ("HOL.simp_implies", _) $ P $ Q) = 1 + count_imp Q
@@ -117,6 +118,7 @@
val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
+
(*No premature instantiation of variables during simplification*)
fun safe_solver_tac prems =
(fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN'
@@ -227,7 +229,7 @@
val let_simproc =
Simplifier.simproc @{theory} "let_simp" ["Let x f"]
- (fn sg => fn ss => fn t =>
+ (fn thy => fn ss => fn t =>
let val ctxt = Simplifier.the_context ss;
val ([t'], ctxt') = Variable.import_terms false [t] ctxt;
in Option.map (hd o Variable.export ctxt' ctxt o single)
@@ -238,9 +240,9 @@
else
let
val n = case f of (Abs (x,_,_)) => x | _ => "x";
- val cx = cterm_of sg x;
+ val cx = cterm_of thy x;
val {T=xT,...} = rep_cterm cx;
- val cf = cterm_of sg f;
+ val cf = cterm_of thy f;
val fx_g = Simplifier.rewrite ss (Thm.capply cf cx);
val (_$_$g) = prop_of fx_g;
val g' = abstract_over (x,g);
@@ -254,10 +256,10 @@
else let
val abs_g'= Abs (n,xT,g');
val g'x = abs_g'$x;
- val g_g'x = symmetric (beta_conversion false (cterm_of sg g'x));
+ val g_g'x = symmetric (beta_conversion false (cterm_of thy g'x));
val rl = cterm_instantiate
- [(f_Let_folded,cterm_of sg f),(x_Let_folded,cx),
- (g_Let_folded,cterm_of sg abs_g')]
+ [(f_Let_folded,cterm_of thy f),(x_Let_folded,cx),
+ (g_Let_folded,cterm_of thy abs_g')]
@{thm Let_folded};
in SOME (rl OF [transitive fx_g g_g'x])
end)
--- a/src/Provers/splitter.ML Sun May 06 18:07:06 2007 +0200
+++ b/src/Provers/splitter.ML Sun May 06 21:49:23 2007 +0200
@@ -102,13 +102,10 @@
val meta_iffD = Data.meta_eq_to_iff RS Data.iffD; (* (P == Q) ==> Q ==> P *)
-val lift =
- let val ct = Thm.read_cterm Pure.thy
- ("(!!x. (Q::('b::{})=>('c::{}))(x) == R(x)) ==> \
- \P(%x. Q(x)) == P(%x. R(x))::'a::{}",propT)
- in OldGoals.prove_goalw_cterm [] ct
- (fn [prem] => [rewtac prem, rtac reflexive_thm 1])
- end;
+val lift = Goal.prove_global Pure.thy ["P", "Q", "R"]
+ [Sign.read_prop Pure.thy "!!x :: 'b. Q(x) == R(x) :: 'c"]
+ (Sign.read_prop Pure.thy "P(%x. Q(x)) == P(%x. R(x))")
+ (fn [prem] => rewtac prem THEN rtac reflexive_thm 1)
val trlift = lift RS transitive_thm;
val _ $ (P $ _) $ _ = concl_of trlift;