isahipster: 98b5feb9ccf1755529315a57f6ca1308625f4129

     1: theory weird_nat_mul3acc_comm13
     2: imports Main
     3:         "$HIPSTER_HOME/IsaHipster"
     4: begin
     5: 
     6: datatype Nat = Z | S "Nat"
     7: 
     8: fun add3acc :: "Nat => Nat => Nat => Nat" where
     9: "add3acc (Z) (Z) z = z"
    10: | "add3acc (Z) (S y2) z = add3acc Z y2 (S z)"
    11: | "add3acc (S x2) y z = add3acc x2 (S y) z"
    12: 
    13: fun mul3acc :: "Nat => Nat => Nat => Nat" where
    14: "mul3acc (Z) y z = Z"
    15: | "mul3acc (S x2) (Z) z = Z"
    16: | "mul3acc (S x2) (S x3) (Z) = Z"
    17: | "mul3acc (S (Z)) (S (Z)) (S (Z)) = S Z"
    18: | "mul3acc (S (Z)) (S (Z)) (S (S x5)) =
    19:      S (add3acc
    20:           (mul3acc Z Z (S x5))
    21:           (add3acc
    22:              (mul3acc (S Z) Z (S x5)) (mul3acc Z (S Z) (S x5))
    23:              (mul3acc Z Z (S Z)))
    24:           (add3acc Z Z (S x5)))"
    25: | "mul3acc (S (Z)) (S (S x6)) (S x4) =
    26:      S (add3acc
    27:           (mul3acc Z (S x6) x4)
    28:           (add3acc
    29:              (mul3acc (S Z) (S x6) x4) (mul3acc Z (S Z) x4)
    30:              (mul3acc Z (S x6) (S Z)))
    31:           (add3acc Z (S x6) x4))"
    32: | "mul3acc (S (S x7)) (S x3) (S x4) =
    33:      S (add3acc
    34:           (mul3acc (S x7) x3 x4)
    35:           (add3acc
    36:              (mul3acc (S Z) x3 x4) (mul3acc (S x7) (S Z) x4)
    37:              (mul3acc (S x7) x3 (S Z)))
    38:           (add3acc (S x7) x3 x4))"
    39: 
    40: (*hipster add3acc mul3acc *)
    41: 
    42: theorem x0 :
    43:   "!! (x :: Nat) (y :: Nat) (z :: Nat) .
    44:      (mul3acc x y z) = (mul3acc z y x)"
    45:   by (tactic {* Subgoal.FOCUS_PARAMS (K (Tactic_Data.hard_tac @{context})) @{context} 1 *})
    46: 
    47: end