src/HOL/Import/HOL4Compat.thy
changeset 39246 9e58f0499f57
parent 37596 248db70c9bcf
child 40607 30d512bf47a7
     1.1 --- a/src/HOL/Import/HOL4Compat.thy	Wed Sep 08 13:25:22 2010 +0200
     1.2 +++ b/src/HOL/Import/HOL4Compat.thy	Wed Sep 08 19:21:46 2010 +0200
     1.3 @@ -33,17 +33,13 @@
     1.4  (*lemma INL_neq_INR: "ALL v1 v2. Sum_Type.Inr v2 ~= Sum_Type.Inl v1"
     1.5    by simp*)
     1.6  
     1.7 -consts
     1.8 -  ISL :: "'a + 'b => bool"
     1.9 -  ISR :: "'a + 'b => bool"
    1.10 -
    1.11 -primrec ISL_def:
    1.12 +primrec ISL :: "'a + 'b => bool" where
    1.13    "ISL (Inl x) = True"
    1.14 -  "ISL (Inr x) = False"
    1.15 +| "ISL (Inr x) = False"
    1.16  
    1.17 -primrec ISR_def:
    1.18 +primrec ISR :: "'a + 'b => bool" where
    1.19    "ISR (Inl x) = False"
    1.20 -  "ISR (Inr x) = True"
    1.21 +| "ISR (Inr x) = True"
    1.22  
    1.23  lemma ISL: "(ALL x. ISL (Inl x)) & (ALL y. ~ISL (Inr y))"
    1.24    by simp
    1.25 @@ -51,14 +47,10 @@
    1.26  lemma ISR: "(ALL x. ISR (Inr x)) & (ALL y. ~ISR (Inl y))"
    1.27    by simp
    1.28  
    1.29 -consts
    1.30 -  OUTL :: "'a + 'b => 'a"
    1.31 -  OUTR :: "'a + 'b => 'b"
    1.32 -
    1.33 -primrec OUTL_def:
    1.34 +primrec OUTL :: "'a + 'b => 'a" where
    1.35    "OUTL (Inl x) = x"
    1.36  
    1.37 -primrec OUTR_def:
    1.38 +primrec OUTR :: "'a + 'b => 'b" where
    1.39    "OUTR (Inr x) = x"
    1.40  
    1.41  lemma OUTL: "OUTL (Inl x) = x"
    1.42 @@ -79,17 +71,13 @@
    1.43  lemma OPTION_MAP_DEF: "(!f x. Option.map f (Some x) = Some (f x)) & (!f. Option.map f None = None)"
    1.44    by simp
    1.45  
    1.46 -consts
    1.47 -  IS_SOME :: "'a option => bool"
    1.48 -  IS_NONE :: "'a option => bool"
    1.49 -
    1.50 -primrec IS_SOME_def:
    1.51 +primrec IS_SOME :: "'a option => bool" where
    1.52    "IS_SOME (Some x) = True"
    1.53 -  "IS_SOME None = False"
    1.54 +| "IS_SOME None = False"
    1.55  
    1.56 -primrec IS_NONE_def:
    1.57 +primrec IS_NONE :: "'a option => bool" where
    1.58    "IS_NONE (Some x) = False"
    1.59 -  "IS_NONE None = True"
    1.60 +| "IS_NONE None = True"
    1.61  
    1.62  lemma IS_NONE_DEF: "(!x. IS_NONE (Some x) = False) & (IS_NONE None = True)"
    1.63    by simp
    1.64 @@ -97,15 +85,12 @@
    1.65  lemma IS_SOME_DEF: "(!x. IS_SOME (Some x) = True) & (IS_SOME None = False)"
    1.66    by simp
    1.67  
    1.68 -consts
    1.69 -  OPTION_JOIN :: "'a option option => 'a option"
    1.70 -
    1.71 -primrec OPTION_JOIN_def:
    1.72 +primrec OPTION_JOIN :: "'a option option => 'a option" where
    1.73    "OPTION_JOIN None = None"
    1.74 -  "OPTION_JOIN (Some x) = x"
    1.75 +| "OPTION_JOIN (Some x) = x"
    1.76  
    1.77  lemma OPTION_JOIN_DEF: "(OPTION_JOIN None = None) & (ALL x. OPTION_JOIN (Some x) = x)"
    1.78 -  by simp;
    1.79 +  by simp
    1.80  
    1.81  lemma PAIR: "(fst x,snd x) = x"
    1.82    by simp
    1.83 @@ -261,14 +246,11 @@
    1.84  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.85    by simp
    1.86  
    1.87 -consts
    1.88 -  list_size :: "('a \<Rightarrow> nat) \<Rightarrow> 'a list \<Rightarrow> nat"
    1.89 +primrec list_size :: "('a \<Rightarrow> nat) \<Rightarrow> 'a list \<Rightarrow> nat" where
    1.90 +  "list_size f [] = 0"
    1.91 +| "list_size f (a0#a1) = 1 + (f a0 + list_size f a1)"
    1.92  
    1.93 -primrec
    1.94 -  "list_size f [] = 0"
    1.95 -  "list_size f (a0#a1) = 1 + (f a0 + list_size f a1)"
    1.96 -
    1.97 -lemma list_size_def: "(!f. list_size f [] = 0) &
    1.98 +lemma list_size_def': "(!f. list_size f [] = 0) &
    1.99           (!f a0 a1. list_size f (a0#a1) = 1 + (f a0 + list_size f a1))"
   1.100    by simp
   1.101  
   1.102 @@ -377,12 +359,9 @@
   1.103  lemma list_exists_DEF: "(!P. list_ex P [] = False) & (!P h t. list_ex P (h#t) = (P h | list_ex P t))"
   1.104    by simp
   1.105  
   1.106 -consts
   1.107 -  map2 :: "[['a,'b]\<Rightarrow>'c,'a list,'b list] \<Rightarrow> 'c list"
   1.108 -
   1.109 -primrec
   1.110 +primrec map2 :: "[['a,'b]\<Rightarrow>'c,'a list,'b list] \<Rightarrow> 'c list" where
   1.111    map2_Nil: "map2 f [] l2 = []"
   1.112 -  map2_Cons: "map2 f (x#xs) l2 = f x (hd l2) # map2 f xs (tl l2)"
   1.113 +| map2_Cons: "map2 f (x#xs) l2 = f x (hd l2) # map2 f xs (tl l2)"
   1.114  
   1.115  lemma MAP2: "(!f. map2 f [] [] = []) & (!f h1 t1 h2 t2. map2 f (h1#t1) (h2#t2) = f h1 h2#map2 f t1 t2)"
   1.116    by simp
   1.117 @@ -419,12 +398,9 @@
   1.118  lemma [hol4rew]: "ZIP (a,b) = zip a b"
   1.119    by (simp add: ZIP_def)
   1.120  
   1.121 -consts
   1.122 -  unzip :: "('a * 'b) list \<Rightarrow> 'a list * 'b list"
   1.123 -
   1.124 -primrec
   1.125 +primrec unzip :: "('a * 'b) list \<Rightarrow> 'a list * 'b list" where
   1.126    unzip_Nil: "unzip [] = ([],[])"
   1.127 -  unzip_Cons: "unzip (xy#xys) = (let zs = unzip xys in (fst xy # fst zs,snd xy # snd zs))"
   1.128 +| unzip_Cons: "unzip (xy#xys) = (let zs = unzip xys in (fst xy # fst zs,snd xy # snd zs))"
   1.129  
   1.130  lemma UNZIP: "(unzip [] = ([],[])) &
   1.131           (!x l. unzip (x#l) = (fst x#fst (unzip l),snd x#snd (unzip l)))"