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 (**commutative-associative**)

    54 lemma add_04: "add m (add n k) = add k (add m n)"

    55 apply(induct)

    56 apply(auto)

    57 oops

    58 

    59 fun dub :: "nat \<Rightarrow> nat" where

    60 "dub 0 = 0" |

    61 "dub m = add m m"

    62 

    63 lemma dub_01: "dub 0 = 0"

    64 apply(induct)

    65 apply(auto)

    66 done

    67 

    68 lemma dub_02: "dub m = add m m"

    69 apply(induction m)

    70 apply(auto)

    71 done

    72 

    73 value "dub 2"

    74 

    75 fun trip :: "nat \<Rightarrow> nat" where

    76 "trip 0 = 0" |

    77 "trip m = add m (add m m)"

    78 

    79 lemma trip_01: "trip 0 = 0"

    80 apply(induct)

    81 apply(auto)

    82 done

    83 

    84 lemma trip_02: "trip m = add m (add m m)"

    85 apply(induction m)

    86 apply(auto)

    87 done

    88 

    89 value "trip 1"

    90 value "trip 2"

    91 

    92 fun mull :: "nat \<Rightarrow> nat \<Rightarrow> nat" where

    93 "mull 0 0 = 0" |

    94 "mull m 0 = 0" |

    95 (**"mull m 1 = m" | **)

    96 "mull m n = m*n" 

    97 

    98 (**Define a function that counts the

    99 number of occurrences of an element in a list **)

   100 (**

   101 fun count :: "'a\<Rightarrow>'a list\<Rightarrow>nat" where

   102 "count  "

   103 **)

   104 

   105 

   106 

   107 

   108 

   109 

   110 

   111 

   112 

   113