# HG changeset patch
# User wenzelm
# Date 1030455633 -7200
# Node ID f506eb568121f05de5e09c46a84d35c56953b5fb
# Parent  825249a031c317e32d842708ef008efb75d09e3b
avoid duplicate fact bindings;

diff -r 825249a031c3 -r f506eb568121 src/HOL/Isar_examples/ExprCompiler.thy
--- a/src/HOL/Isar_examples/ExprCompiler.thy	Tue Aug 27 15:39:39 2002 +0200
+++ b/src/HOL/Isar_examples/ExprCompiler.thy	Tue Aug 27 15:40:33 2002 +0200
@@ -197,7 +197,7 @@
   qed
 qed
 
-theorem correctness: "execute (compile e) env = eval e env"
+theorem correctness': "execute (compile e) env = eval e env"
 proof -
   have exec_compile:
     "ALL stack. exec (compile e) stack env = eval e env # stack"
diff -r 825249a031c3 -r f506eb568121 src/HOL/MiniML/Type.thy
--- a/src/HOL/MiniML/Type.thy	Tue Aug 27 15:39:39 2002 +0200
+++ b/src/HOL/MiniML/Type.thy	Tue Aug 27 15:40:33 2002 +0200
@@ -41,16 +41,16 @@
 consts
   free_tv :: ['a::type_struct] => nat set
 
-primrec
+primrec (free_tv_typ)
   free_tv_TVar    "free_tv (TVar m) = {m}"
   free_tv_Fun     "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
 
-primrec
+primrec (free_tv_type_scheme)
   "free_tv (FVar m) = {m}"
   "free_tv (BVar m) = {}"
   "free_tv (S1 =-> S2) = (free_tv S1) Un (free_tv S2)"
 
-primrec
+primrec (free_tv_list)
   "free_tv [] = {}"
   "free_tv (x#l) = (free_tv x) Un (free_tv l)"
 
@@ -59,12 +59,12 @@
 consts
   free_tv_ML :: ['a::type_struct] => nat list
 
-primrec
+primrec (free_tv_ML_type_scheme)
   "free_tv_ML (FVar m) = [m]"
   "free_tv_ML (BVar m) = []"
   "free_tv_ML (S1 =-> S2) = (free_tv_ML S1) @ (free_tv_ML S2)"
 
-primrec
+primrec (free_tv_ML_list)
   "free_tv_ML [] = []"
   "free_tv_ML (x#l) = (free_tv_ML x) @ (free_tv_ML l)"
 
@@ -82,12 +82,12 @@
 consts
   bound_tv :: ['a::type_struct] => nat set
 
-primrec
+primrec (bound_tv_type_scheme)
   "bound_tv (FVar m) = {}"
   "bound_tv (BVar m) = {m}"
   "bound_tv (S1 =-> S2) = (bound_tv S1) Un (bound_tv S2)"
 
-primrec
+primrec (bound_tv_list)
   "bound_tv [] = {}"
   "bound_tv (x#l) = (bound_tv x) Un (bound_tv l)"
 
@@ -97,7 +97,7 @@
 consts
   min_new_bound_tv :: 'a::type_struct => nat
 
-primrec
+primrec (min_new_bound_tv_type_scheme)
   "min_new_bound_tv (FVar n) = 0"
   "min_new_bound_tv (BVar n) = Suc n"
   "min_new_bound_tv (sch1 =-> sch2) = max (min_new_bound_tv sch1) (min_new_bound_tv sch2)"
@@ -118,11 +118,11 @@
 consts
   app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
 
-primrec
+primrec (app_subst_typ)
   app_subst_TVar "$ S (TVar n) = S n" 
   app_subst_Fun  "$ S (t1 -> t2) = ($ S t1) -> ($ S t2)" 
 
-primrec
+primrec (app_subst_type_scheme)
   "$ S (FVar n) = mk_scheme (S n)"
   "$ S (BVar n) = (BVar n)"
   "$ S (sch1 =-> sch2) = ($ S sch1) =-> ($ S sch2)"
diff -r 825249a031c3 -r f506eb568121 src/HOL/W0/W0.thy
--- a/src/HOL/W0/W0.thy	Tue Aug 27 15:39:39 2002 +0200
+++ b/src/HOL/W0/W0.thy	Tue Aug 27 15:40:33 2002 +0200
@@ -64,7 +64,7 @@
 consts
   app_subst :: "subst \<Rightarrow> 'a::type_struct \<Rightarrow> 'a::type_struct"    ("$")
   -- {* extension of substitution to type structures *}
-primrec
+primrec (app_subst_typ)
   app_subst_TVar: "$s (TVar n) = s n"
   app_subst_Fun: "$s (t1 -> t2) = $s t1 -> $s t2"
 
@@ -75,11 +75,11 @@
   free_tv :: "'a::type_struct \<Rightarrow> nat set"
   -- {* @{text "free_tv s"}: the type variables occuring freely in the type structure @{text s} *}
 
-primrec
+primrec (free_tv_typ)
   "free_tv (TVar m) = {m}"
   "free_tv (t1 -> t2) = free_tv t1 \<union> free_tv t2"
 
-primrec
+primrec (free_tv_list)
   "free_tv [] = {}"
   "free_tv (x # xs) = free_tv x \<union> free_tv xs"
 
diff -r 825249a031c3 -r f506eb568121 src/ZF/Integ/IntDiv.thy
--- a/src/ZF/Integ/IntDiv.thy	Tue Aug 27 15:39:39 2002 +0200
+++ b/src/ZF/Integ/IntDiv.thy	Tue Aug 27 15:40:33 2002 +0200
@@ -956,7 +956,7 @@
 
 subsection{* division of a number by itself *}
 
-lemma lemma1: "[| #0 $< a; a = r $+ a$*q; r $< a |] ==> #1 $<= q"
+lemma self_quotient_aux1: "[| #0 $< a; a = r $+ a$*q; r $< a |] ==> #1 $<= q"
 apply (subgoal_tac "#0 $< a$*q")
 apply (cut_tac w = "#0" and z = "q" in add1_zle_iff)
 apply (simp add: int_0_less_mult_iff)
@@ -967,7 +967,7 @@
 apply (simp add: zcompare_rls)
 done
 
-lemma lemma2: "[| #0 $< a; a = r $+ a$*q; #0 $<= r |] ==> q $<= #1"
+lemma self_quotient_aux2: "[| #0 $< a; a = r $+ a$*q; #0 $<= r |] ==> q $<= #1"
 apply (subgoal_tac "#0 $<= a$* (#1$-q)")
  apply (simp add: int_0_le_mult_iff zcompare_rls)
  apply (blast dest: zle_zless_trans)
@@ -984,11 +984,12 @@
 apply auto
 prefer 4 apply (blast dest: zless_trans)
 apply (blast dest: zless_trans)
-apply (rule_tac [3] a = "$-a" and r = "$-r" in lemma1)
-apply (rule_tac a = "$-a" and r = "$-r" in lemma2)
+apply (rule_tac [3] a = "$-a" and r = "$-r" in self_quotient_aux1)
+apply (rule_tac a = "$-a" and r = "$-r" in self_quotient_aux2)
 apply (rule_tac [6] zminus_equation [THEN iffD1])
 apply (rule_tac [2] zminus_equation [THEN iffD1])
-apply (force intro: lemma1 lemma2 simp add: zadd_commute zmult_zminus)+
+apply (force intro: self_quotient_aux1 self_quotient_aux2
+  simp add: zadd_commute zmult_zminus)+
 done
 
 lemma self_remainder:
@@ -1481,7 +1482,7 @@
 
 (** first, four lemmas to bound the remainder for the cases b<0 and b>0 **)
 
-lemma lemma1:
+lemma zdiv_zmult2_aux1:
      "[| #0 $< c;  b $< r;  r $<= #0 |] ==> b$*c $< b$*(q zmod c) $+ r"
 apply (subgoal_tac "b $* (c $- q zmod c) $< r $* #1")
 apply (simp add: zdiff_zmult_distrib2 zadd_commute zcompare_rls)
@@ -1492,7 +1493,7 @@
 apply (blast intro: zless_imp_zle dest: zless_zle_trans)
 done
 
-lemma lemma2:
+lemma zdiv_zmult2_aux2:
      "[| #0 $< c;   b $< r;  r $<= #0 |] ==> b $* (q zmod c) $+ r $<= #0"
 apply (subgoal_tac "b $* (q zmod c) $<= #0")
  prefer 2
@@ -1504,7 +1505,7 @@
 apply (simp add: zadd_commute)
 done
 
-lemma lemma3:
+lemma zdiv_zmult2_aux3:
      "[| #0 $< c;  #0 $<= r;  r $< b |] ==> #0 $<= b $* (q zmod c) $+ r"
 apply (subgoal_tac "#0 $<= b $* (q zmod c)")
  prefer 2
@@ -1516,7 +1517,7 @@
 apply (simp add: zadd_commute)
 done
 
-lemma lemma4:
+lemma zdiv_zmult2_aux4:
      "[| #0 $< c; #0 $<= r; r $< b |] ==> b $* (q zmod c) $+ r $< b $* c"
 apply (subgoal_tac "r $* #1 $< b $* (c $- q zmod c)")
 apply (simp add: zdiff_zmult_distrib2 zadd_commute zcompare_rls)
@@ -1532,7 +1533,8 @@
       ==> quorem (<a,b$*c>, <q zdiv c, b$*(q zmod c) $+ r>)"
 apply (auto simp add: zmult_ac zmod_zdiv_equality [symmetric] quorem_def
                neq_iff_zless int_0_less_mult_iff 
-               zadd_zmult_distrib2 [symmetric] lemma1 lemma2 lemma3 lemma4)
+               zadd_zmult_distrib2 [symmetric] zdiv_zmult2_aux1 zdiv_zmult2_aux2
+               zdiv_zmult2_aux3 zdiv_zmult2_aux4)
 apply (blast dest: zless_trans)+
 done
 
@@ -1568,16 +1570,16 @@
 
 subsection{* Cancellation of common factors in "zdiv" *}
 
-lemma lemma1:
+lemma zdiv_zmult_zmult1_aux1:
      "[| #0 $< b;  intify(c) \<noteq> #0 |] ==> (c$*a) zdiv (c$*b) = a zdiv b"
 apply (subst zdiv_zmult2_eq)
 apply auto
 done
 
-lemma lemma2:
+lemma zdiv_zmult_zmult1_aux2:
      "[| b $< #0;  intify(c) \<noteq> #0 |] ==> (c$*a) zdiv (c$*b) = a zdiv b"
 apply (subgoal_tac " (c $* ($-a)) zdiv (c $* ($-b)) = ($-a) zdiv ($-b)")
-apply (rule_tac [2] lemma1)
+apply (rule_tac [2] zdiv_zmult_zmult1_aux1)
 apply auto
 done
 
@@ -1585,7 +1587,8 @@
      "[|intify(c) \<noteq> #0; b \<in> int|] ==> (c$*a) zdiv (c$*b) = a zdiv b"
 apply (case_tac "b = #0")
  apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) 
-apply (auto simp add: neq_iff_zless [of b] lemma1 lemma2)
+apply (auto simp add: neq_iff_zless [of b]
+  zdiv_zmult_zmult1_aux1 zdiv_zmult_zmult1_aux2)
 done
 
 lemma zdiv_zmult_zmult1: "intify(c) \<noteq> #0 ==> (c$*a) zdiv (c$*b) = a zdiv b"
@@ -1601,18 +1604,18 @@
 
 subsection{* Distribution of factors over "zmod" *}
 
-lemma lemma1:
+lemma zmod_zmult_zmult1_aux1:
      "[| #0 $< b;  intify(c) \<noteq> #0 |]  
       ==> (c$*a) zmod (c$*b) = c $* (a zmod b)"
 apply (subst zmod_zmult2_eq)
 apply auto
 done
 
-lemma lemma2:
+lemma zmod_zmult_zmult1_aux2:
      "[| b $< #0;  intify(c) \<noteq> #0 |]  
       ==> (c$*a) zmod (c$*b) = c $* (a zmod b)"
 apply (subgoal_tac " (c $* ($-a)) zmod (c $* ($-b)) = c $* (($-a) zmod ($-b))")
-apply (rule_tac [2] lemma1)
+apply (rule_tac [2] zmod_zmult_zmult1_aux1)
 apply auto
 done
 
@@ -1622,7 +1625,8 @@
  apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) 
 apply (case_tac "c = #0")
  apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) 
-apply (auto simp add: neq_iff_zless [of b] lemma1 lemma2)
+apply (auto simp add: neq_iff_zless [of b]
+  zmod_zmult_zmult1_aux1 zmod_zmult_zmult1_aux2)
 done
 
 lemma zmod_zmult_zmult1: "(c$*a) zmod (c$*b) = c $* (a zmod b)"