# HG changeset patch # User wenzelm # Date 1026836769 -7200 # Node ID a2c4faad4d3551893d8515565fedcea17b52e997 # Parent d3c7d05d88398e9f29e6175305b31c39138cf38e adapted to locale defs; diff -r d3c7d05d8839 -r a2c4faad4d35 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Tue Jul 16 18:25:48 2002 +0200 +++ b/src/HOL/Finite_Set.thy Tue Jul 16 18:26:09 2002 +0200 @@ -720,7 +720,8 @@ fold f e A \ fold f e B = fold f e (A Un B) \ fold f e (A Int B)" apply (induct set: Finites) apply simp - apply (simp add: AC LC.fold_insert insert_absorb Int_insert_left) + apply (simp add: AC ACe.axioms ACe_axioms_def + LC_axioms_def LC.fold_insert insert_absorb Int_insert_left) done lemma (in ACe) fold_Un_disjoint: @@ -744,13 +745,15 @@ have "fold (f \ g) e (insert x F \ B) = fold (f \ g) e (insert x (F \ B))" by simp also have "... = (f \ g) x (fold (f \ g) e (F \ B))" - by (rule LC.fold_insert) (insert b insert, auto simp add: left_commute) (* FIXME import of fold_insert (!?) *) + by (rule LC.fold_insert) + (insert b insert, auto simp add: left_commute intro: LC_axioms.intro) also from insert have "fold (f \ g) e (F \ B) = fold (f \ g) e F \ fold (f \ g) e B" by blast also have "(f \ g) x ... = (f \ g) x (fold (f \ g) e F) \ fold (f \ g) e B" by (simp add: AC) also have "(f \ g) x (fold (f \ g) e F) = fold (f \ g) e (insert x F)" - by (rule LC.fold_insert [symmetric]) (insert b insert, auto simp add: left_commute) + by (rule LC.fold_insert [symmetric]) (insert b insert, + auto simp add: left_commute intro: LC_axioms.intro) finally show ?case . qed qed @@ -775,7 +778,8 @@ lemma setsum_insert [simp]: "finite F ==> a \ F ==> setsum f (insert a F) = f a + setsum f F" - by (simp add: setsum_def LC.fold_insert plus_ac0_left_commute) + by (simp add: setsum_def + LC_axioms_def LC.fold_insert plus_ac0_left_commute) lemma setsum_0: "setsum (\i. 0) A = 0" apply (case_tac "finite A") diff -r d3c7d05d8839 -r a2c4faad4d35 src/HOL/MicroJava/BV/LBVComplete.thy --- a/src/HOL/MicroJava/BV/LBVComplete.thy Tue Jul 16 18:25:48 2002 +0200 +++ b/src/HOL/MicroJava/BV/LBVComplete.thy Tue Jul 16 18:26:09 2002 +0200 @@ -31,7 +31,7 @@ apply force done -locale lbvc = lbv + +locale (open) lbvc = lbv + fixes phi :: "'a list" ("\") fixes c :: "'a list" defines cert_def: "c \ make_cert step \ \" diff -r d3c7d05d8839 -r a2c4faad4d35 src/HOL/MicroJava/BV/LBVCorrect.thy --- a/src/HOL/MicroJava/BV/LBVCorrect.thy Tue Jul 16 18:25:48 2002 +0200 +++ b/src/HOL/MicroJava/BV/LBVCorrect.thy Tue Jul 16 18:26:09 2002 +0200 @@ -8,7 +8,7 @@ theory LBVCorrect = LBVSpec + Typing_Framework: -locale lbvs = lbv + +locale (open) lbvs = lbv + fixes s0 :: 'a fixes c :: "'a list" fixes ins :: "'b list" diff -r d3c7d05d8839 -r a2c4faad4d35 src/HOL/MicroJava/BV/LBVSpec.thy --- a/src/HOL/MicroJava/BV/LBVSpec.thy Tue Jul 16 18:25:48 2002 +0200 +++ b/src/HOL/MicroJava/BV/LBVSpec.thy Tue Jul 16 18:26:09 2002 +0200 @@ -51,7 +51,7 @@ "bottom r B \ \x. B <=_r x" -locale lbv = semilat + +locale (open) lbv = semilat + fixes T :: "'a" ("\") fixes B :: "'a" ("\") fixes step :: "'a step_type" diff -r d3c7d05d8839 -r a2c4faad4d35 src/HOL/MicroJava/BV/Semilat.thy --- a/src/HOL/MicroJava/BV/Semilat.thy Tue Jul 16 18:25:48 2002 +0200 +++ b/src/HOL/MicroJava/BV/Semilat.thy Tue Jul 16 18:26:09 2002 +0200 @@ -63,7 +63,7 @@ some_lub :: "('a*'a)set \ 'a \ 'a \ 'a" "some_lub r x y == SOME z. is_lub r x y z"; -locale semilat = +locale (open) semilat = fixes A :: "'a set" and r :: "'a ord" and f :: "'a binop" diff -r d3c7d05d8839 -r a2c4faad4d35 src/HOL/NumberTheory/IntFact.thy --- a/src/HOL/NumberTheory/IntFact.thy Tue Jul 16 18:25:48 2002 +0200 +++ b/src/HOL/NumberTheory/IntFact.thy Tue Jul 16 18:26:09 2002 +0200 @@ -40,7 +40,7 @@ lemma setprod_insert [simp]: "finite A ==> a \ A ==> setprod (insert a A) = a * setprod A" apply (unfold setprod_def) - apply (simp add: zmult_left_commute LC.fold_insert) + apply (simp add: zmult_left_commute LC.fold_insert [OF LC_axioms.intro]) done