simplified locale predicates;
authorwenzelm
Wed Jul 24 22:15:55 2002 +0200 (2002-07-24)
changeset 134218fcdf4a26468
parent 13420 39fca1e5818a
child 13422 af9bc8d87a75
simplified locale predicates;
src/HOL/Finite_Set.thy
src/HOL/HOL.thy
src/HOL/NumberTheory/IntFact.thy
src/HOL/Record.thy
src/HOL/Set.thy
src/HOL/Typedef.thy
src/HOL/Unix/Unix.thy
src/ZF/AC/AC18_AC19.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Wed Jul 24 22:14:42 2002 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Wed Jul 24 22:15:55 2002 +0200
     1.3 @@ -31,7 +31,8 @@
     1.4      P {} ==> (!!F x. finite F ==> x \<notin> F ==> P F ==> P (insert x F)) ==> P F"
     1.5    -- {* Discharging @{text "x \<notin> F"} entails extra work. *}
     1.6  proof -
     1.7 -  assume "P {}" and insert: "!!F x. finite F ==> x \<notin> F ==> P F ==> P (insert x F)"
     1.8 +  assume "P {}" and
     1.9 +    insert: "!!F x. finite F ==> x \<notin> F ==> P F ==> P (insert x F)"
    1.10    assume "finite F"
    1.11    thus "P F"
    1.12    proof induct
    1.13 @@ -54,7 +55,8 @@
    1.14      P {} ==> (!!F a. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)) ==>
    1.15      P F"
    1.16  proof -
    1.17 -  assume "P {}" and insert: "!!F a. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
    1.18 +  assume "P {}" and insert:
    1.19 +    "!!F a. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
    1.20    assume "finite F"
    1.21    thus "F \<subseteq> A ==> P F"
    1.22    proof induct
    1.23 @@ -721,7 +723,7 @@
    1.24    apply (induct set: Finites)
    1.25     apply simp
    1.26    apply (simp add: AC insert_absorb Int_insert_left
    1.27 -    LC.fold_insert [OF LC.intro, OF LC_axioms.intro])
    1.28 +    LC.fold_insert [OF LC.intro])
    1.29    done
    1.30  
    1.31  lemma (in ACe) fold_Un_disjoint:
    1.32 @@ -746,14 +748,14 @@
    1.33        by simp
    1.34      also have "... = (f \<circ> g) x (fold (f \<circ> g) e (F \<union> B))"
    1.35        by (rule LC.fold_insert [OF LC.intro])
    1.36 -        (insert b insert, auto simp add: left_commute intro: LC_axioms.intro)
    1.37 +        (insert b insert, auto simp add: left_commute)
    1.38      also from insert have "fold (f \<circ> g) e (F \<union> B) =
    1.39        fold (f \<circ> g) e F \<cdot> fold (f \<circ> g) e B" by blast
    1.40      also have "(f \<circ> g) x ... = (f \<circ> g) x (fold (f \<circ> g) e F) \<cdot> fold (f \<circ> g) e B"
    1.41        by (simp add: AC)
    1.42      also have "(f \<circ> g) x (fold (f \<circ> g) e F) = fold (f \<circ> g) e (insert x F)"
    1.43        by (rule LC.fold_insert [OF LC.intro, symmetric]) (insert b insert,
    1.44 -	auto simp add: left_commute intro: LC_axioms.intro)
    1.45 +	auto simp add: left_commute)
    1.46      finally show ?case .
    1.47    qed
    1.48  qed
    1.49 @@ -779,7 +781,7 @@
    1.50  lemma setsum_insert [simp]:
    1.51      "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
    1.52    by (simp add: setsum_def
    1.53 -    LC.fold_insert [OF LC.intro, OF LC_axioms.intro] plus_ac0_left_commute)
    1.54 +    LC.fold_insert [OF LC.intro] plus_ac0_left_commute)
    1.55  
    1.56  lemma setsum_0: "setsum (\<lambda>i. 0) A = 0"
    1.57    apply (case_tac "finite A")
    1.58 @@ -936,7 +938,8 @@
    1.59     apply (simp add: card_s_0_eq_empty)
    1.60    apply atomize
    1.61    apply (rotate_tac -1, erule finite_induct)
    1.62 -   apply (simp_all (no_asm_simp) cong add: conj_cong add: card_s_0_eq_empty choose_deconstruct)
    1.63 +   apply (simp_all (no_asm_simp) cong add: conj_cong
    1.64 +     add: card_s_0_eq_empty choose_deconstruct)
    1.65    apply (subst card_Un_disjoint)
    1.66       prefer 4 apply (force simp add: constr_bij)
    1.67      prefer 3 apply force
    1.68 @@ -945,7 +948,8 @@
    1.69    apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
    1.70    done
    1.71  
    1.72 -theorem n_subsets: "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
    1.73 +theorem n_subsets:
    1.74 +    "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
    1.75    by (simp add: n_sub_lemma)
    1.76  
    1.77  end
     2.1 --- a/src/HOL/HOL.thy	Wed Jul 24 22:14:42 2002 +0200
     2.2 +++ b/src/HOL/HOL.thy	Wed Jul 24 22:15:55 2002 +0200
     2.3 @@ -344,7 +344,7 @@
     2.4      "!!P. (ALL x. x=t --> P(x)) = P(t)"
     2.5      "!!P. (ALL x. t=x --> P(x)) = P(t)"
     2.6    by (blast, blast, blast, blast, blast, rules+)
     2.7 - 
     2.8 +
     2.9  lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P --> Q) = (P' --> Q'))"
    2.10    by rules
    2.11  
    2.12 @@ -605,14 +605,9 @@
    2.13    fixes f
    2.14    assumes mono: "A <= B ==> f A <= f B"
    2.15  
    2.16 -lemmas monoI [intro?] = mono.intro [OF mono_axioms.intro]
    2.17 +lemmas monoI [intro?] = mono.intro
    2.18    and monoD [dest?] = mono.mono
    2.19  
    2.20 -lemma mono_def: "mono f == ALL A B. A <= B --> f A <= f B"
    2.21 -  -- compatibility
    2.22 -  by (simp only: atomize_eq mono_def mono_axioms_def)
    2.23 -
    2.24 -
    2.25  constdefs
    2.26    min :: "['a::ord, 'a] => 'a"
    2.27    "min a b == (if a <= b then a else b)"
     3.1 --- a/src/HOL/NumberTheory/IntFact.thy	Wed Jul 24 22:14:42 2002 +0200
     3.2 +++ b/src/HOL/NumberTheory/IntFact.thy	Wed Jul 24 22:15:55 2002 +0200
     3.3 @@ -39,7 +39,7 @@
     3.4  
     3.5  lemma setprod_insert [simp]:
     3.6      "finite A ==> a \<notin> A ==> setprod (insert a A) = a * setprod A"
     3.7 -  by (simp add: setprod_def zmult_left_commute LC.fold_insert [OF LC.intro, OF LC_axioms.intro])
     3.8 +  by (simp add: setprod_def zmult_left_commute LC.fold_insert [OF LC.intro])
     3.9  
    3.10  text {*
    3.11    \medskip @{term d22set} --- recursively defined set including all
     4.1 --- a/src/HOL/Record.thy	Wed Jul 24 22:14:42 2002 +0200
     4.2 +++ b/src/HOL/Record.thy	Wed Jul 24 22:15:55 2002 +0200
     4.3 @@ -18,9 +18,6 @@
     4.4      and dest1: "dest1 == (\<lambda>p. fst (Rep p))"
     4.5      and dest2: "dest2 == (\<lambda>p. snd (Rep p))"
     4.6  
     4.7 -lemmas product_typeI =
     4.8 -  product_type.intro [OF product_type_axioms.intro]
     4.9 -
    4.10  lemma (in product_type)
    4.11      "inject": "(pair x y = pair x' y') = (x = x' \<and> y = y')"
    4.12    by (simp add: pair type_definition.Abs_inject [OF "typedef"])
     5.1 --- a/src/HOL/Set.thy	Wed Jul 24 22:14:42 2002 +0200
     5.2 +++ b/src/HOL/Set.thy	Wed Jul 24 22:15:55 2002 +0200
     5.3 @@ -960,16 +960,16 @@
     5.4  
     5.5  text {* \medskip Monotonicity. *}
     5.6  
     5.7 -lemma mono_Un: "mono f ==> f A \<union> f B \<subseteq> f (A \<union> B)"
     5.8 +lemma mono_Un: includes mono shows "f A \<union> f B \<subseteq> f (A \<union> B)"
     5.9    apply (rule Un_least)
    5.10 -   apply (erule Un_upper1 [THEN [2] monoD])
    5.11 -  apply (erule Un_upper2 [THEN [2] monoD])
    5.12 +   apply (rule Un_upper1 [THEN mono])
    5.13 +  apply (rule Un_upper2 [THEN mono])
    5.14    done
    5.15  
    5.16 -lemma mono_Int: "mono f ==> f (A \<inter> B) \<subseteq> f A \<inter> f B"
    5.17 +lemma mono_Int: includes mono shows "f (A \<inter> B) \<subseteq> f A \<inter> f B"
    5.18    apply (rule Int_greatest)
    5.19 -   apply (erule Int_lower1 [THEN [2] monoD])
    5.20 -  apply (erule Int_lower2 [THEN [2] monoD])
    5.21 +   apply (rule Int_lower1 [THEN mono])
    5.22 +  apply (rule Int_lower2 [THEN mono])
    5.23    done
    5.24  
    5.25  
     6.1 --- a/src/HOL/Typedef.thy	Wed Jul 24 22:14:42 2002 +0200
     6.2 +++ b/src/HOL/Typedef.thy	Wed Jul 24 22:15:55 2002 +0200
     6.3 @@ -15,9 +15,6 @@
     6.4      and Abs_inverse: "y \<in> A ==> Rep (Abs y) = y"
     6.5    -- {* This will be axiomatized for each typedef! *}
     6.6  
     6.7 -lemmas type_definitionI [intro] =
     6.8 -  type_definition.intro [OF type_definition_axioms.intro]
     6.9 -
    6.10  lemma (in type_definition) Rep_inject:
    6.11    "(Rep x = Rep y) = (x = y)"
    6.12  proof
     7.1 --- a/src/HOL/Unix/Unix.thy	Wed Jul 24 22:14:42 2002 +0200
     7.2 +++ b/src/HOL/Unix/Unix.thy	Wed Jul 24 22:15:55 2002 +0200
     7.3 @@ -1131,7 +1131,7 @@
     7.4  text {*
     7.5    So this is our final result:
     7.6  
     7.7 -  @{thm [display] result [OF situation_axioms.intro, no_vars]}
     7.8 +  @{thm [display] result [OF situation.intro, no_vars]}
     7.9  *}
    7.10  
    7.11  end
     8.1 --- a/src/ZF/AC/AC18_AC19.thy	Wed Jul 24 22:14:42 2002 +0200
     8.2 +++ b/src/ZF/AC/AC18_AC19.thy	Wed Jul 24 22:15:55 2002 +0200
     8.3 @@ -36,7 +36,7 @@
     8.4  
     8.5  lemma AC1_AC18: "AC1 ==> PROP AC18"
     8.6  apply (unfold AC1_def)
     8.7 -apply (rule AC18.intro [OF AC18_axioms.intro])
     8.8 +apply (rule AC18.intro)
     8.9  apply (fast elim!: lemma_AC18 apply_type intro!: equalityI INT_I UN_I)
    8.10  done
    8.11