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 fun app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where

    16 "app Nil ys = ys" |

    17 "app (Cons x xs) ys = Cons x (app xs ys)"

    18 

    19 fun rev :: "'a list \<Rightarrow> 'a list" where

    20 "rev Nil = Nil" |

    21 "rev (Cons x xs) = app (rev xs) (Cons x Nil)"Nil))"

    22 

    23 value "1 + (2::nat)"

    24 value "1 + (2::int)"

    25 value "1 - (2::nat)"

    26 value "1 - (2::int)"

    27 

    28 lemma app_Nil2 [simp]: "app xs Nil = xs"

    29 apply(induction xs)

    30 apply(auto)

    31 done

    32 

    33 lemma app_assoc [simp]: "app (app xs ys) zs = app xs (app ys zs)"

    34 apply(induction xs)

    35 apply(auto)

    36 done

    37 

    38 lemma rev_app [simp]: "rev(app xs ys) = app (rev ys) (rev xs)"

    39 apply (induction xs)

    40 apply (auto)

    41 done

    42 

    43 theorem rev_rev [simp]: "rev(rev xs) = xs"

    44 apply (induction xs)

    45 apply (auto)

    46 done

    47 

    48 fun add :: "nat \<Rightarrow> nat \<Rightarrow> nat" where

    49 "add 0 n = n" |

    50 "add (Suc m) n = Suc(add m n)"

    51 

    52 lemma add_02: "add m 0 = m"

    53 apply(induction m)

    54 apply(auto)

    55 done

    56 

    57 value "add 2 3"

    58 

    59 

    60 (**commutative-associative**)

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

    62 apply(induct m)

    63 apply(simp_all)

    64 done

    65 

    66 lemma add_zero: "add n 0 = n"

    67 apply(induct n)

    68 apply(auto)

    69 done

    70 lemma add_zero: "add n 0 = n"

    71 apply(induct n)

    72 apply(auto)

    73 done

    74 lemma add_Suc: "add m (Suc n) = Suc (add m n)"

    75 apply(induct m)

    76 apply(metis add.simps(1))

    77 apply(auto)

    78 done

    79 

    80 lemma add_comm: "add m n = add n m"

    81 apply(induct m)

    82 apply(simp add: add_zero)

    83 apply(simp add: add_Suc)

    84 done

    85 

    86 lemma add_odd: "add m (add n k) = add k (add m n)"

    87 apply(subst add_04)

    88 apply(subst (2) add_comm)

    89 apply(simp)

    90 done

    91 

    92 

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

    94 "dub 0 = 0" |

    95 "dub m = add m m"

    96 

    97 lemma dub_01: "dub 0 = 0"

    98 apply(induct)

    99 apply(auto)

   100 done

   101 

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

   103 apply(induction m)

   104 apply(auto)

   105 done

   106 

   107 value "dub 2"

   108 

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

   110 "trip 0 = 0" |

   111 "trip m = add m (add m m)"

   112 

   113 lemma trip_01: "trip 0 = 0"

   114 apply(induct)

   115 apply(auto)

   116 done

   117 

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

   119 apply(induction m)

   120 apply(auto)

   121 done

   122 

   123 value "trip 1"

   124 value "trip 2"

   125 

   126 fun sum :: "nat \<Rightarrow> nat" where

   127   "sum 0 = 0"

   128 | "sum (Suc n) = (Suc n) + sum n"

   129 

   130 function sum1 :: "nat \<Rightarrow> nat" where

   131   "sum1 0 = 0"

   132 | "n \<noteq> 0 \<Longrightarrow> sum1 n = n + sum1 (n - 1)"

   133 apply(auto)

   134 done

   135 

   136 termination sum1

   137 by (smt2 "termination" diff_less less_than_iff not_gr0 wf_less_than zero_neq_one)

   138 

   139 lemma "sum n = sum1 n"

   140 apply(induct n)

   141 apply(auto)

   142 done

   143 

   144 lemma "sum n = (\<Sum>i \<le> n. i)"

   145 apply(induct n)

   146 apply(simp_all)

   147 done

   148 

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

   150 "mull 0 0 = 0" |

   151 "mull m 0 = 0" |

   152 "mull m 1 = m" | 

   153 (**"mull m (1::nat) = m" | **)

   154 (**"mull m (suc(0)) = m" | **)

   155 "mull m n = mull m (n-(1::nat))" 

   156 apply(pat_completeness)

   157 apply(auto)

   158 

   159 done

   160 

   161   "mull 0 n = 0"

   162 | "mull (Suc m) n = add n (mull m n)" 

   163 

   164 lemma test: "mull m n = m * n"

   165 sorry

   166 

   167 fun poww :: "nat \<Rightarrow> nat \<Rightarrow> nat" where

   168   "poww 0 n = 1"

   169 | "poww (Suc m) n = mull n (poww m n)" 

   170 

   171 

   172 "mull 0 0 = 0" |

   173 "mull m 0 = 0" |

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

   175 (**"mull m (1::nat) = m" | **)

   176 (**"mull m (suc(0)) = m" | **)

   177 "mull m n = mull m (n-(1::nat))" 

   178 

   179 (**Define a function that counts the

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

   181 (**

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

   183 "count  "

   184 **)

   185 

   186 

   187 (* prove n = n * (n + 1) div 2  *)

   188 

   189 

   190 

   191 

   192 

   193 

   194 

   195 

   196 

   197 

   198