first_order_term_adt.pvs

%%% ADT file generated from first_order_terms

first_order_term_adt[constant: TYPE, variable: TYPE+,
                     f_symbol: TYPE]: THEORY
 BEGIN
  ASSUMING
   variable_TCC1: ASSUMPTION EXISTS (x: variable): TRUE;
  ENDASSUMING

  first_order_term: TYPE

  const?, var?, unit?, pair?, app?: [first_order_term -> boolean]

  a: [(const?) -> constant]

  V: [(var?) -> variable]

  term1: [(pair?) -> first_order_term]

  term2: [(pair?) -> first_order_term]

  f_sym: [(app?) -> f_symbol]

  arg: [(app?) -> first_order_term]

  const: [constant -> (const?)]

  variable: [variable -> (var?)]

  unit: (unit?)

  pair: [[first_order_term, first_order_term] -> (pair?)]

  app: [[f_symbol, first_order_term] -> (app?)]

  first_order_term_ord: [first_order_term -> upto(4)]

  first_order_term_ord_defaxiom: AXIOM
         (FORALL (a: constant): first_order_term_ord(const(a)) = 0)
     AND (FORALL (V: variable): first_order_term_ord(variable(V)) = 1)
     AND (first_order_term_ord(unit) = 2)
     AND (FORALL (term1: first_order_term, term2: first_order_term):
            first_order_term_ord(pair(term1, term2)) = 3)
     AND FORALL (f_sym: f_symbol, arg: first_order_term):
           first_order_term_ord(app(f_sym, arg)) = 4;

  ord(x: first_order_term): upto(4) =
      CASES x
        OF const(const1_var): 0,
           variable(variable1_var): 1,
           unit: 2,
           pair(pair1_var, pair2_var): 3,
           app(app1_var, app2_var): 4
        ENDCASES

  first_order_term_const_extensionality: AXIOM
    FORALL (const?_var: (const?), const?_var2: (const?)):
      a(const?_var) = a(const?_var2) IMPLIES const?_var = const?_var2;

  first_order_term_const_eta: AXIOM
    FORALL (const?_var: (const?)): const(a(const?_var)) = const?_var;

  first_order_term_variable_extensionality: AXIOM
    FORALL (var?_var: (var?), var?_var2: (var?)):
      V(var?_var) = V(var?_var2) IMPLIES var?_var = var?_var2;

  first_order_term_variable_eta: AXIOM
    FORALL (var?_var: (var?)): variable(V(var?_var)) = var?_var;

  first_order_term_unit_extensionality: AXIOM
    FORALL (unit?_var: (unit?), unit?_var2: (unit?)):
      unit?_var = unit?_var2;

  first_order_term_pair_extensionality: AXIOM
    FORALL (pair?_var: (pair?), pair?_var2: (pair?)):
      term1(pair?_var) = term1(pair?_var2) AND
       term2(pair?_var) = term2(pair?_var2)
       IMPLIES pair?_var = pair?_var2;

  first_order_term_pair_eta: AXIOM
    FORALL (pair?_var: (pair?)):
      pair(term1(pair?_var), term2(pair?_var)) = pair?_var;

  first_order_term_app_extensionality: AXIOM
    FORALL (app?_var: (app?), app?_var2: (app?)):
      f_sym(app?_var) = f_sym(app?_var2) AND arg(app?_var) = arg(app?_var2)
       IMPLIES app?_var = app?_var2;

  first_order_term_app_eta: AXIOM
    FORALL (app?_var: (app?)):
      app(f_sym(app?_var), arg(app?_var)) = app?_var;

  first_order_term_a_const: AXIOM
    FORALL (const1_var: constant): a(const(const1_var)) = const1_var;

  first_order_term_V_variable: AXIOM
    FORALL (variable1_var: variable):
      V(variable(variable1_var):: (var?)) = variable1_var;

  first_order_term_term1_pair: AXIOM
    FORALL (pair1_var: first_order_term, pair2_var: first_order_term):
      term1(pair(pair1_var, pair2_var)) = pair1_var;

  first_order_term_term2_pair: AXIOM
    FORALL (pair1_var: first_order_term, pair2_var: first_order_term):
      term2(pair(pair1_var, pair2_var)) = pair2_var;

  first_order_term_f_sym_app: AXIOM
    FORALL (app1_var: f_symbol, app2_var: first_order_term):
      f_sym(app(app1_var, app2_var)) = app1_var;

  first_order_term_arg_app: AXIOM
    FORALL (app1_var: f_symbol, app2_var: first_order_term):
      arg(app(app1_var, app2_var)) = app2_var;

  first_order_term_inclusive: AXIOM
    FORALL (first_order_term_var: first_order_term):
           const?(first_order_term_var) OR var?(first_order_term_var)
       OR unit?(first_order_term_var) OR pair?(first_order_term_var)
       OR app?(first_order_term_var);

  first_order_term_induction: AXIOM
    FORALL (p: [first_order_term -> boolean]):
      (     (FORALL (const1_var: constant): p(const(const1_var)))
        AND (FORALL (variable1_var: variable): p(variable(variable1_var)))
        AND p(unit)
        AND (FORALL (pair1_var: first_order_term,
                     pair2_var: first_order_term):
               p(pair1_var) AND p(pair2_var) IMPLIES
                p(pair(pair1_var, pair2_var)))
        AND FORALL (app1_var: f_symbol, app2_var: first_order_term):
              p(app2_var) IMPLIES p(app(app1_var, app2_var)))
       IMPLIES
       FORALL (first_order_term_var: first_order_term):
         p(first_order_term_var);

  every(p1: PRED[constant], p2: PRED[variable], p3: PRED[f_symbol])
       (a1: first_order_term):
        boolean =
      CASES a1
        OF const(const1_var): p1(const1_var),
           variable(variable1_var): p2(variable1_var),
           unit: TRUE,
           pair(pair1_var, pair2_var):
             every(p1, p2, p3)(pair1_var) AND every(p1, p2, p3)(pair2_var),
           app(app1_var, app2_var):
             p3(app1_var) AND every(p1, p2, p3)(app2_var)
        ENDCASES;

  every(p1: PRED[constant], p2: PRED[variable], p3: PRED[f_symbol],
        a1: first_order_term):
        boolean =
      CASES a1
        OF const(const1_var): p1(const1_var),
           variable(variable1_var): p2(variable1_var),
           unit: TRUE,
           pair(pair1_var, pair2_var):
             every(p1, p2, p3, pair1_var) AND every(p1, p2, p3, pair2_var),
           app(app1_var, app2_var):
             p3(app1_var) AND every(p1, p2, p3, app2_var)
        ENDCASES;

  some(p1: PRED[constant], p2: PRED[variable], p3: PRED[f_symbol])
      (a1: first_order_term):
        boolean =
      CASES a1
        OF const(const1_var): p1(const1_var),
           variable(variable1_var): p2(variable1_var),
           unit: FALSE,
           pair(pair1_var, pair2_var):
             some(p1, p2, p3)(pair1_var) OR some(p1, p2, p3)(pair2_var),
           app(app1_var, app2_var):
             p3(app1_var) OR some(p1, p2, p3)(app2_var)
        ENDCASES;

  some(p1: PRED[constant], p2: PRED[variable], p3: PRED[f_symbol],
       a1: first_order_term):
        boolean =
      CASES a1
        OF const(const1_var): p1(const1_var),
           variable(variable1_var): p2(variable1_var),
           unit: FALSE,
           pair(pair1_var, pair2_var):
             some(p1, p2, p3, pair1_var) OR some(p1, p2, p3, pair2_var),
           app(app1_var, app2_var):
             p3(app1_var) OR some(p1, p2, p3, app2_var)
        ENDCASES;

  subterm(x: first_order_term, y: first_order_term):  boolean =
      x = y OR
       CASES y
         OF const(const1_var): FALSE,
            variable(variable1_var): FALSE,
            unit: FALSE,
            pair(pair1_var, pair2_var):
              subterm(x, pair1_var) OR subterm(x, pair2_var),
            app(app1_var, app2_var): subterm(x, app2_var)
         ENDCASES;

  <<:  (strict_well_founded?[first_order_term]) =
      LAMBDA (x: first_order_term, y: first_order_term):
        CASES y
          OF const(const1_var): FALSE,
             variable(variable1_var): FALSE,
             unit: FALSE,
             pair(pair1_var, pair2_var):
               (x = pair1_var OR x << pair1_var) OR
                (x = pair2_var OR x << pair2_var),
             app(app1_var, app2_var): (x = app2_var OR x << app2_var)
          ENDCASES;

  first_order_term_well_founded: AXIOM
    strict_well_founded?[first_order_term](<<);

  reduce_nat(const?_fun: [constant -> nat], var?_fun: [variable -> nat],
             unit?_fun: nat, pair?_fun: [[nat, nat] -> nat],
             app?_fun: [[f_symbol, nat] -> nat]):
        [first_order_term -> nat] =
      LAMBDA (first_order_term_adtvar: first_order_term):
        LET red: [first_order_term -> nat] =
              reduce_nat(const?_fun, var?_fun, unit?_fun, pair?_fun,
                         app?_fun)
          IN
          CASES first_order_term_adtvar
            OF const(const1_var): const?_fun(const1_var),
               variable(variable1_var): var?_fun(variable1_var),
               unit: unit?_fun,
               pair(pair1_var, pair2_var):
                 pair?_fun(red(pair1_var), red(pair2_var)),
               app(app1_var, app2_var): app?_fun(app1_var, red(app2_var))
            ENDCASES;

  REDUCE_nat(const?_fun: [[constant, first_order_term] -> nat],
             var?_fun: [[variable, first_order_term] -> nat],
             unit?_fun: [first_order_term -> nat],
             pair?_fun: [[nat, nat, first_order_term] -> nat],
             app?_fun: [[f_symbol, nat, first_order_term] -> nat]):
        [first_order_term -> nat] =
      LAMBDA (first_order_term_adtvar: first_order_term):
        LET red: [first_order_term -> nat] =
              REDUCE_nat(const?_fun, var?_fun, unit?_fun, pair?_fun,
                         app?_fun)
          IN
          CASES first_order_term_adtvar
            OF const(const1_var):
                 const?_fun(const1_var, first_order_term_adtvar),
               variable(variable1_var):
                 var?_fun(variable1_var, first_order_term_adtvar),
               unit: unit?_fun(first_order_term_adtvar),
               pair(pair1_var, pair2_var):
                 pair?_fun(red(pair1_var), red(pair2_var),
                           first_order_term_adtvar),
               app(app1_var, app2_var):
                 app?_fun(app1_var, red(app2_var), first_order_term_adtvar)
            ENDCASES;

  reduce_ordinal(const?_fun: [constant -> ordinal],
                 var?_fun: [variable -> ordinal], unit?_fun: ordinal,
                 pair?_fun: [[ordinal, ordinal] -> ordinal],
                 app?_fun: [[f_symbol, ordinal] -> ordinal]):
        [first_order_term -> ordinal] =
      LAMBDA (first_order_term_adtvar: first_order_term):
        LET red: [first_order_term -> ordinal] =
              reduce_ordinal(const?_fun, var?_fun, unit?_fun, pair?_fun,
                             app?_fun)
          IN
          CASES first_order_term_adtvar
            OF const(const1_var): const?_fun(const1_var),
               variable(variable1_var): var?_fun(variable1_var),
               unit: unit?_fun,
               pair(pair1_var, pair2_var):
                 pair?_fun(red(pair1_var), red(pair2_var)),
               app(app1_var, app2_var): app?_fun(app1_var, red(app2_var))
            ENDCASES;

  REDUCE_ordinal(const?_fun: [[constant, first_order_term] -> ordinal],
                 var?_fun: [[variable, first_order_term] -> ordinal],
                 unit?_fun: [first_order_term -> ordinal],
                 pair?_fun:
                   [[ordinal, ordinal, first_order_term] -> ordinal],
                 app?_fun:
                   [[f_symbol, ordinal, first_order_term] -> ordinal]):
        [first_order_term -> ordinal] =
      LAMBDA (first_order_term_adtvar: first_order_term):
        LET red: [first_order_term -> ordinal] =
              REDUCE_ordinal(const?_fun, var?_fun, unit?_fun, pair?_fun,
                             app?_fun)
          IN
          CASES first_order_term_adtvar
            OF const(const1_var):
                 const?_fun(const1_var, first_order_term_adtvar),
               variable(variable1_var):
                 var?_fun(variable1_var, first_order_term_adtvar),
               unit: unit?_fun(first_order_term_adtvar),
               pair(pair1_var, pair2_var):
                 pair?_fun(red(pair1_var), red(pair2_var),
                           first_order_term_adtvar),
               app(app1_var, app2_var):
                 app?_fun(app1_var, red(app2_var), first_order_term_adtvar)
            ENDCASES;
 END first_order_term_adt

first_order_term_adt_map[constant: TYPE, variable: TYPE+, f_symbol: TYPE,
                         constant1: TYPE, variable1: TYPE+,
                         f_symbol1: TYPE]: THEORY
 BEGIN
  ASSUMING
   variable_TCC1: ASSUMPTION EXISTS (x: variable): TRUE;

   variable1_TCC1: ASSUMPTION EXISTS (x: variable1): TRUE;
  ENDASSUMING

  IMPORTING first_order_term_adt

  map(f1: [constant -> constant1], f2: [variable -> variable1],
      f3: [f_symbol -> f_symbol1])
     (a1: first_order_term[constant, variable, f_symbol]):
        first_order_term[constant1, variable1, f_symbol1] =
      CASES a1
        OF const(const1_var): const(f1(const1_var)),
           variable(variable1_var): variable(f2(variable1_var)),
           unit: unit,
           pair(pair1_var, pair2_var):
             pair(map(f1, f2, f3)(pair1_var), map(f1, f2, f3)(pair2_var)),
           app(app1_var, app2_var):
             app(f3(app1_var), map(f1, f2, f3)(app2_var))
        ENDCASES;

  map(f1: [constant -> constant1], f2: [variable -> variable1],
      f3: [f_symbol -> f_symbol1],
      a1: first_order_term[constant, variable, f_symbol]):
        first_order_term[constant1, variable1, f_symbol1] =
      CASES a1
        OF const(const1_var): const(f1(const1_var)),
           variable(variable1_var): variable(f2(variable1_var)),
           unit: unit,
           pair(pair1_var, pair2_var):
             pair(map(f1, f2, f3, pair1_var), map(f1, f2, f3, pair2_var)),
           app(app1_var, app2_var):
             app(f3(app1_var), map(f1, f2, f3, app2_var))
        ENDCASES;

  every(R1: [[constant, constant1] -> boolean],
        R2: [[variable, variable1] -> boolean],
        R3: [[f_symbol, f_symbol1] -> boolean])
       (x: first_order_term[constant, variable, f_symbol],
        y: first_order_term[constant1, variable1, f_symbol1]):
        boolean =
           (const?(x) AND const?(y) AND R1(a(x), a(y)))
       OR (var?(x) AND var?(y) AND R2(V(x), V(y)))
       OR (unit?(x) AND unit?(y))
       OR (pair?(x) AND
            pair?(y) AND
             every(R1, R2, R3)(term1(x), term1(y)) AND
              every(R1, R2, R3)(term2(x), term2(y)))
       OR (app?(x) AND
            app?(y) AND
             R3(f_sym(x), f_sym(y)) AND every(R1, R2, R3)(arg(x), arg(y)));
 END first_order_term_adt_map

first_order_term_adt_reduce[constant: TYPE, variable: TYPE+,
                            f_symbol: TYPE, range: TYPE]: THEORY
 BEGIN
  ASSUMING
   variable_TCC1: ASSUMPTION EXISTS (x: variable): TRUE;
  ENDASSUMING

  IMPORTING first_order_term_adt[constant, variable, f_symbol]

  reduce(const?_fun: [constant -> range], var?_fun: [variable -> range],
         unit?_fun: range, pair?_fun: [[range, range] -> range],
         app?_fun: [[f_symbol, range] -> range]):
        [first_order_term[constant, variable, f_symbol] -> range] =
      LAMBDA (first_order_term_adtvar:
                first_order_term[constant, variable, f_symbol]):
        LET red: [first_order_term[constant, variable, f_symbol] -> range]
              =
              reduce(const?_fun, var?_fun, unit?_fun, pair?_fun, app?_fun)
          IN
          CASES first_order_term_adtvar
            OF const(const1_var): const?_fun(const1_var),
               variable(variable1_var): var?_fun(variable1_var),
               unit: unit?_fun,
               pair(pair1_var, pair2_var):
                 pair?_fun(red(pair1_var), red(pair2_var)),
               app(app1_var, app2_var): app?_fun(app1_var, red(app2_var))
            ENDCASES;

  REDUCE(const?_fun:
           [[constant, first_order_term[constant, variable, f_symbol]] ->
              range],
         var?_fun:
           [[variable, first_order_term[constant, variable, f_symbol]] ->
              range],
         unit?_fun:
           [first_order_term[constant, variable, f_symbol] -> range],
         pair?_fun:
           [[range, range,
             first_order_term[constant, variable, f_symbol]] ->
              range],
         app?_fun:
           [[f_symbol, range,
             first_order_term[constant, variable, f_symbol]] ->
              range]):
        [first_order_term[constant, variable, f_symbol] -> range] =
      LAMBDA (first_order_term_adtvar:
                first_order_term[constant, variable, f_symbol]):
        LET red: [first_order_term[constant, variable, f_symbol] -> range]
              =
              REDUCE(const?_fun, var?_fun, unit?_fun, pair?_fun, app?_fun)
          IN
          CASES first_order_term_adtvar
            OF const(const1_var):
                 const?_fun(const1_var, first_order_term_adtvar),
               variable(variable1_var):
                 var?_fun(variable1_var, first_order_term_adtvar),
               unit: unit?_fun(first_order_term_adtvar),
               pair(pair1_var, pair2_var):
                 pair?_fun(red(pair1_var), red(pair2_var),
                           first_order_term_adtvar),
               app(app1_var, app2_var):
                 app?_fun(app1_var, red(app2_var), first_order_term_adtvar)
            ENDCASES;
 END first_order_term_adt_reduce