mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
1822 lines
80 KiB
Plaintext
1822 lines
80 KiB
Plaintext
module Types
|
|
use option.Option
|
|
use int.Int
|
|
use Nat.Nat
|
|
use Functions.Func
|
|
use OptionFuncs.Funcs
|
|
use Sum.Sum
|
|
use Firstorder_symbol_spec.Spec
|
|
use Firstorder_symbol_impl.Types
|
|
use Firstorder_symbol_impl.Logic
|
|
use Firstorder_symbol_impl.Impl
|
|
use Firstorder_term_spec.Spec
|
|
use Firstorder_term_impl.Types
|
|
use Firstorder_term_impl.Logic
|
|
use Firstorder_term_impl.Impl
|
|
use Firstorder_formula_spec.Spec
|
|
use Firstorder_formula_impl.Types
|
|
use Firstorder_formula_impl.Logic
|
|
use Firstorder_formula_impl.Impl
|
|
use Firstorder_formula_list_spec.Spec
|
|
use Firstorder_formula_list_impl.Types
|
|
use Firstorder_formula_list_impl.Logic
|
|
use Firstorder_formula_list_impl.Impl
|
|
use Firstorder_tableau_spec.Spec
|
|
type nl_tableau 'b0 'b1 =
|
|
| NL_Root
|
|
| NL_Node (nl_tableau 'b0 'b1) (nl_fo_formula 'b0 'b1)
|
|
(nl_fo_formula_list 'b0 'b1)
|
|
|
|
|
|
type nlimpl_tableau =
|
|
{ nlrepr_tableau_field : nl_tableau int int ;
|
|
nlfree_var_symbol_set_abstraction_tableau_field : int ;
|
|
nlfree_var_fo_term_set_abstraction_tableau_field : int ;
|
|
ghost model_tableau_field : tableau int int ;
|
|
}
|
|
|
|
type cons_tableau = | NLC_Root
|
|
| NLC_Node (nlimpl_tableau) (nlimpl_fo_formula) (nlimpl_fo_formula_list)
|
|
|
|
|
|
end
|
|
|
|
module Logic
|
|
use option.Option
|
|
use int.Int
|
|
use Nat.Nat
|
|
use Functions.Func
|
|
use OptionFuncs.Funcs
|
|
use Sum.Sum
|
|
use Firstorder_symbol_spec.Spec
|
|
use Firstorder_symbol_impl.Types
|
|
use Firstorder_symbol_impl.Logic
|
|
use Firstorder_symbol_impl.Impl
|
|
use Firstorder_term_spec.Spec
|
|
use Firstorder_term_impl.Types
|
|
use Firstorder_term_impl.Logic
|
|
use Firstorder_term_impl.Impl
|
|
use Firstorder_formula_spec.Spec
|
|
use Firstorder_formula_impl.Types
|
|
use Firstorder_formula_impl.Logic
|
|
use Firstorder_formula_impl.Impl
|
|
use Firstorder_formula_list_spec.Spec
|
|
use Firstorder_formula_list_impl.Types
|
|
use Firstorder_formula_list_impl.Logic
|
|
use Firstorder_formula_list_impl.Impl
|
|
use Firstorder_tableau_spec.Spec
|
|
use Types
|
|
function nat_nlsize_tableau (t:nl_tableau 'b0 'b1) : nat =
|
|
match t with | NL_Root -> let s = one_nat in s
|
|
| NL_Node v0 v1 v2 ->
|
|
let s = one_nat in
|
|
let s = add_nat (nat_nlsize_fo_formula_list v2) s in
|
|
let s = add_nat (nat_nlsize_fo_formula v1) s in
|
|
let s = add_nat (nat_nlsize_tableau v0) s in s
|
|
end
|
|
|
|
with nlsize_tableau (t:nl_tableau 'b0 'b1) : int =
|
|
match t with | NL_Root -> let s = 1 in s
|
|
| NL_Node v0 v1 v2 ->
|
|
let s = 1 in let s = nlsize_fo_formula_list v2 + s in
|
|
let s = nlsize_fo_formula v1 + s in let s = nlsize_tableau v0 +
|
|
s in s
|
|
end
|
|
|
|
let rec lemma nlsize_positive_lemma_tableau (t:nl_tableau 'b0 'b1) : unit
|
|
ensures { nlsize_tableau t > 0 }
|
|
variant { nat_to_int (nat_nlsize_tableau t) } =
|
|
match t with | NL_Root -> ()
|
|
| NL_Node v0 v1 v2 ->
|
|
nlsize_positive_lemma_tableau v0 ;
|
|
nlsize_positive_lemma_fo_formula v1 ;
|
|
nlsize_positive_lemma_fo_formula_list v2 ; ()
|
|
end
|
|
|
|
function nlmodel_tableau (t:nl_tableau 'b0 'b1) (fr0:'b0 -> (symbol 'c0))
|
|
(bnd0: int -> (symbol 'c0)) (fr1:'b1 -> (fo_term 'c0 'c1))
|
|
(bnd1: int -> (fo_term 'c0 'c1)) : tableau 'c0 'c1 =
|
|
match t with | NL_Root -> Root
|
|
| NL_Node v0 v1 v2 ->
|
|
Node
|
|
(nlmodel_tableau v0 ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity)))
|
|
(nlmodel_fo_formula v1 ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity)))
|
|
(nlmodel_fo_formula_list v2 ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity)))
|
|
end
|
|
|
|
let rec lemma nlmodel_subst_commutation_lemma_tableau
|
|
(t:nl_tableau 'b0 'b1) (fr0:'b0 -> (symbol 'c0))
|
|
(bnd0: int -> (symbol 'c0)) (s0:'c0 -> (symbol 'd0))
|
|
(fr1:'b1 -> (fo_term 'c0 'c1)) (bnd1: int -> (fo_term 'c0 'c1))
|
|
(s1:'c1 -> (fo_term 'd0 'd1)) : unit
|
|
ensures {
|
|
nlmodel_tableau t (subst_compose_symbol fr0 s0)
|
|
(subst_compose_symbol bnd0 s0) (subst_compose_fo_term fr1 s0 s1)
|
|
(subst_compose_fo_term bnd1 s0 s1)
|
|
= subst_tableau (nlmodel_tableau t fr0 bnd0 fr1 bnd1) s0 s1 }
|
|
variant { nlsize_tableau t } =
|
|
match t with | NL_Root -> ()
|
|
| NL_Node v0 v1 v2 ->
|
|
nlmodel_subst_commutation_lemma_tableau v0
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity))
|
|
((rename_subst_fo_term s1 identity identity)) ;
|
|
assert {
|
|
subst_compose_symbol (rename_subst_symbol fr0 identity)
|
|
((rename_subst_symbol s0 identity))
|
|
= (rename_subst_symbol (subst_compose_symbol fr0 s0) identity) } ;
|
|
assert {
|
|
subst_compose_symbol (rename_subst_symbol bnd0 identity)
|
|
((rename_subst_symbol s0 identity))
|
|
= (rename_subst_symbol (subst_compose_symbol bnd0 s0) identity)
|
|
} ;
|
|
assert {
|
|
subst_compose_fo_term
|
|
(rename_subst_fo_term fr1 identity identity)
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term s1 identity identity))
|
|
=
|
|
(rename_subst_fo_term (subst_compose_fo_term fr1 s0 s1) identity
|
|
identity)
|
|
} ;
|
|
assert {
|
|
subst_compose_fo_term
|
|
(rename_subst_fo_term bnd1 identity identity)
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term s1 identity identity))
|
|
=
|
|
(rename_subst_fo_term (subst_compose_fo_term bnd1 s0 s1)
|
|
identity identity)
|
|
} ;
|
|
nlmodel_subst_commutation_lemma_fo_formula v1
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity))
|
|
((rename_subst_fo_term s1 identity identity)) ;
|
|
assert {
|
|
subst_compose_symbol (rename_subst_symbol fr0 identity)
|
|
((rename_subst_symbol s0 identity))
|
|
= (rename_subst_symbol (subst_compose_symbol fr0 s0) identity) } ;
|
|
assert {
|
|
subst_compose_symbol (rename_subst_symbol bnd0 identity)
|
|
((rename_subst_symbol s0 identity))
|
|
= (rename_subst_symbol (subst_compose_symbol bnd0 s0) identity)
|
|
} ;
|
|
assert {
|
|
subst_compose_fo_term
|
|
(rename_subst_fo_term fr1 identity identity)
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term s1 identity identity))
|
|
=
|
|
(rename_subst_fo_term (subst_compose_fo_term fr1 s0 s1) identity
|
|
identity)
|
|
} ;
|
|
assert {
|
|
subst_compose_fo_term
|
|
(rename_subst_fo_term bnd1 identity identity)
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term s1 identity identity))
|
|
=
|
|
(rename_subst_fo_term (subst_compose_fo_term bnd1 s0 s1)
|
|
identity identity)
|
|
} ;
|
|
nlmodel_subst_commutation_lemma_fo_formula_list v2
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity))
|
|
((rename_subst_fo_term s1 identity identity)) ;
|
|
assert {
|
|
subst_compose_symbol (rename_subst_symbol fr0 identity)
|
|
((rename_subst_symbol s0 identity))
|
|
= (rename_subst_symbol (subst_compose_symbol fr0 s0) identity) } ;
|
|
assert {
|
|
subst_compose_symbol (rename_subst_symbol bnd0 identity)
|
|
((rename_subst_symbol s0 identity))
|
|
= (rename_subst_symbol (subst_compose_symbol bnd0 s0) identity)
|
|
} ;
|
|
assert {
|
|
subst_compose_fo_term
|
|
(rename_subst_fo_term fr1 identity identity)
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term s1 identity identity))
|
|
=
|
|
(rename_subst_fo_term (subst_compose_fo_term fr1 s0 s1) identity
|
|
identity)
|
|
} ;
|
|
assert {
|
|
subst_compose_fo_term
|
|
(rename_subst_fo_term bnd1 identity identity)
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term s1 identity identity))
|
|
=
|
|
(rename_subst_fo_term (subst_compose_fo_term bnd1 s0 s1)
|
|
identity identity)
|
|
} ;
|
|
()
|
|
end
|
|
|
|
let lemma nlmodel_rename_commutation_lemma_tableau (t:nl_tableau 'b0 'b1)
|
|
(fr0:'b0 -> (symbol 'c0)) (bnd0: int -> (symbol 'c0)) (s0:'c0 -> 'd0)
|
|
(fr1:'b1 -> (fo_term 'c0 'c1)) (bnd1: int -> (fo_term 'c0 'c1))
|
|
(s1:'c1 -> 'd1) : unit
|
|
ensures {
|
|
nlmodel_tableau t (rename_subst_symbol fr0 s0)
|
|
(rename_subst_symbol bnd0 s0) (rename_subst_fo_term fr1 s0 s1)
|
|
(rename_subst_fo_term bnd1 s0 s1)
|
|
= rename_tableau (nlmodel_tableau t fr0 bnd0 fr1 bnd1) s0 s1 }
|
|
=
|
|
nlmodel_subst_commutation_lemma_tableau t fr0 bnd0
|
|
(subst_of_rename_symbol s0) fr1 bnd1 (subst_of_rename_fo_term s1)
|
|
|
|
predicate correct_indexes_tableau (t:nl_tableau 'b0 'b1) =
|
|
match t with | NL_Root -> true
|
|
| NL_Node v0 v1 v2 ->
|
|
correct_indexes_tableau v0 /\ correct_indexes_fo_formula v1 /\
|
|
correct_indexes_fo_formula_list v2
|
|
end
|
|
|
|
function bound_depth_of_symbol_in_tableau (t:nl_tableau 'b0 'b1) : int =
|
|
match t with | NL_Root -> 0
|
|
| NL_Node v0 v1 v2 ->
|
|
let b = bound_depth_of_symbol_in_tableau v0 in let a = b in
|
|
let b = bound_depth_of_symbol_in_fo_formula v1 in
|
|
let a = if a > b then a else b in
|
|
let b = bound_depth_of_symbol_in_fo_formula_list v2 in
|
|
let a = if a > b then a else b in a
|
|
end
|
|
|
|
with bound_depth_of_fo_term_in_tableau (t:nl_tableau 'b0 'b1) : int =
|
|
match t with | NL_Root -> 0
|
|
| NL_Node v0 v1 v2 ->
|
|
let b = bound_depth_of_fo_term_in_tableau v0 in let a = b in
|
|
let b = bound_depth_of_fo_term_in_fo_formula v1 in
|
|
let a = if a > b then a else b in
|
|
let b = bound_depth_of_fo_term_in_fo_formula_list v2 in
|
|
let a = if a > b then a else b in a
|
|
end
|
|
|
|
let rec lemma bound_depth_of_symbol_in_tableau_nonnegative
|
|
(t:nl_tableau 'b0 'b1) : unit requires { correct_indexes_tableau t }
|
|
ensures { bound_depth_of_symbol_in_tableau t >= 0 }
|
|
variant { nlsize_tableau t } =
|
|
match t with | NL_Root -> ()
|
|
| NL_Node v0 v1 v2 ->
|
|
bound_depth_of_symbol_in_tableau_nonnegative v0 ;
|
|
bound_depth_of_symbol_in_fo_formula_nonnegative v1 ;
|
|
bound_depth_of_symbol_in_fo_formula_list_nonnegative v2 ; ()
|
|
end
|
|
|
|
with lemma bound_depth_of_fo_term_in_tableau_nonnegative
|
|
(t:nl_tableau 'b0 'b1) : unit requires { correct_indexes_tableau t }
|
|
ensures { bound_depth_of_fo_term_in_tableau t >= 0 }
|
|
variant { nlsize_tableau t } =
|
|
match t with | NL_Root -> ()
|
|
| NL_Node v0 v1 v2 ->
|
|
bound_depth_of_fo_term_in_tableau_nonnegative v0 ;
|
|
bound_depth_of_fo_term_in_fo_formula_nonnegative v1 ;
|
|
bound_depth_of_fo_term_in_fo_formula_list_nonnegative v2 ; ()
|
|
end
|
|
|
|
let rec lemma model_equal_tableau (t:nl_tableau 'b0 'b1)
|
|
(fr10: 'b0 -> (symbol 'c0)) (fr20: 'b0 -> (symbol 'c0))
|
|
(bnd10: int -> (symbol 'c0)) (bnd20: int -> (symbol 'c0))
|
|
(fr11: 'b1 -> (fo_term 'c0 'c1)) (fr21: 'b1 -> (fo_term 'c0 'c1))
|
|
(bnd11: int -> (fo_term 'c0 'c1)) (bnd21: int -> (fo_term 'c0 'c1)) :
|
|
unit
|
|
requires {
|
|
forall i:int. 0 <= i < bound_depth_of_symbol_in_tableau t -> bnd10 i =
|
|
bnd20 i
|
|
}
|
|
requires { fr10 = fr20 }
|
|
requires {
|
|
forall i:int. 0 <= i < bound_depth_of_fo_term_in_tableau t -> bnd11 i
|
|
= bnd21 i
|
|
}
|
|
requires { fr11 = fr21 } requires { correct_indexes_tableau t }
|
|
ensures { nlmodel_tableau t fr10 bnd10 fr11 bnd11 =
|
|
nlmodel_tableau t fr20 bnd20 fr21 bnd21 }
|
|
variant { nlsize_tableau t } =
|
|
match t with | NL_Root -> ()
|
|
| NL_Node v0 v1 v2 ->
|
|
model_equal_tableau v0 ((rename_subst_symbol fr10 identity))
|
|
((rename_subst_symbol fr20 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr11 identity identity))
|
|
((rename_subst_fo_term fr21 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity)) ;
|
|
model_equal_fo_formula v1 ((rename_subst_symbol fr10 identity))
|
|
((rename_subst_symbol fr20 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr11 identity identity))
|
|
((rename_subst_fo_term fr21 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity)) ;
|
|
model_equal_fo_formula_list v2
|
|
((rename_subst_symbol fr10 identity))
|
|
((rename_subst_symbol fr20 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr11 identity identity))
|
|
((rename_subst_fo_term fr21 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity)) ;
|
|
()
|
|
end
|
|
|
|
predicate nlimpl_tableau_ok (t:nlimpl_tableau) =
|
|
nlmodel_tableau t.nlrepr_tableau_field subst_id_symbol
|
|
(const (Var_symbol ((-1)))) subst_id_fo_term
|
|
(const (Var_fo_term ((-1)))) = t.model_tableau_field
|
|
/\ correct_indexes_tableau t.nlrepr_tableau_field /\
|
|
bound_depth_of_symbol_in_tableau t.nlrepr_tableau_field = 0 /\
|
|
bound_depth_of_fo_term_in_tableau t.nlrepr_tableau_field = 0 /\
|
|
(forall x:int. is_symbol_free_var_in_tableau x t.model_tableau_field ->
|
|
(x) < (t.nlfree_var_symbol_set_abstraction_tableau_field))
|
|
/\
|
|
(forall x:int. is_fo_term_free_var_in_tableau x t.model_tableau_field ->
|
|
(x) < (t.nlfree_var_fo_term_set_abstraction_tableau_field))
|
|
|
|
predicate cons_ok_tableau (c:cons_tableau) =
|
|
match c with | NLC_Root -> true
|
|
| NLC_Node v0 v1 v2 -> nlimpl_tableau_ok v0 /\ nlimpl_fo_formula_ok v1
|
|
/\ nlimpl_fo_formula_list_ok v2
|
|
end
|
|
|
|
predicate cons_rel_tableau (c:cons_tableau) (t:nlimpl_tableau) =
|
|
match c with | NLC_Root -> t.model_tableau_field = Root
|
|
| NLC_Node v0 v1 v2 -> t.model_tableau_field =
|
|
Node (rename_tableau v0.model_tableau_field identity identity)
|
|
(rename_fo_formula v1.model_fo_formula_field identity identity)
|
|
(rename_fo_formula_list v2.model_fo_formula_list_field identity
|
|
identity)
|
|
end
|
|
|
|
predicate cons_open_rel_tableau (c:cons_tableau) (t:nlimpl_tableau) =
|
|
match c with
|
|
| NLC_Root ->
|
|
match t.model_tableau_field with | Root -> true
|
|
| Node w0 w1 w2 -> false
|
|
end
|
|
| NLC_Node v0 v1 v2 ->
|
|
match t.model_tableau_field with | Root -> false
|
|
| Node w0 w1 w2 ->
|
|
v0.model_tableau_field = (rename_tableau w0 identity identity) /\
|
|
v1.model_fo_formula_field =
|
|
(rename_fo_formula w1 identity identity)
|
|
/\
|
|
v2.model_fo_formula_list_field =
|
|
(rename_fo_formula_list w2 identity identity)
|
|
end
|
|
end
|
|
|
|
|
|
end
|
|
|
|
module Impl
|
|
use option.Option
|
|
use int.Int
|
|
use Nat.Nat
|
|
use Functions.Func
|
|
use OptionFuncs.Funcs
|
|
use Sum.Sum
|
|
use Firstorder_symbol_spec.Spec
|
|
use Firstorder_symbol_impl.Types
|
|
use Firstorder_symbol_impl.Logic
|
|
use Firstorder_symbol_impl.Impl
|
|
use Firstorder_term_spec.Spec
|
|
use Firstorder_term_impl.Types
|
|
use Firstorder_term_impl.Logic
|
|
use Firstorder_term_impl.Impl
|
|
use Firstorder_formula_spec.Spec
|
|
use Firstorder_formula_impl.Types
|
|
use Firstorder_formula_impl.Logic
|
|
use Firstorder_formula_impl.Impl
|
|
use Firstorder_formula_list_spec.Spec
|
|
use Firstorder_formula_list_impl.Types
|
|
use Firstorder_formula_list_impl.Logic
|
|
use Firstorder_formula_list_impl.Impl
|
|
use Firstorder_tableau_spec.Spec
|
|
use Types
|
|
use Logic
|
|
let rec bind_var_symbol_in_tableau (t:nl_tableau int int) (x:int) (i:int)
|
|
(ghost fr0: int -> (symbol 'b0)) (ghost bnd0: int -> (symbol 'b0))
|
|
(ghost fr1: int -> (fo_term 'b0 'b1))
|
|
(ghost bnd1: int -> (fo_term 'b0 'b1)) : nl_tableau int int
|
|
requires { correct_indexes_tableau t }
|
|
requires { bound_depth_of_symbol_in_tableau t <= i }
|
|
variant { nlsize_tableau t }
|
|
ensures { bound_depth_of_symbol_in_tableau result <= i + 1 }
|
|
ensures { correct_indexes_tableau result }
|
|
ensures { bound_depth_of_fo_term_in_tableau t =
|
|
bound_depth_of_fo_term_in_tableau result }
|
|
ensures { nlmodel_tableau result fr0 bnd0 fr1 bnd1 =
|
|
nlmodel_tableau t (update fr0 x (bnd0 i)) bnd0 fr1 bnd1 }
|
|
=
|
|
match t with | NL_Root -> NL_Root
|
|
| NL_Node v0 v1 v2 ->
|
|
assert { (rename_symbol (bnd0 i) identity) =
|
|
(eval ((rename_subst_symbol bnd0 identity)) (i+0)) };
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol (update fr0 x (bnd0 i)) identity))
|
|
((update ((rename_subst_symbol fr0 identity)) x
|
|
(rename_symbol (bnd0 i) identity)))
|
|
};
|
|
assert { (rename_subst_symbol (update fr0 x (bnd0 i)) identity) =
|
|
(update ((rename_subst_symbol fr0 identity)) x
|
|
(eval ((rename_subst_symbol bnd0 identity)) (i+0)))
|
|
};
|
|
assert { (rename_symbol (bnd0 i) identity) =
|
|
(eval ((rename_subst_symbol bnd0 identity)) (i+0)) };
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol (update fr0 x (bnd0 i)) identity))
|
|
((update ((rename_subst_symbol fr0 identity)) x
|
|
(rename_symbol (bnd0 i) identity)))
|
|
};
|
|
assert { (rename_subst_symbol (update fr0 x (bnd0 i)) identity) =
|
|
(update ((rename_subst_symbol fr0 identity)) x
|
|
(eval ((rename_subst_symbol bnd0 identity)) (i+0)))
|
|
};
|
|
assert { (rename_symbol (bnd0 i) identity) =
|
|
(eval ((rename_subst_symbol bnd0 identity)) (i+0)) };
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol (update fr0 x (bnd0 i)) identity))
|
|
((update ((rename_subst_symbol fr0 identity)) x
|
|
(rename_symbol (bnd0 i) identity)))
|
|
};
|
|
assert { (rename_subst_symbol (update fr0 x (bnd0 i)) identity) =
|
|
(update ((rename_subst_symbol fr0 identity)) x
|
|
(eval ((rename_subst_symbol bnd0 identity)) (i+0)))
|
|
};
|
|
NL_Node
|
|
(bind_var_symbol_in_tableau v0 x (i+0)
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity)))
|
|
(bind_var_symbol_in_fo_formula v1 x (i+0)
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity)))
|
|
(bind_var_symbol_in_fo_formula_list v2 x (i+0)
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity)))
|
|
end
|
|
|
|
with bind_var_fo_term_in_tableau (t:nl_tableau int int) (x:int) (i:int)
|
|
(ghost fr0: int -> (symbol 'b0)) (ghost bnd0: int -> (symbol 'b0))
|
|
(ghost fr1: int -> (fo_term 'b0 'b1))
|
|
(ghost bnd1: int -> (fo_term 'b0 'b1)) : nl_tableau int int
|
|
requires { correct_indexes_tableau t }
|
|
requires { bound_depth_of_fo_term_in_tableau t <= i }
|
|
variant { nlsize_tableau t }
|
|
ensures { bound_depth_of_fo_term_in_tableau result <= i + 1 }
|
|
ensures { correct_indexes_tableau result }
|
|
ensures { bound_depth_of_symbol_in_tableau t =
|
|
bound_depth_of_symbol_in_tableau result }
|
|
ensures { nlmodel_tableau result fr0 bnd0 fr1 bnd1 =
|
|
nlmodel_tableau t fr0 bnd0 (update fr1 x (bnd1 i)) bnd1 }
|
|
=
|
|
match t with | NL_Root -> NL_Root
|
|
| NL_Node v0 v1 v2 ->
|
|
assert { (rename_fo_term (bnd1 i) identity identity) =
|
|
(eval ((rename_subst_fo_term bnd1 identity identity)) (i+0)) };
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term (update fr1 x (bnd1 i)) identity
|
|
identity))
|
|
((update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(rename_fo_term (bnd1 i) identity identity)))
|
|
};
|
|
assert {
|
|
(rename_subst_fo_term (update fr1 x (bnd1 i)) identity identity)
|
|
=
|
|
(update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(eval ((rename_subst_fo_term bnd1 identity identity)) (i+0)))
|
|
};
|
|
assert { (rename_fo_term (bnd1 i) identity identity) =
|
|
(eval ((rename_subst_fo_term bnd1 identity identity)) (i+0)) };
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term (update fr1 x (bnd1 i)) identity
|
|
identity))
|
|
((update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(rename_fo_term (bnd1 i) identity identity)))
|
|
};
|
|
assert {
|
|
(rename_subst_fo_term (update fr1 x (bnd1 i)) identity identity)
|
|
=
|
|
(update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(eval ((rename_subst_fo_term bnd1 identity identity)) (i+0)))
|
|
};
|
|
assert { (rename_fo_term (bnd1 i) identity identity) =
|
|
(eval ((rename_subst_fo_term bnd1 identity identity)) (i+0)) };
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term (update fr1 x (bnd1 i)) identity
|
|
identity))
|
|
((update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(rename_fo_term (bnd1 i) identity identity)))
|
|
};
|
|
assert {
|
|
(rename_subst_fo_term (update fr1 x (bnd1 i)) identity identity)
|
|
=
|
|
(update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(eval ((rename_subst_fo_term bnd1 identity identity)) (i+0)))
|
|
};
|
|
NL_Node
|
|
(bind_var_fo_term_in_tableau v0 x (i+0)
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity)))
|
|
(bind_var_fo_term_in_fo_formula v1 x (i+0)
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity)))
|
|
(bind_var_fo_term_in_fo_formula_list v2 x (i+0)
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity)))
|
|
end
|
|
|
|
let rec unbind_var_symbol_in_tableau (t:nl_tableau int int) (i:int)
|
|
(x:nl_symbol int) (ghost fr0: int -> (symbol 'b0))
|
|
(ghost bnd10: int -> (symbol 'b0)) (ghost fr1: int -> (fo_term 'b0 'b1))
|
|
(ghost bnd11: int -> (fo_term 'b0 'b1))
|
|
(ghost bnd20: int -> (symbol 'b0)) : nl_tableau int int
|
|
requires { i >= 0 } requires { correct_indexes_tableau t }
|
|
requires { bound_depth_of_symbol_in_tableau t <= i + 1 }
|
|
requires { correct_indexes_symbol x }
|
|
requires { bound_depth_of_symbol_in_symbol x = 0 }
|
|
variant { nlsize_tableau t }
|
|
ensures { correct_indexes_tableau result }
|
|
ensures { bound_depth_of_symbol_in_tableau result <= i }
|
|
ensures { bound_depth_of_fo_term_in_tableau result =
|
|
bound_depth_of_fo_term_in_tableau t }
|
|
ensures { nlmodel_tableau result fr0 bnd10 fr1 bnd11 =
|
|
nlmodel_tableau t fr0 (update bnd10 i (nlmodel_symbol x fr0 bnd20)) fr1
|
|
bnd11
|
|
}
|
|
=
|
|
match t with | NL_Root -> NL_Root
|
|
| NL_Node v0 v1 v2 ->
|
|
assert { rename_symbol (nlmodel_symbol x fr0 bnd20) identity =
|
|
nlmodel_symbol x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol
|
|
(update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity))
|
|
(update ((rename_subst_symbol bnd10 identity)) (i+0)
|
|
(rename_symbol (nlmodel_symbol x fr0 bnd20) identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_symbol
|
|
(update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity)
|
|
=
|
|
update ((rename_subst_symbol bnd10 identity)) (i+0)
|
|
(nlmodel_symbol x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
} ;
|
|
assert { rename_symbol (nlmodel_symbol x fr0 bnd20) identity =
|
|
nlmodel_symbol x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol
|
|
(update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity))
|
|
(update ((rename_subst_symbol bnd10 identity)) (i+0)
|
|
(rename_symbol (nlmodel_symbol x fr0 bnd20) identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_symbol
|
|
(update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity)
|
|
=
|
|
update ((rename_subst_symbol bnd10 identity)) (i+0)
|
|
(nlmodel_symbol x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
} ;
|
|
assert { rename_symbol (nlmodel_symbol x fr0 bnd20) identity =
|
|
nlmodel_symbol x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol
|
|
(update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity))
|
|
(update ((rename_subst_symbol bnd10 identity)) (i+0)
|
|
(rename_symbol (nlmodel_symbol x fr0 bnd20) identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_symbol
|
|
(update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity)
|
|
=
|
|
update ((rename_subst_symbol bnd10 identity)) (i+0)
|
|
(nlmodel_symbol x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
} ;
|
|
NL_Node
|
|
(unbind_var_symbol_in_tableau v0 (i+0) x
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
(unbind_var_symbol_in_fo_formula v1 (i+0) x
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
(unbind_var_symbol_in_fo_formula_list v2 (i+0) x
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
end
|
|
|
|
with unbind_var_fo_term_in_tableau (t:nl_tableau int int) (i:int)
|
|
(x:nl_fo_term int int) (ghost fr0: int -> (symbol 'b0))
|
|
(ghost bnd10: int -> (symbol 'b0)) (ghost fr1: int -> (fo_term 'b0 'b1))
|
|
(ghost bnd11: int -> (fo_term 'b0 'b1))
|
|
(ghost bnd20: int -> (symbol 'b0))
|
|
(ghost bnd21: int -> (fo_term 'b0 'b1)) : nl_tableau int int
|
|
requires { i >= 0 } requires { correct_indexes_tableau t }
|
|
requires { bound_depth_of_fo_term_in_tableau t <= i + 1 }
|
|
requires { correct_indexes_fo_term x }
|
|
requires { bound_depth_of_symbol_in_fo_term x = 0 }
|
|
requires { bound_depth_of_fo_term_in_fo_term x = 0 }
|
|
variant { nlsize_tableau t }
|
|
ensures { correct_indexes_tableau result }
|
|
ensures { bound_depth_of_fo_term_in_tableau result <= i }
|
|
ensures { bound_depth_of_symbol_in_tableau result =
|
|
bound_depth_of_symbol_in_tableau t }
|
|
ensures { nlmodel_tableau result fr0 bnd10 fr1 bnd11 =
|
|
nlmodel_tableau t fr0 bnd10 fr1
|
|
(update bnd11 i (nlmodel_fo_term x fr0 bnd20 fr1 bnd21))
|
|
}
|
|
=
|
|
match t with | NL_Root -> NL_Root
|
|
| NL_Node v0 v1 v2 ->
|
|
assert {
|
|
rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr1 bnd21) identity
|
|
identity
|
|
=
|
|
nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term
|
|
(update bnd11 i (nlmodel_fo_term x fr0 bnd20 fr1 bnd21))
|
|
identity identity))
|
|
(update ((rename_subst_fo_term bnd11 identity identity)) (i+0)
|
|
(rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr1 bnd21)
|
|
identity identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_fo_term
|
|
(update bnd11 i (nlmodel_fo_term x fr0 bnd20 fr1 bnd21))
|
|
identity identity)
|
|
=
|
|
update ((rename_subst_fo_term bnd11 identity identity)) (i+0)
|
|
(nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
} ;
|
|
assert {
|
|
rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr1 bnd21) identity
|
|
identity
|
|
=
|
|
nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term
|
|
(update bnd11 i (nlmodel_fo_term x fr0 bnd20 fr1 bnd21))
|
|
identity identity))
|
|
(update ((rename_subst_fo_term bnd11 identity identity)) (i+0)
|
|
(rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr1 bnd21)
|
|
identity identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_fo_term
|
|
(update bnd11 i (nlmodel_fo_term x fr0 bnd20 fr1 bnd21))
|
|
identity identity)
|
|
=
|
|
update ((rename_subst_fo_term bnd11 identity identity)) (i+0)
|
|
(nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
} ;
|
|
assert {
|
|
rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr1 bnd21) identity
|
|
identity
|
|
=
|
|
nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term
|
|
(update bnd11 i (nlmodel_fo_term x fr0 bnd20 fr1 bnd21))
|
|
identity identity))
|
|
(update ((rename_subst_fo_term bnd11 identity identity)) (i+0)
|
|
(rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr1 bnd21)
|
|
identity identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_fo_term
|
|
(update bnd11 i (nlmodel_fo_term x fr0 bnd20 fr1 bnd21))
|
|
identity identity)
|
|
=
|
|
update ((rename_subst_fo_term bnd11 identity identity)) (i+0)
|
|
(nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
} ;
|
|
NL_Node
|
|
(unbind_var_fo_term_in_tableau v0 (i+0) x
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
(unbind_var_fo_term_in_fo_formula v1 (i+0) x
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
(unbind_var_fo_term_in_fo_formula_list v2 (i+0) x
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
end
|
|
|
|
let rec subst_base_symbol_in_tableau (t:nl_tableau int int) (x:int)
|
|
(u:nl_symbol int) (ghost fr0: int -> (symbol 'b0))
|
|
(ghost bnd10: int -> (symbol 'b0)) (ghost fr1: int -> (fo_term 'b0 'b1))
|
|
(ghost bnd11: int -> (fo_term 'b0 'b1))
|
|
(ghost bnd20: int -> (symbol 'b0)) : nl_tableau int int
|
|
requires { correct_indexes_tableau t }
|
|
requires { correct_indexes_symbol u }
|
|
requires { bound_depth_of_symbol_in_symbol u = 0 }
|
|
variant { nlsize_tableau t }
|
|
ensures { correct_indexes_tableau result }
|
|
ensures { bound_depth_of_symbol_in_tableau result =
|
|
bound_depth_of_symbol_in_tableau t }
|
|
ensures { bound_depth_of_fo_term_in_tableau result =
|
|
bound_depth_of_fo_term_in_tableau t }
|
|
ensures { nlmodel_tableau result fr0 bnd10 fr1 bnd11 =
|
|
nlmodel_tableau t (update fr0 x (nlmodel_symbol u fr0 bnd20)) bnd10 fr1
|
|
bnd11
|
|
}
|
|
=
|
|
match t with | NL_Root -> NL_Root
|
|
| NL_Node v0 v1 v2 ->
|
|
assert { rename_symbol (nlmodel_symbol u fr0 bnd20) identity =
|
|
nlmodel_symbol u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol
|
|
(update fr0 x (nlmodel_symbol u fr0 bnd20)) identity))
|
|
(update ((rename_subst_symbol fr0 identity)) x
|
|
(rename_symbol (nlmodel_symbol u fr0 bnd20) identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_symbol (update fr0 x (nlmodel_symbol u fr0 bnd20))
|
|
identity)
|
|
=
|
|
update ((rename_subst_symbol fr0 identity)) x
|
|
(nlmodel_symbol u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
} ;
|
|
assert { rename_symbol (nlmodel_symbol u fr0 bnd20) identity =
|
|
nlmodel_symbol u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol
|
|
(update fr0 x (nlmodel_symbol u fr0 bnd20)) identity))
|
|
(update ((rename_subst_symbol fr0 identity)) x
|
|
(rename_symbol (nlmodel_symbol u fr0 bnd20) identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_symbol (update fr0 x (nlmodel_symbol u fr0 bnd20))
|
|
identity)
|
|
=
|
|
update ((rename_subst_symbol fr0 identity)) x
|
|
(nlmodel_symbol u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
} ;
|
|
assert { rename_symbol (nlmodel_symbol u fr0 bnd20) identity =
|
|
nlmodel_symbol u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol
|
|
(update fr0 x (nlmodel_symbol u fr0 bnd20)) identity))
|
|
(update ((rename_subst_symbol fr0 identity)) x
|
|
(rename_symbol (nlmodel_symbol u fr0 bnd20) identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_symbol (update fr0 x (nlmodel_symbol u fr0 bnd20))
|
|
identity)
|
|
=
|
|
update ((rename_subst_symbol fr0 identity)) x
|
|
(nlmodel_symbol u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
} ;
|
|
NL_Node
|
|
(subst_base_symbol_in_tableau v0 x u
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
(subst_base_symbol_in_fo_formula v1 x u
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
(subst_base_symbol_in_fo_formula_list v2 x u
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
end
|
|
|
|
with subst_base_fo_term_in_tableau (t:nl_tableau int int) (x:int)
|
|
(u:nl_fo_term int int) (ghost fr0: int -> (symbol 'b0))
|
|
(ghost bnd10: int -> (symbol 'b0)) (ghost fr1: int -> (fo_term 'b0 'b1))
|
|
(ghost bnd11: int -> (fo_term 'b0 'b1))
|
|
(ghost bnd20: int -> (symbol 'b0))
|
|
(ghost bnd21: int -> (fo_term 'b0 'b1)) : nl_tableau int int
|
|
requires { correct_indexes_tableau t }
|
|
requires { correct_indexes_fo_term u }
|
|
requires { bound_depth_of_symbol_in_fo_term u = 0 }
|
|
requires { bound_depth_of_fo_term_in_fo_term u = 0 }
|
|
variant { nlsize_tableau t }
|
|
ensures { correct_indexes_tableau result }
|
|
ensures { bound_depth_of_symbol_in_tableau result =
|
|
bound_depth_of_symbol_in_tableau t }
|
|
ensures { bound_depth_of_fo_term_in_tableau result =
|
|
bound_depth_of_fo_term_in_tableau t }
|
|
ensures { nlmodel_tableau result fr0 bnd10 fr1 bnd11 =
|
|
nlmodel_tableau t fr0 bnd10
|
|
(update fr1 x (nlmodel_fo_term u fr0 bnd20 fr1 bnd21)) bnd11
|
|
}
|
|
=
|
|
match t with | NL_Root -> NL_Root
|
|
| NL_Node v0 v1 v2 ->
|
|
assert {
|
|
rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr1 bnd21) identity
|
|
identity
|
|
=
|
|
nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term
|
|
(update fr1 x (nlmodel_fo_term u fr0 bnd20 fr1 bnd21))
|
|
identity identity))
|
|
(update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr1 bnd21)
|
|
identity identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_fo_term
|
|
(update fr1 x (nlmodel_fo_term u fr0 bnd20 fr1 bnd21)) identity
|
|
identity)
|
|
=
|
|
update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
} ;
|
|
assert {
|
|
rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr1 bnd21) identity
|
|
identity
|
|
=
|
|
nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term
|
|
(update fr1 x (nlmodel_fo_term u fr0 bnd20 fr1 bnd21))
|
|
identity identity))
|
|
(update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr1 bnd21)
|
|
identity identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_fo_term
|
|
(update fr1 x (nlmodel_fo_term u fr0 bnd20 fr1 bnd21)) identity
|
|
identity)
|
|
=
|
|
update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
} ;
|
|
assert {
|
|
rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr1 bnd21) identity
|
|
identity
|
|
=
|
|
nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term
|
|
(update fr1 x (nlmodel_fo_term u fr0 bnd20 fr1 bnd21))
|
|
identity identity))
|
|
(update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr1 bnd21)
|
|
identity identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_fo_term
|
|
(update fr1 x (nlmodel_fo_term u fr0 bnd20 fr1 bnd21)) identity
|
|
identity)
|
|
=
|
|
update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
} ;
|
|
NL_Node
|
|
(subst_base_fo_term_in_tableau v0 x u
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
(subst_base_fo_term_in_fo_formula v1 x u
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
(subst_base_fo_term_in_fo_formula_list v2 x u
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
end
|
|
|
|
let construct_tableau (c:cons_tableau) : nlimpl_tableau
|
|
requires { cons_ok_tableau c } ensures { nlimpl_tableau_ok result }
|
|
ensures { cons_rel_tableau c result }
|
|
(*ensures { cons_open_rel_tableau c result }*) =
|
|
match c with
|
|
| NLC_Root ->
|
|
let res =
|
|
{ nlrepr_tableau_field = (NL_Root) ;
|
|
nlfree_var_symbol_set_abstraction_tableau_field = 0 ;
|
|
nlfree_var_fo_term_set_abstraction_tableau_field = 0 ;
|
|
model_tableau_field = ghost (Root) ;
|
|
}
|
|
in
|
|
assert {
|
|
forall x:int.
|
|
is_symbol_free_var_in_tableau x res.model_tableau_field ->
|
|
(false) && (x) <
|
|
(res.nlfree_var_symbol_set_abstraction_tableau_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_fo_term_free_var_in_tableau x res.model_tableau_field ->
|
|
(false) && (x) <
|
|
(res.nlfree_var_fo_term_set_abstraction_tableau_field)
|
|
} ;
|
|
res
|
|
| NLC_Node v0 v1 v2 -> assert { nlimpl_tableau_ok v0 } ;
|
|
assert { nlimpl_fo_formula_ok v1 } ;
|
|
assert { nlimpl_fo_formula_list_ok v2 } ;
|
|
let res =
|
|
{
|
|
nlrepr_tableau_field =
|
|
(NL_Node (let v0 = v0.nlrepr_tableau_field in v0)
|
|
(let v1 = v1.nlrepr_fo_formula_field in v1)
|
|
(let v2 = v2.nlrepr_fo_formula_list_field in v2)) ;
|
|
nlfree_var_symbol_set_abstraction_tableau_field =
|
|
(let aux (a:int) (b:int) : int
|
|
ensures { result >= a /\ result >= b } =
|
|
if a < b then b else a in
|
|
aux
|
|
((let aux (a:int) (b:int) : int
|
|
ensures { result >= a /\ result >= b } =
|
|
if a < b then b else a in
|
|
aux
|
|
(v0.nlfree_var_symbol_set_abstraction_tableau_field)
|
|
(v1.nlfree_var_symbol_set_abstraction_fo_formula_field)))
|
|
(v2.nlfree_var_symbol_set_abstraction_fo_formula_list_field)) ;
|
|
nlfree_var_fo_term_set_abstraction_tableau_field =
|
|
(let aux (a:int) (b:int) : int
|
|
ensures { result >= a /\ result >= b } =
|
|
if a < b then b else a in
|
|
aux
|
|
((let aux (a:int) (b:int) : int
|
|
ensures { result >= a /\ result >= b } =
|
|
if a < b then b else a in
|
|
aux
|
|
(v0.nlfree_var_fo_term_set_abstraction_tableau_field)
|
|
(v1.nlfree_var_fo_term_set_abstraction_fo_formula_field)))
|
|
(v2.nlfree_var_fo_term_set_abstraction_fo_formula_list_field)) ;
|
|
model_tableau_field = ghost
|
|
(Node (rename_tableau v0.model_tableau_field identity identity)
|
|
(rename_fo_formula v1.model_fo_formula_field identity
|
|
identity)
|
|
(rename_fo_formula_list v2.model_fo_formula_list_field
|
|
identity identity)) ;
|
|
}
|
|
in
|
|
assert {
|
|
forall x:int.
|
|
is_symbol_free_var_in_tableau x
|
|
(rename_tableau v0.model_tableau_field identity identity)
|
|
->
|
|
(forall y:int.
|
|
(is_symbol_free_var_in_tableau y v0.model_tableau_field /\
|
|
eval (identity) y = x) -> x = eval (identity) y && x = y &&
|
|
is_symbol_free_var_in_tableau x v0.model_tableau_field)
|
|
&& is_symbol_free_var_in_tableau x v0.model_tableau_field && (x)
|
|
< (v0.nlfree_var_symbol_set_abstraction_tableau_field) && (x) <
|
|
(res.nlfree_var_symbol_set_abstraction_tableau_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_fo_term_free_var_in_tableau x
|
|
(rename_tableau v0.model_tableau_field identity identity)
|
|
->
|
|
(forall y:int.
|
|
(is_fo_term_free_var_in_tableau y v0.model_tableau_field /\
|
|
eval (identity) y = x) -> x = eval (identity) y && x = y &&
|
|
is_fo_term_free_var_in_tableau x v0.model_tableau_field)
|
|
&& is_fo_term_free_var_in_tableau x v0.model_tableau_field && (x)
|
|
< (v0.nlfree_var_fo_term_set_abstraction_tableau_field) && (x) <
|
|
(res.nlfree_var_fo_term_set_abstraction_tableau_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_symbol_free_var_in_fo_formula x
|
|
(rename_fo_formula v1.model_fo_formula_field identity identity)
|
|
->
|
|
(forall y:int.
|
|
(is_symbol_free_var_in_fo_formula y v1.model_fo_formula_field
|
|
/\ eval (identity) y = x) -> x = eval (identity) y &&
|
|
x = y &&
|
|
is_symbol_free_var_in_fo_formula x v1.model_fo_formula_field)
|
|
&& is_symbol_free_var_in_fo_formula x v1.model_fo_formula_field
|
|
&& (x) < (v1.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
&& (x) < (res.nlfree_var_symbol_set_abstraction_tableau_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_fo_term_free_var_in_fo_formula x
|
|
(rename_fo_formula v1.model_fo_formula_field identity identity)
|
|
->
|
|
(forall y:int.
|
|
(is_fo_term_free_var_in_fo_formula y v1.model_fo_formula_field
|
|
/\ eval (identity) y = x) -> x = eval (identity) y &&
|
|
x = y &&
|
|
is_fo_term_free_var_in_fo_formula x v1.model_fo_formula_field)
|
|
&& is_fo_term_free_var_in_fo_formula x v1.model_fo_formula_field
|
|
&& (x) < (v1.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
&& (x) < (res.nlfree_var_fo_term_set_abstraction_tableau_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_symbol_free_var_in_fo_formula_list x
|
|
(rename_fo_formula_list v2.model_fo_formula_list_field identity
|
|
identity)
|
|
->
|
|
(forall y:int.
|
|
(is_symbol_free_var_in_fo_formula_list y
|
|
v2.model_fo_formula_list_field
|
|
/\ eval (identity) y = x) -> x = eval (identity) y &&
|
|
x = y &&
|
|
is_symbol_free_var_in_fo_formula_list x
|
|
v2.model_fo_formula_list_field)
|
|
&&
|
|
is_symbol_free_var_in_fo_formula_list x
|
|
v2.model_fo_formula_list_field
|
|
&& (x) <
|
|
(v2.nlfree_var_symbol_set_abstraction_fo_formula_list_field) &&
|
|
(x) < (res.nlfree_var_symbol_set_abstraction_tableau_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_fo_term_free_var_in_fo_formula_list x
|
|
(rename_fo_formula_list v2.model_fo_formula_list_field identity
|
|
identity)
|
|
->
|
|
(forall y:int.
|
|
(is_fo_term_free_var_in_fo_formula_list y
|
|
v2.model_fo_formula_list_field
|
|
/\ eval (identity) y = x) -> x = eval (identity) y &&
|
|
x = y &&
|
|
is_fo_term_free_var_in_fo_formula_list x
|
|
v2.model_fo_formula_list_field)
|
|
&&
|
|
is_fo_term_free_var_in_fo_formula_list x
|
|
v2.model_fo_formula_list_field
|
|
&& (x) <
|
|
(v2.nlfree_var_fo_term_set_abstraction_fo_formula_list_field) &&
|
|
(x) < (res.nlfree_var_fo_term_set_abstraction_tableau_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_symbol_free_var_in_tableau x res.model_tableau_field ->
|
|
(is_symbol_free_var_in_tableau x
|
|
(rename_tableau v0.model_tableau_field identity identity) \/
|
|
is_symbol_free_var_in_fo_formula x
|
|
(rename_fo_formula v1.model_fo_formula_field identity
|
|
identity)
|
|
\/
|
|
is_symbol_free_var_in_fo_formula_list x
|
|
(rename_fo_formula_list v2.model_fo_formula_list_field
|
|
identity identity))
|
|
&& (x) < (res.nlfree_var_symbol_set_abstraction_tableau_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_fo_term_free_var_in_tableau x res.model_tableau_field ->
|
|
(is_fo_term_free_var_in_tableau x
|
|
(rename_tableau v0.model_tableau_field identity identity) \/
|
|
is_fo_term_free_var_in_fo_formula x
|
|
(rename_fo_formula v1.model_fo_formula_field identity
|
|
identity)
|
|
\/
|
|
is_fo_term_free_var_in_fo_formula_list x
|
|
(rename_fo_formula_list v2.model_fo_formula_list_field
|
|
identity identity))
|
|
&& (x) < (res.nlfree_var_fo_term_set_abstraction_tableau_field)
|
|
} ;
|
|
assert {
|
|
extensionalEqual (rename_subst_symbol subst_id_symbol identity)
|
|
((rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
|
|
identity))
|
|
} ;
|
|
assert { rename_subst_symbol subst_id_symbol identity =
|
|
(rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
|
|
identity)
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
((rename_subst_fo_term
|
|
(subst_id_fo_term:(int)->(fo_term (int) (int))) identity
|
|
identity))
|
|
} ;
|
|
assert { rename_subst_fo_term subst_id_fo_term identity identity =
|
|
(rename_subst_fo_term
|
|
(subst_id_fo_term:(int)->(fo_term (int) (int))) identity
|
|
identity)
|
|
} ;
|
|
model_equal_tableau v0.nlrepr_tableau_field
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
((rename_subst_symbol (const (Var_symbol (-1))) identity))
|
|
(rename_subst_symbol (const (Var_symbol (-1))) identity)
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
((rename_subst_fo_term (const (Var_fo_term (-1))) identity
|
|
identity))
|
|
(rename_subst_fo_term (const (Var_fo_term (-1))) identity identity) ;
|
|
(*assert {
|
|
extensionalEqual (rcompose (identity) (identity))
|
|
((identity : (int) -> (int)))
|
|
} ;
|
|
assert { rcompose (identity) (identity) = (identity : (int) -> (int))
|
|
} ;*)
|
|
(*assert {
|
|
extensionalEqual (rcompose (identity) (identity))
|
|
((identity : (int) -> (int)))
|
|
} ;
|
|
assert { rcompose (identity) (identity) = (identity : (int) -> (int))
|
|
} ;*)
|
|
assert {
|
|
extensionalEqual (rename_subst_symbol subst_id_symbol identity)
|
|
((rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
|
|
identity))
|
|
} ;
|
|
assert { rename_subst_symbol subst_id_symbol identity =
|
|
(rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
|
|
identity)
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
((rename_subst_fo_term
|
|
(subst_id_fo_term:(int)->(fo_term (int) (int))) identity
|
|
identity))
|
|
} ;
|
|
assert { rename_subst_fo_term subst_id_fo_term identity identity =
|
|
(rename_subst_fo_term
|
|
(subst_id_fo_term:(int)->(fo_term (int) (int))) identity
|
|
identity)
|
|
} ;
|
|
model_equal_fo_formula v1.nlrepr_fo_formula_field
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
((rename_subst_symbol (const (Var_symbol (-1))) identity))
|
|
(rename_subst_symbol (const (Var_symbol (-1))) identity)
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
((rename_subst_fo_term (const (Var_fo_term (-1))) identity
|
|
identity))
|
|
(rename_subst_fo_term (const (Var_fo_term (-1))) identity identity) ;
|
|
(*assert {
|
|
extensionalEqual (rcompose (identity) (identity))
|
|
((identity : (int) -> (int)))
|
|
} ;
|
|
assert { rcompose (identity) (identity) = (identity : (int) -> (int))
|
|
} ;*)
|
|
(*assert {
|
|
extensionalEqual (rcompose (identity) (identity))
|
|
((identity : (int) -> (int)))
|
|
} ;
|
|
assert { rcompose (identity) (identity) = (identity : (int) -> (int))
|
|
} ;*)
|
|
assert {
|
|
extensionalEqual (rename_subst_symbol subst_id_symbol identity)
|
|
((rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
|
|
identity))
|
|
} ;
|
|
assert { rename_subst_symbol subst_id_symbol identity =
|
|
(rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
|
|
identity)
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
((rename_subst_fo_term
|
|
(subst_id_fo_term:(int)->(fo_term (int) (int))) identity
|
|
identity))
|
|
} ;
|
|
assert { rename_subst_fo_term subst_id_fo_term identity identity =
|
|
(rename_subst_fo_term
|
|
(subst_id_fo_term:(int)->(fo_term (int) (int))) identity
|
|
identity)
|
|
} ;
|
|
model_equal_fo_formula_list v2.nlrepr_fo_formula_list_field
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
((rename_subst_symbol (const (Var_symbol (-1))) identity))
|
|
(rename_subst_symbol (const (Var_symbol (-1))) identity)
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
((rename_subst_fo_term (const (Var_fo_term (-1))) identity
|
|
identity))
|
|
(rename_subst_fo_term (const (Var_fo_term (-1))) identity identity) ;
|
|
(*assert {
|
|
extensionalEqual (rcompose (identity) (identity))
|
|
((identity : (int) -> (int)))
|
|
} ;
|
|
assert { rcompose (identity) (identity) = (identity : (int) -> (int))
|
|
} ;*)
|
|
(*assert {
|
|
extensionalEqual (rcompose (identity) (identity))
|
|
((identity : (int) -> (int)))
|
|
} ;
|
|
assert { rcompose (identity) (identity) = (identity : (int) -> (int))
|
|
} ;*)
|
|
res
|
|
end
|
|
|
|
let destruct_tableau (t:nlimpl_tableau) : cons_tableau
|
|
requires { nlimpl_tableau_ok t } ensures { cons_ok_tableau result }
|
|
ensures { cons_rel_tableau result t }
|
|
ensures { cons_open_rel_tableau result t } =
|
|
let fv0 = t.nlfree_var_symbol_set_abstraction_tableau_field in
|
|
let fv1 = t.nlfree_var_fo_term_set_abstraction_tableau_field in
|
|
match t.nlrepr_tableau_field with
|
|
| NL_Root ->
|
|
assert { t.model_tableau_field = Root } ;
|
|
let () =
|
|
match t.model_tableau_field with | Root -> ()
|
|
| Node x0 x1 x2 -> absurd
|
|
end
|
|
in let res = NLC_Root in res
|
|
| NL_Node v0 v1 v2 ->
|
|
assert { t.model_tableau_field =
|
|
Node
|
|
(nlmodel_tableau v0
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
(rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity)
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
(rename_subst_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int))
|
|
identity identity))
|
|
(nlmodel_fo_formula v1
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
(rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity)
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
(rename_subst_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int))
|
|
identity identity))
|
|
(nlmodel_fo_formula_list v2
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
(rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity)
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
(rename_subst_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int))
|
|
identity identity))
|
|
} ;
|
|
let (mv0 , mv1 , mv2) =
|
|
match t.model_tableau_field with | Root -> absurd
|
|
| Node x0 x1 x2 -> (x0 , x1 , x2)
|
|
end
|
|
in
|
|
assert { mv0 =
|
|
nlmodel_tableau v0
|
|
((rename_subst_symbol subst_id_symbol identity))
|
|
((rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity))
|
|
((rename_subst_fo_term subst_id_fo_term identity identity))
|
|
((rename_subst_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int))
|
|
identity identity))
|
|
} ;
|
|
assert { mv1 =
|
|
nlmodel_fo_formula v1
|
|
((rename_subst_symbol subst_id_symbol identity))
|
|
((rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity))
|
|
((rename_subst_fo_term subst_id_fo_term identity identity))
|
|
((rename_subst_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int))
|
|
identity identity))
|
|
} ;
|
|
assert { mv2 =
|
|
nlmodel_fo_formula_list v2
|
|
((rename_subst_symbol subst_id_symbol identity))
|
|
((rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity))
|
|
((rename_subst_fo_term subst_id_fo_term identity identity))
|
|
((rename_subst_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int))
|
|
identity identity))
|
|
} ;
|
|
assert { bound_depth_of_symbol_in_tableau v0 <= 0 } ;
|
|
assert {
|
|
forall x:int. is_symbol_free_var_in_tableau x mv0 ->
|
|
is_symbol_free_var_in_tableau x t.model_tableau_field && (x) <
|
|
(t.nlfree_var_symbol_set_abstraction_tableau_field)
|
|
} ;
|
|
assert { bound_depth_of_fo_term_in_tableau v0 <= 0 } ;
|
|
assert {
|
|
forall x:int. is_fo_term_free_var_in_tableau x mv0 ->
|
|
is_fo_term_free_var_in_tableau x t.model_tableau_field && (x) <
|
|
(t.nlfree_var_fo_term_set_abstraction_tableau_field)
|
|
} ;
|
|
assert { bound_depth_of_symbol_in_fo_formula v1 <= 0 } ;
|
|
assert {
|
|
forall x:int. is_symbol_free_var_in_fo_formula x mv1 ->
|
|
is_symbol_free_var_in_tableau x t.model_tableau_field && (x) <
|
|
(t.nlfree_var_symbol_set_abstraction_tableau_field)
|
|
} ;
|
|
assert { bound_depth_of_fo_term_in_fo_formula v1 <= 0 } ;
|
|
assert {
|
|
forall x:int. is_fo_term_free_var_in_fo_formula x mv1 ->
|
|
is_fo_term_free_var_in_tableau x t.model_tableau_field && (x) <
|
|
(t.nlfree_var_fo_term_set_abstraction_tableau_field)
|
|
} ;
|
|
assert { bound_depth_of_symbol_in_fo_formula_list v2 <= 0 } ;
|
|
assert {
|
|
forall x:int. is_symbol_free_var_in_fo_formula_list x mv2 ->
|
|
is_symbol_free_var_in_tableau x t.model_tableau_field && (x) <
|
|
(t.nlfree_var_symbol_set_abstraction_tableau_field)
|
|
} ;
|
|
assert { bound_depth_of_fo_term_in_fo_formula_list v2 <= 0 } ;
|
|
assert {
|
|
forall x:int. is_fo_term_free_var_in_fo_formula_list x mv2 ->
|
|
is_fo_term_free_var_in_tableau x t.model_tableau_field && (x) <
|
|
(t.nlfree_var_fo_term_set_abstraction_tableau_field)
|
|
} ;
|
|
model_equal_tableau v0 subst_id_symbol
|
|
(rename_subst_symbol
|
|
((rename_subst_symbol subst_id_symbol identity)) (identity)) ((
|
|
const (Var_symbol (-1)) : int -> (symbol int)))
|
|
(rename_subst_symbol
|
|
((rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity))
|
|
(identity))
|
|
subst_id_fo_term
|
|
(rename_subst_fo_term
|
|
((rename_subst_fo_term subst_id_fo_term identity identity))
|
|
(identity) (identity)) ((const (Var_fo_term (-1)) :
|
|
int -> (fo_term int int)))
|
|
(rename_subst_fo_term
|
|
((rename_subst_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int))
|
|
identity identity))
|
|
(identity) (identity)) ;
|
|
model_equal_fo_formula v1 subst_id_symbol
|
|
(rename_subst_symbol
|
|
((rename_subst_symbol subst_id_symbol identity)) (identity)) ((
|
|
const (Var_symbol (-1)) : int -> (symbol int)))
|
|
(rename_subst_symbol
|
|
((rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity))
|
|
(identity))
|
|
subst_id_fo_term
|
|
(rename_subst_fo_term
|
|
((rename_subst_fo_term subst_id_fo_term identity identity))
|
|
(identity) (identity)) ((const (Var_fo_term (-1)) :
|
|
int -> (fo_term int int)))
|
|
(rename_subst_fo_term
|
|
((rename_subst_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int))
|
|
identity identity))
|
|
(identity) (identity)) ;
|
|
model_equal_fo_formula_list v2 subst_id_symbol
|
|
(rename_subst_symbol
|
|
((rename_subst_symbol subst_id_symbol identity)) (identity)) ((
|
|
const (Var_symbol (-1)) : int -> (symbol int)))
|
|
(rename_subst_symbol
|
|
((rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity))
|
|
(identity))
|
|
subst_id_fo_term
|
|
(rename_subst_fo_term
|
|
((rename_subst_fo_term subst_id_fo_term identity identity))
|
|
(identity) (identity)) ((const (Var_fo_term (-1)) :
|
|
int -> (fo_term int int)))
|
|
(rename_subst_fo_term
|
|
((rename_subst_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int))
|
|
identity identity))
|
|
(identity) (identity)) ;
|
|
let ghost mrv0 = rename_tableau mv0 identity identity in
|
|
let ghost mrv1 = rename_fo_formula mv1 identity identity in
|
|
let ghost mrv2 = rename_fo_formula_list mv2 identity identity in
|
|
let resv0 =
|
|
{ nlrepr_tableau_field = v0 ;
|
|
nlfree_var_symbol_set_abstraction_tableau_field = fv0 ;
|
|
nlfree_var_fo_term_set_abstraction_tableau_field = fv1 ;
|
|
model_tableau_field = ghost mrv0 ;
|
|
}
|
|
in
|
|
let resv1 =
|
|
{ nlrepr_fo_formula_field = v1 ;
|
|
nlfree_var_symbol_set_abstraction_fo_formula_field = fv0 ;
|
|
nlfree_var_fo_term_set_abstraction_fo_formula_field = fv1 ;
|
|
model_fo_formula_field = ghost mrv1 ;
|
|
}
|
|
in
|
|
let resv2 =
|
|
{ nlrepr_fo_formula_list_field = v2 ;
|
|
nlfree_var_symbol_set_abstraction_fo_formula_list_field = fv0 ;
|
|
nlfree_var_fo_term_set_abstraction_fo_formula_list_field =
|
|
fv1 ;
|
|
model_fo_formula_list_field = ghost mrv2 ;
|
|
}
|
|
in let res = NLC_Node resv0 resv1 resv2 in
|
|
free_var_equivalence_of_rename_tableau mv0 (identity)
|
|
(rcompose (identity) (identity)) (identity)
|
|
(rcompose (identity) (identity)) ;
|
|
free_var_equivalence_of_rename_fo_formula mv1 (identity)
|
|
(rcompose (identity) (identity)) (identity)
|
|
(rcompose (identity) (identity)) ;
|
|
free_var_equivalence_of_rename_fo_formula_list mv2 (identity)
|
|
(rcompose (identity) (identity)) (identity)
|
|
(rcompose (identity) (identity)) ;
|
|
assert {
|
|
forall x:int. is_symbol_free_var_in_tableau x mrv0 ->
|
|
(forall y:int.
|
|
(is_symbol_free_var_in_tableau y mv0 /\ eval (identity) y =
|
|
x)
|
|
-> x = y &&
|
|
is_symbol_free_var_in_tableau x t.model_tableau_field && (x)
|
|
< (fv0))
|
|
&& (x) < (fv0)
|
|
} ;
|
|
assert {
|
|
forall x:int. is_fo_term_free_var_in_tableau x mrv0 ->
|
|
(forall y:int.
|
|
(is_fo_term_free_var_in_tableau y mv0 /\ eval (identity) y =
|
|
x)
|
|
-> x = y &&
|
|
is_fo_term_free_var_in_tableau x t.model_tableau_field &&
|
|
(x) < (fv1))
|
|
&& (x) < (fv1)
|
|
} ;
|
|
assert {
|
|
forall x:int. is_symbol_free_var_in_fo_formula x mrv1 ->
|
|
(forall y:int.
|
|
(is_symbol_free_var_in_fo_formula y mv1 /\ eval (identity) y
|
|
= x)
|
|
-> x = y &&
|
|
is_symbol_free_var_in_tableau x t.model_tableau_field && (x)
|
|
< (fv0))
|
|
&& (x) < (fv0)
|
|
} ;
|
|
assert {
|
|
forall x:int. is_fo_term_free_var_in_fo_formula x mrv1 ->
|
|
(forall y:int.
|
|
(is_fo_term_free_var_in_fo_formula y mv1 /\
|
|
eval (identity) y = x)
|
|
-> x = y &&
|
|
is_fo_term_free_var_in_tableau x t.model_tableau_field &&
|
|
(x) < (fv1))
|
|
&& (x) < (fv1)
|
|
} ;
|
|
assert {
|
|
forall x:int. is_symbol_free_var_in_fo_formula_list x mrv2 ->
|
|
(forall y:int.
|
|
(is_symbol_free_var_in_fo_formula_list y mv2 /\
|
|
eval (identity) y = x)
|
|
-> x = y &&
|
|
is_symbol_free_var_in_tableau x t.model_tableau_field && (x)
|
|
< (fv0))
|
|
&& (x) < (fv0)
|
|
} ;
|
|
assert {
|
|
forall x:int. is_fo_term_free_var_in_fo_formula_list x mrv2 ->
|
|
(forall y:int.
|
|
(is_fo_term_free_var_in_fo_formula_list y mv2 /\
|
|
eval (identity) y = x)
|
|
-> x = y &&
|
|
is_fo_term_free_var_in_tableau x t.model_tableau_field &&
|
|
(x) < (fv1))
|
|
&& (x) < (fv1)
|
|
} ;
|
|
res
|
|
end
|
|
|
|
let nlsubst_symbol_in_tableau (t:nlimpl_tableau) (x:int)
|
|
(u:nlimpl_symbol) : nlimpl_tableau requires { nlimpl_tableau_ok t }
|
|
requires { nlimpl_symbol_ok u } ensures { nlimpl_tableau_ok result }
|
|
ensures { result.model_tableau_field =
|
|
subst_tableau t.model_tableau_field
|
|
(update (subst_id_symbol: (int) -> (symbol (int))) x
|
|
u.model_symbol_field)
|
|
(subst_id_fo_term: (int) -> (fo_term (int) (int)))
|
|
}
|
|
=
|
|
model_equal_tableau t.nlrepr_tableau_field
|
|
(subst_compose_symbol subst_id_symbol
|
|
((update (subst_id_symbol: (int) -> (symbol (int))) x
|
|
u.model_symbol_field)))
|
|
((update (subst_id_symbol: (int) -> (symbol (int))) x
|
|
u.model_symbol_field))
|
|
(subst_compose_symbol (const (Var_symbol (-1)))
|
|
((update (subst_id_symbol: (int) -> (symbol (int))) x
|
|
u.model_symbol_field)))
|
|
((const (Var_symbol (-1))))
|
|
(subst_compose_fo_term subst_id_fo_term
|
|
((update (subst_id_symbol: (int) -> (symbol (int))) x
|
|
u.model_symbol_field))
|
|
((subst_id_fo_term: (int) -> (fo_term (int) (int)))))
|
|
((subst_id_fo_term: (int) -> (fo_term (int) (int))))
|
|
(subst_compose_fo_term (const (Var_fo_term (-1)))
|
|
((update (subst_id_symbol: (int) -> (symbol (int))) x
|
|
u.model_symbol_field))
|
|
((subst_id_fo_term: (int) -> (fo_term (int) (int)))))
|
|
((const (Var_fo_term (-1))));
|
|
let res =
|
|
{
|
|
nlrepr_tableau_field =
|
|
subst_base_symbol_in_tableau t.nlrepr_tableau_field x
|
|
u.nlrepr_symbol_field (subst_id_symbol)
|
|
((const (Var_symbol (-1)))) (subst_id_fo_term)
|
|
((const (Var_fo_term (-1)))) ((const (Var_symbol (-1)))) ;
|
|
nlfree_var_symbol_set_abstraction_tableau_field =
|
|
(let aux (a:int) (b:int) : int
|
|
ensures { result >= a /\ result >= b } = if a < b then b else a
|
|
in
|
|
aux (t.nlfree_var_symbol_set_abstraction_tableau_field)
|
|
(u.nlfree_var_symbol_set_abstraction_symbol_field)) ;
|
|
nlfree_var_fo_term_set_abstraction_tableau_field =
|
|
t.nlfree_var_fo_term_set_abstraction_tableau_field ;
|
|
model_tableau_field = ghost
|
|
subst_tableau t.model_tableau_field
|
|
(update (subst_id_symbol: (int) -> (symbol (int))) x
|
|
u.model_symbol_field)
|
|
(subst_id_fo_term: (int) -> (fo_term (int) (int))) ;
|
|
}
|
|
in
|
|
assert {
|
|
forall x2:int. is_symbol_free_var_in_tableau x2 res.model_tableau_field
|
|
->
|
|
(true /\
|
|
(forall y:int.
|
|
(is_symbol_free_var_in_tableau y t.model_tableau_field /\
|
|
is_symbol_free_var_in_symbol x2
|
|
(eval
|
|
((update (subst_id_symbol: (int) -> (symbol (int))) x
|
|
u.model_symbol_field))
|
|
y))
|
|
->
|
|
((x = y -> (x2) <
|
|
(res.nlfree_var_symbol_set_abstraction_tableau_field))
|
|
/\
|
|
(x <> y -> x2 = y && (x2) <
|
|
(res.nlfree_var_symbol_set_abstraction_tableau_field)))
|
|
&& (x2) <
|
|
(res.nlfree_var_symbol_set_abstraction_tableau_field))
|
|
/\
|
|
(forall y:int.
|
|
(is_fo_term_free_var_in_tableau y t.model_tableau_field /\
|
|
is_symbol_free_var_in_fo_term x2
|
|
(eval ((subst_id_fo_term: (int) -> (fo_term (int) (int))))
|
|
y))
|
|
-> false))
|
|
&& (x2) < (res.nlfree_var_symbol_set_abstraction_tableau_field)
|
|
} ;
|
|
assert {
|
|
forall x2:int.
|
|
is_fo_term_free_var_in_tableau x2 res.model_tableau_field ->
|
|
(true /\
|
|
(forall y:int.
|
|
(is_fo_term_free_var_in_tableau y t.model_tableau_field /\
|
|
is_fo_term_free_var_in_fo_term x2
|
|
(eval ((subst_id_fo_term: (int) -> (fo_term (int) (int))))
|
|
y))
|
|
-> x2 = y && (x2) <
|
|
(res.nlfree_var_fo_term_set_abstraction_tableau_field)))
|
|
&& (x2) < (res.nlfree_var_fo_term_set_abstraction_tableau_field)
|
|
} ;
|
|
res
|
|
|
|
let nlsubst_fo_term_in_tableau (t:nlimpl_tableau) (x:int)
|
|
(u:nlimpl_fo_term) : nlimpl_tableau requires { nlimpl_tableau_ok t }
|
|
requires { nlimpl_fo_term_ok u } ensures { nlimpl_tableau_ok result }
|
|
ensures { result.model_tableau_field =
|
|
subst_tableau t.model_tableau_field
|
|
(subst_id_symbol: (int) -> (symbol (int)))
|
|
(update (subst_id_fo_term: (int) -> (fo_term (int) (int))) x
|
|
u.model_fo_term_field)
|
|
}
|
|
=
|
|
model_equal_tableau t.nlrepr_tableau_field
|
|
(subst_compose_symbol subst_id_symbol
|
|
((subst_id_symbol: (int) -> (symbol (int)))))
|
|
((subst_id_symbol: (int) -> (symbol (int))))
|
|
(subst_compose_symbol (const (Var_symbol (-1)))
|
|
((subst_id_symbol: (int) -> (symbol (int)))))
|
|
((const (Var_symbol (-1))))
|
|
(subst_compose_fo_term subst_id_fo_term
|
|
((subst_id_symbol: (int) -> (symbol (int))))
|
|
((update (subst_id_fo_term: (int) -> (fo_term (int) (int))) x
|
|
u.model_fo_term_field)))
|
|
((update (subst_id_fo_term: (int) -> (fo_term (int) (int))) x
|
|
u.model_fo_term_field))
|
|
(subst_compose_fo_term (const (Var_fo_term (-1)))
|
|
((subst_id_symbol: (int) -> (symbol (int))))
|
|
((update (subst_id_fo_term: (int) -> (fo_term (int) (int))) x
|
|
u.model_fo_term_field)))
|
|
((const (Var_fo_term (-1))));
|
|
let res =
|
|
{
|
|
nlrepr_tableau_field =
|
|
subst_base_fo_term_in_tableau t.nlrepr_tableau_field x
|
|
u.nlrepr_fo_term_field (subst_id_symbol)
|
|
((const (Var_symbol (-1)))) (subst_id_fo_term)
|
|
((const (Var_fo_term (-1)))) ((const (Var_symbol (-1))))
|
|
((const (Var_fo_term (-1)))) ;
|
|
nlfree_var_symbol_set_abstraction_tableau_field =
|
|
(let aux (a:int) (b:int) : int
|
|
ensures { result >= a /\ result >= b } = if a < b then b else a
|
|
in
|
|
aux (t.nlfree_var_symbol_set_abstraction_tableau_field)
|
|
(u.nlfree_var_symbol_set_abstraction_fo_term_field)) ;
|
|
nlfree_var_fo_term_set_abstraction_tableau_field =
|
|
(let aux (a:int) (b:int) : int
|
|
ensures { result >= a /\ result >= b } = if a < b then b else a
|
|
in
|
|
aux (t.nlfree_var_fo_term_set_abstraction_tableau_field)
|
|
(u.nlfree_var_fo_term_set_abstraction_fo_term_field)) ;
|
|
model_tableau_field = ghost
|
|
subst_tableau t.model_tableau_field
|
|
(subst_id_symbol: (int) -> (symbol (int)))
|
|
(update (subst_id_fo_term: (int) -> (fo_term (int) (int))) x
|
|
u.model_fo_term_field) ;
|
|
}
|
|
in
|
|
assert {
|
|
forall x2:int. is_symbol_free_var_in_tableau x2 res.model_tableau_field
|
|
->
|
|
(true /\
|
|
(forall y:int.
|
|
(is_symbol_free_var_in_tableau y t.model_tableau_field /\
|
|
is_symbol_free_var_in_symbol x2
|
|
(eval ((subst_id_symbol: (int) -> (symbol (int)))) y))
|
|
-> x2 = y && (x2) <
|
|
(res.nlfree_var_symbol_set_abstraction_tableau_field))
|
|
/\
|
|
(forall y:int.
|
|
(is_fo_term_free_var_in_tableau y t.model_tableau_field /\
|
|
is_symbol_free_var_in_fo_term x2
|
|
(eval
|
|
((update
|
|
(subst_id_fo_term: (int) -> (fo_term (int) (int)))
|
|
x u.model_fo_term_field))
|
|
y))
|
|
->
|
|
((x = y -> (x2) <
|
|
(res.nlfree_var_symbol_set_abstraction_tableau_field))
|
|
/\ (x <> y -> false)) && (x2) <
|
|
(res.nlfree_var_symbol_set_abstraction_tableau_field)))
|
|
&& (x2) < (res.nlfree_var_symbol_set_abstraction_tableau_field)
|
|
} ;
|
|
assert {
|
|
forall x2:int.
|
|
is_fo_term_free_var_in_tableau x2 res.model_tableau_field ->
|
|
(true /\
|
|
(forall y:int.
|
|
(is_fo_term_free_var_in_tableau y t.model_tableau_field /\
|
|
is_fo_term_free_var_in_fo_term x2
|
|
(eval
|
|
((update
|
|
(subst_id_fo_term: (int) -> (fo_term (int) (int)))
|
|
x u.model_fo_term_field))
|
|
y))
|
|
->
|
|
((x = y -> (x2) <
|
|
(res.nlfree_var_fo_term_set_abstraction_tableau_field))
|
|
/\
|
|
(x <> y -> x2 = y && (x2) <
|
|
(res.nlfree_var_fo_term_set_abstraction_tableau_field)))
|
|
&& (x2) <
|
|
(res.nlfree_var_fo_term_set_abstraction_tableau_field)))
|
|
&& (x2) < (res.nlfree_var_fo_term_set_abstraction_tableau_field)
|
|
} ;
|
|
res
|
|
|
|
|
|
end
|