avoid duplicate fact bindings;
authorwenzelm
Tue Aug 27 15:40:33 2002 +0200 (2002-08-27)
changeset 13537f506eb568121
parent 13536 825249a031c3
child 13538 359c085c4def
avoid duplicate fact bindings;
src/HOL/Isar_examples/ExprCompiler.thy
src/HOL/MiniML/Type.thy
src/HOL/W0/W0.thy
src/ZF/Integ/IntDiv.thy
     1.1 --- a/src/HOL/Isar_examples/ExprCompiler.thy	Tue Aug 27 15:39:39 2002 +0200
     1.2 +++ b/src/HOL/Isar_examples/ExprCompiler.thy	Tue Aug 27 15:40:33 2002 +0200
     1.3 @@ -197,7 +197,7 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 -theorem correctness: "execute (compile e) env = eval e env"
     1.8 +theorem correctness': "execute (compile e) env = eval e env"
     1.9  proof -
    1.10    have exec_compile:
    1.11      "ALL stack. exec (compile e) stack env = eval e env # stack"
     2.1 --- a/src/HOL/MiniML/Type.thy	Tue Aug 27 15:39:39 2002 +0200
     2.2 +++ b/src/HOL/MiniML/Type.thy	Tue Aug 27 15:40:33 2002 +0200
     2.3 @@ -41,16 +41,16 @@
     2.4  consts
     2.5    free_tv :: ['a::type_struct] => nat set
     2.6  
     2.7 -primrec
     2.8 +primrec (free_tv_typ)
     2.9    free_tv_TVar    "free_tv (TVar m) = {m}"
    2.10    free_tv_Fun     "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
    2.11  
    2.12 -primrec
    2.13 +primrec (free_tv_type_scheme)
    2.14    "free_tv (FVar m) = {m}"
    2.15    "free_tv (BVar m) = {}"
    2.16    "free_tv (S1 =-> S2) = (free_tv S1) Un (free_tv S2)"
    2.17  
    2.18 -primrec
    2.19 +primrec (free_tv_list)
    2.20    "free_tv [] = {}"
    2.21    "free_tv (x#l) = (free_tv x) Un (free_tv l)"
    2.22  
    2.23 @@ -59,12 +59,12 @@
    2.24  consts
    2.25    free_tv_ML :: ['a::type_struct] => nat list
    2.26  
    2.27 -primrec
    2.28 +primrec (free_tv_ML_type_scheme)
    2.29    "free_tv_ML (FVar m) = [m]"
    2.30    "free_tv_ML (BVar m) = []"
    2.31    "free_tv_ML (S1 =-> S2) = (free_tv_ML S1) @ (free_tv_ML S2)"
    2.32  
    2.33 -primrec
    2.34 +primrec (free_tv_ML_list)
    2.35    "free_tv_ML [] = []"
    2.36    "free_tv_ML (x#l) = (free_tv_ML x) @ (free_tv_ML l)"
    2.37  
    2.38 @@ -82,12 +82,12 @@
    2.39  consts
    2.40    bound_tv :: ['a::type_struct] => nat set
    2.41  
    2.42 -primrec
    2.43 +primrec (bound_tv_type_scheme)
    2.44    "bound_tv (FVar m) = {}"
    2.45    "bound_tv (BVar m) = {m}"
    2.46    "bound_tv (S1 =-> S2) = (bound_tv S1) Un (bound_tv S2)"
    2.47  
    2.48 -primrec
    2.49 +primrec (bound_tv_list)
    2.50    "bound_tv [] = {}"
    2.51    "bound_tv (x#l) = (bound_tv x) Un (bound_tv l)"
    2.52  
    2.53 @@ -97,7 +97,7 @@
    2.54  consts
    2.55    min_new_bound_tv :: 'a::type_struct => nat
    2.56  
    2.57 -primrec
    2.58 +primrec (min_new_bound_tv_type_scheme)
    2.59    "min_new_bound_tv (FVar n) = 0"
    2.60    "min_new_bound_tv (BVar n) = Suc n"
    2.61    "min_new_bound_tv (sch1 =-> sch2) = max (min_new_bound_tv sch1) (min_new_bound_tv sch2)"
    2.62 @@ -118,11 +118,11 @@
    2.63  consts
    2.64    app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
    2.65  
    2.66 -primrec
    2.67 +primrec (app_subst_typ)
    2.68    app_subst_TVar "$ S (TVar n) = S n" 
    2.69    app_subst_Fun  "$ S (t1 -> t2) = ($ S t1) -> ($ S t2)" 
    2.70  
    2.71 -primrec
    2.72 +primrec (app_subst_type_scheme)
    2.73    "$ S (FVar n) = mk_scheme (S n)"
    2.74    "$ S (BVar n) = (BVar n)"
    2.75    "$ S (sch1 =-> sch2) = ($ S sch1) =-> ($ S sch2)"
     3.1 --- a/src/HOL/W0/W0.thy	Tue Aug 27 15:39:39 2002 +0200
     3.2 +++ b/src/HOL/W0/W0.thy	Tue Aug 27 15:40:33 2002 +0200
     3.3 @@ -64,7 +64,7 @@
     3.4  consts
     3.5    app_subst :: "subst \<Rightarrow> 'a::type_struct \<Rightarrow> 'a::type_struct"    ("$")
     3.6    -- {* extension of substitution to type structures *}
     3.7 -primrec
     3.8 +primrec (app_subst_typ)
     3.9    app_subst_TVar: "$s (TVar n) = s n"
    3.10    app_subst_Fun: "$s (t1 -> t2) = $s t1 -> $s t2"
    3.11  
    3.12 @@ -75,11 +75,11 @@
    3.13    free_tv :: "'a::type_struct \<Rightarrow> nat set"
    3.14    -- {* @{text "free_tv s"}: the type variables occuring freely in the type structure @{text s} *}
    3.15  
    3.16 -primrec
    3.17 +primrec (free_tv_typ)
    3.18    "free_tv (TVar m) = {m}"
    3.19    "free_tv (t1 -> t2) = free_tv t1 \<union> free_tv t2"
    3.20  
    3.21 -primrec
    3.22 +primrec (free_tv_list)
    3.23    "free_tv [] = {}"
    3.24    "free_tv (x # xs) = free_tv x \<union> free_tv xs"
    3.25  
     4.1 --- a/src/ZF/Integ/IntDiv.thy	Tue Aug 27 15:39:39 2002 +0200
     4.2 +++ b/src/ZF/Integ/IntDiv.thy	Tue Aug 27 15:40:33 2002 +0200
     4.3 @@ -956,7 +956,7 @@
     4.4  
     4.5  subsection{* division of a number by itself *}
     4.6  
     4.7 -lemma lemma1: "[| #0 $< a; a = r $+ a$*q; r $< a |] ==> #1 $<= q"
     4.8 +lemma self_quotient_aux1: "[| #0 $< a; a = r $+ a$*q; r $< a |] ==> #1 $<= q"
     4.9  apply (subgoal_tac "#0 $< a$*q")
    4.10  apply (cut_tac w = "#0" and z = "q" in add1_zle_iff)
    4.11  apply (simp add: int_0_less_mult_iff)
    4.12 @@ -967,7 +967,7 @@
    4.13  apply (simp add: zcompare_rls)
    4.14  done
    4.15  
    4.16 -lemma lemma2: "[| #0 $< a; a = r $+ a$*q; #0 $<= r |] ==> q $<= #1"
    4.17 +lemma self_quotient_aux2: "[| #0 $< a; a = r $+ a$*q; #0 $<= r |] ==> q $<= #1"
    4.18  apply (subgoal_tac "#0 $<= a$* (#1$-q)")
    4.19   apply (simp add: int_0_le_mult_iff zcompare_rls)
    4.20   apply (blast dest: zle_zless_trans)
    4.21 @@ -984,11 +984,12 @@
    4.22  apply auto
    4.23  prefer 4 apply (blast dest: zless_trans)
    4.24  apply (blast dest: zless_trans)
    4.25 -apply (rule_tac [3] a = "$-a" and r = "$-r" in lemma1)
    4.26 -apply (rule_tac a = "$-a" and r = "$-r" in lemma2)
    4.27 +apply (rule_tac [3] a = "$-a" and r = "$-r" in self_quotient_aux1)
    4.28 +apply (rule_tac a = "$-a" and r = "$-r" in self_quotient_aux2)
    4.29  apply (rule_tac [6] zminus_equation [THEN iffD1])
    4.30  apply (rule_tac [2] zminus_equation [THEN iffD1])
    4.31 -apply (force intro: lemma1 lemma2 simp add: zadd_commute zmult_zminus)+
    4.32 +apply (force intro: self_quotient_aux1 self_quotient_aux2
    4.33 +  simp add: zadd_commute zmult_zminus)+
    4.34  done
    4.35  
    4.36  lemma self_remainder:
    4.37 @@ -1481,7 +1482,7 @@
    4.38  
    4.39  (** first, four lemmas to bound the remainder for the cases b<0 and b>0 **)
    4.40  
    4.41 -lemma lemma1:
    4.42 +lemma zdiv_zmult2_aux1:
    4.43       "[| #0 $< c;  b $< r;  r $<= #0 |] ==> b$*c $< b$*(q zmod c) $+ r"
    4.44  apply (subgoal_tac "b $* (c $- q zmod c) $< r $* #1")
    4.45  apply (simp add: zdiff_zmult_distrib2 zadd_commute zcompare_rls)
    4.46 @@ -1492,7 +1493,7 @@
    4.47  apply (blast intro: zless_imp_zle dest: zless_zle_trans)
    4.48  done
    4.49  
    4.50 -lemma lemma2:
    4.51 +lemma zdiv_zmult2_aux2:
    4.52       "[| #0 $< c;   b $< r;  r $<= #0 |] ==> b $* (q zmod c) $+ r $<= #0"
    4.53  apply (subgoal_tac "b $* (q zmod c) $<= #0")
    4.54   prefer 2
    4.55 @@ -1504,7 +1505,7 @@
    4.56  apply (simp add: zadd_commute)
    4.57  done
    4.58  
    4.59 -lemma lemma3:
    4.60 +lemma zdiv_zmult2_aux3:
    4.61       "[| #0 $< c;  #0 $<= r;  r $< b |] ==> #0 $<= b $* (q zmod c) $+ r"
    4.62  apply (subgoal_tac "#0 $<= b $* (q zmod c)")
    4.63   prefer 2
    4.64 @@ -1516,7 +1517,7 @@
    4.65  apply (simp add: zadd_commute)
    4.66  done
    4.67  
    4.68 -lemma lemma4:
    4.69 +lemma zdiv_zmult2_aux4:
    4.70       "[| #0 $< c; #0 $<= r; r $< b |] ==> b $* (q zmod c) $+ r $< b $* c"
    4.71  apply (subgoal_tac "r $* #1 $< b $* (c $- q zmod c)")
    4.72  apply (simp add: zdiff_zmult_distrib2 zadd_commute zcompare_rls)
    4.73 @@ -1532,7 +1533,8 @@
    4.74        ==> quorem (<a,b$*c>, <q zdiv c, b$*(q zmod c) $+ r>)"
    4.75  apply (auto simp add: zmult_ac zmod_zdiv_equality [symmetric] quorem_def
    4.76                 neq_iff_zless int_0_less_mult_iff 
    4.77 -               zadd_zmult_distrib2 [symmetric] lemma1 lemma2 lemma3 lemma4)
    4.78 +               zadd_zmult_distrib2 [symmetric] zdiv_zmult2_aux1 zdiv_zmult2_aux2
    4.79 +               zdiv_zmult2_aux3 zdiv_zmult2_aux4)
    4.80  apply (blast dest: zless_trans)+
    4.81  done
    4.82  
    4.83 @@ -1568,16 +1570,16 @@
    4.84  
    4.85  subsection{* Cancellation of common factors in "zdiv" *}
    4.86  
    4.87 -lemma lemma1:
    4.88 +lemma zdiv_zmult_zmult1_aux1:
    4.89       "[| #0 $< b;  intify(c) \<noteq> #0 |] ==> (c$*a) zdiv (c$*b) = a zdiv b"
    4.90  apply (subst zdiv_zmult2_eq)
    4.91  apply auto
    4.92  done
    4.93  
    4.94 -lemma lemma2:
    4.95 +lemma zdiv_zmult_zmult1_aux2:
    4.96       "[| b $< #0;  intify(c) \<noteq> #0 |] ==> (c$*a) zdiv (c$*b) = a zdiv b"
    4.97  apply (subgoal_tac " (c $* ($-a)) zdiv (c $* ($-b)) = ($-a) zdiv ($-b)")
    4.98 -apply (rule_tac [2] lemma1)
    4.99 +apply (rule_tac [2] zdiv_zmult_zmult1_aux1)
   4.100  apply auto
   4.101  done
   4.102  
   4.103 @@ -1585,7 +1587,8 @@
   4.104       "[|intify(c) \<noteq> #0; b \<in> int|] ==> (c$*a) zdiv (c$*b) = a zdiv b"
   4.105  apply (case_tac "b = #0")
   4.106   apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) 
   4.107 -apply (auto simp add: neq_iff_zless [of b] lemma1 lemma2)
   4.108 +apply (auto simp add: neq_iff_zless [of b]
   4.109 +  zdiv_zmult_zmult1_aux1 zdiv_zmult_zmult1_aux2)
   4.110  done
   4.111  
   4.112  lemma zdiv_zmult_zmult1: "intify(c) \<noteq> #0 ==> (c$*a) zdiv (c$*b) = a zdiv b"
   4.113 @@ -1601,18 +1604,18 @@
   4.114  
   4.115  subsection{* Distribution of factors over "zmod" *}
   4.116  
   4.117 -lemma lemma1:
   4.118 +lemma zmod_zmult_zmult1_aux1:
   4.119       "[| #0 $< b;  intify(c) \<noteq> #0 |]  
   4.120        ==> (c$*a) zmod (c$*b) = c $* (a zmod b)"
   4.121  apply (subst zmod_zmult2_eq)
   4.122  apply auto
   4.123  done
   4.124  
   4.125 -lemma lemma2:
   4.126 +lemma zmod_zmult_zmult1_aux2:
   4.127       "[| b $< #0;  intify(c) \<noteq> #0 |]  
   4.128        ==> (c$*a) zmod (c$*b) = c $* (a zmod b)"
   4.129  apply (subgoal_tac " (c $* ($-a)) zmod (c $* ($-b)) = c $* (($-a) zmod ($-b))")
   4.130 -apply (rule_tac [2] lemma1)
   4.131 +apply (rule_tac [2] zmod_zmult_zmult1_aux1)
   4.132  apply auto
   4.133  done
   4.134  
   4.135 @@ -1622,7 +1625,8 @@
   4.136   apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) 
   4.137  apply (case_tac "c = #0")
   4.138   apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) 
   4.139 -apply (auto simp add: neq_iff_zless [of b] lemma1 lemma2)
   4.140 +apply (auto simp add: neq_iff_zless [of b]
   4.141 +  zmod_zmult_zmult1_aux1 zmod_zmult_zmult1_aux2)
   4.142  done
   4.143  
   4.144  lemma zmod_zmult_zmult1: "(c$*a) zmod (c$*b) = c $* (a zmod b)"