Commit 6007bad4 authored by François Bobot's avatar François Bobot

examples : select -> set, logic rec -> axioms

parent e0d88b28
......@@ -9,27 +9,29 @@ theory Sorted
logic n : int = 4
logic sorted(m : array) =
forall x y:int. x<=y -> Real.(<=)(select m x) (select m y)
forall x y:int. x<=y -> Real.(<=)(get m x) (get m y)
logic count(m : array) (i j : int) (v : real) : int =
if i = j then 0 else
let c = count m (i+1) j v in
(if select m i = v then c + 1 else c)
logic count(m : array) (i j : int) (v : real) : int
axiom Count :
forall m : array. forall i j : int. forall v : real. count m i j v =
(if i = j then 0 else
let c = count m (i+1) j v in
(if get m i = v then c + 1 else c))
logic model(m1 : array) (m2 : multi) =
forall v:real. count m1 1 (n+1) v = select m2 v
forall v:real. count m1 1 (n+1) v = get m2 v
(*
logic model_aux(m1 : array, i : int) : multi
axiom Model_aux_def1 :
forall m1 : array. forall i : int. forall v : real.
1 <= i and i <= n ->
select(model_aux(m1,i),v) =
if select(m1,i)=v then select(model_aux(m1,i+1),v) + 1
else select(model_aux(m1,i+1),v)
get(model_aux(m1,i),v) =
if get(m1,i)=v then get(model_aux(m1,i+1),v) + 1
else get(model_aux(m1,i+1),v)
axiom Model_aux_def2 :
forall m1 : array. forall v : real. select(model_aux(m1,n+1),v) = 0
forall m1 : array. forall v : real. get(model_aux(m1,n+1),v) = 0
logic model(m1 : array, m2 : multi) = model_aux(m1, 1) = m2
*)
......@@ -41,32 +43,32 @@ theory Sorted
goal G :
forall m1 : array.
select m1 1 = 42. ->
select m1 2 = 13. ->
select m1 3 = 42. ->
select m1 4 = 45. ->
get m1 1 = 42. ->
get m1 2 = 13. ->
get m1 3 = 42. ->
get m1 4 = 45. ->
forall m2 : array.
forall multi : multi.
model m1 multi ->
model m2 multi ->
sorted m2 ->
select m2 1 = 13. and
select m2 2 = 42. and
select m2 3 = 42. and
select m2 4 = 45.
get m2 1 = 13. and
get m2 2 = 42. and
get m2 3 = 42. and
get m2 4 = 45.
(* goal G_false :
forall m1 : array.
select m1 1 = 42. ->
select m1 2 = 13. ->
select m1 3 = 42. ->
get m1 1 = 42. ->
get m1 2 = 13. ->
get m1 3 = 42. ->
forall m2 : array.
forall multi : multi.
model m1 multi ->
model m2 multi ->
sorted m2 ->
select m2 1 = 42. and
select m2 2 = 13. and
select m2 3 = 42.
get m2 1 = 42. and
get m2 2 = 13. and
get m2 3 = 42.
*)
end
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment