Commit 4184d53b authored by MARCHE Claude's avatar MARCHE Claude

Prover example: some other proofs were missing....

parent 7003b9c2
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="3">
<file
name="../Choice.mlw"
verified="true"
expanded="true">
<theory
name="Choice"
locfile="../Choice.mlw"
loclnum="2" loccnumb="7" loccnume="13"
verified="true"
expanded="true">
</theory>
</file>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../Choice.mlw" expanded="true">
<theory name="Choice" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
</file>
</why3session>
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
module Sem
use import Choice.Choice
use import Functions.Func
use export HighOrd
......@@ -13,26 +13,26 @@ module Sem
use import list.List
use import option.Option
use import OptionFuncs.Funcs
type model 'ls 'st = {
interp_fun : func 'ls (func (list 'st) 'st) ;
interp_pred : func 'ls (pred (list 'st)) ;
type model 'fsymb 'st = {
interp_fun : func 'fsymb (func (list 'st) 'st) ;
interp_pred : func 'fsymb (pred (list 'st)) ;
}
function term_semantic (t:fo_term 'ls 'b) (m:model 'ls 'st)
function term_semantic (t:fo_term 'fsymb 'b) (m:model 'fsymb 'st)
(rho:func 'b 'st) : 'st = match t with
| Var_fo_term x -> rho x
| App (Var_symbol f) l -> let ifun = m.interp_fun in
ifun f (term_list_semantic l m rho)
end
with term_list_semantic (t:fo_term_list 'ls 'b) (m:model 'ls 'st)
with term_list_semantic (t:fo_term_list 'fsymb 'b) (m:model 'fsymb 'st)
(rho:func 'b 'st) : list 'st = match t with
| FONil -> Nil
| FOCons x q -> Cons (term_semantic x m rho) (term_list_semantic q m rho)
end
predicate formula_semantic (t:fo_formula 'ls 'b) (m:model 'ls 'st)
predicate formula_semantic (t:fo_formula 'fsymb 'b) (m:model 'fsymb 'st)
(rho:func 'b 'st) = match t with
| Forall t -> forall x:'st.
formula_semantic t m (ocase rho x)
......@@ -46,29 +46,29 @@ module Sem
| PApp (Var_symbol p) l -> let ipred = m.interp_pred in
ipred p (term_list_semantic l m rho)
end
predicate formula_list_conj_semantic (t:fo_formula_list 'ls 'b)
(m:model 'ls 'st) (rho:func 'b 'st) = match t with
predicate formula_list_conj_semantic (t:fo_formula_list 'fsymb 'b)
(m:model 'fsymb 'st) (rho:func 'b 'st) = match t with
| FOFNil -> true
| FOFCons x q -> formula_semantic x m rho /\
formula_list_conj_semantic q m rho
end
predicate formula_list_disj_semantic (t:fo_formula_list 'ls 'b)
(m:model 'ls 'st) (rho:func 'b 'st) = match t with
predicate formula_list_disj_semantic (t:fo_formula_list 'fsymb 'b)
(m:model 'fsymb 'st) (rho:func 'b 'st) = match t with
| FOFNil -> false
| FOFCons x q -> formula_semantic x m rho \/
formula_list_disj_semantic q m rho
end
predicate tableau_node (b:bool) (phib:fo_formula_list 'ls 'b)
(phi0:fo_formula 'ls 'b) (m:model 'ls 'st) (rho:func 'b 'st) =
predicate tableau_node (b:bool) (phib:fo_formula_list 'fsymb 'b)
(phi0:fo_formula 'fsymb 'b) (m:model 'fsymb 'st) (rho:func 'b 'st) =
( b = True /\ formula_semantic phi0 m rho)
\/ formula_list_disj_semantic phib m rho
(* This one work by accumulation, as it is related to a context. *)
predicate tableau_semantic_with (t:tableau 'ls 'b)
(b:bool) (m:model 'ls 'st) (rho:func 'b 'st) =
predicate tableau_semantic_with (t:tableau 'fsymb 'b)
(b:bool) (m:model 'fsymb 'st) (rho:func 'b 'st) =
match t with
| Root -> b = True
| Node tnext phi0 phib ->
......@@ -77,17 +77,17 @@ module Sem
else False in
tableau_semantic_with tnext b' m rho
end
(* Abstraction-definition axiom :
function semantic_subst (s:func 'b (fo_term 'ls 'c))
(m:model 'ls 'st) (rho:func 'c 'st) : func 'b 'st =
function semantic_subst (s:func 'b (fo_term 'fsymb 'c))
(m:model 'fsymb 'st) (rho:func 'c 'st) : func 'b 'st =
(\ x:'b. term_semantic (s x) m rho) *)
function semantic_subst (s:func 'b (fo_term 'ls 'c))
(m:model 'ls 'st) (rho:func 'c 'st) : func 'b 'st
axiom semantic_subst_def : forall s:func 'b (fo_term 'ls 'c),
m:model 'ls 'st, rho:func 'c 'st, x:'b.
function semantic_subst (s:func 'b (fo_term 'fsymb 'c))
(m:model 'fsymb 'st) (rho:func 'c 'st) : func 'b 'st
axiom semantic_subst_def : forall s:func 'b (fo_term 'fsymb 'c),
m:model 'fsymb 'st, rho:func 'c 'st, x:'b.
semantic_subst s m rho x = term_semantic (s x) m rho
(*(* Abstraction-definition axiom :
constant symbol_name : func (symbol 'b) 'b =
(\ x:symbol 'b. match x with Var_symbol x -> x end) *)
......@@ -104,26 +104,26 @@ module Sem
(rcompose symbol_name subst_id_symbol) } ;
assert { extensionalEqual (identity:func 'b 'b)
(rcompose subst_id_symbol symbol_name) }*)
function model_rename (r:func 'b 'c) (m:model 'c 'st) :
model 'b 'st = {
interp_fun = rcompose r m.interp_fun ;
interp_pred = rcompose r m.interp_pred ;
}
lemma model_rename_id : forall m:model 'b 'st.
model_rename identity m = m
(* semantic commutation with substitution.
Required for example for
universal quantification elimination deduction rule:
forall x. phi -> phi[x <- t] come from this lemma
(*and generally speaking, quantifier handling*) *)
let rec lemma term_semantic_subst_commutation (t:fo_term 'ls 'b)
(m:model 'ls2 'st) (rho : func 'c 'st)
(thetal:func 'ls 'ls2)
(theta:func 'b (fo_term 'ls2 'c)) : unit
let rec lemma term_semantic_subst_commutation (t:fo_term 'fsymb 'b)
(m:model 'fsymb2 'st) (rho : func 'c 'st)
(thetal:func 'fsymb 'fsymb2)
(theta:func 'b (fo_term 'fsymb2 'c)) : unit
ensures { term_semantic (
subst_fo_term t (rcompose thetal subst_id_symbol) theta) m rho =
term_semantic t (model_rename thetal m) (semantic_subst theta m rho) }
......@@ -141,11 +141,11 @@ module Sem
assert { eval m.interp_fun (thetal f) l2 =
eval m2.interp_fun f l2 }
end
with lemma term_list_semantic_subst_commutation (t:fo_term_list 'ls 'b)
(m:model 'ls2 'st) (rho : func 'c 'st)
(thetal:func 'ls 'ls2)
(theta:func 'b (fo_term 'ls2 'c)) : unit
with lemma term_list_semantic_subst_commutation (t:fo_term_list 'fsymb 'b)
(m:model 'fsymb2 'st) (rho : func 'c 'st)
(thetal:func 'fsymb 'fsymb2)
(theta:func 'b (fo_term 'fsymb2 'c)) : unit
ensures { term_list_semantic (
subst_fo_term_list t (rcompose thetal subst_id_symbol) theta) m rho =
term_list_semantic t (model_rename thetal m)
......@@ -157,10 +157,10 @@ module Sem
| FOCons x q -> term_semantic_subst_commutation x m rho thetal theta ;
term_list_semantic_subst_commutation q m rho thetal theta
end
let lemma term_list_semantic_rename_commutation (t:fo_term_list 'ls 'b)
(m:model 'ls2 'st) (rho:func 'c 'st)
(thetal:func 'ls 'ls2) (theta:func 'b 'c) : unit
let lemma term_list_semantic_rename_commutation (t:fo_term_list 'fsymb 'b)
(m:model 'fsymb2 'st) (rho:func 'c 'st)
(thetal:func 'fsymb 'fsymb2) (theta:func 'b 'c) : unit
ensures { term_list_semantic (
rename_fo_term_list t thetal theta) m rho =
term_list_semantic t (model_rename thetal m)
......@@ -169,19 +169,19 @@ module Sem
let p1 = rcompose theta rho in
let p2 = semantic_subst (rcompose theta subst_id_fo_term) m rho in
assert { extensionalEqual p1 p2 && p1 = p2 }
let lemma term_semantic_rename_commutation (t:fo_term 'ls 'b)
(m:model 'ls2 'st) (rho:func 'c 'st)
(thetal:func 'ls 'ls2) (theta:func 'b 'c) : unit
let lemma term_semantic_rename_commutation (t:fo_term 'fsymb 'b)
(m:model 'fsymb2 'st) (rho:func 'c 'st)
(thetal:func 'fsymb 'fsymb2) (theta:func 'b 'c) : unit
ensures { term_semantic (rename_fo_term t thetal theta) m rho =
term_semantic t (model_rename thetal m) (rcompose theta rho) }
=
assert { extensionalEqual (rcompose theta rho)
(semantic_subst (subst_of_rename_fo_term theta) m rho) }
let lemma semantic_lifting_commutation (theta:func 'b (fo_term 'ls 'c))
(rho : func 'c 'st) (m:model 'ls 'st) (x:'st) : unit
let lemma semantic_lifting_commutation (theta:func 'b (fo_term 'fsymb 'c))
(rho : func 'c 'st) (m:model 'fsymb 'st) (x:'st) : unit
ensures { semantic_subst (olifts_fo_term theta) m (ocase rho x) =
ocase (semantic_subst theta m rho) x }
=
......@@ -195,21 +195,21 @@ module Sem
| Some z -> p1 (Some z) = p2 (Some z) end
&& p1 x = p2 x } ;
assert { extensionalEqual p1 p2 }
let lemma formula_semantic_subst_commutation (t0:fo_formula 'ls 'b)
(m0:model 'ls2 'st)
(thetal0:func 'ls 'ls2)
(theta0:func 'b (fo_term 'ls2 'c))
let lemma formula_semantic_subst_commutation (t0:fo_formula 'fsymb 'b)
(m0:model 'fsymb2 'st)
(thetal0:func 'fsymb 'fsymb2)
(theta0:func 'b (fo_term 'fsymb2 'c))
(rho:func 'c 'st) : unit
ensures { formula_semantic (
subst_fo_formula t0 (rcompose thetal0 subst_id_symbol) theta0) m0 rho
<-> formula_semantic t0
(model_rename thetal0 m0) (semantic_subst theta0 m0 rho) }
=
let rec ghost aux (t:fo_formula 'ls3 'b2)
(m:model 'ls4 'st)
(thetal:func 'ls3 'ls4)
(theta:func 'b2 (fo_term 'ls4 'c2)) : unit
let rec ghost aux (t:fo_formula 'fsymb3 'b2)
(m:model 'fsymb4 'st)
(thetal:func 'fsymb3 'fsymb4)
(theta:func 'b2 (fo_term 'fsymb4 'c2)) : unit
ensures { forall rho:func 'c2 'st.
formula_semantic (
subst_fo_formula t (rcompose thetal subst_id_symbol) theta) m rho
......@@ -257,10 +257,10 @@ module Sem
formula_semantic t2 m rho) }
end in
aux t0 m0 thetal0 theta0
let lemma formula_semantic_rename_commutation
(t:fo_formula 'ls 'b) (m:model 'ls2 'st)
(thetal:func 'ls 'ls2)
(t:fo_formula 'fsymb 'b) (m:model 'fsymb2 'st)
(thetal:func 'fsymb 'fsymb2)
(theta:func 'b 'c) (rho:func 'c 'st) : unit
ensures { formula_semantic (rename_fo_formula t thetal theta) m rho
<-> formula_semantic t (model_rename thetal m) (rcompose theta rho) }
......@@ -270,10 +270,10 @@ module Sem
subst_fo_formula t (rcompose thetal subst_id_symbol) thetas } ;
let p1 = rcompose theta rho in let p2 = semantic_subst thetas m rho in
assert { extensionalEqual p1 p2 && p1 = p2 }
let lemma formula_semantic_term_subst_commutation
(t:fo_formula 'ls 'b) (m:model 'ls 'st)
(theta:func 'b (fo_term 'ls 'c)) (rho:func 'c 'st) : unit
(t:fo_formula 'fsymb 'b) (m:model 'fsymb 'st)
(theta:func 'b (fo_term 'fsymb 'c)) (rho:func 'c 'st) : unit
ensures {
formula_semantic (subst_fo_formula t subst_id_symbol theta) m rho <->
formula_semantic t m (semantic_subst theta m rho) }
......@@ -282,19 +282,19 @@ module Sem
let rho2 = semantic_subst theta m rho in
assert { formula_semantic t2 m rho <->
formula_semantic t (model_rename identity m) rho2 }
let lemma formula_semantic_term_rename_commutation
(t:fo_formula 'ls 'b) (m:model 'ls 'st)
(t:fo_formula 'fsymb 'b) (m:model 'fsymb 'st)
(theta:func 'b 'c) (rho:func 'c 'st) : unit
ensures { formula_semantic (rename_fo_formula t identity theta) m rho <->
formula_semantic t m (rcompose theta rho) }
=
()
let rec lemma formula_list_conj_semantic_subst_commutation
(t:fo_formula_list 'ls 'b) (m:model 'ls2 'st)
(thetal:func 'ls 'ls2)
(theta:func 'b (fo_term 'ls2 'c)) (rho:func 'c 'st) : unit
(t:fo_formula_list 'fsymb 'b) (m:model 'fsymb2 'st)
(thetal:func 'fsymb 'fsymb2)
(theta:func 'b (fo_term 'fsymb2 'c)) (rho:func 'c 'st) : unit
ensures { formula_list_conj_semantic (
subst_fo_formula_list t (rcompose thetal subst_id_symbol) theta) m rho
<-> formula_list_conj_semantic t
......@@ -303,11 +303,11 @@ module Sem
=
match t with | FOFNil -> () | FOFCons _ q ->
formula_list_conj_semantic_subst_commutation q m thetal theta rho end
let rec lemma formula_list_disj_semantic_subst_commutation
(t:fo_formula_list 'ls 'b) (m:model 'ls2 'st)
(thetal:func 'ls 'ls2)
(theta:func 'b (fo_term 'ls2 'c)) (rho:func 'c 'st) : unit
(t:fo_formula_list 'fsymb 'b) (m:model 'fsymb2 'st)
(thetal:func 'fsymb 'fsymb2)
(theta:func 'b (fo_term 'fsymb2 'c)) (rho:func 'c 'st) : unit
ensures { formula_list_disj_semantic (
subst_fo_formula_list t (rcompose thetal subst_id_symbol) theta) m rho
<-> formula_list_disj_semantic t
......@@ -317,30 +317,30 @@ module Sem
match t with | FOFNil -> () | FOFCons _ q ->
formula_list_disj_semantic_subst_commutation q m thetal theta rho end
let lemma formula_list_conj_semantic_term_subst_commutation
(t:fo_formula_list 'ls 'b) (m:model 'ls 'st)
(theta:func 'b (fo_term 'ls 'c)) (rho:func 'c 'st) : unit
(t:fo_formula_list 'fsymb 'b) (m:model 'fsymb 'st)
(theta:func 'b (fo_term 'fsymb 'c)) (rho:func 'c 'st) : unit
ensures { formula_list_conj_semantic
(subst_fo_formula_list t subst_id_symbol theta) m rho <->
formula_list_conj_semantic t m (semantic_subst theta m rho) }
=
formula_list_conj_semantic_subst_commutation t m identity theta rho
let lemma formula_list_disj_semantic_term_subst_commutation
(t:fo_formula_list 'ls 'b) (m:model 'ls 'st)
(theta:func 'b (fo_term 'ls 'c)) (rho:func 'c 'st) : unit
(t:fo_formula_list 'fsymb 'b) (m:model 'fsymb 'st)
(theta:func 'b (fo_term 'fsymb 'c)) (rho:func 'c 'st) : unit
ensures { formula_list_disj_semantic
(subst_fo_formula_list t subst_id_symbol theta) m rho <->
formula_list_disj_semantic t m (semantic_subst theta m rho) }
=
formula_list_disj_semantic_subst_commutation t m identity theta rho
let rec lemma tableau_semantic_subst_commutation
(t:tableau 'ls 'b) (m:model 'ls2 'st)
(t:tableau 'fsymb 'b) (m:model 'fsymb2 'st)
(b:bool)
(thetal:func 'ls 'ls2)
(theta:func 'b (fo_term 'ls2 'c)) (rho:func 'c 'st) : unit
(thetal:func 'fsymb 'fsymb2)
(theta:func 'b (fo_term 'fsymb2 'c)) (rho:func 'c 'st) : unit
ensures { tableau_semantic_with (
subst_tableau t (rcompose thetal subst_id_symbol) theta) b m rho
<-> tableau_semantic_with t b
......@@ -358,20 +358,20 @@ module Sem
else False in
tableau_semantic_subst_commutation tnext m b' thetal theta rho
end
let lemma tableau_semantic_term_subst_commutation
(t:tableau 'ls 'b) (b:bool) (m:model 'ls 'st)
(theta:func 'b (fo_term 'ls 'c)) (rho:func 'c 'st) : unit
(t:tableau 'fsymb 'b) (b:bool) (m:model 'fsymb 'st)
(theta:func 'b (fo_term 'fsymb 'c)) (rho:func 'c 'st) : unit
ensures { tableau_semantic_with (
subst_tableau t subst_id_symbol theta) b m rho <->
tableau_semantic_with t b m (semantic_subst theta m rho) }
=
tableau_semantic_subst_commutation t m b identity theta rho
let rec lemma term_semantic_depend_only_free_var
(t:fo_term 'ls 'b) (m1 m2:model 'ls 'st)
(t:fo_term 'fsymb 'b) (m1 m2:model 'fsymb 'st)
(rho1 rho2:func 'b 'st) : unit
requires { forall f:'ls. is_symbol_free_var_in_fo_term f t ->
requires { forall f:'fsymb. is_symbol_free_var_in_fo_term f t ->
eval m1.interp_fun f = eval m2.interp_fun f /\
eval m1.interp_pred f = eval m2.interp_pred f }
requires { forall x:'b. is_fo_term_free_var_in_fo_term x t ->
......@@ -382,11 +382,11 @@ module Sem
match t with Var_fo_term x -> () | App (Var_symbol f) l ->
term_list_semantic_depend_only_free_var l m1 m2 rho1 rho2 ;
assert { is_symbol_free_var_in_fo_term f t } end
with lemma term_list_semantic_depend_only_free_var
(t:fo_term_list 'ls 'b) (m1 m2:model 'ls 'st)
(t:fo_term_list 'fsymb 'b) (m1 m2:model 'fsymb 'st)
(rho1 rho2:func 'b 'st) : unit
requires { forall f:'ls. is_symbol_free_var_in_fo_term_list f t ->
requires { forall f:'fsymb. is_symbol_free_var_in_fo_term_list f t ->
eval m1.interp_fun f = eval m2.interp_fun f /\
eval m1.interp_pred f = eval m2.interp_pred f }
requires { forall x:'b. is_fo_term_free_var_in_fo_term_list x t ->
......@@ -397,19 +397,19 @@ module Sem
match t with FONil -> () | FOCons x q ->
term_semantic_depend_only_free_var x m1 m2 rho1 rho2 ;
term_list_semantic_depend_only_free_var q m1 m2 rho1 rho2 end
let lemma formula_semantic_depend_only_free_var
(t:fo_formula 'ls0 'b0) (m1 m2:model 'ls0 'st0)
(t:fo_formula 'fsymb0 'b0) (m1 m2:model 'fsymb0 'st0)
(rho1 rho2:func 'b0 'st0) : unit
requires { forall f:'ls0. is_symbol_free_var_in_fo_formula f t ->
requires { forall f:'fsymb0. is_symbol_free_var_in_fo_formula f t ->
eval m1.interp_fun f = eval m2.interp_fun f /\
eval m1.interp_pred f = eval m2.interp_pred f }
requires { forall x:'b0. is_fo_term_free_var_in_fo_formula x t ->
rho1 x = rho2 x }
ensures { formula_semantic t m1 rho1 <-> formula_semantic t m2 rho2 }
=
let rec aux (t:fo_formula 'ls 'b) (m1 m2:model 'ls 'st) : unit
requires { forall f:'ls. is_symbol_free_var_in_fo_formula f t ->
let rec aux (t:fo_formula 'fsymb 'b) (m1 m2:model 'fsymb 'st) : unit
requires { forall f:'fsymb. is_symbol_free_var_in_fo_formula f t ->
eval m1.interp_fun f = eval m2.interp_fun f /\
eval m1.interp_pred f = eval m2.interp_pred f }
ensures { forall rho1 rho2:func 'b 'st.
......@@ -456,11 +456,11 @@ module Sem
eval m2.interp_pred p (term_list_semantic l m2 rho2)) }
end in
aux t m1 m2
let rec lemma formula_list_conj_semantic_depend_only_free_var
(t:fo_formula_list 'ls 'b) (m1 m2:model 'ls 'st)
(t:fo_formula_list 'fsymb 'b) (m1 m2:model 'fsymb 'st)
(rho1 rho2:func 'b 'st) : unit
requires { forall f:'ls. is_symbol_free_var_in_fo_formula_list f t ->
requires { forall f:'fsymb. is_symbol_free_var_in_fo_formula_list f t ->
eval m1.interp_fun f = eval m2.interp_fun f /\
eval m1.interp_pred f = eval m2.interp_pred f }
requires { forall x:'b. is_fo_term_free_var_in_fo_formula_list x t ->
......@@ -472,11 +472,11 @@ module Sem
match t with FOFNil -> () | FOFCons x q ->
formula_semantic_depend_only_free_var x m1 m2 rho1 rho2 ;
formula_list_conj_semantic_depend_only_free_var q m1 m2 rho1 rho2 end
let rec lemma formula_list_disj_semantic_depend_only_free_var
(t:fo_formula_list 'ls 'b) (m1 m2:model 'ls 'st)
(t:fo_formula_list 'fsymb 'b) (m1 m2:model 'fsymb 'st)
(rho1 rho2:func 'b 'st) : unit
requires { forall f:'ls. is_symbol_free_var_in_fo_formula_list f t ->
requires { forall f:'fsymb. is_symbol_free_var_in_fo_formula_list f t ->
eval m1.interp_fun f = eval m2.interp_fun f /\
eval m1.interp_pred f = eval m2.interp_pred f }
requires { forall x:'b. is_fo_term_free_var_in_fo_formula_list x t ->
......@@ -488,79 +488,79 @@ module Sem
match t with FOFNil -> () | FOFCons x q ->
formula_semantic_depend_only_free_var x m1 m2 rho1 rho2 ;
formula_list_disj_semantic_depend_only_free_var q m1 m2 rho1 rho2 end
predicate formula_list_mem (phi:fo_formula 'ls 'b)
(l:fo_formula_list 'ls 'b) = match l with
predicate formula_list_mem (phi:fo_formula 'fsymb 'b)
(l:fo_formula_list 'fsymb 'b) = match l with
| FOFNil -> false | FOFCons x q -> x = phi \/ formula_list_mem phi q end
let rec lemma formula_list_conj_semantic_other_def
(l:fo_formula_list 'ls 'b) (m:model 'ls 'st)
(l:fo_formula_list 'fsymb 'b) (m:model 'fsymb 'st)
(rho:func 'b 'st) : unit
ensures { formula_list_conj_semantic l m rho <->
(forall phi:fo_formula 'ls 'b.
(forall phi:fo_formula 'fsymb 'b.
formula_list_mem phi l -> formula_semantic phi m rho) }
variant { size_fo_formula_list l }
= match l with FOFNil -> () | FOFCons _ q ->
formula_list_conj_semantic_other_def q m rho end
let rec lemma formula_list_disj_semantic_other_def
(l:fo_formula_list 'ls 'b) (m:model 'ls 'st)
(l:fo_formula_list 'fsymb 'b) (m:model 'fsymb 'st)
(rho:func 'b 'st) : unit
ensures { formula_list_disj_semantic l m rho <->
(exists phi:fo_formula 'ls 'b.
(exists phi:fo_formula 'fsymb 'b.
formula_list_mem phi l /\ formula_semantic phi m rho) }
variant { size_fo_formula_list l }
= match l with FOFNil -> () | FOFCons x q ->
formula_list_disj_semantic_other_def q m rho end
(* Problem : validity/unsatifiability are not even axiomatizable in why3,
since we would have to introduce it from a type quantification.
However, we can define a demonstrability predicate and show for it
the same elimination principle as unsatisfiability. *)
(* Demonstration object (not directly a predicate,
so we can actually construct the proof object ourselves). *)
(* G |- A can be read as : for every model+interpretation,
if /\G is true then A too.
Which in particular mean : if G |- false, G have no model,
so we can use G |- false instead of unsat predicate as long
as it can represent all our demonstration steps. *)
(*type demonstration 'ls 'b =
(*type demonstration 'fsymb 'b =
| Axiom
| ModusPonens (demonstration 'ls 'b) (demonstration 'ls 'b)
(fo_formula 'ls 'b)
| Abstraction (demonstration 'ls 'b) (fo_formula 'ls 'b)
(fo_formula 'ls 'b)
| ConjunctionIntro (demonstration 'ls 'b) (fo_formula 'ls 'b)
(demonstration 'ls 'b) (fo_formula 'ls 'b)
| ConjunctionLeft (demonstration 'ls 'b) (fo_formula 'ls 'b)
| ConjunctionRight (demonstration 'ls 'b) (fo_formula 'ls 'b)
| DisjunctionLeft (demonstration 'ls 'b) (fo_formula 'ls 'b)
(fo_formula 'ls 'b)
| DisjunctionRight (demonstration 'ls 'b) (fo_formula 'ls 'b)
(fo_formula 'ls 'b)
| DisjunctionElim (demonstration 'ls 'b) (demonstration 'ls 'b)
(demonstration 'ls 'b) (fo_formula 'ls 'b) (fo_formula 'ls 'b)
| UniversalInstantiation (demonstration 'ls 'b)
(fo_formula 'ls (option 'b)) (fo_term 'ls 'b)
| Instantiation (demonstration 'ls 'b)
(fo_formula_list 'ls 'b)
(fo_formula 'ls 'b) 'b (fo_term 'ls 'b)
| ExistentialIntroduction (demonstration 'ls 'b)
(fo_formula 'ls (option 'b)) (fo_term 'ls 'b)
| ExistentialElimination (demonstration 'ls 'b)
(demonstration 'ls 'b)
(fo_formula 'ls (option 'b)) (fo_formula 'ls (option 'b))
| PointlessExistential (demonstration 'ls 'b)
| ExFalso (demonstration 'ls 'b)
| ModusPonens (demonstration 'fsymb 'b) (demonstration 'fsymb 'b)
(fo_formula 'fsymb 'b)
| Abstraction (demonstration 'fsymb 'b) (fo_formula 'fsymb 'b)
(fo_formula 'fsymb 'b)
| ConjunctionIntro (demonstration 'fsymb 'b) (fo_formula 'fsymb 'b)
(demonstration 'fsymb 'b) (fo_formula 'fsymb 'b)
| ConjunctionLeft (demonstration 'fsymb 'b) (fo_formula 'fsymb 'b)
| ConjunctionRight (demonstration 'fsymb 'b) (fo_formula 'fsymb 'b)
| DisjunctionLeft (demonstration 'fsymb 'b) (fo_formula 'fsymb 'b)
(fo_formula 'fsymb 'b)
| DisjunctionRight (demonstration 'fsymb 'b) (fo_formula 'fsymb 'b)
(fo_formula 'fsymb 'b)
| DisjunctionElim (demonstration 'fsymb 'b) (demonstration 'fsymb 'b)
(demonstration 'fsymb 'b) (fo_formula 'fsymb 'b) (fo_formula 'fsymb 'b)
| UniversalInstantiation (demonstration 'fsymb 'b)
(fo_formula 'fsymb (option 'b)) (fo_term 'fsymb 'b)
| Instantiation (demonstration 'fsymb 'b)
(fo_formula_list 'fsymb 'b)
(fo_formula 'fsymb 'b) 'b (fo_term 'fsymb 'b)
| ExistentialIntroduction (demonstration 'fsymb 'b)
(fo_formula 'fsymb (option 'b)) (fo_term 'fsymb 'b)
| ExistentialElimination (demonstration 'fsymb 'b)
(demonstration 'fsymb 'b)
(fo_formula 'fsymb (option 'b)) (fo_formula 'fsymb (option 'b))
| PointlessExistential (demonstration 'fsymb 'b)
| ExFalso (demonstration 'fsymb 'b)
| Trivial
| Weakening (demonstration 'ls 'b) (fo_formula_list 'ls 'b)
| Skolemization (demonstration 'ls 'b) (fo_formula 'ls 'b) 'ls*)
(*predicate is_skolem_axiom (phi:fo_formula 'ls 'b) (f:'ls)
(env:fo_term_list 'ls 'b) =
| Weakening (demonstration 'fsymb 'b) (fo_formula_list 'fsymb 'b)
| Skolemization (demonstration 'fsymb 'b) (fo_formula 'fsymb 'b) 'fsymb*)
(*predicate is_skolem_axiom (phi:fo_formula 'fsymb 'b) (f:'fsymb)
(env:fo_term_list 'fsymb 'b) =
match phi with
| Forall phi2 -> is_skolem_axiom phi2 f
(FOCons (Var_fo_term None) (rename_fo_term_list env identity some))
......@@ -570,7 +570,7 @@ module Sem
not(is_symbol_free_var_in_fo_formula f phi2)
| _ -> false
end*)