tuned
authorhaftmann
Sun May 06 21:49:23 2007 +0200 (2007-05-06)
changeset 22838466599ecf610
parent 22837 82cceaf768c8
child 22839 ede26eb5e549
tuned
src/HOL/FunDef.thy
src/HOL/Library/ExecutableRat.thy
src/HOL/Library/ExecutableSet.thy
src/HOL/Product_Type.thy
src/HOL/Sum_Type.thy
src/HOL/Tools/inductive_package.ML
src/HOL/arith_data.ML
src/HOL/simpdata.ML
src/Provers/splitter.ML
     1.1 --- a/src/HOL/FunDef.thy	Sun May 06 18:07:06 2007 +0200
     1.2 +++ b/src/HOL/FunDef.thy	Sun May 06 21:49:23 2007 +0200
     1.3 @@ -100,22 +100,21 @@
     1.4  
     1.5  setup FundefPackage.setup
     1.6  
     1.7 -lemma let_cong:
     1.8 -    "M = N ==> (!!x. x = N ==> f x = g x) ==> Let M f = Let N g"
     1.9 +lemma let_cong [fundef_cong]:
    1.10 +  "M = N \<Longrightarrow> (\<And>x. x = N \<Longrightarrow> f x = g x) \<Longrightarrow> Let M f = Let N g"
    1.11    unfolding Let_def by blast
    1.12  
    1.13  lemmas [fundef_cong] =
    1.14 -  let_cong if_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
    1.15 -
    1.16 +  if_cong image_cong INT_cong UN_cong
    1.17 +  bex_cong ball_cong imp_cong
    1.18  
    1.19  lemma split_cong [fundef_cong]:
    1.20 -  "\<lbrakk> \<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y; p = q \<rbrakk>
    1.21 +  "(\<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y) \<Longrightarrow> p = q
    1.22      \<Longrightarrow> split f p = split g q"
    1.23    by (auto simp: split_def)
    1.24  
    1.25  lemma comp_cong [fundef_cong]:
    1.26 -  "f (g x) = f' (g' x')
    1.27 -    ==>  (f o g) x = (f' o g') x'"
    1.28 +  "f (g x) = f' (g' x') \<Longrightarrow> (f o g) x = (f' o g') x'"
    1.29    unfolding o_apply .
    1.30  
    1.31  end
     2.1 --- a/src/HOL/Library/ExecutableRat.thy	Sun May 06 18:07:06 2007 +0200
     2.2 +++ b/src/HOL/Library/ExecutableRat.thy	Sun May 06 21:49:23 2007 +0200
     2.3 @@ -92,7 +92,7 @@
     2.4  subsubsection {* code lemmas *}
     2.5  
     2.6  lemma number_of_rat [code unfold]:
     2.7 -  "(number_of k \<Colon> rat) \<equiv> Fract k 1"
     2.8 +  "(number_of k \<Colon> rat) = Fract k 1"
     2.9    unfolding Fract_of_int_eq rat_number_of_def by simp
    2.10  
    2.11  lemma rat_minus [code func]:
     3.1 --- a/src/HOL/Library/ExecutableSet.thy	Sun May 06 18:07:06 2007 +0200
     3.2 +++ b/src/HOL/Library/ExecutableSet.thy	Sun May 06 21:49:23 2007 +0200
     3.3 @@ -347,7 +347,7 @@
     3.4    "insert"  ("{*insertl*}")
     3.5    "op Un"   ("{*unionl*}")
     3.6    "op Int"  ("{*intersect*}")
     3.7 -  "HOL.minus" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
     3.8 +  "minus" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
     3.9              ("{*flip subtract*}")
    3.10    "image"   ("{*map_distinct*}")
    3.11    "Union"   ("{*unions*}")
     4.1 --- a/src/HOL/Product_Type.thy	Sun May 06 18:07:06 2007 +0200
     4.2 +++ b/src/HOL/Product_Type.thy	Sun May 06 21:49:23 2007 +0200
     4.3 @@ -70,7 +70,7 @@
     4.4  global
     4.5  
     4.6  typedef (Prod)
     4.7 -  ('a, 'b) "*"    (infixr 20)
     4.8 +  ('a, 'b) "*"    (infixr "*" 20)
     4.9      = "{f. EX a b. f = Pair_Rep (a::'a) (b::'b)}"
    4.10  proof
    4.11    fix a b show "Pair_Rep a b : ?Prod"
     5.1 --- a/src/HOL/Sum_Type.thy	Sun May 06 18:07:06 2007 +0200
     5.2 +++ b/src/HOL/Sum_Type.thy	Sun May 06 21:49:23 2007 +0200
     5.3 @@ -23,7 +23,7 @@
     5.4  global
     5.5  
     5.6  typedef (Sum)
     5.7 -  ('a, 'b) "+"          (infixr 10)
     5.8 +  ('a, 'b) "+"          (infixr "+" 10)
     5.9      = "{f. (? a. f = Inl_Rep(a::'a)) | (? b. f = Inr_Rep(b::'b))}"
    5.10    by auto
    5.11  
     6.1 --- a/src/HOL/Tools/inductive_package.ML	Sun May 06 18:07:06 2007 +0200
     6.2 +++ b/src/HOL/Tools/inductive_package.ML	Sun May 06 21:49:23 2007 +0200
     6.3 @@ -397,7 +397,9 @@
     6.4  local
     6.5  
     6.6  (*delete needless equality assumptions*)
     6.7 -val refl_thin = prove_goal HOL.thy "!!P. a = a ==> P ==> P" (fn _ => [assume_tac 1]);
     6.8 +val refl_thin = Goal.prove_global HOL.thy [] []
     6.9 +  (Sign.read_prop HOL.thy "!!P. a = a ==> P ==> P")
    6.10 +  (fn _ => assume_tac 1);
    6.11  val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE];
    6.12  val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
    6.13  
     7.1 --- a/src/HOL/arith_data.ML	Sun May 06 18:07:06 2007 +0200
     7.2 +++ b/src/HOL/arith_data.ML	Sun May 06 21:49:23 2007 +0200
     7.3 @@ -51,8 +51,6 @@
     7.4        (HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
     7.5      (K (EVERY [expand_tac, norm_tac ss]))));
     7.6  
     7.7 -val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s"
     7.8 -  (fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]);
     7.9  
    7.10  (* rewriting *)
    7.11  
    7.12 @@ -60,9 +58,6 @@
    7.13    let val ss0 = HOL_ss addsimps rules
    7.14    in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
    7.15  
    7.16 -val add_rules = [thm "add_Suc", thm "add_Suc_right", thm "add_0", thm "add_0_right"];
    7.17 -val mult_rules = [thm "mult_Suc", thm "mult_Suc_right", thm "mult_0", thm "mult_0_right"];
    7.18 -
    7.19  fun prep_simproc (name, pats, proc) =
    7.20    Simplifier.simproc (the_context ()) name pats proc;
    7.21  
    7.22 @@ -88,13 +83,14 @@
    7.23    val mk_sum = mk_norm_sum;
    7.24    val dest_sum = dest_sum;
    7.25    val prove_conv = prove_conv;
    7.26 -  val norm_tac1 = simp_all_tac add_rules;
    7.27 +  val norm_tac1 = simp_all_tac [@{thm "add_Suc"}, @{thm "add_Suc_right"},
    7.28 +    @{thm "add_0"}, @{thm "add_0_right"}];
    7.29    val norm_tac2 = simp_all_tac @{thms add_ac};
    7.30    fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
    7.31  end;
    7.32  
    7.33  fun gen_uncancel_tac rule ct =
    7.34 -  rtac (instantiate' [] [NONE, SOME ct] (rule RS subst_equals)) 1;
    7.35 +  rtac (instantiate' [] [NONE, SOME ct] (rule RS @{thm subst_equals})) 1;
    7.36  
    7.37  (* nat eq *)
    7.38  
    7.39 @@ -103,7 +99,7 @@
    7.40    open Sum;
    7.41    val mk_bal = HOLogic.mk_eq;
    7.42    val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
    7.43 -  val uncancel_tac = gen_uncancel_tac (thm "nat_add_left_cancel");
    7.44 +  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel"};
    7.45  end);
    7.46  
    7.47  (* nat less *)
    7.48 @@ -113,7 +109,7 @@
    7.49    open Sum;
    7.50    val mk_bal = HOLogic.mk_binrel "Orderings.less";
    7.51    val dest_bal = HOLogic.dest_bin "Orderings.less" HOLogic.natT;
    7.52 -  val uncancel_tac = gen_uncancel_tac (thm "nat_add_left_cancel_less");
    7.53 +  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
    7.54  end);
    7.55  
    7.56  (* nat le *)
    7.57 @@ -123,7 +119,7 @@
    7.58    open Sum;
    7.59    val mk_bal = HOLogic.mk_binrel "Orderings.less_eq";
    7.60    val dest_bal = HOLogic.dest_bin "Orderings.less_eq" HOLogic.natT;
    7.61 -  val uncancel_tac = gen_uncancel_tac (thm "nat_add_left_cancel_le");
    7.62 +  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
    7.63  end);
    7.64  
    7.65  (* nat diff *)
    7.66 @@ -133,7 +129,7 @@
    7.67    open Sum;
    7.68    val mk_bal = HOLogic.mk_binop "HOL.minus";
    7.69    val dest_bal = HOLogic.dest_bin "HOL.minus" HOLogic.natT;
    7.70 -  val uncancel_tac = gen_uncancel_tac (thm "diff_cancel");
    7.71 +  val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"};
    7.72  end);
    7.73  
    7.74  (** prepare nat_cancel simprocs **)
    7.75 @@ -922,61 +918,31 @@
    7.76  val fast_arith_neq_limit   = Fast_Arith.fast_arith_neq_limit;
    7.77  val fast_arith_split_limit = LA_Data_Ref.fast_arith_split_limit;
    7.78  
    7.79 -local
    7.80 -
    7.81  (* reduce contradictory <= to False.
    7.82 -   Most of the work is done by the cancel tactics.
    7.83 -*)
    7.84 -val add_rules =
    7.85 - [thm "add_zero_left", thm "add_zero_right", thm "Zero_not_Suc", thm "Suc_not_Zero",
    7.86 -  thm "le_0_eq", thm "One_nat_def", thm "order_less_irrefl", thm "zero_neq_one",
    7.87 -  thm "zero_less_one", thm "zero_le_one", thm "zero_neq_one" RS not_sym, thm "not_one_le_zero",
    7.88 -  thm "not_one_less_zero"];
    7.89 -
    7.90 -val add_mono_thms_ordered_semiring = map (fn s => prove_goal (the_context ()) s
    7.91 - (fn prems => [cut_facts_tac prems 1,
    7.92 -               blast_tac (claset() addIs [@{thm add_mono}]) 1]))
    7.93 -["(i <= j) & (k <= l) ==> i + k <= j + (l::'a::pordered_ab_semigroup_add)",
    7.94 - "(i  = j) & (k <= l) ==> i + k <= j + (l::'a::pordered_ab_semigroup_add)",
    7.95 - "(i <= j) & (k  = l) ==> i + k <= j + (l::'a::pordered_ab_semigroup_add)",
    7.96 - "(i  = j) & (k  = l) ==> i + k  = j + (l::'a::pordered_ab_semigroup_add)"
    7.97 -];
    7.98 -
    7.99 -val mono_ss = simpset() addsimps
   7.100 -  [@{thm add_mono}, @{thm add_strict_mono},
   7.101 -     @{thm add_less_le_mono}, @{thm add_le_less_mono}];
   7.102 -
   7.103 -val add_mono_thms_ordered_field =
   7.104 -  map (fn s => prove_goal (the_context ()) s
   7.105 -                 (fn prems => [cut_facts_tac prems 1, asm_simp_tac mono_ss 1]))
   7.106 -    ["(i<j) & (k=l)   ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)",
   7.107 -     "(i=j) & (k<l)   ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)",
   7.108 -     "(i<j) & (k<=l)  ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)",
   7.109 -     "(i<=j) & (k<l)  ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)",
   7.110 -     "(i<j) & (k<l)   ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)"];
   7.111 -
   7.112 -in
   7.113 +   Most of the work is done by the cancel tactics. *)
   7.114  
   7.115  val init_lin_arith_data =
   7.116   Fast_Arith.setup #>
   7.117   Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
   7.118     {add_mono_thms = add_mono_thms @
   7.119 -    add_mono_thms_ordered_semiring @ add_mono_thms_ordered_field,
   7.120 +    @{thms add_mono_thms_ordered_semiring} @ @{thms add_mono_thms_ordered_field},
   7.121      mult_mono_thms = mult_mono_thms,
   7.122      inj_thms = inj_thms,
   7.123      lessD = lessD @ [thm "Suc_leI"],
   7.124      neqE = [@{thm linorder_neqE_nat},
   7.125        get_thm (theory "Ring_and_Field") (Name "linorder_neqE_ordered_idom")],
   7.126 -    simpset = HOL_basic_ss addsimps add_rules
   7.127 -                   addsimprocs [ab_group_add_cancel.sum_conv,
   7.128 -                                ab_group_add_cancel.rel_conv]
   7.129 -                   (*abel_cancel helps it work in abstract algebraic domains*)
   7.130 -                   addsimprocs nat_cancel_sums_add}) #>
   7.131 +    simpset = HOL_basic_ss
   7.132 +      addsimps [@{thm "add_zero_left"}, @{thm "add_zero_right"},
   7.133 +        @{thm "Zero_not_Suc"}, @{thm "Suc_not_Zero"}, @{thm "le_0_eq"}, @{thm "One_nat_def"},
   7.134 +        @{thm "order_less_irrefl"}, @{thm "zero_neq_one"}, @{thm "zero_less_one"},
   7.135 +        @{thm "zero_le_one"}, @{thm "zero_neq_one"} RS not_sym, @{thm "not_one_le_zero"},
   7.136 +        @{thm "not_one_less_zero"}]
   7.137 +      addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
   7.138 +       (*abel_cancel helps it work in abstract algebraic domains*)
   7.139 +      addsimprocs nat_cancel_sums_add}) #>
   7.140    ArithTheoryData.init #>
   7.141    arith_discrete "nat";
   7.142  
   7.143 -end;
   7.144 -
   7.145  val fast_nat_arith_simproc =
   7.146    Simplifier.simproc (the_context ()) "fast_nat_arith"
   7.147      ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] Fast_Arith.lin_arith_prover;
     8.1 --- a/src/HOL/simpdata.ML	Sun May 06 18:07:06 2007 +0200
     8.2 +++ b/src/HOL/simpdata.ML	Sun May 06 21:49:23 2007 +0200
     8.3 @@ -55,6 +55,7 @@
     8.4  (* Produce theorems of the form
     8.5    (P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y)
     8.6  *)
     8.7 +
     8.8  fun lift_meta_eq_to_obj_eq i st =
     8.9    let
    8.10      fun count_imp (Const ("HOL.simp_implies", _) $ P $ Q) = 1 + count_imp Q
    8.11 @@ -117,6 +118,7 @@
    8.12  
    8.13  val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
    8.14  
    8.15 +
    8.16  (*No premature instantiation of variables during simplification*)
    8.17  fun safe_solver_tac prems =
    8.18    (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN'
    8.19 @@ -227,7 +229,7 @@
    8.20  
    8.21  val let_simproc =
    8.22    Simplifier.simproc @{theory} "let_simp" ["Let x f"]
    8.23 -   (fn sg => fn ss => fn t =>
    8.24 +   (fn thy => fn ss => fn t =>
    8.25       let val ctxt = Simplifier.the_context ss;
    8.26           val ([t'], ctxt') = Variable.import_terms false [t] ctxt;
    8.27       in Option.map (hd o Variable.export ctxt' ctxt o single)
    8.28 @@ -238,9 +240,9 @@
    8.29           else
    8.30            let
    8.31               val n = case f of (Abs (x,_,_)) => x | _ => "x";
    8.32 -             val cx = cterm_of sg x;
    8.33 +             val cx = cterm_of thy x;
    8.34               val {T=xT,...} = rep_cterm cx;
    8.35 -             val cf = cterm_of sg f;
    8.36 +             val cf = cterm_of thy f;
    8.37               val fx_g = Simplifier.rewrite ss (Thm.capply cf cx);
    8.38               val (_$_$g) = prop_of fx_g;
    8.39               val g' = abstract_over (x,g);
    8.40 @@ -254,10 +256,10 @@
    8.41                 else let
    8.42                       val abs_g'= Abs (n,xT,g');
    8.43                       val g'x = abs_g'$x;
    8.44 -                     val g_g'x = symmetric (beta_conversion false (cterm_of sg g'x));
    8.45 +                     val g_g'x = symmetric (beta_conversion false (cterm_of thy g'x));
    8.46                       val rl = cterm_instantiate
    8.47 -                               [(f_Let_folded,cterm_of sg f),(x_Let_folded,cx),
    8.48 -                                (g_Let_folded,cterm_of sg abs_g')]
    8.49 +                               [(f_Let_folded,cterm_of thy f),(x_Let_folded,cx),
    8.50 +                                (g_Let_folded,cterm_of thy abs_g')]
    8.51                                 @{thm Let_folded};
    8.52                     in SOME (rl OF [transitive fx_g g_g'x])
    8.53                     end)
     9.1 --- a/src/Provers/splitter.ML	Sun May 06 18:07:06 2007 +0200
     9.2 +++ b/src/Provers/splitter.ML	Sun May 06 21:49:23 2007 +0200
     9.3 @@ -102,13 +102,10 @@
     9.4  
     9.5  val meta_iffD = Data.meta_eq_to_iff RS Data.iffD;  (* (P == Q) ==> Q ==> P *)
     9.6  
     9.7 -val lift =
     9.8 -  let val ct = Thm.read_cterm Pure.thy
     9.9 -           ("(!!x. (Q::('b::{})=>('c::{}))(x) == R(x)) ==> \
    9.10 -            \P(%x. Q(x)) == P(%x. R(x))::'a::{}",propT)
    9.11 -  in OldGoals.prove_goalw_cterm [] ct
    9.12 -     (fn [prem] => [rewtac prem, rtac reflexive_thm 1])
    9.13 -  end;
    9.14 +val lift = Goal.prove_global Pure.thy ["P", "Q", "R"]
    9.15 +  [Sign.read_prop Pure.thy "!!x :: 'b. Q(x) == R(x) :: 'c"]
    9.16 +  (Sign.read_prop Pure.thy "P(%x. Q(x)) == P(%x. R(x))")
    9.17 +  (fn [prem] => rewtac prem THEN rtac reflexive_thm 1)
    9.18  
    9.19  val trlift = lift RS transitive_thm;
    9.20  val _ $ (P $ _) $ _ = concl_of trlift;