qualified exports from locales;
authorwenzelm
Thu Jan 10 01:10:58 2002 +0100 (2002-01-10)
changeset 12693827818b891c7
parent 12692 df42e9a53a02
child 12694 9950c1ce9d24
qualified exports from locales;
src/HOL/Finite_Set.ML
src/HOL/Finite_Set.thy
src/HOL/NumberTheory/IntFact.thy
     1.1 --- a/src/HOL/Finite_Set.ML	Wed Jan 09 17:56:46 2002 +0100
     1.2 +++ b/src/HOL/Finite_Set.ML	Thu Jan 10 01:10:58 2002 +0100
     1.3 @@ -97,18 +97,18 @@
     1.4  val finite_subset = thm "finite_subset";
     1.5  val finite_subset_induct = thm "finite_subset_induct";
     1.6  val finite_trancl = thm "finite_trancl";
     1.7 -val foldSet_determ = thm "foldSet_determ";
     1.8 +val foldSet_determ = thm "LC.foldSet_determ";
     1.9  val foldSet_imp_finite = thm "foldSet_imp_finite";
    1.10 -val fold_Un_Int = thm "fold_Un_Int";
    1.11 -val fold_Un_disjoint = thm "fold_Un_disjoint";
    1.12 -val fold_Un_disjoint2 = thm "fold_Un_disjoint2";
    1.13 -val fold_commute = thm "fold_commute";
    1.14 +val fold_Un_Int = thm "ACe.fold_Un_Int";
    1.15 +val fold_Un_disjoint = thm "ACe.fold_Un_disjoint";
    1.16 +val fold_Un_disjoint2 = thm "ACe.fold_Un_disjoint2";
    1.17 +val fold_commute = thm "LC.fold_commute";
    1.18  val fold_def = thm "fold_def";
    1.19  val fold_empty = thm "fold_empty";
    1.20 -val fold_equality = thm "fold_equality";
    1.21 -val fold_insert = thm "fold_insert";
    1.22 -val fold_nest_Un_Int = thm "fold_nest_Un_Int";
    1.23 -val fold_nest_Un_disjoint = thm "fold_nest_Un_disjoint";
    1.24 +val fold_equality = thm "LC.fold_equality";
    1.25 +val fold_insert = thm "LC.fold_insert";
    1.26 +val fold_nest_Un_Int = thm "LC.fold_nest_Un_Int";
    1.27 +val fold_nest_Un_disjoint = thm "LC.fold_nest_Un_disjoint";
    1.28  val n_sub_lemma = thm "n_sub_lemma";
    1.29  val n_subsets = thm "n_subsets";
    1.30  val psubset_card_mono = thm "psubset_card_mono";
     2.1 --- a/src/HOL/Finite_Set.thy	Wed Jan 09 17:56:46 2002 +0100
     2.2 +++ b/src/HOL/Finite_Set.thy	Thu Jan 10 01:10:58 2002 +0100
     2.3 @@ -711,7 +711,7 @@
     2.4      AC: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"  "x \<cdot> y = y \<cdot> x"  "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
     2.5    by (rule assoc, rule commute, rule left_commute)  (* FIXME localize "lemmas" (!??) *)
     2.6  
     2.7 -lemma (in ACe [simp]) left_ident: "e \<cdot> x = x"
     2.8 +lemma (in ACe) left_ident [simp]: "e \<cdot> x = x"
     2.9  proof -
    2.10    have "x \<cdot> e = x" by (rule ident)
    2.11    thus ?thesis by (subst commute)
    2.12 @@ -722,7 +722,7 @@
    2.13      fold f e A \<cdot> fold f e B = fold f e (A Un B) \<cdot> fold f e (A Int B)"
    2.14    apply (induct set: Finites)
    2.15     apply simp
    2.16 -  apply (simp add: AC fold_insert insert_absorb Int_insert_left)
    2.17 +  apply (simp add: AC LC.fold_insert insert_absorb Int_insert_left)
    2.18    done
    2.19  
    2.20  lemma (in ACe) fold_Un_disjoint:
    2.21 @@ -746,13 +746,13 @@
    2.22      have "fold (f \<circ> g) e (insert x F \<union> B) = fold (f \<circ> g) e (insert x (F \<union> B))"
    2.23        by simp
    2.24      also have "... = (f \<circ> g) x (fold (f \<circ> g) e (F \<union> B))"
    2.25 -      by (rule fold_insert) (insert b insert, auto simp add: left_commute)  (* FIXME import of fold_insert (!?) *)
    2.26 +      by (rule LC.fold_insert) (insert b insert, auto simp add: left_commute)  (* FIXME import of fold_insert (!?) *)
    2.27      also from insert have "fold (f \<circ> g) e (F \<union> B) =
    2.28        fold (f \<circ> g) e F \<cdot> fold (f \<circ> g) e B" by blast
    2.29      also have "(f \<circ> g) x ... = (f \<circ> g) x (fold (f \<circ> g) e F) \<cdot> fold (f \<circ> g) e B"
    2.30        by (simp add: AC)
    2.31      also have "(f \<circ> g) x (fold (f \<circ> g) e F) = fold (f \<circ> g) e (insert x F)"
    2.32 -      by (rule fold_insert [symmetric]) (insert b insert, auto simp add: left_commute)
    2.33 +      by (rule LC.fold_insert [symmetric]) (insert b insert, auto simp add: left_commute)
    2.34      finally show ?case .
    2.35    qed
    2.36  qed
    2.37 @@ -777,7 +777,7 @@
    2.38  
    2.39  lemma setsum_insert [simp]:
    2.40      "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
    2.41 -  by (simp add: setsum_def fold_insert plus_ac0_left_commute)
    2.42 +  by (simp add: setsum_def LC.fold_insert plus_ac0_left_commute)
    2.43  
    2.44  lemma setsum_0: "setsum (\<lambda>i. 0) A = 0"
    2.45    apply (case_tac "finite A")
     3.1 --- a/src/HOL/NumberTheory/IntFact.thy	Wed Jan 09 17:56:46 2002 +0100
     3.2 +++ b/src/HOL/NumberTheory/IntFact.thy	Thu Jan 10 01:10:58 2002 +0100
     3.3 @@ -40,7 +40,7 @@
     3.4  lemma setprod_insert [simp]:
     3.5      "finite A ==> a \<notin> A ==> setprod (insert a A) = a * setprod A"
     3.6    apply (unfold setprod_def)
     3.7 -  apply (simp add: zmult_left_commute fold_insert [standard])
     3.8 +  apply (simp add: zmult_left_commute LC.fold_insert)
     3.9    done
    3.10  
    3.11