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.5  
     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.9  
    1.10  lemma one: "ALL v. v = ()"
    1.11 -  by simp;
    1.12 +  by simp
    1.13  
    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.18  
    1.19  lemma pair_case_def: "split = split"
    1.20 -  ..;
    1.21 +  ..
    1.22  
    1.23  lemma LESS_OR_EQ: "m <= (n::nat) = (m < n | m = n)"
    1.24    by auto
    1.25 @@ -128,12 +128,12 @@
    1.26  
    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.46  
    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.51  
    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.55  
    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.59  
    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.106  
   1.107 @@ -411,7 +411,7 @@
   1.108    by (simp add: Let_def)
   1.109  
   1.110  lemma REVERSE: "(rev [] = []) & (!h t. rev (h#t) = (rev t) @ [h])"
   1.111 -  by simp;
   1.112 +  by simp
   1.113  
   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.133  
   1.134  lemma REAL_LT_TOTAL: "((x::real) = y) | x < y | y < x"
   1.135 -  by auto;
   1.136 +  by auto
   1.137  
   1.138  lemma [hol4rew]: "real (0::nat) = 0"
   1.139    by simp