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 

    54 (**commutative-associative**)

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

    56 apply(induct m)

    57 apply(simp_all)

    58 done

    59 

    60 lemma add_zero: "add n 0 = n"

    61 apply(induct n)

    62 apply(auto)

    63 done

    64 

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

    66 apply(induct m)

    67 apply(metis add.simps(1))

    68 apply(auto)

    69 done

    70 

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

    72 apply(induct m)

    73 apply(simp add: add_zero)

    74 apply(simp add: add_Suc)

    75 done

    76 

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

    78 apply(subst add_04)

    79 apply(subst (2) add_comm)

    80 apply(simp)

    81 done

    82 

    83 

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

    85 "dub 0 = 0" |

    86 "dub m = add m m"

    87 

    88 lemma dub_01: "dub 0 = 0"

    89 apply(induct)

    90 apply(auto)

    91 done

    92 

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

    94 apply(induction m)

    95 apply(auto)

    96 done

    97 

    98 value "dub 2"

    99 

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

   101 "trip 0 = 0" |

   102 "trip m = add m (add m m)"

   103 

   104 lemma trip_01: "trip 0 = 0"

   105 apply(induct)

   106 apply(auto)

   107 done

   108 

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

   110 apply(induction m)

   111 apply(auto)

   112 done

   113 

   114 value "trip 1"

   115 value "trip 2"

   116 

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

   118   "sum 0 = 0"

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

   120 

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

   122   "sum1 0 = 0"

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

   124 apply(auto)

   125 done

   126 

   127 termination sum1

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

   129 

   130 lemma "sum n = sum1 n"

   131 apply(induct n)

   132 apply(auto)

   133 done

   134 

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

   136 apply(induct n)

   137 apply(simp_all)

   138 done

   139 

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

   141 "mull 0 0 = 0" |

   142 "mull m 0 = 0" |

   143 "mull m 1 = m" | 

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

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

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

   147 apply(pat_completeness)

   148 apply(auto)

   149 

   150 done

   151 

   152   "mull 0 n = 0"

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

   154 

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

   156 sorry

   157 

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

   159   "poww 0 n = 1"

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

   161 

   162 

   163 "mull 0 0 = 0" |

   164 "mull m 0 = 0" |

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

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

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

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

   169 

   170 (**Define a function that counts the

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

   172 (**

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

   174 "count  "

   175 **)

   176 

   177 

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

   179 

   180 

   181 

   182 

   183 

   184 

   185 

   186 

   187 

   188 

   189