thys/MyFirst.thy~
changeset 16 a92c10af61bd
child 20 c11651bbebf5
equal deleted inserted replaced
15:bdabf71fa35b 16:a92c10af61bd
       
     1 theory MyFirst
       
     2 imports Main
       
     3 begin
       
     4 
       
     5 datatype 'a list = Nil | Cons 'a "'a list"
       
     6 
       
     7 fun app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
       
     8 "app Nil ys = ys" |
       
     9 "app (Cons x xs) ys = Cons x (app xs ys)"
       
    10 
       
    11 fun rev :: "'a list \<Rightarrow> 'a list" where
       
    12 "rev Nil = Nil" |
       
    13 "rev (Cons x xs) = app (rev xs) (Cons x Nil)"
       
    14 
       
    15 value "rev(Cons True (Cons False Nil))"
       
    16 
       
    17 value "1 + (2::nat)"
       
    18 value "1 + (2::int)"
       
    19 value "1 - (2::nat)"
       
    20 value "1 - (2::int)"
       
    21 
       
    22 lemma app_Nil2 [simp]: "app xs Nil = xs"
       
    23 apply(induction xs)
       
    24 apply(auto)
       
    25 done
       
    26 
       
    27 lemma app_assoc [simp]: "app (app xs ys) zs = app xs (app ys zs)"
       
    28 apply(induction xs)
       
    29 apply(auto)
       
    30 done
       
    31 
       
    32 lemma rev_app [simp]: "rev(app xs ys) = app (rev ys) (rev xs)"
       
    33 apply (induction xs)
       
    34 apply (auto)
       
    35 done
       
    36 
       
    37 theorem rev_rev [simp]: "rev(rev xs) = xs"
       
    38 apply (induction xs)
       
    39 apply (auto)
       
    40 done
       
    41 
       
    42 fun add :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
       
    43 "add 0 n = n" |
       
    44 "add (Suc m) n = Suc(add m n)"
       
    45 
       
    46 lemma add_02: "add m 0 = m"
       
    47 apply(induction m)
       
    48 apply(auto)
       
    49 done
       
    50 
       
    51 value "add 2 3"
       
    52 
       
    53 lemma add_04: "add m (add n k) = add k (add m n)"
       
    54 apply(induct)
       
    55 apply(auto)
       
    56 oops
       
    57 
       
    58 fun dub :: "nat \<Rightarrow> nat" where
       
    59 "dub 0 = 0" |
       
    60 "dub m = add m m"
       
    61 
       
    62 lemma dub_01: "dub 0 = 0"
       
    63 apply(induct)
       
    64 apply(auto)
       
    65 done
       
    66 
       
    67 lemma dub_02: "dub m = add m m"
       
    68 apply(induction m)
       
    69 apply(auto)
       
    70 done
       
    71 
       
    72 value "dub 2"
       
    73 
       
    74 fun trip :: "nat \<Rightarrow> nat" where
       
    75 "trip 0 = 0" |
       
    76 "trip m = add m (add m m)"
       
    77 
       
    78 lemma trip_01: "trip 0 = 0"
       
    79 apply(induct)
       
    80 apply(auto)
       
    81 done
       
    82 
       
    83 lemma trip_02: "trip m = add m (add m m)"
       
    84 apply(induction m)
       
    85 apply(auto)
       
    86 done
       
    87 
       
    88 value "trip 1"
       
    89 value "trip 2"
       
    90 
       
    91 fun mull :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
       
    92 "mull 0 0 = 0" |
       
    93 "mull m 0 = 0" |
       
    94 "mull m 1 = m" |
       
    95 "mull m n = 0" 
       
    96 
       
    97 (**
       
    98 fun count :: "'a\<Rightarrow>'a list\<Rightarrow>nat" where
       
    99 "count  "
       
   100 **)
       
   101 
       
   102 
       
   103 
       
   104 
       
   105 
       
   106 
       
   107 
       
   108 
       
   109 
       
   110