isahipster: 614f3b2981c88ecfc9b5c9f773fb00f0a2b66bb6

     1: theory sort_NStoogeSort2Permutes
     2: imports Main
     3:         "$HIPSTER_HOME/IsaHipster"
     4: begin
     5: 
     6: datatype 'a list = Nil2 | Cons2 "'a" "'a list"
     7: 
     8: datatype ('a, 'b) Pair2 = Pair "'a" "'b"
     9: 
    10: datatype Nat = Z | S "Nat"
    11: 
    12: fun twoThirds :: "Nat => Nat" where
    13: "twoThirds (Z) = Z"
    14: | "twoThirds (S (Z)) = S Z"
    15: | "twoThirds (S (S (Z))) = S Z"
    16: | "twoThirds (S (S (S n))) = S (S (twoThirds n))"
    17: 
    18: fun third :: "Nat => Nat" where
    19: "third (Z) = Z"
    20: | "third (S (Z)) = Z"
    21: | "third (S (S (Z))) = Z"
    22: | "third (S (S (S n))) = S (third n)"
    23: 
    24: fun take :: "Nat => 'a list => 'a list" where
    25: "take (Z) y = Nil2"
    26: | "take (S z) (Nil2) = Nil2"
    27: | "take (S z) (Cons2 x2 x3) = Cons2 x2 (take z x3)"
    28: 
    29: fun sort2 :: "int => int => int list" where
    30: "sort2 x y =
    31:    (if x <= y then Cons2 x (Cons2 y (Nil2)) else
    32:       Cons2 y (Cons2 x (Nil2)))"
    33: 
    34: fun length :: "'t list => Nat" where
    35: "length (Nil2) = Z"
    36: | "length (Cons2 y xs) = S (length xs)"
    37: 
    38: fun drop :: "Nat => 'a list => 'a list" where
    39: "drop (Z) y = y"
    40: | "drop (S z) (Nil2) = Nil2"
    41: | "drop (S z) (Cons2 x2 x3) = drop z x3"
    42: 
    43: fun splitAt :: "Nat => 'a list =>
    44:               (('a list), ('a list)) Pair2" where
    45: "splitAt x y = Pair (take x y) (drop x y)"
    46: 
    47: fun count :: "int => int list => Nat" where
    48: "count x (Nil2) = Z"
    49: | "count x (Cons2 z xs) =
    50:      (if x = z then S (count x xs) else count x xs)"
    51: 
    52: fun append :: "'a list => 'a list => 'a list" where
    53: "append (Nil2) y = y"
    54: | "append (Cons2 z xs) y = Cons2 z (append xs y)"
    55: 
    56: function nstooge2sort2 :: "int list => int list"
    57:          and nstoogesort2 :: "int list => int list"
    58:          and nstooge2sort1 :: "int list => int list" where
    59: "nstooge2sort2 x =
    60:    case splitAt (twoThirds (length x)) x of
    61:      | Pair ys zs =>
    62:          case splitAt (twoThirds (length x)) x of
    63:            | Pair xs zs2 => append (nstoogesort2 ys) zs2
    64:          end
    65:    end"
    66: | "nstoogesort2 (Nil2) = Nil2"
    67: | "nstoogesort2 (Cons2 y (Nil2)) = Cons2 y (Nil2)"
    68: | "nstoogesort2 (Cons2 y (Cons2 y2 (Nil2))) = sort2 y y2"
    69: | "nstoogesort2 (Cons2 y (Cons2 y2 (Cons2 x3 x4))) =
    70:      nstooge2sort2
    71:        (nstooge2sort1 (nstooge2sort2 (Cons2 y (Cons2 y2 (Cons2 x3 x4)))))"
    72: | "nstooge2sort1 x =
    73:      case splitAt (third (length x)) x of
    74:        | Pair ys zs =>
    75:            case splitAt (third (length x)) x of
    76:              | Pair xs zs2 => append ys (nstoogesort2 zs2)
    77:            end
    78:      end"
    79: by pat_completeness auto
    80: 
    81: (*hipster twoThirds
    82:           third
    83:           take
    84:           sort2
    85:           length
    86:           drop
    87:           splitAt
    88:           count
    89:           append
    90:           nstooge2sort2
    91:           nstoogesort2
    92:           nstooge2sort1 *)
    93: 
    94: theorem x0 :
    95:   "!! (x :: int) (y :: int list) .
    96:      (count x (nstoogesort2 y)) = (count x y)"
    97:   by (tactic {* Subgoal.FOCUS_PARAMS (K (Tactic_Data.hard_tac @{context})) @{context} 1 *})
    98: 
    99: end