isahipster: 3c99d568679255589c8ed3e529be7668955ed2a8

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