# HG changeset patch
# User paulson
# Date 1246542186 -3600
# Node ID b8784cb17a3583752a9716db6c579b1df7faae53
# Parent  1a7ade46061b8a02c87de7ccf0a9fcd9e073500e# Parent  a8e9ccfc427a26d3dd4070d711355d98ebab4225
merged

diff -r 1a7ade46061b -r b8784cb17a35 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Jul 02 15:37:22 2009 +0200
+++ b/src/HOL/Finite_Set.thy	Thu Jul 02 14:43:06 2009 +0100
@@ -528,7 +528,7 @@
 subsection {* A fold functional for finite sets *}
 
 text {* The intended behaviour is
-@{text "fold f z {x\<^isub>1, ..., x\<^isub>n} = f x\<^isub>1 (\<dots> (f x\<^isub>n z)\<dots>)"}
+@{text "fold f z {x1, ..., xn} = f x1 (\<dots> (f xn z)\<dots>)"}
 if @{text f} is ``left-commutative'':
 *}
 
@@ -1883,14 +1883,14 @@
   (if a:A then setprod f A / f a else setprod f A)"
 by (erule finite_induct) (auto simp add: insert_Diff_if)
 
-lemma setprod_inversef: "finite A ==>
-  ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==>
-  setprod (inverse \<circ> f) A = inverse (setprod f A)"
+lemma setprod_inversef: 
+  fixes f :: "'b \<Rightarrow> 'a::{field,division_by_zero}"
+  shows "finite A ==> setprod (inverse \<circ> f) A = inverse (setprod f A)"
 by (erule finite_induct) auto
 
 lemma setprod_dividef:
-   "[|finite A;
-      \<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|]
+  fixes f :: "'b \<Rightarrow> 'a::{field,division_by_zero}"
+  shows  "finite A
     ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
 apply (subgoal_tac
          "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
@@ -2725,16 +2725,16 @@
 begin
 
 definition
-  Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^bsub>fin\<^esub>_" [900] 900)
+  Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>fin_" [900] 900)
 where
   "Inf_fin = fold1 inf"
 
 definition
-  Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^bsub>fin\<^esub>_" [900] 900)
+  Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>fin_" [900] 900)
 where
   "Sup_fin = fold1 sup"
 
-lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<le> \<Squnion>\<^bsub>fin\<^esub>A"
+lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>finA \<le> \<Squnion>finA"
 apply(unfold Sup_fin_def Inf_fin_def)
 apply(subgoal_tac "EX a. a:A")
 prefer 2 apply blast
@@ -2745,13 +2745,13 @@
 done
 
 lemma sup_Inf_absorb [simp]:
-  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^bsub>fin\<^esub>A) = a"
+  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>finA) = a"
 apply(subst sup_commute)
 apply(simp add: Inf_fin_def sup_absorb2 fold1_belowI)
 done
 
 lemma inf_Sup_absorb [simp]:
-  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^bsub>fin\<^esub>A) = a"
+  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>finA) = a"
 by (simp add: Sup_fin_def inf_absorb1
   lower_semilattice.fold1_belowI [OF dual_lattice])
 
@@ -2763,7 +2763,7 @@
 lemma sup_Inf1_distrib:
   assumes "finite A"
     and "A \<noteq> {}"
-  shows "sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}"
+  shows "sup x (\<Sqinter>finA) = \<Sqinter>fin{sup x a|a. a \<in> A}"
 proof -
   interpret ab_semigroup_idem_mult inf
     by (rule ab_semigroup_idem_mult_inf)
@@ -2775,7 +2775,7 @@
 
 lemma sup_Inf2_distrib:
   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
-  shows "sup (\<Sqinter>\<^bsub>fin\<^esub>A) (\<Sqinter>\<^bsub>fin\<^esub>B) = \<Sqinter>\<^bsub>fin\<^esub>{sup a b|a b. a \<in> A \<and> b \<in> B}"
+  shows "sup (\<Sqinter>finA) (\<Sqinter>finB) = \<Sqinter>fin{sup a b|a b. a \<in> A \<and> b \<in> B}"
 using A proof (induct rule: finite_ne_induct)
   case singleton thus ?case
     by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def])
@@ -2792,13 +2792,13 @@
     thus ?thesis by(simp add: insert(1) B(1))
   qed
   have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
-  have "sup (\<Sqinter>\<^bsub>fin\<^esub>(insert x A)) (\<Sqinter>\<^bsub>fin\<^esub>B) = sup (inf x (\<Sqinter>\<^bsub>fin\<^esub>A)) (\<Sqinter>\<^bsub>fin\<^esub>B)"
+  have "sup (\<Sqinter>fin(insert x A)) (\<Sqinter>finB) = sup (inf x (\<Sqinter>finA)) (\<Sqinter>finB)"
     using insert by (simp add: fold1_insert_idem_def [OF Inf_fin_def])
-  also have "\<dots> = inf (sup x (\<Sqinter>\<^bsub>fin\<^esub>B)) (sup (\<Sqinter>\<^bsub>fin\<^esub>A) (\<Sqinter>\<^bsub>fin\<^esub>B))" by(rule sup_inf_distrib2)
-  also have "\<dots> = inf (\<Sqinter>\<^bsub>fin\<^esub>{sup x b|b. b \<in> B}) (\<Sqinter>\<^bsub>fin\<^esub>{sup a b|a b. a \<in> A \<and> b \<in> B})"
+  also have "\<dots> = inf (sup x (\<Sqinter>finB)) (sup (\<Sqinter>finA) (\<Sqinter>finB))" by(rule sup_inf_distrib2)
+  also have "\<dots> = inf (\<Sqinter>fin{sup x b|b. b \<in> B}) (\<Sqinter>fin{sup a b|a b. a \<in> A \<and> b \<in> B})"
     using insert by(simp add:sup_Inf1_distrib[OF B])
-  also have "\<dots> = \<Sqinter>\<^bsub>fin\<^esub>({sup x b |b. b \<in> B} \<union> {sup a b |a b. a \<in> A \<and> b \<in> B})"
-    (is "_ = \<Sqinter>\<^bsub>fin\<^esub>?M")
+  also have "\<dots> = \<Sqinter>fin({sup x b |b. b \<in> B} \<union> {sup a b |a b. a \<in> A \<and> b \<in> B})"
+    (is "_ = \<Sqinter>fin?M")
     using B insert
     by (simp add: Inf_fin_def fold1_Un2 [OF finB _ finAB ne])
   also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
@@ -2808,7 +2808,7 @@
 
 lemma inf_Sup1_distrib:
   assumes "finite A" and "A \<noteq> {}"
-  shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}"
+  shows "inf x (\<Squnion>finA) = \<Squnion>fin{inf x a|a. a \<in> A}"
 proof -
   interpret ab_semigroup_idem_mult sup
     by (rule ab_semigroup_idem_mult_sup)
@@ -2819,7 +2819,7 @@
 
 lemma inf_Sup2_distrib:
   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
-  shows "inf (\<Squnion>\<^bsub>fin\<^esub>A) (\<Squnion>\<^bsub>fin\<^esub>B) = \<Squnion>\<^bsub>fin\<^esub>{inf a b|a b. a \<in> A \<and> b \<in> B}"
+  shows "inf (\<Squnion>finA) (\<Squnion>finB) = \<Squnion>fin{inf a b|a b. a \<in> A \<and> b \<in> B}"
 using A proof (induct rule: finite_ne_induct)
   case singleton thus ?case
     by(simp add: inf_Sup1_distrib [OF B] fold1_singleton_def [OF Sup_fin_def])
@@ -2836,13 +2836,13 @@
   have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
   interpret ab_semigroup_idem_mult sup
     by (rule ab_semigroup_idem_mult_sup)
-  have "inf (\<Squnion>\<^bsub>fin\<^esub>(insert x A)) (\<Squnion>\<^bsub>fin\<^esub>B) = inf (sup x (\<Squnion>\<^bsub>fin\<^esub>A)) (\<Squnion>\<^bsub>fin\<^esub>B)"
+  have "inf (\<Squnion>fin(insert x A)) (\<Squnion>finB) = inf (sup x (\<Squnion>finA)) (\<Squnion>finB)"
     using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def])
-  also have "\<dots> = sup (inf x (\<Squnion>\<^bsub>fin\<^esub>B)) (inf (\<Squnion>\<^bsub>fin\<^esub>A) (\<Squnion>\<^bsub>fin\<^esub>B))" by(rule inf_sup_distrib2)
-  also have "\<dots> = sup (\<Squnion>\<^bsub>fin\<^esub>{inf x b|b. b \<in> B}) (\<Squnion>\<^bsub>fin\<^esub>{inf a b|a b. a \<in> A \<and> b \<in> B})"
+  also have "\<dots> = sup (inf x (\<Squnion>finB)) (inf (\<Squnion>finA) (\<Squnion>finB))" by(rule inf_sup_distrib2)
+  also have "\<dots> = sup (\<Squnion>fin{inf x b|b. b \<in> B}) (\<Squnion>fin{inf a b|a b. a \<in> A \<and> b \<in> B})"
     using insert by(simp add:inf_Sup1_distrib[OF B])
-  also have "\<dots> = \<Squnion>\<^bsub>fin\<^esub>({inf x b |b. b \<in> B} \<union> {inf a b |a b. a \<in> A \<and> b \<in> B})"
-    (is "_ = \<Squnion>\<^bsub>fin\<^esub>?M")
+  also have "\<dots> = \<Squnion>fin({inf x b |b. b \<in> B} \<union> {inf a b |a b. a \<in> A \<and> b \<in> B})"
+    (is "_ = \<Squnion>fin?M")
     using B insert
     by (simp add: Sup_fin_def fold1_Un2 [OF finB _ finAB ne])
   also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
@@ -2861,7 +2861,7 @@
 
 lemma Inf_fin_Inf:
   assumes "finite A" and "A \<noteq> {}"
-  shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
+  shows "\<Sqinter>finA = Inf A"
 proof -
     interpret ab_semigroup_idem_mult inf
     by (rule ab_semigroup_idem_mult_inf)
@@ -2872,7 +2872,7 @@
 
 lemma Sup_fin_Sup:
   assumes "finite A" and "A \<noteq> {}"
-  shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
+  shows "\<Squnion>finA = Sup A"
 proof -
   interpret ab_semigroup_idem_mult sup
     by (rule ab_semigroup_idem_mult_sup)
diff -r 1a7ade46061b -r b8784cb17a35 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Thu Jul 02 15:37:22 2009 +0200
+++ b/src/HOL/Tools/res_atp.ML	Thu Jul 02 14:43:06 2009 +0100
@@ -219,8 +219,7 @@
 	    handle ConstFree => false
     in    
 	case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ rhs) => 
-		   defs lhs rhs andalso
-		   (Output.debug (fn () => "Definition found: " ^ name ^ "_" ^ Int.toString n); true)
+		   defs lhs rhs 
 		 | _ => false
     end;
 
@@ -276,8 +275,7 @@
 fun relevance_filter max_new theory_const thy axioms goals = 
  if run_relevance_filter andalso pass_mark >= 0.1
  then
-  let val _ = Output.debug (fn () => "Start of relevance filtering");
-      val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms
+  let val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms
       val goal_const_tab = get_goal_consts_typs thy goals
       val _ = Output.debug (fn () => ("Initial constants: " ^
                                  space_implode ", " (Symtab.keys goal_const_tab)));
@@ -406,8 +404,6 @@
 fun check_named ("",th) = (warning ("No name for theorem " ^ Display.string_of_thm th); false)
   | check_named (_,th) = true;
 
-fun display_thm (name,th) = Output.debug (fn () => name ^ ": " ^ Display.string_of_thm th);
-
 (* get lemmas from claset, simpset, atpset and extra supplied rules *)
 fun get_clasimp_atp_lemmas ctxt =
   let val included_thms =
@@ -419,7 +415,6 @@
     let val atpset_thms =
             if include_atpset then ResAxioms.atpset_rules_of ctxt
             else []
-        val _ = (Output.debug (fn () => "ATP theorems: ");  app display_thm atpset_thms)
     in  atpset_thms  end
   in
     filter check_named included_thms
diff -r 1a7ade46061b -r b8784cb17a35 src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Thu Jul 02 15:37:22 2009 +0200
+++ b/src/HOL/Tools/res_clause.ML	Thu Jul 02 14:43:06 2009 +0100
@@ -381,8 +381,6 @@
   | iter_type_class_pairs thy tycons classes =
       let val cpairs = type_class_pairs thy tycons classes
           val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs))) \\ classes \\ HOLogic.typeS
-          val _ = if null newclasses then ()
-                  else Output.debug (fn _ => "New classes: " ^ space_implode ", " newclasses)
           val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
       in  (classes' union classes, cpairs' union cpairs)  end;
 
diff -r 1a7ade46061b -r b8784cb17a35 src/HOL/Tools/res_hol_clause.ML
--- a/src/HOL/Tools/res_hol_clause.ML	Thu Jul 02 15:37:22 2009 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML	Thu Jul 02 14:43:06 2009 +0100
@@ -419,13 +419,13 @@
         val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses
         fun needed c = valOf (Symtab.lookup ct c) > 0
         val IK = if needed "c_COMBI" orelse needed "c_COMBK"
-                 then (Output.debug (fn () => "Include combinator I K"); cnf_helper_thms thy [comb_I,comb_K])
+                 then cnf_helper_thms thy [comb_I,comb_K]
                  else []
         val BC = if needed "c_COMBB" orelse needed "c_COMBC"
-                 then (Output.debug (fn () => "Include combinator B C"); cnf_helper_thms thy [comb_B,comb_C])
+                 then cnf_helper_thms thy [comb_B,comb_C]
                  else []
         val S = if needed "c_COMBS"
-                then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms thy [comb_S])
+                then cnf_helper_thms thy [comb_S]
                 else []
         val other = cnf_helper_thms thy [fequal_imp_equal,equal_imp_fequal]
     in