# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# 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:
-  "\<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
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 @@
   "(\<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>