first_order_terms.pvs

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%  Properties of Terms (Antiunify th) %%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Mariano Miguel Moscato    AMA/NASA LaRC Formal Methods
% Maria Julia Dias Lima     Universidade de Brasilia
% Mauricio Ayala-Rincon     Universidade de Brasilia
% Temur Kutsia              RISC/Johannes Kepler Universitaet Linz
% Thaynara Arielly de Lima  Universidade Federal de Goias
% Gabriel Ferreira Silva    Universidade de Brasilia
%
%    Last modified 3rd December, 2024
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% definition of a term
first_order_term[constant:TYPE, variable:TYPE+, f_symbol:TYPE]: DATATYPE 
    BEGIN
	const (a: constant): const?
	variable (V: variable): var?
	unit: unit?
	pair (term1: first_order_term, term2: first_order_term): pair?
	app (f_sym: f_symbol, arg: first_order_term): app?
    END first_order_term


% %%%%%%%%%%%%%%%%%%%%%%%%%%
 first_order_terms_properties: THEORY
 BEGIN

% definition of variable, constant and syntactic function symbols 
variable: TYPE = nat
constant: TYPE = nat

f_symbol: TYPE = string


 IMPORTING first_order_term[constant, variable, f_symbol], structures@more_list_props, 
 	   nominal@list_aux_equational_reasoning[first_order_term],
	   nominal@list_aux_equational_reasoning2parameters[nat, first_order_term]



sym, f: VAR string     
n, i, j: VAR nat
lst_nat: VAR list[nat]

t, s, t1: VAR first_order_term
X: var variable

 fin_set_t: VAR finite_set[first_order_term]

args: TYPE = list[first_order_term]
args, args1, args2: VAR args
lst_args: VAR list[args]

lst_vars: VAR list[variable]
lst_lst_vars: VAR list[list[variable]]

% the size of a term 
size(t): RECURSIVE posnat =
    CASES t OF
        const(a): 1,
	variable(X): 1, 
	unit: 1, 
	pair(t1, t2): 1 + size(term1(t)) + size(term2(t)),
	app(sym, arg): 1  + size(arg)
    ENDCASES
MEASURE t BY <<

% size of finite_set of first_order_term 

size(fin_set_t) : RECURSIVE nat =
IF  empty?(fin_set_t) THEN 0
ELSE size(choose(fin_set_t)) + size(rest(fin_set_t))
ENDIF
MEASURE card(fin_set_t)

% size of args, i.e., a list of terms
size(args): RECURSIVE nat =
     IF null?(args) THEN 1
     ELSE LET t = car(args) IN size(t) + size(cdr(args)) 
     ENDIF 
MEASURE length(args) 

% size of lst_args, i.e., a list of args
size(lst_args): RECURSIVE nat =
     IF null?(lst_args) THEN 1
     ELSE LET args = car(lst_args) IN size(args) + size(cdr(lst_args)) 
     ENDIF 
MEASURE length(lst_args) 


% membership for a list of arguments
member(t, lst_args): RECURSIVE bool =
     IF null?(lst_args) THEN FALSE
     ELSE LET args = car(lst_args) IN
     	      member(t, args) OR member(t, cdr(lst_args))
     ENDIF 
MEASURE lst_args BY <<

% returns the function symbol of a function t
sym(t): string = 
    IF app?(t) THEN f_sym(t)
    ELSE "-"
    ENDIF

% tests whether t is a function symbol
func?(t): bool =
    IF app?(t) THEN TRUE
    ELSE FALSE
    ENDIF 

% test if t and s are functions that are not headed by the same symbol 
dif_func?(t, s): bool = (app?(t) AND app?(s) AND sym(t) /= sym(s))

% returns true if "t" and "s" are headed by the same function symbol 
same_func?(t, s): bool = 
    app?(t) AND ord(t) = ord(s) AND sym(t) = sym(s) 

% get the number of arguments of a term "t"
% if it encounters function whose root is "sym" it goes inside the function
num_arg(sym, t): RECURSIVE nat =
    IF pair?(t) THEN num_arg(sym, term1(t)) + num_arg(sym, term2(t))
    ELSE 1
    ENDIF
MEASURE t BY << 


% select the nth (index start at one) argument of an a term.
% if it encounters a function whose root is "sym" it goes inside the function
select(sym, t)(n): RECURSIVE first_order_term =
    IF pair?(t) THEN
        LET n1 = num_arg(sym, term1(t)) IN
        IF n <= n1 THEN select(sym, term1(t))(n)
        ELSE select(sym, term2(t))(n-n1)
        ENDIF
    ELSE t
    ENDIF 
MEASURE t BY <<

% returns true case i > 0 and i <= n.
nice_ind?(i, n): bool = i > 0 AND i <= n

% returns true case nice_ind?(i, n) for every "i" in "lst_nat"
nice_ind?(lst_nat, n): RECURSIVE bool =
    IF null?(lst_nat) THEN TRUE
    ELSE nice_ind?(car(lst_nat), n) AND nice_ind?(cdr(lst_nat), n)
    ENDIF
MEASURE lst_nat BY << 

% receives a term
% if its a pair, flatten it in a list 
% else return a list containing only the term 
flatten_pair(t): RECURSIVE args =
    IF pair?(t) THEN append(flatten_pair(term1(t)), flatten_pair(term2(t)))
    ELSE cons(t, null) 
    ENDIF
MEASURE t BY << 

% represented in our paper as Args_f(t), this function get the arguments of a term t.
% if it encounters a function whose root is "sym" it goes inside the function
get_args(sym)(t): args =
    LET n = num_arg(sym, t), lst_until_n = from_min2max[nat](1, n) IN 
    	map(select(sym, t))(lst_until_n)
    
% obtain a term to represent a whole list of terms
get_term_from_args(args): RECURSIVE first_order_term =
    IF null?(args) THEN unit
    ELSIF length(args) = 1 THEN car(args)
    ELSE pair(car(args), get_term_from_args(cdr(args)))
    ENDIF
MEASURE args BY << 

% returns TRUE if all arguments of args are variables, FALSE otherwise
all_var?(args): RECURSIVE bool =
   IF null?(args) THEN TRUE
   ELSE var?(car(args)) AND all_var?(cdr(args))
   ENDIF
MEASURE args BY << 

% extends all_var? to a list of arguments
all_var?(lst_args): RECURSIVE bool =
   IF null?(lst_args) THEN TRUE 
   ELSE all_var?(car(lst_args)) AND all_var?(cdr(lst_args))
   ENDIF
MEASURE lst_args BY << 

% returns true if for every "t" in args, "t" is not a pair 
no_pair?(args): bool =
   FORALL t: member(t, args) IMPLIES NOT pair?(t) 

% options of a term:
first_order_term_opt: LEMMA
    (const?(t) AND t = const(a(t))) OR (var?(t) AND t = variable(V(t))) OR
    t = unit OR (pair?(t) AND t = pair(term1(t), term2(t))) OR (app?(t) AND t = app(f_sym(t), arg(t)))


% membership in a lst of arguments
member_t_lst_args: LEMMA
    member(t, lst_args) IFF
    EXISTS args:
        member(args, lst_args) AND member(t, args)

% size
size_ge1: LEMMA
    size(t) >= 1
    
size_args_ge1: LEMMA
    size(args) >= 1

% num_arg
num_arg_ge1: LEMMA
    num_arg(f, t) > 0 

num_arg_ge1_type_t: LEMMA
    num_arg(f, t) > 1 IMPLIES pair?(t) 

num_arg_not_pair: LEMMA
    NOT pair?(t) IMPLIES num_arg(f, t) = 1

% select
select_num_arg: LEMMA
    num_arg(f, select(f, t)(i)) = 1

select_not_pair: LEMMA
    NOT pair?(select(f, t)(i))


select_le1: LEMMA
    n <= 1 IMPLIES select(f, t)(n) = select(f, t)(1)

select_ge_num_arg: LEMMA
    LET n = num_arg(f, t) IN 
    i >= n IMPLIES select(f, t)(i) = select(f, t)(n) 

select_size: LEMMA
    size(select(f, t)(n)) <= size(t) 
    
% remove
remove_size_args: LEMMA
    i < length(args) IMPLIES size(remove(args, i)) < size(args)

remove_size_lst_args: LEMMA
    i < length(lst_args) AND j < length(nth(lst_args, i)) IMPLIES
    size(remove(lst_args, i, j)) < size(lst_args) 

% get args
get_args_len: LEMMA
    length(get_args(f)(t)) = num_arg(f, t) 

get_args_null: LEMMA
    NOT null?(get_args(f)(t))

get_args_pair: LEMMA
    get_args(f)(pair(t, s)) = append(get_args(f)(t), get_args(f)(s))

get_args_mem_not_pair: LEMMA
    member(s, get_args(f)(t)) IMPLIES NOT pair?(s)

get_args_mem_select1: LEMMA 
    member(select(f, t)(1), get_args(f)(t))

get_args_mem_selecti: LEMMA  
    member(select(f, t)(i), get_args(f)(t))

get_args_not_pair: LEMMA
    NOT pair?(t) IMPLIES get_args(f)(t) = cons(t, null)

get_args_nth: LEMMA
    nice_ind?(i, num_arg(f, t)) IMPLIES
    nth(get_args(f)(t), i-1) = select(f, t)(i) 

get_args_get_term_from_args: LEMMA
    NOT null?(args) IMPLIES
    get_args(f)(get_term_from_args(args)) = flatten(map(get_args(f))(args))

get_args_get_term_from_args_len: LEMMA 
    length(get_args(f)(get_term_from_args(args))) >= length(args)

%%% additional lemmas about variables of a first_order_term, subterms and proper subterms
IMPORTING list_aux_equational_reasoning[variable], list_aux_equational_reasoning2parameters[first_order_term, variable], list_aux_equational_reasoning2parameters[first_order_term, first_order_term]

% needed for some tccs
subterms_aux_TCC: LEMMA every[number, number, f_symbol]
          (LAMBDA (x: number): number_field_pred(x) AND real_pred(x) AND rational_pred(x)
              AND integer_pred(x) AND (x >= 0), LAMBDA (x: number):
           number_field_pred(x) AND real_pred(x) AND rational_pred(x)
           AND integer_pred(x) AND (x >= 0), LAMBDA (x: f_symbol):
           TRUE)
          (select(sym, t)(n))

% variables of a term "t".
vars(t): RECURSIVE finite_set[variable] =
   CASES t OF
        const(a): emptyset,
	variable(X): singleton(X), 
	unit: emptyset, 
	pair(t1, t2): union(vars(t1), vars(t2)),
	app(sym, arg): vars(arg)
    ENDCASES
MEASURE size(t)
       
% variables of a finite set of terms
vars(fin_set_t): RECURSIVE finite_set[variable] = 
   IF empty?(fin_set_t) THEN emptyset
   ELSE union(vars(choose(fin_set_t)), vars(rest(fin_set_t)))
   ENDIF
MEASURE card(fin_set_t)

vars(args): RECURSIVE finite_set[variable] = 
   IF null?(args) THEN emptyset
   ELSE union(vars(car(args)), vars(cdr(args)))
   ENDIF
MEASURE args BY << 

vars(lst_args): RECURSIVE finite_set[variable] = 
   IF null?(lst_args) THEN emptyset
   ELSE union(vars(car(lst_args)), vars(cdr(lst_args)))
   ENDIF
MEASURE lst_args BY << 

vars(lst_lst_vars): RECURSIVE finite_set[variable] = 
   IF null?(lst_lst_vars) THEN emptyset
   ELSE LET vars_car = list2set(car(lst_lst_vars)) IN
   	    union(vars_car, vars(cdr(lst_lst_vars)))
   ENDIF 
MEASURE lst_lst_vars BY << 


% list of variables of a term
lst_vars(t): RECURSIVE list[variable] =
   CASES t OF
        const(a): null,
	variable(X): cons(X, null), 
	unit: null, 
	pair(t1, t2): append(lst_vars(t1), lst_vars(t2)),
	app(sym, arg): lst_vars(arg)
    ENDCASES
MEASURE size(t)

% select only the non-variable arguments 
not_var_args(args): RECURSIVE args = 
   IF null?(args) THEN null 
   ELSE LET t = car(args) IN
   	IF var?(t) THEN not_var_args(cdr(args))
	ELSE cons(t, not_var_args(cdr(args)))
	ENDIF
   ENDIF 
MEASURE args BY << 

not_var_args(sym)(t): args =
   LET args = get_args(sym)(t) IN
   not_var_args(args)

% set of all subterms of t
subterms(t): RECURSIVE finite_set[first_order_term] =
   CASES t OF
        const(a): singleton(t),
	variable(X): singleton(t), 
	unit: singleton(t), 
	pair(t1, t2): union(subterms(t1), subterms(t2)),
	app(sym, arg): union(singleton(t), subterms(arg)) 
    ENDCASES
MEASURE size(t)

% extends subterm to a list of terms
subterms(args): RECURSIVE finite_set[first_order_term] =
    IF null?(args) THEN emptyset
    ELSE LET t = car(args) IN
    	 union(subterms(t), subterms(cdr(args)))
    ENDIF
MEASURE args BY << 

subterms(fin_set_t): RECURSIVE finite_set[first_order_term] =
   IF empty?(fin_set_t) THEN emptyset
   ELSE union(subterms(choose(fin_set_t)), subterms(rest(fin_set_t)))
   ENDIF
MEASURE card(fin_set_t)

% set of all proper subterms of t
prop_subterms(t): RECURSIVE finite_set[first_order_term] =
   IF pair?(t) THEN union(prop_subterms(term1(t)), prop_subterms(term2(t)))
   ELSE {s | member(s, subterms(t)) AND s /= t}
   ENDIF
MEASURE t BY << 

% if a term is not a pair, return 1
% else, return the number of elements in the pair
num_arg(t): RECURSIVE nat =
   IF pair?(t) THEN num_arg(term1(t)) + num_arg(term2(t)) 
   ELSE 1
   ENDIF
MEASURE t BY << 

get_args(t): args =
   cons(t, null)



no_pair?(fin_set_t): bool = FORALL t: member(t, fin_set_t) IMPLIES NOT pair?(t)

% this alternative definition of size 
size2(t): RECURSIVE nat =
    CASES t OF
        const(a): 1,
	variable(X): 1, 
	unit: 1, 
	pair(t1, t2): size2(term1(t)) + size2(term2(t)),
	app(sym, arg): 1  + size2(arg)
    ENDCASES
MEASURE size(t)

% receives a list of naturals [1, ..., n]
% returns a list of variables, with the corresponding indices: [X1, ..., Xn]
var_lst(lst_nat): RECURSIVE list[first_order_term] = 
   IF null?(lst_nat) THEN null
   ELSE LET i = car(lst_nat) IN cons(variable(i), var_lst(cdr(lst_nat)))
   ENDIF
MEASURE lst_nat BY << 

% lemmas
% vars 
vars_append: LEMMA
   vars(append(args1, args2)) = union(vars(args1), vars(args2))

vars_correct: LEMMA
   member(X, vars(t)) AND member(t, fin_set_t)
   IMPLIES member(X, vars(fin_set_t))

vars_singleton: LEMMA
    vars(singleton(t)) = vars(t) 

vars_finset: LEMMA
    member(X, vars(fin_set_t)) IFF
    EXISTS t:
        member(t, fin_set_t) AND member(X, vars(t))

vars_args: LEMMA
   member(X, vars(args)) IFF
   EXISTS t:
      member(t, args) AND member(X, vars(t))

vars_lst_args: LEMMA
   member(X, vars(lst_args)) IFF
   EXISTS args:
      member(args, lst_args) AND member(X, vars(args))

vars_lst_lst_vars: LEMMA
   member(X, vars(lst_lst_vars)) IFF
   EXISTS lst_vars:
      member(X, lst_vars) AND member(lst_vars, lst_lst_vars)

vars_map: LEMMA
   Union(list2set(map(vars)(args))) = vars(args)

vars_get_args: LEMMA
   vars(get_args(f)(t)) = vars(t) 

vars_select: LEMMA  
   subset?(vars(select(f, t)(i)), vars(t))
 
vars_lst_vars: LEMMA
   vars(t) = list2set(lst_vars(t))

var_lst_len: LEMMA 
   length(var_lst(lst_nat)) = length(lst_nat)

var_lst_nth: LEMMA 
   i < length(lst_nat) IMPLIES 
   nth(var_lst(lst_nat), i) = variable(nth(lst_nat, i))

var_lst_mem: LEMMA 
   member(t, var_lst(lst_nat)) IFF (var?(t) AND member(V(t), lst_nat))

% all_var
all_var?_append: LEMMA
    all_var?(append(args1, args2)) = (all_var?(args1) AND all_var?(args2))

all_var?_get_repeat_lst: LEMMA
    var?(t) IMPLIES all_var?(get_repeat_lst(t, n))

all_var?_split: LEMMA
    all_var?(args) IMPLIES all_var?(split(args, n)`1)

all_var?_split2: LEMMA
    all_var?(args) IMPLIES all_var?(split(args, n)`2)

IMPORTING
          list_aux_equational_reasoning[args], list_aux_equational_reasoning2parameters[first_order_term, first_order_term], list_aux_equational_reasoning2parameters[first_order_term, variable]

all_var?_get_repeat_lst_null: LEMMA
    all_var?(get_repeat_lst[args](null, n))

all_var?_split_lst_args: LEMMA
    all_var?(lst_args) IMPLIES all_var?(split(lst_args, n)`1)

all_var?_split_lst_args2: LEMMA
    all_var?(lst_args) IMPLIES all_var?(split(lst_args, n)`2)

all_var?_args: LEMMA
    all_var?(args) IFF
    FORALL t:
       member(t, args) IMPLIES var?(t) 

all_var?_lst_args: LEMMA
    all_var?(lst_args) IFF
    FORALL args:
       member(args, lst_args) IMPLIES all_var?(args) 
    
% not_var_args
not_var_args_append: LEMMA
    not_var_args(append(args1, args2)) = append(not_var_args(args1), not_var_args(args2))

not_var_args_nth: LEMMA
    i < length(not_var_args(args)) IMPLIES EXISTS j:
    j < length(args) AND
    nth(not_var_args(args), i) = nth(args, j) 
    
not_var_args_mem: LEMMA
    member(t, not_var_args(args)) IMPLIES member(t, args)

not_var_args_mem2: LEMMA
    member(t, not_var_args(args)) IFF member(t, args) AND
    NOT var?(t) 

not_var_args_get_args: LEMMA
    member(s, not_var_args(f)(t)) IMPLIES member(s, get_args(f)(t))

not_var_args_get_args2: LEMMA
    member(s, not_var_args(f)(t)) IFF member(s, get_args(f)(t)) AND
    NOT var?(s)

not_var_args_nth2: LEMMA
    i < length(not_var_args(f)(t)) IMPLIES EXISTS j:
    j < length(get_args(f)(t)) AND
    nth(not_var_args(f)(t), i) = nth(get_args(f)(t), j) 

% subterms and prop subterms
subterm_fin_set: LEMMA
   member(s, subterms(fin_set_t)) IFF
   EXISTS t:
      member(t, fin_set_t) AND member(s, subterms(t))
   
subterm_args: LEMMA
   member(s, subterms(args)) IFF
   EXISTS t:
      member(t, args) AND member(s, subterms(t))
   
subterm_singleton: LEMMA
   subterms(singleton(t)) = subterms(t)

subterm_reflexive: LEMMA
   NOT pair?(t) IMPLIES member(t, subterms(t))

subterm_not_pair: LEMMA
   member(s, subterms(t)) IMPLIES NOT pair?(s)

subterm_reflexive_finset: LEMMA
   no_pair?(fin_set_t) AND member(t, fin_set_t) IMPLIES member(t, subterms(fin_set_t))

select_subterms: LEMMA
   member(select(f, t)(n), subterms(t))

subterm_fin_set_mem: LEMMA
   member(t, fin_set_t) IMPLIES subset?(subterms(t), subterms(fin_set_t))

vars_subterm: LEMMA
   (member(X, vars(s)) AND member(s, subterms(t))) IMPLIES member(X, vars(t))

vars_subterm2: LEMMA
   member(X, vars(s)) IMPLIES EXISTS t: member(X, vars(t)) AND member(t, subterms(s))

subterm_size: LEMMA
   member(s, subterms(t)) IMPLIES size(s) <= size(t) 

subterm_transitive: LEMMA
   member(s, subterms(t)) AND member(t, subterms(t1)) IMPLIES
   member(s, subterms(t1))

get_args_subterms: LEMMA
   member(s, get_args(f)(t)) IMPLIES subset?(subterms(s), subterms(t))

get_args_subterms2: LEMMA
   member(s, get_args(f)(t)) IMPLIES member(s, subterms(t))

prop_subterm_subterm_size: LEMMA
    member(s, prop_subterms(t)) IMPLIES member(s, subterms(t)) AND size(s) < size(t)

prop_subterm_subterm: LEMMA
    member(s, prop_subterms(t)) IMPLIES member(s, subterms(t)) AND s /= t
    
vars_prop_subterm: LEMMA
   (member(X, vars(s)) AND member(s, prop_subterms(t))) IMPLIES member(X, vars(t))

% flatten_pair
var_flatten_pair_implies_var: LEMMA
   member(variable(X), list2set(flatten_pair(t))) IMPLIES member(X, vars(t))

flatten_pair_not_pair: LEMMA
   member(s, flatten_pair(t)) IMPLIES NOT pair?(s) 

flatten_pair_subterms: LEMMA
   member(s, flatten_pair(t)) IMPLIES member(s, subterms(t)) 

flatten_pair_size: LEMMA
   member(s, flatten_pair(t)) IMPLIES size(s) <= size(t)

same_func_sym: LEMMA
    same_func?(t, s) = same_func?(s, t)

same_func_trans: LEMMA
    same_func?(t, s) AND same_func?(s, t1) IMPLIES same_func?(t, t1) 

same_func_dif_func: LEMMA
    func?(t) AND func?(s) IMPLIES (same_func?(t, s) OR dif_func?(t, s))

dif_func_sym: LEMMA
    dif_func?(s, t) = dif_func?(t, s)

cond_dif_func: LEMMA
    dif_func?(s, t) AND same_func?(t, t1) IMPLIES dif_func?(s, t1)

% size2
size2_ge0: LEMMA
    size2(t) > 0 

size2_get_args: LEMMA
    size2(t) = sum(map(size2)(get_args(f)(t)))

 END first_order_terms_properties