# HG changeset patch # User haftmann # Date 1178480963 -7200 # Node ID 466599ecf610e96cb6c4de4db066528f6d8bac82 # Parent 82cceaf768c8040880caf785423a4f817dd27806 tuned diff -r 82cceaf768c8 -r 466599ecf610 src/HOL/FunDef.thy --- 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 \ (\x. x = N \ f x = g x) \ 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]: - "\ \x y. (x, y) = q \ f x y = g x y; p = q \ + "(\x y. (x, y) = q \ f x y = g x y) \ p = q \ 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') \ (f o g) x = (f' o g') x'" unfolding o_apply . end diff -r 82cceaf768c8 -r 466599ecf610 src/HOL/Library/ExecutableRat.thy --- 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 \ rat) \ Fract k 1" + "(number_of k \ rat) = Fract k 1" unfolding Fract_of_int_eq rat_number_of_def by simp lemma rat_minus [code func]: diff -r 82cceaf768c8 -r 466599ecf610 src/HOL/Library/ExecutableSet.thy --- 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 \ 'a set \ 'a set" + "minus" :: "'a set \ 'a set \ 'a set" ("{*flip subtract*}") "image" ("{*map_distinct*}") "Union" ("{*unions*}") diff -r 82cceaf768c8 -r 466599ecf610 src/HOL/Product_Type.thy --- 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" diff -r 82cceaf768c8 -r 466599ecf610 src/HOL/Sum_Type.thy --- 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 diff -r 82cceaf768c8 -r 466599ecf610 src/HOL/Tools/inductive_package.ML --- 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; diff -r 82cceaf768c8 -r 466599ecf610 src/HOL/arith_data.ML --- 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 i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)", - "(i=j) & (k i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)", - "(i i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)", - "(i<=j) & (k i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)", - "(i 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; diff -r 82cceaf768c8 -r 466599ecf610 src/HOL/simpdata.ML --- 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) diff -r 82cceaf768c8 -r 466599ecf610 src/Provers/splitter.ML --- 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;