Theory Shallow_Micro_Rust.Tuple

(* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
   SPDX-License-Identifier: MIT *)

(*<*)
theory Tuple
  imports
    Core_Expression
begin
(*>*)

datatype tnil = TNil

abbreviation(input) tuple_base_pair :: ‹('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
                                        ('s, 'arg1, 'c, 'abort, 'i, 'o) expression ⇒
                                        ('s, 'arg0 × 'arg1 × tnil, 'c, 'abort, 'i, 'o) expression› where
  ‹tuple_base_pair ≡ bindlift2 (λx y. (x, y, TNil))›

abbreviation(input) tuple_cons :: ‹('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
                                   ('s, 'arg1, 'c, 'abort, 'i, 'o) expression ⇒
                                   ('s, 'arg0 × 'arg1, 'c, 'abort, 'i, 'o) expression› where
  ‹tuple_cons ≡ bindlift2 (λx y. (x, y))›

abbreviation(input) tuple_index_0 :: ‹('s, 'arg0 × 'arg1, 'c, 'abort, 'i, 'o) expression ⇒
                                      ('s, 'arg0, 'c, 'abort, 'i, 'o) expression› where
  ‹tuple_index_0 ≡ bindlift1 fst›

abbreviation(input) tuple_index_1 :: ‹('s, 'arg0 × 'arg1 × 'arg2, 'c, 'abort, 'i, 'o) expression ⇒
                                      ('s, 'arg1, 'c, 'abort, 'i, 'o) expression› where
  ‹tuple_index_1 ≡ bindlift1 (fst ∘ snd)›

abbreviation(input) tuple_index_2 :: ‹('s, 'arg0 × 'arg1 × 'arg2 × 'arg3, 'c, 'abort, 'i, 'o) expression ⇒
                                      ('s, 'arg2, 'c, 'abort, 'i, 'o) expression› where
  ‹tuple_index_2 ≡ bindlift1 (fst ∘ snd ∘ snd)›

abbreviation(input) tuple_index_3 :: ‹('s, 'arg0 × 'arg1 × 'arg2 × 'arg3 × 'arg4, 'c, 'abort, 'i, 'o) expression ⇒
                                      ('s, 'arg3, 'c, 'abort, 'i, 'o) expression› where
  ‹tuple_index_3 ≡ bindlift1 (fst ∘ snd ∘ snd ∘ snd)›

abbreviation(input) tuple_index_4 :: ‹('s, 'arg0 × 'arg1 × 'arg2 × 'arg3 × 'arg4 × 'arg5, 'c, 'abort, 'i, 'o) expression ⇒
                                      ('s, 'arg4, 'c, 'abort, 'i, 'o) expression› where
  ‹tuple_index_4 ≡ bindlift1 (fst ∘ snd ∘ snd ∘ snd ∘ snd)›

abbreviation(input) tuple_index_5 :: ‹('s, 'arg0 × 'arg1 × 'arg2 × 'arg3 × 'arg4 × 'arg5 × 'arg6, 'c, 'abort, 'i, 'o) expression ⇒
                                      ('s, 'arg5, 'c, 'abort, 'i, 'o) expression› where
  ‹tuple_index_5 ≡ bindlift1 (fst ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd)›

abbreviation(input) tuple_index_6 :: ‹('s, 'arg0 × 'arg1 × 'arg2 × 'arg3 × 'arg4 × 'arg5 × 'arg6 × 'arg7, 'c, 'abort, 'i, 'o) expression ⇒
                                      ('s, 'arg6, 'c, 'abort, 'i, 'o) expression› where
  ‹tuple_index_6 ≡ bindlift1 (fst ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd)›

abbreviation(input) tuple_index_7 :: ‹('s, 'arg0 × 'arg1 × 'arg2 × 'arg3 × 'arg4 × 'arg5 × 'arg6 × 'arg7 × 'arg8, 'c, 'abort, 'i, 'o) expression ⇒
                                      ('s, 'arg7, 'c, 'abort, 'i, 'o) expression› where
  ‹tuple_index_7 ≡ bindlift1 (fst ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd)›

abbreviation(input) tuple_index_8 :: ‹('s, 'arg0 × 'arg1 × 'arg2 × 'arg3 × 'arg4 × 'arg5 × 'arg6 × 'arg7 × 'arg8 × 'arg9, 'c, 'abort, 'i, 'o) expression ⇒
                                      ('s, 'arg8, 'c, 'abort, 'i, 'o) expression› where
  ‹tuple_index_8 ≡ bindlift1 (fst ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd)›

abbreviation(input) tuple_index_9 :: ‹('s, 'arg0 × 'arg1 × 'arg2 × 'arg3 × 'arg4 × 'arg5 × 'arg6 × 'arg7 × 'arg8 × 'arg9 × 'arg10, 'c, 'abort, 'i, 'o) expression ⇒
                                      ('s, 'arg9, 'c, 'abort, 'i, 'o) expression› where
  ‹tuple_index_9 ≡ bindlift1 (fst ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd)›

abbreviation(input) tuple_index_10 :: ‹('s, 'arg0 × 'arg1 × 'arg2 × 'arg3 × 'arg4 × 'arg5 × 'arg6 × 'arg7 × 'arg8 × 'arg9 × 'arg10 × 'arg11, 'c, 'abort, 'i, 'o) expression ⇒
                                       ('s, 'arg10, 'c, 'abort, 'i, 'o) expression› where
  ‹tuple_index_10 ≡ bindlift1 (fst ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd)›

abbreviation(input) tuple_index_11 :: ‹('s, 'arg0 × 'arg1 × 'arg2 × 'arg3 × 'arg4 × 'arg5 × 'arg6 × 'arg7 × 'arg8 × 'arg9 × 'arg10 × 'arg11 × 'arg12, 'c, 'abort, 'i, 'o) expression ⇒
                                       ('s, 'arg11, 'c, 'abort, 'i, 'o) expression› where
  ‹tuple_index_11 ≡ bindlift1 (fst ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd)›

abbreviation(input) tuple_index_12 :: ‹('s, 'arg0 × 'arg1 × 'arg2 × 'arg3 × 'arg4 × 'arg5 × 'arg6 × 'arg7 × 'arg8 × 'arg9 × 'arg10 × 'arg11 × 'arg12 × 'arg13, 'c, 'abort, 'i, 'o) expression ⇒
                                       ('s, 'arg12, 'c, 'abort, 'i, 'o) expression› where
  ‹tuple_index_12 ≡ bindlift1 (fst ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd)›

abbreviation(input) tuple_index_13 :: ‹('s, 'arg0 × 'arg1 × 'arg2 × 'arg3 × 'arg4 × 'arg5 × 'arg6 × 'arg7 × 'arg8 × 'arg9 × 'arg10 × 'arg11 × 'arg12 × 'arg13 × 'arg14, 'c, 'abort, 'i, 'o) expression ⇒
                                       ('s, 'arg13, 'c, 'abort, 'i, 'o) expression› where
  ‹tuple_index_13 ≡ bindlift1 (fst ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd)›

abbreviation(input) tuple_index_14 :: ‹('s, 'arg0 × 'arg1 × 'arg2 × 'arg3 × 'arg4 × 'arg5 × 'arg6 × 'arg7 × 'arg8 × 'arg9 × 'arg10 × 'arg11 × 'arg12 × 'arg13 × 'arg14 × 'arg15, 'c, 'abort, 'i, 'o) expression ⇒
                                       ('s, 'arg14, 'c, 'abort, 'i, 'o) expression› where
  ‹tuple_index_14 ≡ bindlift1 (fst ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd)›

abbreviation(input) tuple_index_15 :: ‹('s, 'arg0 × 'arg1 × 'arg2 × 'arg3 × 'arg4 × 'arg5 × 'arg6 × 'arg7 × 'arg8 × 'arg9 × 'arg10 × 'arg11 × 'arg12 × 'arg13 × 'arg14 × 'arg15 × 'arg16, 'c, 'abort, 'i, 'o) expression ⇒
                                       ('s, 'arg15, 'c, 'abort, 'i, 'o) expression› where
  ‹tuple_index_15 ≡ bindlift1 (fst ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd)›

(*<*)
end
(*>*)