# HG changeset patch
# User haftmann
# Date 1253626786 -7200
# Node ID 72e8608dce540de78180d34165ab82d13314fc82
# Parent  72979e93f919c0b09a505b4c7ab1957210be323c# Parent  46a20c74bd91e8857a71e9cfb5b8275f6f83737d
merged

diff -r 46a20c74bd91 -r 72e8608dce54 NEWS
--- a/NEWS	Mon Sep 21 16:02:00 2009 +0200
+++ b/NEWS	Tue Sep 22 15:39:46 2009 +0200
@@ -107,6 +107,10 @@
 also their lattice counterparts le_inf_iff and le_sup_iff have to be
 deleted to achieve the desired effect.
 
+* Rules inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no
+simp rules by default any longer.  The same applies to
+min_max.inf_absorb1 etc.!  INCOMPATIBILITY.
+
 * Power operations on relations and functions are now one dedicate
 constant "compow" with infix syntax "^^".  Power operations on
 multiplicative monoids retains syntax "^" and is now defined generic
diff -r 46a20c74bd91 -r 72e8608dce54 lib/Tools/usedir
--- a/lib/Tools/usedir	Mon Sep 21 16:02:00 2009 +0200
+++ b/lib/Tools/usedir	Tue Sep 22 15:39:46 2009 +0200
@@ -262,7 +262,7 @@
 else
   { echo "$ITEM FAILED";
     echo "(see also $LOG)";
-    echo; tail "$LOG"; echo; } >&2
+    echo; tail -n 20 "$LOG"; echo; } >&2
 fi
 
 exit "$RC"
diff -r 46a20c74bd91 -r 72e8608dce54 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Mon Sep 21 16:02:00 2009 +0200
+++ b/src/HOL/Complete_Lattice.thy	Tue Sep 22 15:39:46 2009 +0200
@@ -76,11 +76,11 @@
 
 lemma sup_bot [simp]:
   "x \<squnion> bot = x"
-  using bot_least [of x] by (simp add: sup_commute)
+  using bot_least [of x] by (simp add: sup_commute sup_absorb2)
 
 lemma inf_top [simp]:
   "x \<sqinter> top = x"
-  using top_greatest [of x] by (simp add: inf_commute)
+  using top_greatest [of x] by (simp add: inf_commute inf_absorb2)
 
 definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
   "SUPR A f = \<Squnion> (f ` A)"
diff -r 46a20c74bd91 -r 72e8608dce54 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Mon Sep 21 16:02:00 2009 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Tue Sep 22 15:39:46 2009 +0200
@@ -1904,7 +1904,7 @@
 	show "0 < real x * 2/3" using * by auto
 	show "real ?max + 1 \<le> real x * 2/3" using * up
 	  by (cases "0 < real x * real (lapprox_posrat prec 2 3) - 1",
-	      auto simp add: real_of_float_max)
+	      auto simp add: real_of_float_max min_max.sup_absorb1)
       qed
       finally have "real (?lb_horner (Float 1 -1)) + real (?lb_horner ?max)
 	\<le> ln (real x)"
diff -r 46a20c74bd91 -r 72e8608dce54 src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Mon Sep 21 16:02:00 2009 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Tue Sep 22 15:39:46 2009 +0200
@@ -512,7 +512,7 @@
   assumes g0: "numgcd t = 0"
   shows "Inum bs t = 0"
   using g0[simplified numgcd_def] 
-  by (induct t rule: numgcdh.induct, auto simp add: natabs0 maxcoeff_pos)
+  by (induct t rule: numgcdh.induct, auto simp add: natabs0 maxcoeff_pos min_max.sup_absorb2)
 
 lemma numgcdh_pos: assumes gp: "g \<ge> 0" shows "numgcdh t g \<ge> 0"
   using gp
diff -r 46a20c74bd91 -r 72e8608dce54 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Sep 21 16:02:00 2009 +0200
+++ b/src/HOL/Finite_Set.thy	Tue Sep 22 15:39:46 2009 +0200
@@ -2964,11 +2964,11 @@
 
 lemma dual_max:
   "ord.max (op \<ge>) = min"
-  by (auto simp add: ord.max_def_raw expand_fun_eq)
+  by (auto simp add: ord.max_def_raw min_def expand_fun_eq)
 
 lemma dual_min:
   "ord.min (op \<ge>) = max"
-  by (auto simp add: ord.min_def_raw expand_fun_eq)
+  by (auto simp add: ord.min_def_raw max_def expand_fun_eq)
 
 lemma strict_below_fold1_iff:
   assumes "finite A" and "A \<noteq> {}"
diff -r 46a20c74bd91 -r 72e8608dce54 src/HOL/Hoare_Parallel/Graph.thy
--- a/src/HOL/Hoare_Parallel/Graph.thy	Mon Sep 21 16:02:00 2009 +0200
+++ b/src/HOL/Hoare_Parallel/Graph.thy	Tue Sep 22 15:39:46 2009 +0200
@@ -187,6 +187,8 @@
 
 subsubsection{* Graph 3 *}
 
+declare min_max.inf_absorb1 [simp] min_max.inf_absorb2 [simp]
+
 lemma Graph3: 
   "\<lbrakk> T\<in>Reach E; R<length E \<rbrakk> \<Longrightarrow> Reach(E[R:=(fst(E!R),T)]) \<subseteq> Reach E"
 apply (unfold Reach_def)
@@ -307,6 +309,8 @@
 apply force
 done
 
+declare min_max.inf_absorb1 [simp del] min_max.inf_absorb2 [simp del]
+
 subsubsection {* Graph 5 *}
 
 lemma Graph5: 
diff -r 46a20c74bd91 -r 72e8608dce54 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Mon Sep 21 16:02:00 2009 +0200
+++ b/src/HOL/Lattices.thy	Tue Sep 22 15:39:46 2009 +0200
@@ -127,10 +127,10 @@
 lemma inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
   by (rule antisym) (auto intro: le_infI2)
 
-lemma inf_absorb1[simp]: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
+lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
   by (rule antisym) auto
 
-lemma inf_absorb2[simp]: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
+lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
   by (rule antisym) auto
 
 lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
@@ -155,10 +155,10 @@
 lemma sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
   by (rule antisym) (auto intro: le_supI2)
 
-lemma sup_absorb1[simp]: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
+lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
   by (rule antisym) auto
 
-lemma sup_absorb2[simp]: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
+lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
   by (rule antisym) auto
 
 lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
@@ -229,11 +229,11 @@
 
 lemma less_infI1:
   "a \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
-  by (auto simp add: less_le intro: le_infI1)
+  by (auto simp add: less_le inf_absorb1 intro: le_infI1)
 
 lemma less_infI2:
   "b \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
-  by (auto simp add: less_le intro: le_infI2)
+  by (auto simp add: less_le inf_absorb2 intro: le_infI2)
 
 end
 
diff -r 46a20c74bd91 -r 72e8608dce54 src/HOL/Lim.thy
--- a/src/HOL/Lim.thy	Mon Sep 21 16:02:00 2009 +0200
+++ b/src/HOL/Lim.thy	Tue Sep 22 15:39:46 2009 +0200
@@ -544,7 +544,7 @@
     case True thus ?thesis using `0 < s` by auto
   next
     case False hence "s / 2 \<ge> (x - b) / 2" by auto
-    hence "?x = (x + b) / 2" by(simp add:field_simps)
+    hence "?x = (x + b) / 2" by (simp add: field_simps min_max.inf_absorb2)
     thus ?thesis using `b < x` by auto
   qed
   hence "0 \<le> f ?x" using all_le `?x < x` by auto
diff -r 46a20c74bd91 -r 72e8608dce54 src/HOL/MicroJava/BV/Effect.thy
--- a/src/HOL/MicroJava/BV/Effect.thy	Mon Sep 21 16:02:00 2009 +0200
+++ b/src/HOL/MicroJava/BV/Effect.thy	Tue Sep 22 15:39:46 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/MicroJava/BV/Effect.thy
-    ID:         $Id$
     Author:     Gerwin Klein
     Copyright   2000 Technische Universitaet Muenchen
 *)
@@ -391,7 +390,7 @@
   with Pair 
   have "?app s \<Longrightarrow> ?P s" by (simp only:)
   moreover
-  have "?P s \<Longrightarrow> ?app s" by (unfold app_def) (clarsimp)
+  have "?P s \<Longrightarrow> ?app s" by (clarsimp simp add: min_max.inf_absorb2)
   ultimately
   show ?thesis by (rule iffI) 
 qed 
diff -r 46a20c74bd91 -r 72e8608dce54 src/HOL/MicroJava/BV/LBVSpec.thy
--- a/src/HOL/MicroJava/BV/LBVSpec.thy	Mon Sep 21 16:02:00 2009 +0200
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy	Tue Sep 22 15:39:46 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/MicroJava/BV/LBVSpec.thy
-    ID:         $Id$
     Author:     Gerwin Klein
     Copyright   1999 Technische Universitaet Muenchen
 *)
@@ -293,7 +292,7 @@
   shows "wtl (take (pc+1) is) c 0 s = wtc c pc (wtl (take pc is) c 0 s)"
 proof -
   from suc have "take (pc+1) is=(take pc is)@[is!pc]" by (simp add: take_Suc)
-  with suc wtl show ?thesis by (simp)
+  with suc wtl show ?thesis by (simp add: min_max.inf_absorb2)
 qed
 
 lemma (in lbv) wtl_all:
@@ -308,7 +307,7 @@
   with all have take: "?wtl (take pc is@i#r) \<noteq> \<top>" by simp 
   from pc have "is!pc = drop pc is ! 0" by simp
   with Cons have "is!pc = i" by simp
-  with take pc show ?thesis by (auto)
+  with take pc show ?thesis by (auto simp add: min_max.inf_absorb2)
 qed
 
 section "preserves-type"
diff -r 46a20c74bd91 -r 72e8608dce54 src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Mon Sep 21 16:02:00 2009 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Tue Sep 22 15:39:46 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/MicroJava/Comp/CorrCompTp.thy
-    ID:         $Id$
     Author:     Martin Strecker
 *)
 
@@ -1058,7 +1057,7 @@
 lemma bc_mt_corresp_New: "\<lbrakk>is_class cG cname \<rbrakk>
   \<Longrightarrow> bc_mt_corresp [New cname] (pushST [Class cname]) (ST, LT) cG rT mxr (Suc 0)"
 apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
-    max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
+    max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
 apply (intro strip)
 apply (rule conjI)
 apply (rule check_type_mono, assumption, simp)
@@ -1069,7 +1068,7 @@
   bc_mt_corresp [Pop] (popST (Suc 0)) (T # ST, LT) cG rT mxr (Suc 0)"
   apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
   apply (simp add: max_ssize_def ssize_sto_def max_of_list_def) 
-  apply (simp add: check_type_simps)
+  apply (simp add: check_type_simps min_max.sup_absorb1)
   apply clarify
   apply (rule_tac x="(length ST)" in exI)
   apply simp+
@@ -1092,7 +1091,7 @@
   \<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T]) sttp cG rT mxr (Suc 0)"
 apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+)
   apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
-              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
+              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
   apply (intro strip)
   apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
@@ -1111,7 +1110,7 @@
   \<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T']) sttp cG rT mxr (Suc 0)"
 apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+)
   apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
-              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
+              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
   apply (intro strip)
   apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
@@ -1127,7 +1126,7 @@
   \<Longrightarrow> bc_mt_corresp [Load i] 
          (\<lambda>(ST, LT). pushST [ok_val (LT ! i)] (ST, LT)) (ST, LT) cG rT mxr (Suc 0)"
 apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
-            max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
+            max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
   apply (intro strip)
   apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
@@ -1148,10 +1147,10 @@
 lemma bc_mt_corresp_Store_init: "\<lbrakk> i < length LT \<rbrakk>
   \<Longrightarrow> bc_mt_corresp [Store i] (storeST i T) (T # ST, LT) cG rT mxr (Suc 0)"
  apply (simp add: bc_mt_corresp_def storeST_def wt_instr_altern_def eff_def norm_eff_def)
-  apply (simp add: max_ssize_def  max_of_list_def )
+  apply (simp add: max_ssize_def  max_of_list_def)
   apply (simp add: ssize_sto_def)
   apply (intro strip)
-apply (simp add: check_type_simps)
+apply (simp add: check_type_simps min_max.sup_absorb1)
 apply clarify
 apply (rule conjI)
 apply (rule_tac x="(length ST)" in exI)
@@ -1159,14 +1158,13 @@
 done
 
 
-
 lemma bc_mt_corresp_Store: "\<lbrakk> i < length LT; cG  \<turnstile>  LT[i := OK T] <=l LT \<rbrakk>
   \<Longrightarrow> bc_mt_corresp [Store i] (popST (Suc 0)) (T # ST, LT) cG rT mxr (Suc 0)"
   apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
   apply (simp add: sup_state_conv)
   apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
  apply (intro strip)
-apply (simp add: check_type_simps)
+apply (simp add: check_type_simps min_max.sup_absorb1)
 apply clarify
 apply (rule_tac x="(length ST)" in exI)
 apply simp+
@@ -1176,7 +1174,7 @@
 lemma bc_mt_corresp_Dup: "
   bc_mt_corresp [Dup] dupST (T # ST, LT) cG rT mxr (Suc 0)"
  apply (simp add: bc_mt_corresp_def dupST_def wt_instr_altern_def
-             max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
+             max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
   apply (intro strip)
   apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
@@ -1189,7 +1187,7 @@
 lemma bc_mt_corresp_Dup_x1: "
   bc_mt_corresp [Dup_x1] dup_x1ST (T1 # T2 # ST, LT) cG rT mxr (Suc 0)"
   apply (simp add: bc_mt_corresp_def dup_x1ST_def wt_instr_altern_def
-              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
+              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
   apply (intro strip)
   apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
@@ -1206,7 +1204,7 @@
          (PrimT Integer # PrimT Integer # ST, LT) cG rT mxr (Suc 0)"
   apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def)
   apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
-  apply (simp add: check_type_simps)
+  apply (simp add: check_type_simps min_max.sup_absorb1)
   apply clarify
   apply (rule_tac x="Suc (length ST)" in exI)
   apply simp+
@@ -1249,7 +1247,7 @@
   apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
 
   apply (intro strip)
-apply (simp add: check_type_simps)
+apply (simp add: check_type_simps min_max.sup_absorb1)
 apply clarify
 apply (rule_tac x="Suc (length ST)" in exI)
 apply simp+
diff -r 46a20c74bd91 -r 72e8608dce54 src/HOL/Nominal/Examples/Crary.thy
--- a/src/HOL/Nominal/Examples/Crary.thy	Mon Sep 21 16:02:00 2009 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy	Tue Sep 22 15:39:46 2009 +0200
@@ -408,20 +408,7 @@
 
 declare trm.inject[simp del]
 
-lemma whn_eqvt[eqvt]:
-  fixes pi::"name prm"
-  assumes a: "t \<Down> t'"
-  shows "(pi\<bullet>t) \<Down> (pi\<bullet>t')"
-using a
-apply(induct)
-apply(rule QAN_Reduce)
-apply(rule whr_def.eqvt)
-apply(assumption)+
-apply(rule QAN_Normal)
-apply(auto)
-apply(drule_tac pi="rev pi" in whr_def.eqvt)
-apply(perm_simp)
-done
+equivariance whn_def
 
 lemma red_unicity : 
   assumes a: "x \<leadsto> a" 
@@ -631,6 +618,7 @@
 apply (force)
 apply (rule ty_cases)
 done
+
 termination by lexicographic_order
 
 lemma logical_monotonicity:
@@ -968,7 +956,7 @@
   then show  "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T" using main_lemma(1) val by simp
 qed
 
-text {* We leave soundness as an exercise - like in the book :-) \\ 
+text {* We leave soundness as an exercise - just like Crary in the ATS book :-) \\ 
  @{prop[mode=IfThen] "\<lbrakk>\<Gamma> \<turnstile> s \<Leftrightarrow> t : T; \<Gamma> \<turnstile> t : T; \<Gamma> \<turnstile> s : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T"} \\
  @{prop "\<lbrakk>\<Gamma> \<turnstile> s \<leftrightarrow> t : T; \<Gamma> \<turnstile> t : T; \<Gamma> \<turnstile> s : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T"} 
 *}
diff -r 46a20c74bd91 -r 72e8608dce54 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Mon Sep 21 16:02:00 2009 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Tue Sep 22 15:39:46 2009 +0200
@@ -2623,74 +2623,77 @@
   avoiding a finitely supported c and there is a permutation
   which 'translates' between both sets.
 *}
+
 lemma at_set_avoiding_aux:
   fixes Xs::"'a set"
   and   As::"'a set"
   assumes at: "at TYPE('a)"
-  and     a: "finite Xs"
   and     b: "Xs \<subseteq> As"
   and     c: "finite As"
   and     d: "finite ((supp c)::'a set)"
-  shows "\<exists>(Ys::'a set) (pi::'a prm). Ys\<sharp>*c \<and> Ys \<inter> As = {} \<and> (pi\<bullet>Xs=Ys) \<and> 
-          set pi \<subseteq> Xs \<times> Ys \<and> finite Ys"
-using a b c
-proof (induct)
-  case empty
-  have "({}::'a set)\<sharp>*c" by (simp add: fresh_star_def)
-  moreover
-  have "({}::'a set) \<inter> As = {}" by simp
-  moreover
-  have "([]::'a prm)\<bullet>{} = ({}::'a set)" 
-    by (rule pt1[OF pt_fun_inst, OF at_pt_inst[OF at], OF pt_bool_inst, OF at])
-  moreover
-  have "set ([]::'a prm) \<subseteq> {} \<times> {}" by simp
-  moreover 
-  have "finite ({}::'a set)" by simp
-  ultimately show ?case by blast
-next
-  case (insert x Xs)
-  then have ih: "\<exists>Ys pi. Ys\<sharp>*c \<and> Ys \<inter> As = {} \<and> pi\<bullet>Xs = Ys \<and> set pi \<subseteq> Xs \<times> Ys \<and> finite Ys" by simp
-  then obtain Ys pi where a1: "Ys\<sharp>*c" and a2: "Ys \<inter> As = {}" and a3: "pi\<bullet>Xs = Ys" and 
-                          a4: "set pi \<subseteq> Xs \<times> Ys" and a5: "finite Ys" by blast
-  have b: "x\<notin>Xs" by fact
-  have d1: "finite As" by fact
-  have d2: "finite Xs" by fact
-  have d3: "insert x Xs \<subseteq> As" by fact
-  have "\<exists>y::'a. y\<sharp>(c,x,Ys,As)" using d d1 a5
-    by (rule_tac at_exists_fresh'[OF at])
-       (simp add: supp_prod at_supp[OF at] at_fin_set_supp[OF at])
-  then obtain y::"'a" where  e: "y\<sharp>(c,x,Ys,As)" by blast
-  have "({y}\<union>Ys)\<sharp>*c" using a1 e by (simp add: fresh_star_def)
-  moreover
-  have "({y}\<union>Ys)\<inter>As = {}" using a2 d1 e by (simp add: fresh_prod at_fin_set_fresh[OF at])
-  moreover
-  have "(((pi\<bullet>x,y)#pi)\<bullet>(insert x Xs)) = {y}\<union>Ys"
-  proof -
-    have eq: "[(pi\<bullet>x,y)]\<bullet>Ys = Ys" 
+  shows "\<exists>(pi::'a prm). (pi\<bullet>Xs)\<sharp>*c \<and> (pi\<bullet>Xs) \<inter> As = {} \<and> set pi \<subseteq> Xs \<times> (pi\<bullet>Xs)"
+proof -
+  from b c have "finite Xs" by (simp add: finite_subset)
+  then show ?thesis using b 
+  proof (induct)
+    case empty
+    have "({}::'a set)\<sharp>*c" by (simp add: fresh_star_def)
+    moreover
+    have "({}::'a set) \<inter> As = {}" by simp
+    moreover
+    have "set ([]::'a prm) \<subseteq> {} \<times> {}" by simp
+    moreover
+    have "([]::'a prm)\<bullet>{} = ({}::'a set)" 
+      by (rule pt1[OF pt_fun_inst, OF at_pt_inst[OF at] pt_bool_inst at])
+    ultimately show ?case by simp
+  next
+    case (insert x Xs)
+    then have ih: "\<exists>pi. (pi\<bullet>Xs)\<sharp>*c \<and> (pi\<bullet>Xs) \<inter> As = {} \<and> set pi \<subseteq> Xs \<times> (pi\<bullet>Xs)" by simp
+    then obtain pi where a1: "(pi\<bullet>Xs)\<sharp>*c" and a2: "(pi\<bullet>Xs) \<inter> As = {}" and 
+      a4: "set pi \<subseteq> Xs \<times> (pi\<bullet>Xs)" by blast
+    have b: "x\<notin>Xs" by fact
+    have d1: "finite As" by fact
+    have d2: "finite Xs" by fact
+    have d3: "({x} \<union> Xs) \<subseteq> As" using insert(4) by simp
+    from d d1 d2
+    obtain y::"'a" where fr: "y\<sharp>(c,pi\<bullet>Xs,As)" 
+      apply(rule_tac at_exists_fresh[OF at, where x="(c,pi\<bullet>Xs,As)"])
+      apply(auto simp add: supp_prod at_supp[OF at] at_fin_set_supp[OF at]
+	pt_supp_finite_pi[OF pt_fun_inst[OF at_pt_inst[OF at] pt_bool_inst at] at])
+      done
+    have "({y}\<union>(pi\<bullet>Xs))\<sharp>*c" using a1 fr by (simp add: fresh_star_def)
+    moreover
+    have "({y}\<union>(pi\<bullet>Xs))\<inter>As = {}" using a2 d1 fr 
+      by (simp add: fresh_prod at_fin_set_fresh[OF at])
+    moreover
+    have "pi\<bullet>x=x" using a4 b a2 d3 
+      by (rule_tac at_prm_fresh2[OF at]) (auto)
+    then have "set ((pi\<bullet>x,y)#pi) \<subseteq> ({x} \<union> Xs) \<times> ({y}\<union>(pi\<bullet>Xs))" using a4 by auto
+    moreover
+    have "(((pi\<bullet>x,y)#pi)\<bullet>({x} \<union> Xs)) = {y}\<union>(pi\<bullet>Xs)"
     proof -
-      have "(pi\<bullet>x)\<sharp>Ys" using a3[symmetric] b d2 
-	by(simp add: pt_fresh_bij[OF pt_fun_inst, OF at_pt_inst[OF at], OF pt_bool_inst, OF at, OF at]
-                     at_fin_set_fresh[OF at])
-      moreover
-      have "y\<sharp>Ys" using e by simp
-      ultimately show "[(pi\<bullet>x,y)]\<bullet>Ys = Ys" 
-	by (simp add: pt_fresh_fresh[OF pt_fun_inst, OF at_pt_inst[OF at], OF pt_bool_inst, OF at, OF at])
+      have eq: "[(pi\<bullet>x,y)]\<bullet>(pi\<bullet>Xs) = (pi\<bullet>Xs)" 
+      proof -
+	have "(pi\<bullet>x)\<sharp>(pi\<bullet>Xs)" using b d2 
+	  by(simp add: pt_fresh_bij[OF pt_fun_inst, OF at_pt_inst[OF at], 
+            OF pt_bool_inst, OF at, OF at]
+            at_fin_set_fresh[OF at])
+	moreover
+	have "y\<sharp>(pi\<bullet>Xs)" using fr by simp
+	ultimately show "[(pi\<bullet>x,y)]\<bullet>(pi\<bullet>Xs) = (pi\<bullet>Xs)" 
+	  by (simp add: pt_fresh_fresh[OF pt_fun_inst, 
+            OF at_pt_inst[OF at], OF pt_bool_inst, OF at, OF at])
+      qed
+      have "(((pi\<bullet>x,y)#pi)\<bullet>({x}\<union>Xs)) = ([(pi\<bullet>x,y)]\<bullet>(pi\<bullet>({x}\<union>Xs)))"
+	by (simp add: pt2[symmetric, OF pt_fun_inst, OF at_pt_inst[OF at], 
+          OF pt_bool_inst, OF at])
+      also have "\<dots> = {y}\<union>([(pi\<bullet>x,y)]\<bullet>(pi\<bullet>Xs))" 
+	by (simp only: union_eqvt perm_set_eq[OF at_pt_inst[OF at], OF at] at_calc[OF at])(auto)
+      finally show "(((pi\<bullet>x,y)#pi)\<bullet>({x} \<union> Xs)) = {y}\<union>(pi\<bullet>Xs)" using eq by simp
     qed
-    have "(((pi\<bullet>x,y)#pi)\<bullet>({x}\<union>Xs)) = ([(pi\<bullet>x,y)]\<bullet>(pi\<bullet>({x}\<union>Xs)))"
-      by (simp add: pt2[symmetric, OF pt_fun_inst, OF at_pt_inst[OF at], OF pt_bool_inst, OF at])
-    also have "\<dots> = {y}\<union>([(pi\<bullet>x,y)]\<bullet>(pi\<bullet>Xs))" 
-      by (simp only: union_eqvt perm_set_eq[OF at_pt_inst[OF at], OF at] at_calc[OF at])(auto)
-    also have "\<dots> = {y}\<union>([(pi\<bullet>x,y)]\<bullet>Ys)" using a3 by simp
-    also have "\<dots> = {y}\<union>Ys" using eq by simp
-    finally show "(((pi\<bullet>x,y)#pi)\<bullet>(insert x Xs)) = {y}\<union>Ys" by auto
+    ultimately 
+    show ?case by (rule_tac x="(pi\<bullet>x,y)#pi" in exI) (auto)
   qed
-  moreover
-  have "pi\<bullet>x=x" using a4 b a2 a3 d3 by (rule_tac at_prm_fresh2[OF at]) (auto)
-  then have "set ((pi\<bullet>x,y)#pi) \<subseteq> (insert x Xs) \<times> ({y}\<union>Ys)" using a4 by auto
-  moreover 
-  have "finite ({y}\<union>Ys)" using a5 by simp
-  ultimately 
-  show ?case by blast
 qed
 
 lemma at_set_avoiding:
@@ -2698,10 +2701,10 @@
   assumes at: "at TYPE('a)"
   and     a: "finite Xs"
   and     b: "finite ((supp c)::'a set)"
-  obtains pi::"'a prm" where "(pi \<bullet> Xs) \<sharp>* c" and "set pi \<subseteq> Xs \<times> (pi \<bullet> Xs)"
-  using a b
-  by (frule_tac As="Xs" in at_set_avoiding_aux[OF at]) auto
- 
+  obtains pi::"'a prm" where "(pi\<bullet>Xs)\<sharp>*c" and "set pi \<subseteq> Xs \<times> (pi\<bullet>Xs)"
+using a b at_set_avoiding_aux[OF at, where Xs="Xs" and As="Xs" and c="c"]
+by (blast)
+
 section {* composition instances *}
 (* ============================= *)
 
diff -r 46a20c74bd91 -r 72e8608dce54 src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Mon Sep 21 16:02:00 2009 +0200
+++ b/src/HOL/OrderedGroup.thy	Tue Sep 22 15:39:46 2009 +0200
@@ -1075,17 +1075,16 @@
 lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)
 
 lemma pprt_eq_id [simp, noatp]: "0 \<le> x \<Longrightarrow> pprt x = x"
-by (simp add: pprt_def sup_aci)
-
+  by (simp add: pprt_def sup_aci sup_absorb1)
 
 lemma nprt_eq_id [simp, noatp]: "x \<le> 0 \<Longrightarrow> nprt x = x"
-by (simp add: nprt_def inf_aci)
+  by (simp add: nprt_def inf_aci inf_absorb1)
 
 lemma pprt_eq_0 [simp, noatp]: "x \<le> 0 \<Longrightarrow> pprt x = 0"
-by (simp add: pprt_def sup_aci)
+  by (simp add: pprt_def sup_aci sup_absorb2)
 
 lemma nprt_eq_0 [simp, noatp]: "0 \<le> x \<Longrightarrow> nprt x = 0"
-by (simp add: nprt_def inf_aci)
+  by (simp add: nprt_def inf_aci inf_absorb2)
 
 lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0"
 proof -
@@ -1119,7 +1118,7 @@
   "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
 proof
   assume "0 <= a + a"
-  hence a:"inf (a+a) 0 = 0" by (simp add: inf_commute)
+  hence a:"inf (a+a) 0 = 0" by (simp add: inf_commute inf_absorb1)
   have "(inf a 0)+(inf a 0) = inf (inf (a+a) 0) a" (is "?l=_")
     by (simp add: add_sup_inf_distribs inf_aci)
   hence "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute)
@@ -1135,7 +1134,7 @@
   assume assm: "a + a = 0"
   then have "a + a + - a = - a" by simp
   then have "a + (a + - a) = - a" by (simp only: add_assoc)
-  then have a: "- a = a" by simp (*FIXME tune proof*)
+  then have a: "- a = a" by simp
   show "a = 0" apply (rule antisym)
   apply (unfold neg_le_iff_le [symmetric, of a])
   unfolding a apply simp
@@ -1275,7 +1274,7 @@
 proof -
   note add_le_cancel_right [of a a "- a", symmetric, simplified]
   moreover note add_le_cancel_right [of "-a" a a, symmetric, simplified]
-  then show ?thesis by (auto simp: sup_max)
+  then show ?thesis by (auto simp: sup_max min_max.sup_absorb1 min_max.sup_absorb2)
 qed
 
 lemma abs_if_lattice:
diff -r 46a20c74bd91 -r 72e8608dce54 src/HOL/SMT/IsaMakefile
--- a/src/HOL/SMT/IsaMakefile	Mon Sep 21 16:02:00 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-
-## targets
-
-default: HOL-SMT
-images: HOL-SMT
-test: 
-
-all: images test
-
-
-## global settings
-
-SRC = $(ISABELLE_HOME)/src
-OUT = $(ISABELLE_OUTPUT)
-LOG = $(OUT)/log
-
-USEDIR = $(ISATOOL) usedir -v true 
-
-
-## HOL-SMT
-
-HOL-SMT: $(OUT)/HOL-SMT
-
-$(OUT)/HOL-SMT: $(OUT)/HOL-Word ROOT.ML SMT_Definitions.thy SMT.thy \
-  Tools/cancel_conj_disj.ML Tools/smt_normalize.ML Tools/smt_monomorph.ML \
-  Tools/smt_translate.ML Tools/smt_builtin.ML Tools/smtlib_interface.ML \
-  Tools/smt_solver.ML Tools/cvc3_solver.ML Tools/yices_solver.ML \
-  Tools/z3_interface.ML Tools/z3_solver.ML Tools/z3_model.ML \
-  Tools/z3_proof.ML Tools/z3_proof_rules.ML Tools/z3_proof_terms.ML
-	@$(USEDIR) -b HOL-Word HOL-SMT
-
-$(OUT)/HOL-Word:
-	@$(ISATOOL) make HOL-Word -C $(SRC)/HOL
-
-
-## clean
-
-clean:
-	@rm -f $(OUT)/HOL-SMT
diff -r 46a20c74bd91 -r 72e8608dce54 src/HOL/SMT/Tools/smt_solver.ML
--- a/src/HOL/SMT/Tools/smt_solver.ML	Mon Sep 21 16:02:00 2009 +0200
+++ b/src/HOL/SMT/Tools/smt_solver.ML	Tue Sep 22 15:39:46 2009 +0200
@@ -55,8 +55,6 @@
 
 exception SMT_COUNTEREXAMPLE of bool * term list
 
-val theory_of = Context.cases I ProofContext.theory_of
-
 
 datatype interface = Interface of {
   normalize: SMT_Normalize.config list,
@@ -177,12 +175,12 @@
 val solver_name_of = snd o SelectedSolver.get
 
 fun select_solver name gen =
-  if is_none (lookup_solver (theory_of gen) name)
+  if is_none (lookup_solver (Context.theory_of gen) name)
   then error ("SMT solver not registered: " ^ quote name)
   else SelectedSolver.map (K (serial (), name)) gen
 
 fun raw_solver_of gen =
-  (case lookup_solver (theory_of gen) (solver_name_of gen) of
+  (case lookup_solver (Context.theory_of gen) (solver_name_of gen) of
     NONE => error "No SMT solver selected"
   | SOME (s, _) => s)
 
@@ -228,11 +226,11 @@
 fun print_setup gen =
   let
     val t = string_of_int (Config.get_generic gen timeout)
-    val names = sort string_ord (all_solver_names_of (theory_of gen))
+    val names = sort string_ord (all_solver_names_of (Context.theory_of gen))
     val ns = if null names then [no_solver] else names
     val take_info = (fn (_, []) => NONE | info => SOME info)
     val infos =
-      theory_of gen
+      Context.theory_of gen
       |> Symtab.dest o Solvers.get
       |> map_filter (fn (n, (_, info)) => take_info (n, info gen))
       |> sort (prod_ord string_ord (K EQUAL))
diff -r 46a20c74bd91 -r 72e8608dce54 src/HOL/SMT/lib/scripts/remote_smt.pl
diff -r 46a20c74bd91 -r 72e8608dce54 src/HOL/UNITY/Simple/Common.thy
--- a/src/HOL/UNITY/Simple/Common.thy	Mon Sep 21 16:02:00 2009 +0200
+++ b/src/HOL/UNITY/Simple/Common.thy	Tue Sep 22 15:39:46 2009 +0200
@@ -66,7 +66,7 @@
 lemma "mk_total_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV)
        \<in> {m} co (maxfg m)"
 apply (simp add: mk_total_program_def) 
-apply (simp add: constrains_def maxfg_def gasc)
+apply (simp add: constrains_def maxfg_def gasc min_max.sup_absorb2)
 done
 
 (*This one is  t := t+1 if t <max (ftime t) (gtime t) *)
@@ -74,7 +74,7 @@
           (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }, UNIV)   
        \<in> {m} co (maxfg m)"
 apply (simp add: mk_total_program_def) 
-apply (simp add: constrains_def maxfg_def gasc)
+apply (simp add: constrains_def maxfg_def gasc min_max.sup_absorb2)
 done
 
 
diff -r 46a20c74bd91 -r 72e8608dce54 src/HOL/Word/BinBoolList.thy
--- a/src/HOL/Word/BinBoolList.thy	Mon Sep 21 16:02:00 2009 +0200
+++ b/src/HOL/Word/BinBoolList.thy	Tue Sep 22 15:39:46 2009 +0200
@@ -919,7 +919,7 @@
   apply (drule spec)
   apply (erule trans)
   apply (drule_tac x = "bin_cat y n a" in spec)
-  apply (simp add : bin_cat_assoc_sym)
+  apply (simp add : bin_cat_assoc_sym min_max.inf_absorb2)
   done
 
 lemma bin_rcat_bl:
diff -r 46a20c74bd91 -r 72e8608dce54 src/HOL/Word/BinGeneral.thy
--- a/src/HOL/Word/BinGeneral.thy	Mon Sep 21 16:02:00 2009 +0200
+++ b/src/HOL/Word/BinGeneral.thy	Tue Sep 22 15:39:46 2009 +0200
@@ -508,7 +508,7 @@
 lemma sbintrunc_sbintrunc_min [simp]:
   "sbintrunc m (sbintrunc n w) = sbintrunc (min m n) w"
   apply (rule bin_eqI)
-  apply (auto simp: nth_sbintr)
+  apply (auto simp: nth_sbintr min_max.inf_absorb1 min_max.inf_absorb2)
   done
 
 lemmas bintrunc_Pls = 
diff -r 46a20c74bd91 -r 72e8608dce54 src/HOL/Word/WordDefinition.thy
--- a/src/HOL/Word/WordDefinition.thy	Mon Sep 21 16:02:00 2009 +0200
+++ b/src/HOL/Word/WordDefinition.thy	Tue Sep 22 15:39:46 2009 +0200
@@ -381,14 +381,14 @@
   apply (unfold word_size)
   apply (subst word_ubin.norm_Rep [symmetric]) 
   apply (simp only: bintrunc_bintrunc_min word_size)
-  apply simp
+  apply (simp add: min_max.inf_absorb2)
   done
 
 lemma wi_bintr': 
   "wb = word_of_int bin ==> n >= size wb ==> 
     word_of_int (bintrunc n bin) = wb"
   unfolding word_size
-  by (clarsimp simp add : word_ubin.norm_eq_iff [symmetric])
+  by (clarsimp simp add: word_ubin.norm_eq_iff [symmetric] min_max.inf_absorb1)
 
 lemmas bintr_uint = bintr_uint' [unfolded word_size]
 lemmas wi_bintr = wi_bintr' [unfolded word_size]
diff -r 46a20c74bd91 -r 72e8608dce54 src/HOL/Word/WordShift.thy
--- a/src/HOL/Word/WordShift.thy	Mon Sep 21 16:02:00 2009 +0200
+++ b/src/HOL/Word/WordShift.thy	Tue Sep 22 15:39:46 2009 +0200
@@ -1017,8 +1017,8 @@
   (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) = 
   word_of_int (bin_cat w (size b) (uint b))"
   apply (unfold word_cat_def word_size) 
-  apply (clarsimp simp add : word_ubin.norm_eq_iff [symmetric]
-      word_ubin.eq_norm bintr_cat)
+  apply (clarsimp simp add: word_ubin.norm_eq_iff [symmetric]
+      word_ubin.eq_norm bintr_cat min_max.inf_absorb1)
   done
 
 lemma word_cat_split_alt:
diff -r 46a20c74bd91 -r 72e8608dce54 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Mon Sep 21 16:02:00 2009 +0200
+++ b/src/Pure/Isar/code.ML	Tue Sep 22 15:39:46 2009 +0200
@@ -505,9 +505,10 @@
 
 (*those following are permissive wrt. to overloaded constants!*)
 
+val head_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
 fun const_typ_eqn thy thm =
   let
-    val (c, ty) = (dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm;
+    val (c, ty) = head_eqn thm;
     val c' = AxClass.unoverload_const thy (c, ty);
   in (c', ty) end;
 
@@ -523,8 +524,8 @@
 
 fun same_typscheme thy thms =
   let
-    fun tvars_of t = rev (Term.add_tvars t []);
-    val vss = map (tvars_of o Thm.prop_of) thms;
+    fun tvars_of T = rev (Term.add_tvarsT T []);
+    val vss = map (tvars_of o snd o head_eqn) thms;
     fun inter_sorts vs =
       fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs [];
     val sorts = map_transpose inter_sorts vss;
@@ -547,7 +548,7 @@
 fun case_certificate thm =
   let
     val ((head, raw_case_expr), cases) = (apfst Logic.dest_equals
-      o apsnd Logic.dest_conjunctions o Logic.dest_implies o Thm.prop_of) thm;
+      o apsnd Logic.dest_conjunctions o Logic.dest_implies o Thm.plain_prop_of) thm;
     val _ = case head of Free _ => true
       | Var _ => true
       | _ => raise TERM ("case_cert", []);