# HG changeset patch # User berghofe # Date 1170867098 -3600 # Node ID ce1459004c8de804f0a06ee206650734904f988e # Parent 9785397cc344de3b6f9b2d643398c423287777df Adapted to changes in Finite_Set theory. diff -r 9785397cc344 -r ce1459004c8d src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Wed Feb 07 17:46:03 2007 +0100 +++ b/src/HOL/Nominal/nominal_atoms.ML Wed Feb 07 17:51:38 2007 +0100 @@ -16,7 +16,7 @@ structure NominalAtoms : NOMINAL_ATOMS = struct -val Finites_emptyI = thm "Finites.emptyI"; +val finite_emptyI = thm "finite.emptyI"; val Collect_const = thm "Collect_const"; @@ -67,8 +67,8 @@ let val name = ak_name ^ "_infinite" val axiom = HOLogic.mk_Trueprop (HOLogic.mk_not - (HOLogic.mk_mem (HOLogic.mk_UNIV T, - Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT T))))) + (Const ("Finite_Set.finite", HOLogic.mk_setT T --> HOLogic.boolT) $ + HOLogic.mk_UNIV T)) in ((name, axiom), []) end) ak_names_types) thy1; @@ -252,9 +252,9 @@ val ty = TFree("'a",["HOL.type"]); val x = Free ("x", ty); val csupp = Const ("Nominal.supp", ty --> HOLogic.mk_setT T); - val cfinites = Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT T)) + val cfinite = Const ("Finite_Set.finite", HOLogic.mk_setT T --> HOLogic.boolT) - val axiom1 = HOLogic.mk_Trueprop (HOLogic.mk_mem (csupp $ x, cfinites)); + val axiom1 = HOLogic.mk_Trueprop (cfinite $ (csupp $ x)); in AxClass.define_class_i (cl_name, [pt_name]) [] [((cl_name ^ "1", []), [axiom1])] thy @@ -481,7 +481,7 @@ rtac ((at_thm RS fs_at_inst) RS fs1) 1] end else let val dj_inst = PureThy.get_thm thy' (Name ("dj_"^ak_name'^"_"^ak_name)); - val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, Finites_emptyI]; + val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, finite_emptyI]; in EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1] end) in AxClass.prove_arity (qu_name,[],[qu_class]) proof thy' @@ -618,7 +618,7 @@ let val qu_class = Sign.full_name thy ("fs_"^ak_name); val supp_def = thm "Nominal.supp_def"; - val simp_s = HOL_ss addsimps [supp_def,Collect_const,Finites_emptyI,defn]; + val simp_s = HOL_ss addsimps [supp_def,Collect_const,finite_emptyI,defn]; val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1]; in AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy diff -r 9785397cc344 -r ce1459004c8d src/HOL/Nominal/nominal_package.ML --- a/src/HOL/Nominal/nominal_package.ML Wed Feb 07 17:46:03 2007 +0100 +++ b/src/HOL/Nominal/nominal_package.ML Wed Feb 07 17:51:38 2007 +0100 @@ -18,7 +18,7 @@ structure NominalPackage : NOMINAL_PACKAGE = struct -val Finites_emptyI = thm "Finites.emptyI"; +val finite_emptyI = thm "finite.emptyI"; val finite_Diff = thm "finite_Diff"; val finite_Un = thm "finite_Un"; val Un_iff = thm "Un_iff"; @@ -1016,7 +1016,7 @@ (fn _ => simp_tac (HOL_basic_ss addsimps (supp_def :: Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un :: - symmetric empty_def :: Finites_emptyI :: simp_thms @ + symmetric empty_def :: finite_emptyI :: simp_thms @ abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1) in (supp_thm, @@ -1091,9 +1091,9 @@ let val atomT = Type (atom, []) in map standard (List.take (split_conj_thm (Goal.prove_global thy8 [] [] (HOLogic.mk_Trueprop - (foldr1 HOLogic.mk_conj (map (fn (s, T) => HOLogic.mk_mem - (Const ("Nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T), - Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT atomT)))) + (foldr1 HOLogic.mk_conj (map (fn (s, T) => + Const ("Finite_Set.finite", HOLogic.mk_setT atomT --> HOLogic.boolT) $ + (Const ("Nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T))) (indnames ~~ recTs)))) (fn _ => indtac dt_induct indnames 1 THEN ALLGOALS (asm_full_simp_tac (simpset_of thy8 addsimps @@ -1202,8 +1202,8 @@ val ind_prems' = map (fn (_, f as Free (_, T)) => list_all_free ([("x", fsT')], - HOLogic.mk_Trueprop (HOLogic.mk_mem (f $ Free ("x", fsT'), - Const ("Finite_Set.Finites", HOLogic.mk_setT (body_type T)))))) fresh_fs @ + HOLogic.mk_Trueprop (Const ("Finite_Set.finite", body_type T --> + HOLogic.boolT) $ (f $ Free ("x", fsT'))))) fresh_fs @ List.concat (map (fn (((i, (_, _, constrs)), (_, idxss)), T) => map (make_ind_prem fsT' (fn T => fn t => fn u => HOLogic.Not $ HOLogic.mk_mem (t, the (AList.lookup op = fresh_fs T) $ u)) i T) @@ -1480,8 +1480,8 @@ HOLogic.mk_Trueprop (List.nth (rec_preds, i) $ Free y)) (recs ~~ frees''); val prems5 = mk_fresh3 (recs ~~ frees'') frees'; val prems6 = maps (fn aT => map (fn y as (_, T) => HOLogic.mk_Trueprop - (HOLogic.mk_mem (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ Free y, - Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT aT))))) + (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $ + (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ Free y))) frees'') atomTs; val prems7 = map (fn x as (_, T) => HOLogic.mk_Trueprop (Const ("Nominal.fresh", T --> fsT' --> HOLogic.boolT) $ @@ -1563,9 +1563,9 @@ val name = Sign.base_name (fst (dest_Type aT)); val fs_name = PureThy.get_thm thy11 (Name ("fs_" ^ name ^ "1")); val aset = HOLogic.mk_setT aT; - val finites = Const ("Finite_Set.Finites", HOLogic.mk_setT aset); - val fins = map (fn (f, T) => HOLogic.mk_Trueprop (HOLogic.mk_mem - (Const ("Nominal.supp", T --> aset) $ f, finites))) + val finite = Const ("Finite_Set.finite", aset --> HOLogic.boolT); + val fins = map (fn (f, T) => HOLogic.mk_Trueprop + (finite $ (Const ("Nominal.supp", T --> aset) $ f))) (rec_fns ~~ rec_fn_Ts) in map (fn th => standard (th RS mp)) (split_conj_thm @@ -1577,7 +1577,7 @@ val y = Free ("y" ^ string_of_int i, U) in HOLogic.mk_imp (R $ x $ y, - HOLogic.mk_mem (Const ("Nominal.supp", U --> aset) $ y, finites)) + finite $ (Const ("Nominal.supp", U --> aset) $ y)) end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ (1 upto length recTs))))) (fn fins => (rtac rec_induct THEN_ALL_NEW cut_facts_tac fins) 1 THEN REPEAT (NominalPermeq.finite_guess_tac (HOL_ss addsimps [fs_name]) 1)))) @@ -1597,9 +1597,9 @@ end; val finite_premss = map (fn aT => - map (fn (f, T) => HOLogic.mk_Trueprop (HOLogic.mk_mem - (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ f, - Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT aT))))) + map (fn (f, T) => HOLogic.mk_Trueprop + (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $ + (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ f))) (rec_fns ~~ rec_fn_Ts)) dt_atomTs; val rec_fresh_thms = map (fn ((aT, eqvt_ths), finite_prems) => @@ -1715,9 +1715,9 @@ in (freshs1 @ [term_of cx], freshs2 @ ths, ctxt') end; val finite_ctxt_prems = map (fn aT => - HOLogic.mk_Trueprop (HOLogic.mk_mem - (Const ("Nominal.supp", fsT' --> HOLogic.mk_setT aT) $ rec_ctxt, - Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT aT))))) dt_atomTs; + HOLogic.mk_Trueprop + (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $ + (Const ("Nominal.supp", fsT' --> HOLogic.mk_setT aT) $ rec_ctxt))) dt_atomTs; val rec_unique_thms = split_conj_thm (Goal.prove (ProofContext.init thy11) (map fst rec_unique_frees) diff -r 9785397cc344 -r ce1459004c8d src/HOL/Nominal/nominal_permeq.ML --- a/src/HOL/Nominal/nominal_permeq.ML Wed Feb 07 17:46:03 2007 +0100 +++ b/src/HOL/Nominal/nominal_permeq.ML Wed Feb 07 17:51:38 2007 +0100 @@ -48,7 +48,7 @@ structure NominalPermeq : NOMINAL_PERMEQ = struct -val Finites_emptyI = thm "Finites.emptyI"; +val finite_emptyI = thm "finite.emptyI"; val finite_Un = thm "finite_Un"; (* pulls out dynamically a thm via the proof state *) @@ -264,8 +264,7 @@ let val goal = List.nth(cprems_of st, i-1) in case Logic.strip_assums_concl (term_of goal) of - _ $ (Const ("op :", _) $ (Const ("Nominal.supp", T) $ x) $ - Const ("Finite_Set.Finites", _)) => + _ $ (Const ("Finite_Set.finite", _) $ (Const ("Nominal.supp", T) $ x)) => let val cert = Thm.cterm_of (sign_of_thm st); val ps = Logic.strip_params (term_of goal); @@ -281,7 +280,7 @@ Logic.strip_assums_concl (hd (prems_of supports_rule')); val supports_rule'' = Drule.cterm_instantiate [(cert (head_of S), cert s')] supports_rule' - val ss' = ss addsimps [supp_prod, supp_unit, finite_Un, Finites_emptyI] + val ss' = ss addsimps [supp_prod, supp_unit, finite_Un, finite_emptyI] in (tactical ("guessing of the right supports-set", EVERY [compose_tac (false, supports_rule'', 2) i, @@ -319,7 +318,7 @@ val supports_fresh_rule'' = Drule.cterm_instantiate [(cert (head_of S), cert s')] supports_fresh_rule' val ss1 = ss addsimps [symmetric fresh_def,fresh_prod,fresh_unit] - val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,Finites_emptyI] + val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI] (* FIXME sometimes these rewrite rules are already in the ss, *) (* which produces a warning *) in diff -r 9785397cc344 -r ce1459004c8d src/HOL/NumberTheory/BijectionRel.thy --- a/src/HOL/NumberTheory/BijectionRel.thy Wed Feb 07 17:46:03 2007 +0100 +++ b/src/HOL/NumberTheory/BijectionRel.thy Wed Feb 07 17:51:38 2007 +0100 @@ -71,7 +71,7 @@ "!!F a. F \ A ==> a \ A ==> a \ F ==> P F ==> P (insert a F)" shows "P F" using major subs - apply (induct set: Finites) + apply (induct set: finite) apply (blast intro: cases)+ done diff -r 9785397cc344 -r ce1459004c8d src/HOL/NumberTheory/Euler.thy --- a/src/HOL/NumberTheory/Euler.thy Wed Feb 07 17:46:03 2007 +0100 +++ b/src/HOL/NumberTheory/Euler.thy Wed Feb 07 17:51:38 2007 +0100 @@ -118,7 +118,7 @@ lemma card_setsum_aux: "[| finite S; \X \ S. finite (X::int set); \X \ S. card X = n |] ==> setsum card S = setsum (%x. n) S" - by (induct set: Finites) auto + by (induct set: finite) auto lemma SetS_card: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==> int(card(SetS a p)) = (p - 1) div 2" diff -r 9785397cc344 -r ce1459004c8d src/HOL/NumberTheory/EvenOdd.thy --- a/src/HOL/NumberTheory/EvenOdd.thy Wed Feb 07 17:46:03 2007 +0100 +++ b/src/HOL/NumberTheory/EvenOdd.thy Wed Feb 07 17:51:38 2007 +0100 @@ -242,7 +242,7 @@ lemma neg_one_special: "finite A ==> ((-1 :: int) ^ card A) * (-1 ^ card A) = 1" - by (induct set: Finites) auto + by (induct set: finite) auto lemma neg_one_power: "(-1::int)^n = 1 | (-1::int)^n = -1" by (induct n) auto diff -r 9785397cc344 -r ce1459004c8d src/HOL/NumberTheory/Finite2.thy --- a/src/HOL/NumberTheory/Finite2.thy Wed Feb 07 17:46:03 2007 +0100 +++ b/src/HOL/NumberTheory/Finite2.thy Wed Feb 07 17:51:38 2007 +0100 @@ -38,19 +38,19 @@ qed lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)" - apply (induct set: Finites) + apply (induct set: finite) apply (auto simp add: left_distrib right_distrib int_eq_of_nat) done lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) = int(c) * int(card X)" - apply (induct set: Finites) + apply (induct set: finite) apply (auto simp add: zadd_zmult_distrib2) done lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A = c * setsum f A" - by (induct set: Finites) (auto simp add: zadd_zmult_distrib2) + by (induct set: finite) (auto simp add: zadd_zmult_distrib2) subsection {* Cardinality of explicit finite sets *} diff -r 9785397cc344 -r ce1459004c8d src/HOL/NumberTheory/Gauss.thy --- a/src/HOL/NumberTheory/Gauss.thy Wed Feb 07 17:46:03 2007 +0100 +++ b/src/HOL/NumberTheory/Gauss.thy Wed Feb 07 17:51:38 2007 +0100 @@ -444,7 +444,7 @@ "setprod uminus E"], auto) done also have "setprod uminus E = (setprod id E) * (-1)^(card E)" - using finite_E by (induct set: Finites) auto + using finite_E by (induct set: finite) auto then have "setprod uminus E = (-1) ^ (card E) * (setprod id E)" by (simp add: zmult_commute) with two show ?thesis @@ -484,7 +484,7 @@ by (simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric]) moreover have "setprod (%x. x * a) A = setprod (%x. a) A * setprod id A" - using finite_A by (induct set: Finites) auto + using finite_A by (induct set: finite) auto ultimately have "[setprod id A = ((-1)^(card E) * (setprod (%x. a) A * setprod id A))] (mod p)" by simp diff -r 9785397cc344 -r ce1459004c8d src/HOL/NumberTheory/Int2.thy --- a/src/HOL/NumberTheory/Int2.thy Wed Feb 07 17:46:03 2007 +0100 +++ b/src/HOL/NumberTheory/Int2.thy Wed Feb 07 17:51:38 2007 +0100 @@ -175,7 +175,7 @@ lemma all_relprime_prod_relprime: "[| finite A; \x \ A. (zgcd(x,y) = 1) |] ==> zgcd (setprod id A,y) = 1" - by (induct set: Finites) (auto simp add: zgcd_zgcd_zmult) + by (induct set: finite) (auto simp add: zgcd_zgcd_zmult) subsection {* Some properties of MultInv *} diff -r 9785397cc344 -r ce1459004c8d src/HOL/Real/ferrante_rackoff_proof.ML --- a/src/HOL/Real/ferrante_rackoff_proof.ML Wed Feb 07 17:46:03 2007 +0100 +++ b/src/HOL/Real/ferrante_rackoff_proof.ML Wed Feb 07 17:51:38 2007 +0100 @@ -47,7 +47,7 @@ fun inC T = Const("op :",[T,Type("set",[T])] ---> HOLogic.boolT); val ss = simpset_of sg fun proveinU t = prove_bysimp sg ss ((inC rT)$t$hU) - val uf = prove_bysimp sg ss ((inC rsT)$hU$Const("Finite_Set.Finites",Type("set",[rsT]))) + val uf = prove_bysimp sg ss (Const ("Finite_Set.finite", rsT --> HOLogic.boolT) $ hU) in (U,cterm_of sg hU,map proveinU U,uf) end;