# HG changeset patch # User Cezary Kaliszyk # Date 1314861385 -32400 # Node ID 8a2fd7418435b48a067e631762630cda9f4d23b7 # Parent 076a45f65e126c2d56dab4dde14b9b91cfaeb4a5 HOL/Import: observe distinction between sets and predicates (where possible) diff -r 076a45f65e12 -r 8a2fd7418435 src/HOL/Import/HOLLight/HOLLight.thy --- a/src/HOL/Import/HOLLight/HOLLight.thy Wed Aug 31 13:28:29 2011 -0700 +++ b/src/HOL/Import/HOLLight/HOLLight.thy Thu Sep 01 16:16:25 2011 +0900 @@ -759,12 +759,12 @@ ==> EX f::nat => 'A. ALL x::nat. f x = H f x" by (import hollight WF_REC_num) -lemma WF_MEASURE: "wfP (%(a::'A) b::'A. measure (m::'A => nat) (a, b))" +lemma WF_MEASURE: "wfP (%(a::'A) b::'A. (a, b) : measure (m::'A => nat))" by (import hollight WF_MEASURE) lemma MEASURE_LE: "(ALL x::'q_12099. - measure (m::'q_12099 => nat) (x, a::'q_12099) --> - measure m (x, b::'q_12099)) = + (x, a::'q_12099) : measure (m::'q_12099 => nat) --> + (x, b::'q_12099) : measure m) = (m a <= m b)" by (import hollight MEASURE_LE) diff -r 076a45f65e12 -r 8a2fd7418435 src/HOL/Import/HOLLight/hollight.imp --- a/src/HOL/Import/HOLLight/hollight.imp Wed Aug 31 13:28:29 2011 -0700 +++ b/src/HOL/Import/HOLLight/hollight.imp Thu Sep 01 16:16:25 2011 +0900 @@ -590,6 +590,8 @@ "UNIONS_INSERT" > "Complete_Lattice.Union_insert" "UNIONS_IMAGE" > "HOLLight.hollight.UNIONS_IMAGE" "UNIONS_GSPEC" > "HOLLight.hollight.UNIONS_GSPEC" + "UNIONS_2" > "Complete_Lattice.Un_eq_Union" + "UNIONS_1" > "Complete_Lattice.complete_lattice_class.Sup_singleton" "UNIONS_0" > "Complete_Lattice.Union_empty" "UNCURRY_def" > "HOLLight.hollight.UNCURRY_def" "TYDEF_recspace" > "HOLLight.hollight.TYDEF_recspace" @@ -1595,6 +1597,8 @@ "INTERS_INSERT" > "Complete_Lattice.Inter_insert" "INTERS_IMAGE" > "HOLLight.hollight.INTERS_IMAGE" "INTERS_GSPEC" > "HOLLight.hollight.INTERS_GSPEC" + "INTERS_2" > "Complete_Lattice.Int_eq_Inter" + "INTERS_1" > "Complete_Lattice.complete_lattice_class.Inf_singleton" "INTERS_0" > "Complete_Lattice.Inter_empty" "INSERT_UNIV" > "HOLLight.hollight.INSERT_UNIV" "INSERT_UNION_EQ" > "Set.Un_insert_left" @@ -1684,7 +1688,7 @@ "HAS_SIZE_0" > "HOLLight.hollight.HAS_SIZE_0" "GE_C" > "HOLLight.hollight.GE_C" "FUN_IN_IMAGE" > "Set.imageI" - "FUN_EQ_THM" > "Fun.fun_eq_iff" + "FUN_EQ_THM" > "HOL.fun_eq_iff" "FUNCTION_FACTORS_RIGHT" > "HOLLight.hollight.FUNCTION_FACTORS_RIGHT" "FUNCTION_FACTORS_LEFT" > "HOLLight.hollight.FUNCTION_FACTORS_LEFT" "FST" > "Product_Type.fst_conv" @@ -2010,7 +2014,7 @@ "DEF__equal__equal__greaterthan_" > "HOLLightCompat.DEF__equal__equal__greaterthan_" "DEF__equal__equal_" > "HOLLight.hollight.DEF__equal__equal_" "DEF__equal__c" > "HOLLight.hollight.DEF__equal__c" - "DEF__dot__dot_" > "HOLLightCompat.DEF__dot__dot_" + "DEF__dot__dot_" > "HOLLightCompat.dotdot_def" "DEF__backslash__slash_" > "HOL.or_def" "DEF__UNGUARDED_PATTERN" > "HOLLight.hollight.DEF__UNGUARDED_PATTERN" "DEF__SEQPATTERN" > "HOLLight.hollight.DEF__SEQPATTERN" @@ -2080,7 +2084,7 @@ "DEF_IMAGE" > "HOLLightCompat.DEF_IMAGE" "DEF_I" > "Fun.id_apply" "DEF_HAS_SIZE" > "HOLLight.hollight.DEF_HAS_SIZE" - "DEF_GSPEC" > "HOLLightCompat.DEF_GSPEC" + "DEF_GSPEC" > "Set.Collect_def" "DEF_GEQ" > "HOLLightCompat.DEF_GEQ" "DEF_GABS" > "HOLLightCompat.DEF_GABS" "DEF_FST" > "HOLLightCompat.DEF_FST" diff -r 076a45f65e12 -r 8a2fd7418435 src/HOL/Import/HOLLightCompat.thy --- a/src/HOL/Import/HOLLightCompat.thy Wed Aug 31 13:28:29 2011 -0700 +++ b/src/HOL/Import/HOLLightCompat.thy Thu Sep 01 16:16:25 2011 +0900 @@ -22,19 +22,16 @@ by simp lemma num_Axiom: - "\e f. \!fn. fn 0 = e \ (\n. fn (Suc n) = f (fn n) n)" - apply (intro allI) - apply (rule_tac a="nat_rec e (%n e. f e n)" in ex1I) - apply auto - apply (simp add: fun_eq_iff) - apply (intro allI) - apply (induct_tac xa) + "\!fn. fn 0 = e \ (\n. fn (Suc n) = f (fn n) n)" + apply (rule ex1I[of _ "nat_rec e (%n e. f e n)"]) + apply (auto simp add: fun_eq_iff) + apply (induct_tac x) apply simp_all done lemma SUC_INJ: "\m n. Suc m = Suc n \ m = n" - by auto + by simp lemma PAIR: "(fst x, snd x) = x" @@ -47,8 +44,7 @@ lemma DEF__star_: "op * = (SOME mult. (\n. mult 0 n = 0) \ (\m n. mult (Suc m) n = mult m n + n))" apply (rule some_equality[symmetric]) - apply auto - apply (rule ext)+ + apply (auto simp add: fun_eq_iff) apply (induct_tac x) apply auto done @@ -93,30 +89,32 @@ lemma DEF_WF: "wfP = (\u. \P. (\x. P x) \ (\x. P x \ (\y. u y x \ \ P y)))" unfolding fun_eq_iff - apply (intro allI, rule, intro allI impI, elim exE) - apply (drule_tac wfE_min[to_pred, unfolded mem_def]) - apply assumption - prefer 2 - apply assumption - apply auto[1] - apply (intro wfI_min[to_pred, unfolded mem_def]) - apply (drule_tac x="Q" in spec) - apply auto - apply (rule_tac x="xb" in bexI) - apply (auto simp add: mem_def) - done +proof (intro allI iffI impI wfI_min[to_pred], elim exE wfE_min[to_pred]) + fix P :: "'a \ bool" and xa :: "'a" + assume "P xa" + then show "xa \ Collect P" by simp +next + fix x P xa z + assume "P xa" "z \ {a. P a}" "\y. x y z \ y \ {a. P a}" + then show "\xa. P xa \ (\y. x y xa \ \ P y)" by auto +next + fix x :: "'a \ 'a \ bool" and xa :: "'a" and Q + assume a: "xa \ Q" + assume b: "\P. Ex P \ (\xa. P xa \ (\y. x y xa \ \ P y))" + then have "Ex (\x. x \ Q) \ (\xa. (\x. x \ Q) xa \ (\y. x y xa \ \ (\x. x \ Q) y))" by auto + then show "\z\Q. \y. x y z \ y \ Q" using a by auto +qed -lemma DEF_UNIV: "UNIV = (%x. True)" - by (auto simp add: mem_def) +lemma DEF_UNIV: "top = (%x. True)" + by (rule ext) (simp add: top1I) lemma DEF_UNIONS: "Sup = (\u. {ua. \x. (\ua. ua \ u \ x \ ua) \ ua = x})" - by (simp add: fun_eq_iff Collect_def) - (metis UnionE complete_lattice_class.Sup_upper mem_def predicate1D) + by (auto simp add: Union_eq) lemma DEF_UNION: "op \ = (\u ua. {ub. \x. (x \ u \ x \ ua) \ ub = x})" - by (auto simp add: mem_def fun_eq_iff Collect_def) + by auto lemma DEF_SUBSET: "op \ = (\u ua. \x. x \ u \ x \ ua)" by (metis set_rev_mp subsetI) @@ -129,7 +127,7 @@ definition [simp, hol4rew]: "SETSPEC x P y \ P & x = y" lemma DEF_PSUBSET: "op \ = (\u ua. u \ ua & u \ ua)" - by (auto simp add: mem_def fun_eq_iff) + by (metis psubset_eq) definition [hol4rew]: "Pred n = n - (Suc 0)" @@ -174,8 +172,8 @@ definition "MEASURE = (%u x y. (u x :: nat) < u y)" lemma [hol4rew]: - "MEASURE u = (%a b. measure u (a, b))" - unfolding MEASURE_def measure_def fun_eq_iff inv_image_def Collect_def + "MEASURE u = (%a b. (a, b) \ measure u)" + unfolding MEASURE_def measure_def by simp definition @@ -187,12 +185,11 @@ lemma DEF_INTERS: "Inter = (\u. {ua. \x. (\ua. ua \ u \ x \ ua) \ ua = x})" - by (auto simp add: fun_eq_iff mem_def Collect_def) - (metis InterD InterI mem_def)+ + by auto lemma DEF_INTER: "op \ = (\u ua. {ub. \x. (x \ u \ x \ ua) \ ub = x})" - by (auto simp add: mem_def fun_eq_iff Collect_def) + by auto lemma DEF_INSERT: "insert = (%u ua y. y \ ua | y = u)" @@ -202,10 +199,6 @@ "op ` = (\u ua. {ub. \y. (\x. x \ ua \ y = u x) \ ub = y})" by (simp add: fun_eq_iff image_def Bex_def) -lemma DEF_GSPEC: - "Collect = (\u. u)" - by (simp add: Collect_def ext) - lemma DEF_GEQ: "(op =) = (op =)" by simp @@ -226,9 +219,7 @@ apply (erule finite_induct) apply auto[2] apply (drule_tac x="finite" in spec) - apply auto - apply (metis Collect_def Collect_empty_eq finite.emptyI) - by (metis (no_types) finite.insertI predicate1I sup.commute sup_absorb1) + by (metis finite_insert infinite_imp_nonempty infinite_super predicate1I) lemma DEF_FACT: "fact = (SOME FACT. FACT 0 = 1 & (\n. FACT (Suc n) = Suc n * FACT n))" @@ -260,10 +251,9 @@ apply simp_all done -lemma DEF_EMPTY: "{} = (%x. False)" - unfolding fun_eq_iff empty_def - by auto - +lemma DEF_EMPTY: "bot = (%x. False)" + by (rule ext) auto + lemma DEF_DIV: "op div = (SOME q. \r. \m n. if n = (0 :: nat) then q m n = 0 \ r m n = m else m = q m n * n + r m n \ r m n < n)" @@ -286,8 +276,7 @@ lemma DEF_DIFF: "op - = (\u ua. {ub. \x. (x \ u \ x \ ua) \ ub = x})" - by (simp add: fun_eq_iff Collect_def) - (metis DiffE DiffI mem_def) + by (metis set_diff_eq) definition [hol4rew]: "DELETE s e = s - {e}" @@ -345,11 +334,8 @@ lemma DEF_CHOICE: "Eps = (%u. SOME x. x \ u)" by (simp add: mem_def) -definition dotdot :: "nat => nat => nat => bool" - where "dotdot == %(u::nat) ua::nat. {ub::nat. EX x::nat. (u <= x & x <= ua) & ub = x}" - -lemma DEF__dot__dot_: "dotdot = (%u ua. {ub. EX x. (u <= x & x <= ua) & ub = x})" - by (simp add: dotdot_def) +definition dotdot :: "nat => nat => nat set" + where "dotdot u ua = {ub. EX x. (u <= x & x <= ua) & ub = x}" lemma [hol4rew]: "dotdot a b = {a..b}" unfolding fun_eq_iff atLeastAtMost_def atLeast_def atMost_def dotdot_def diff -r 076a45f65e12 -r 8a2fd7418435 src/HOL/Import/HOLLightReal.thy --- a/src/HOL/Import/HOLLightReal.thy Wed Aug 31 13:28:29 2011 -0700 +++ b/src/HOL/Import/HOLLightReal.thy Thu Sep 01 16:16:25 2011 +0900 @@ -301,10 +301,7 @@ "(\(x :: real). P x) \ (\(M :: real). \x. P x \ x \ M) \ (\M. (\x. P x \ x \ M) \ (\M'. (\x. P x \ x \ M') \ M \ M'))" - apply (intro allI impI, elim conjE) - apply (drule complete_real[unfolded Ball_def mem_def]) - apply simp_all - done + using complete_real[unfolded Ball_def, of "Collect P"] by auto lemma REAL_COMPLETE_SOMEPOS: "(\(x :: real). P x \ 0 \ x) \ (\M. \x. P x \ x \ M) \