HOL/Import: observe distinction between sets and predicates (where possible)
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Thu Sep 01 16:16:25 2011 +0900 (2011-09-01 ago)
changeset 446338a2fd7418435
parent 44632 076a45f65e12
child 44634 2ac4ff398bc3
HOL/Import: observe distinction between sets and predicates (where possible)
src/HOL/Import/HOLLight/HOLLight.thy
src/HOL/Import/HOLLight/hollight.imp
src/HOL/Import/HOLLightCompat.thy
src/HOL/Import/HOLLightReal.thy
     1.1 --- a/src/HOL/Import/HOLLight/HOLLight.thy	Wed Aug 31 13:28:29 2011 -0700
     1.2 +++ b/src/HOL/Import/HOLLight/HOLLight.thy	Thu Sep 01 16:16:25 2011 +0900
     1.3 @@ -759,12 +759,12 @@
     1.4  ==> EX f::nat => 'A. ALL x::nat. f x = H f x"
     1.5    by (import hollight WF_REC_num)
     1.6  
     1.7 -lemma WF_MEASURE: "wfP (%(a::'A) b::'A. measure (m::'A => nat) (a, b))"
     1.8 +lemma WF_MEASURE: "wfP (%(a::'A) b::'A. (a, b) : measure (m::'A => nat))"
     1.9    by (import hollight WF_MEASURE)
    1.10  
    1.11  lemma MEASURE_LE: "(ALL x::'q_12099.
    1.12 -    measure (m::'q_12099 => nat) (x, a::'q_12099) -->
    1.13 -    measure m (x, b::'q_12099)) =
    1.14 +    (x, a::'q_12099) : measure (m::'q_12099 => nat) -->
    1.15 +    (x, b::'q_12099) : measure m) =
    1.16  (m a <= m b)"
    1.17    by (import hollight MEASURE_LE)
    1.18  
     2.1 --- a/src/HOL/Import/HOLLight/hollight.imp	Wed Aug 31 13:28:29 2011 -0700
     2.2 +++ b/src/HOL/Import/HOLLight/hollight.imp	Thu Sep 01 16:16:25 2011 +0900
     2.3 @@ -590,6 +590,8 @@
     2.4    "UNIONS_INSERT" > "Complete_Lattice.Union_insert"
     2.5    "UNIONS_IMAGE" > "HOLLight.hollight.UNIONS_IMAGE"
     2.6    "UNIONS_GSPEC" > "HOLLight.hollight.UNIONS_GSPEC"
     2.7 +  "UNIONS_2" > "Complete_Lattice.Un_eq_Union"
     2.8 +  "UNIONS_1" > "Complete_Lattice.complete_lattice_class.Sup_singleton"
     2.9    "UNIONS_0" > "Complete_Lattice.Union_empty"
    2.10    "UNCURRY_def" > "HOLLight.hollight.UNCURRY_def"
    2.11    "TYDEF_recspace" > "HOLLight.hollight.TYDEF_recspace"
    2.12 @@ -1595,6 +1597,8 @@
    2.13    "INTERS_INSERT" > "Complete_Lattice.Inter_insert"
    2.14    "INTERS_IMAGE" > "HOLLight.hollight.INTERS_IMAGE"
    2.15    "INTERS_GSPEC" > "HOLLight.hollight.INTERS_GSPEC"
    2.16 +  "INTERS_2" > "Complete_Lattice.Int_eq_Inter"
    2.17 +  "INTERS_1" > "Complete_Lattice.complete_lattice_class.Inf_singleton"
    2.18    "INTERS_0" > "Complete_Lattice.Inter_empty"
    2.19    "INSERT_UNIV" > "HOLLight.hollight.INSERT_UNIV"
    2.20    "INSERT_UNION_EQ" > "Set.Un_insert_left"
    2.21 @@ -1684,7 +1688,7 @@
    2.22    "HAS_SIZE_0" > "HOLLight.hollight.HAS_SIZE_0"
    2.23    "GE_C" > "HOLLight.hollight.GE_C"
    2.24    "FUN_IN_IMAGE" > "Set.imageI"
    2.25 -  "FUN_EQ_THM" > "Fun.fun_eq_iff"
    2.26 +  "FUN_EQ_THM" > "HOL.fun_eq_iff"
    2.27    "FUNCTION_FACTORS_RIGHT" > "HOLLight.hollight.FUNCTION_FACTORS_RIGHT"
    2.28    "FUNCTION_FACTORS_LEFT" > "HOLLight.hollight.FUNCTION_FACTORS_LEFT"
    2.29    "FST" > "Product_Type.fst_conv"
    2.30 @@ -2010,7 +2014,7 @@
    2.31    "DEF__equal__equal__greaterthan_" > "HOLLightCompat.DEF__equal__equal__greaterthan_"
    2.32    "DEF__equal__equal_" > "HOLLight.hollight.DEF__equal__equal_"
    2.33    "DEF__equal__c" > "HOLLight.hollight.DEF__equal__c"
    2.34 -  "DEF__dot__dot_" > "HOLLightCompat.DEF__dot__dot_"
    2.35 +  "DEF__dot__dot_" > "HOLLightCompat.dotdot_def"
    2.36    "DEF__backslash__slash_" > "HOL.or_def"
    2.37    "DEF__UNGUARDED_PATTERN" > "HOLLight.hollight.DEF__UNGUARDED_PATTERN"
    2.38    "DEF__SEQPATTERN" > "HOLLight.hollight.DEF__SEQPATTERN"
    2.39 @@ -2080,7 +2084,7 @@
    2.40    "DEF_IMAGE" > "HOLLightCompat.DEF_IMAGE"
    2.41    "DEF_I" > "Fun.id_apply"
    2.42    "DEF_HAS_SIZE" > "HOLLight.hollight.DEF_HAS_SIZE"
    2.43 -  "DEF_GSPEC" > "HOLLightCompat.DEF_GSPEC"
    2.44 +  "DEF_GSPEC" > "Set.Collect_def"
    2.45    "DEF_GEQ" > "HOLLightCompat.DEF_GEQ"
    2.46    "DEF_GABS" > "HOLLightCompat.DEF_GABS"
    2.47    "DEF_FST" > "HOLLightCompat.DEF_FST"
     3.1 --- a/src/HOL/Import/HOLLightCompat.thy	Wed Aug 31 13:28:29 2011 -0700
     3.2 +++ b/src/HOL/Import/HOLLightCompat.thy	Thu Sep 01 16:16:25 2011 +0900
     3.3 @@ -22,19 +22,16 @@
     3.4    by simp
     3.5  
     3.6  lemma num_Axiom:
     3.7 -  "\<forall>e f. \<exists>!fn. fn 0 = e \<and> (\<forall>n. fn (Suc n) = f (fn n) n)"
     3.8 -  apply (intro allI)
     3.9 -  apply (rule_tac a="nat_rec e (%n e. f e n)" in ex1I)
    3.10 -  apply auto
    3.11 -  apply (simp add: fun_eq_iff)
    3.12 -  apply (intro allI)
    3.13 -  apply (induct_tac xa)
    3.14 +  "\<exists>!fn. fn 0 = e \<and> (\<forall>n. fn (Suc n) = f (fn n) n)"
    3.15 +  apply (rule ex1I[of _ "nat_rec e (%n e. f e n)"])
    3.16 +  apply (auto simp add: fun_eq_iff)
    3.17 +  apply (induct_tac x)
    3.18    apply simp_all
    3.19    done
    3.20  
    3.21  lemma SUC_INJ:
    3.22    "\<forall>m n. Suc m = Suc n \<longleftrightarrow> m = n"
    3.23 -  by auto
    3.24 +  by simp
    3.25  
    3.26  lemma PAIR:
    3.27    "(fst x, snd x) = x"
    3.28 @@ -47,8 +44,7 @@
    3.29  lemma DEF__star_:
    3.30    "op * = (SOME mult. (\<forall>n. mult 0 n = 0) \<and> (\<forall>m n. mult (Suc m) n = mult m n + n))"
    3.31    apply (rule some_equality[symmetric])
    3.32 -  apply auto
    3.33 -  apply (rule ext)+
    3.34 +  apply (auto simp add: fun_eq_iff)
    3.35    apply (induct_tac x)
    3.36    apply auto
    3.37    done
    3.38 @@ -93,30 +89,32 @@
    3.39  lemma DEF_WF:
    3.40    "wfP = (\<lambda>u. \<forall>P. (\<exists>x. P x) \<longrightarrow> (\<exists>x. P x \<and> (\<forall>y. u y x \<longrightarrow> \<not> P y)))"
    3.41    unfolding fun_eq_iff
    3.42 -  apply (intro allI, rule, intro allI impI, elim exE)
    3.43 -  apply (drule_tac wfE_min[to_pred, unfolded mem_def])
    3.44 -  apply assumption
    3.45 -  prefer 2
    3.46 -  apply assumption
    3.47 -  apply auto[1]
    3.48 -  apply (intro wfI_min[to_pred, unfolded mem_def])
    3.49 -  apply (drule_tac x="Q" in spec)
    3.50 -  apply auto
    3.51 -  apply (rule_tac x="xb" in bexI)
    3.52 -  apply (auto simp add: mem_def)
    3.53 -  done
    3.54 +proof (intro allI iffI impI wfI_min[to_pred], elim exE wfE_min[to_pred])
    3.55 +  fix P :: "'a \<Rightarrow> bool" and xa :: "'a"
    3.56 +  assume "P xa"
    3.57 +  then show "xa \<in> Collect P" by simp
    3.58 +next
    3.59 +  fix x P xa z
    3.60 +  assume "P xa" "z \<in> {a. P a}" "\<And>y. x y z \<Longrightarrow> y \<notin> {a. P a}"
    3.61 +  then show "\<exists>xa. P xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> P y)" by auto
    3.62 +next
    3.63 +  fix x :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and xa :: "'a" and Q
    3.64 +  assume a: "xa \<in> Q"
    3.65 +  assume b: "\<forall>P. Ex P \<longrightarrow> (\<exists>xa. P xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> P y))"
    3.66 +  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
    3.67 +  then show "\<exists>z\<in>Q. \<forall>y. x y z \<longrightarrow> y \<notin> Q" using a by auto
    3.68 +qed
    3.69  
    3.70 -lemma DEF_UNIV: "UNIV = (%x. True)"
    3.71 -  by (auto simp add: mem_def)
    3.72 +lemma DEF_UNIV: "top = (%x. True)"
    3.73 +  by (rule ext) (simp add: top1I)
    3.74  
    3.75  lemma DEF_UNIONS:
    3.76    "Sup = (\<lambda>u. {ua. \<exists>x. (\<exists>ua. ua \<in> u \<and> x \<in> ua) \<and> ua = x})"
    3.77 -  by (simp add: fun_eq_iff Collect_def)
    3.78 -     (metis UnionE complete_lattice_class.Sup_upper mem_def predicate1D)
    3.79 +  by (auto simp add: Union_eq)
    3.80  
    3.81  lemma DEF_UNION:
    3.82    "op \<union> = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<or> x \<in> ua) \<and> ub = x})"
    3.83 -  by (auto simp add: mem_def fun_eq_iff Collect_def)
    3.84 +  by auto
    3.85  
    3.86  lemma DEF_SUBSET: "op \<subseteq> = (\<lambda>u ua. \<forall>x. x \<in> u \<longrightarrow> x \<in> ua)"
    3.87    by (metis set_rev_mp subsetI)
    3.88 @@ -129,7 +127,7 @@
    3.89  definition [simp, hol4rew]: "SETSPEC x P y \<longleftrightarrow> P & x = y"
    3.90  
    3.91  lemma DEF_PSUBSET: "op \<subset> = (\<lambda>u ua. u \<subseteq> ua & u \<noteq> ua)"
    3.92 -  by (auto simp add: mem_def fun_eq_iff)
    3.93 +  by (metis psubset_eq)
    3.94  
    3.95  definition [hol4rew]: "Pred n = n - (Suc 0)"
    3.96  
    3.97 @@ -174,8 +172,8 @@
    3.98  definition "MEASURE = (%u x y. (u x :: nat) < u y)"
    3.99  
   3.100  lemma [hol4rew]:
   3.101 -  "MEASURE u = (%a b. measure u (a, b))"
   3.102 -  unfolding MEASURE_def measure_def fun_eq_iff inv_image_def Collect_def
   3.103 +  "MEASURE u = (%a b. (a, b) \<in> measure u)"
   3.104 +  unfolding MEASURE_def measure_def
   3.105    by simp
   3.106  
   3.107  definition
   3.108 @@ -187,12 +185,11 @@
   3.109  
   3.110  lemma DEF_INTERS:
   3.111    "Inter = (\<lambda>u. {ua. \<exists>x. (\<forall>ua. ua \<in> u \<longrightarrow> x \<in> ua) \<and> ua = x})"
   3.112 -  by (auto simp add: fun_eq_iff mem_def Collect_def)
   3.113 -     (metis InterD InterI mem_def)+
   3.114 +  by auto
   3.115  
   3.116  lemma DEF_INTER:
   3.117    "op \<inter> = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<and> x \<in> ua) \<and> ub = x})"
   3.118 -  by (auto simp add: mem_def fun_eq_iff Collect_def)
   3.119 +  by auto
   3.120  
   3.121  lemma DEF_INSERT:
   3.122    "insert = (%u ua y. y \<in> ua | y = u)"
   3.123 @@ -202,10 +199,6 @@
   3.124    "op ` = (\<lambda>u ua. {ub. \<exists>y. (\<exists>x. x \<in> ua \<and> y = u x) \<and> ub = y})"
   3.125    by (simp add: fun_eq_iff image_def Bex_def)
   3.126  
   3.127 -lemma DEF_GSPEC:
   3.128 -  "Collect = (\<lambda>u. u)"
   3.129 -  by (simp add: Collect_def ext)
   3.130 -
   3.131  lemma DEF_GEQ:
   3.132    "(op =) = (op =)"
   3.133    by simp
   3.134 @@ -226,9 +219,7 @@
   3.135    apply (erule finite_induct)
   3.136    apply auto[2]
   3.137    apply (drule_tac x="finite" in spec)
   3.138 -  apply auto
   3.139 -  apply (metis Collect_def Collect_empty_eq finite.emptyI)
   3.140 -  by (metis (no_types) finite.insertI predicate1I sup.commute sup_absorb1)
   3.141 +  by (metis finite_insert infinite_imp_nonempty infinite_super predicate1I)
   3.142  
   3.143  lemma DEF_FACT:
   3.144    "fact = (SOME FACT. FACT 0 = 1 & (\<forall>n. FACT (Suc n) = Suc n * FACT n))"
   3.145 @@ -260,10 +251,9 @@
   3.146    apply simp_all
   3.147    done
   3.148  
   3.149 -lemma DEF_EMPTY: "{} = (%x. False)"
   3.150 -  unfolding fun_eq_iff empty_def
   3.151 -  by auto
   3.152 -
   3.153 +lemma DEF_EMPTY: "bot = (%x. False)"
   3.154 +  by (rule ext) auto
   3.155 +  
   3.156  lemma DEF_DIV:
   3.157    "op div = (SOME q. \<exists>r. \<forall>m n. if n = (0 :: nat) then q m n = 0 \<and> r m n = m
   3.158       else m = q m n * n + r m n \<and> r m n < n)"
   3.159 @@ -286,8 +276,7 @@
   3.160  
   3.161  lemma DEF_DIFF:
   3.162    "op - = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<and> x \<notin> ua) \<and> ub = x})"
   3.163 -  by (simp add: fun_eq_iff Collect_def)
   3.164 -     (metis DiffE DiffI mem_def)
   3.165 +  by (metis set_diff_eq)
   3.166  
   3.167  definition [hol4rew]: "DELETE s e = s - {e}"
   3.168  
   3.169 @@ -345,11 +334,8 @@
   3.170  lemma DEF_CHOICE: "Eps = (%u. SOME x. x \<in> u)"
   3.171    by (simp add: mem_def)
   3.172  
   3.173 -definition dotdot :: "nat => nat => nat => bool"
   3.174 -  where "dotdot == %(u::nat) ua::nat. {ub::nat. EX x::nat. (u <= x & x <= ua) & ub = x}"
   3.175 -
   3.176 -lemma DEF__dot__dot_: "dotdot = (%u ua. {ub. EX x. (u <= x & x <= ua) & ub = x})"
   3.177 -  by (simp add: dotdot_def)
   3.178 +definition dotdot :: "nat => nat => nat set"
   3.179 +  where "dotdot u ua = {ub. EX x. (u <= x & x <= ua) & ub = x}"
   3.180  
   3.181  lemma [hol4rew]: "dotdot a b = {a..b}"
   3.182    unfolding fun_eq_iff atLeastAtMost_def atLeast_def atMost_def dotdot_def
     4.1 --- a/src/HOL/Import/HOLLightReal.thy	Wed Aug 31 13:28:29 2011 -0700
     4.2 +++ b/src/HOL/Import/HOLLightReal.thy	Thu Sep 01 16:16:25 2011 +0900
     4.3 @@ -301,10 +301,7 @@
     4.4    "(\<exists>(x :: real). P x) \<and> (\<exists>(M :: real). \<forall>x. P x \<longrightarrow> x \<le> M) \<longrightarrow>
     4.5     (\<exists>M. (\<forall>x. P x \<longrightarrow> x \<le> M) \<and>
     4.6            (\<forall>M'. (\<forall>x. P x \<longrightarrow> x \<le> M') \<longrightarrow> M \<le> M'))"
     4.7 -  apply (intro allI impI, elim conjE)
     4.8 -  apply (drule complete_real[unfolded Ball_def mem_def])
     4.9 -  apply simp_all
    4.10 -  done
    4.11 +  using complete_real[unfolded Ball_def, of "Collect P"] by auto
    4.12  
    4.13  lemma REAL_COMPLETE_SOMEPOS:
    4.14    "(\<exists>(x :: real). P x \<and> 0 \<le> x) \<and> (\<exists>M. \<forall>x. P x \<longrightarrow> x \<le> M) \<longrightarrow>