# 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 \<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
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 \<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]:
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 \<Rightarrow> 'a set \<Rightarrow> 'a set"
+  "minus" :: "'a set \<Rightarrow> 'a set \<Rightarrow> '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<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;
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;