--- 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)
--- 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"
--- 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:
- "\<forall>e f. \<exists>!fn. fn 0 = e \<and> (\<forall>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)
+ "\<exists>!fn. fn 0 = e \<and> (\<forall>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:
"\<forall>m n. Suc m = Suc n \<longleftrightarrow> m = n"
- by auto
+ by simp
lemma PAIR:
"(fst x, snd x) = x"
@@ -47,8 +44,7 @@
lemma DEF__star_:
"op * = (SOME mult. (\<forall>n. mult 0 n = 0) \<and> (\<forall>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 = (\<lambda>u. \<forall>P. (\<exists>x. P x) \<longrightarrow> (\<exists>x. P x \<and> (\<forall>y. u y x \<longrightarrow> \<not> 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 \<Rightarrow> bool" and xa :: "'a"
+ assume "P xa"
+ then show "xa \<in> Collect P" by simp
+next
+ fix x P xa z
+ assume "P xa" "z \<in> {a. P a}" "\<And>y. x y z \<Longrightarrow> y \<notin> {a. P a}"
+ then show "\<exists>xa. P xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> P y)" by auto
+next
+ fix x :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and xa :: "'a" and Q
+ assume a: "xa \<in> Q"
+ assume b: "\<forall>P. Ex P \<longrightarrow> (\<exists>xa. P xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> P y))"
+ then have "Ex (\<lambda>x. x \<in> Q) \<longrightarrow> (\<exists>xa. (\<lambda>x. x \<in> Q) xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> (\<lambda>x. x \<in> Q) y))" by auto
+ then show "\<exists>z\<in>Q. \<forall>y. x y z \<longrightarrow> y \<notin> 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 = (\<lambda>u. {ua. \<exists>x. (\<exists>ua. ua \<in> u \<and> x \<in> ua) \<and> 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 \<union> = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<or> x \<in> ua) \<and> ub = x})"
- by (auto simp add: mem_def fun_eq_iff Collect_def)
+ by auto
lemma DEF_SUBSET: "op \<subseteq> = (\<lambda>u ua. \<forall>x. x \<in> u \<longrightarrow> x \<in> ua)"
by (metis set_rev_mp subsetI)
@@ -129,7 +127,7 @@
definition [simp, hol4rew]: "SETSPEC x P y \<longleftrightarrow> P & x = y"
lemma DEF_PSUBSET: "op \<subset> = (\<lambda>u ua. u \<subseteq> ua & u \<noteq> 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) \<in> measure u)"
+ unfolding MEASURE_def measure_def
by simp
definition
@@ -187,12 +185,11 @@
lemma DEF_INTERS:
"Inter = (\<lambda>u. {ua. \<exists>x. (\<forall>ua. ua \<in> u \<longrightarrow> x \<in> ua) \<and> ua = x})"
- by (auto simp add: fun_eq_iff mem_def Collect_def)
- (metis InterD InterI mem_def)+
+ by auto
lemma DEF_INTER:
"op \<inter> = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<and> x \<in> ua) \<and> ub = x})"
- by (auto simp add: mem_def fun_eq_iff Collect_def)
+ by auto
lemma DEF_INSERT:
"insert = (%u ua y. y \<in> ua | y = u)"
@@ -202,10 +199,6 @@
"op ` = (\<lambda>u ua. {ub. \<exists>y. (\<exists>x. x \<in> ua \<and> y = u x) \<and> ub = y})"
by (simp add: fun_eq_iff image_def Bex_def)
-lemma DEF_GSPEC:
- "Collect = (\<lambda>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 & (\<forall>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. \<exists>r. \<forall>m n. if n = (0 :: nat) then q m n = 0 \<and> r m n = m
else m = q m n * n + r m n \<and> r m n < n)"
@@ -286,8 +276,7 @@
lemma DEF_DIFF:
"op - = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<and> x \<notin> ua) \<and> 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 \<in> 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
--- 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 @@
"(\<exists>(x :: real). P x) \<and> (\<exists>(M :: real). \<forall>x. P x \<longrightarrow> x \<le> M) \<longrightarrow>
(\<exists>M. (\<forall>x. P x \<longrightarrow> x \<le> M) \<and>
(\<forall>M'. (\<forall>x. P x \<longrightarrow> x \<le> M') \<longrightarrow> M \<le> 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:
"(\<exists>(x :: real). P x \<and> 0 \<le> x) \<and> (\<exists>M. \<forall>x. P x \<longrightarrow> x \<le> M) \<longrightarrow>