src/HOL/Import/HOL4Compat.thy
 changeset 41550 efa734d9b221 parent 41413 64cd30d6b0b8 child 44690 b6d8b11ed399
1.1 --- a/src/HOL/Import/HOL4Compat.thy	Fri Jan 14 15:43:04 2011 +0100
1.2 +++ b/src/HOL/Import/HOL4Compat.thy	Fri Jan 14 15:44:47 2011 +0100
1.3 @@ -64,10 +64,10 @@
1.4    by simp
1.6  lemma sum_case_def: "(ALL f g x. sum_case f g (Inl x) = f x) & (ALL f g y. sum_case f g (Inr y) = g y)"
1.7 -  by simp;
1.8 +  by simp
1.10  lemma one: "ALL v. v = ()"
1.11 -  by simp;
1.12 +  by simp
1.14  lemma option_case_def: "(!u f. option_case u f None = u) & (!u f x. option_case u f (Some x) = f x)"
1.15    by simp
1.16 @@ -103,7 +103,7 @@
1.17    by (simp add: map_pair_def split_def)
1.19  lemma pair_case_def: "split = split"
1.20 -  ..;
1.21 +  ..
1.23  lemma LESS_OR_EQ: "m <= (n::nat) = (m < n | m = n)"
1.24    by auto
1.25 @@ -128,12 +128,12 @@
1.27  lemma LESS_DEF: "m < n = (? P. (!n. P (Suc n) --> P n) & P m & ~P n)"
1.28  proof safe
1.29 -  assume "m < n"
1.30 +  assume 1: "m < n"
1.31    def P == "%n. n <= m"
1.32    have "(!n. P (Suc n) \<longrightarrow> P n) & P m & ~P n"
1.33    proof (auto simp add: P_def)
1.34      assume "n <= m"
1.35 -    from prems
1.36 +    with 1
1.37      show False
1.38        by auto
1.39    qed
1.40 @@ -187,7 +187,7 @@
1.41      show "m < n"
1.42        ..
1.43    qed
1.44 -qed;
1.45 +qed
1.47  definition FUNPOW :: "('a => 'a) => nat => 'a => 'a" where
1.48    "FUNPOW f n == f ^^ n"
1.49 @@ -242,10 +242,10 @@
1.50    by auto
1.52  lemma num_case_def: "(!b f. nat_case b f 0 = b) & (!b f n. nat_case b f (Suc n) = f n)"
1.53 -  by simp;
1.54 +  by simp
1.56  lemma divides_def: "(a::nat) dvd b = (? q. b = q * a)"
1.57 -  by (auto simp add: dvd_def);
1.58 +  by (auto simp add: dvd_def)
1.60  lemma list_case_def: "(!v f. list_case v f [] = v) & (!v f a0 a1. list_case v f (a0#a1) = f a0 a1)"
1.61    by simp
1.62 @@ -263,21 +263,21 @@
1.63             (list_case v f M = list_case v' f' M')"
1.64  proof clarify
1.65    fix M M' v f
1.66 -  assume "M' = [] \<longrightarrow> v = v'"
1.67 -    and "!a0 a1. M' = a0 # a1 \<longrightarrow> f a0 a1 = f' a0 a1"
1.68 +  assume 1: "M' = [] \<longrightarrow> v = v'"
1.69 +    and 2: "!a0 a1. M' = a0 # a1 \<longrightarrow> f a0 a1 = f' a0 a1"
1.70    show "list_case v f M' = list_case v' f' M'"
1.71    proof (rule List.list.case_cong)
1.72      show "M' = M'"
1.73        ..
1.74    next
1.75      assume "M' = []"
1.76 -    with prems
1.77 +    with 1 2
1.78      show "v = v'"
1.79        by auto
1.80    next
1.81      fix a0 a1
1.82      assume "M' = a0 # a1"
1.83 -    with prems
1.84 +    with 1 2
1.85      show "f a0 a1 = f' a0 a1"
1.86        by auto
1.87    qed
1.88 @@ -302,14 +302,14 @@
1.89      by auto
1.90  next
1.91    fix fn1 fn2
1.92 -  assume "ALL h t. fn1 (h # t) = f (fn1 t) h t"
1.93 -  assume "ALL h t. fn2 (h # t) = f (fn2 t) h t"
1.94 -  assume "fn2 [] = fn1 []"
1.95 +  assume 1: "ALL h t. fn1 (h # t) = f (fn1 t) h t"
1.96 +  assume 2: "ALL h t. fn2 (h # t) = f (fn2 t) h t"
1.97 +  assume 3: "fn2 [] = fn1 []"
1.98    show "fn1 = fn2"
1.99    proof
1.100      fix xs
1.101      show "fn1 xs = fn2 xs"
1.102 -      by (induct xs,simp_all add: prems)
1.103 +      by (induct xs) (simp_all add: 1 2 3)
1.104    qed
1.105  qed
1.107 @@ -411,7 +411,7 @@
1.110  lemma REVERSE: "(rev [] = []) & (!h t. rev (h#t) = (rev t) @ [h])"
1.111 -  by simp;
1.112 +  by simp
1.114  lemma REAL_SUP_ALLPOS: "\<lbrakk> ALL x. P (x::real) \<longrightarrow> 0 < x ; EX x. P x; EX z. ALL x. P x \<longrightarrow> x < z \<rbrakk> \<Longrightarrow> EX s. ALL y. (EX x. P x & y < x) = (y < s)"
1.115  proof safe
1.116 @@ -424,12 +424,11 @@
1.117      show "ALL x : Collect P. 0 < x"
1.118      proof safe
1.119        fix x
1.120 -      assume "P x"
1.121 +      assume P: "P x"
1.122        from allx
1.123        have "P x \<longrightarrow> 0 < x"
1.124          ..
1.125 -      thus "0 < x"
1.126 -        by (simp add: prems)
1.127 +      with P show "0 < x" by simp
1.128      qed
1.129    next
1.130      from px
1.131 @@ -461,7 +460,7 @@
1.132    by simp
1.134  lemma REAL_LT_TOTAL: "((x::real) = y) | x < y | y < x"
1.135 -  by auto;
1.136 +  by auto
1.138  lemma [hol4rew]: "real (0::nat) = 0"
1.139    by simp