isahipster: cac39e5a52da875fc01be5f4c3eed6bafc4b8dbd

     1: theory prop_64
     2: imports Main
     3:         "$HIPSTER_HOME/IsaHipster"
     4: begin
     5:   datatype 'a list = Nil2 | Cons2 "'a" "'a list"
     6:   datatype Nat = Z | S "Nat"
     7:   fun last :: "Nat list => Nat" where
     8:   "last (Nil2) = Z"
     9:   | "last (Cons2 y (Nil2)) = y"
    10:   | "last (Cons2 y (Cons2 x2 x3)) = last (Cons2 x2 x3)"
    11:   fun append :: "'a list => 'a list => 'a list" where
    12:   "append (Nil2) y = y"
    13:   | "append (Cons2 z xs) y = Cons2 z (append xs y)"
    14:   (*hipster last append *)
    15:   theorem x0 :
    16:     "(last (append xs (Cons2 x (Nil2)))) = x"
    17:     by (tactic {* Subgoal.FOCUS_PARAMS (K (Tactic_Data.hard_tac @{context})) @{context} 1 *})
    18: end