diff --git a/examples/bts/264_destruct_if.mlw b/examples/bts/264_destruct_if.mlw index 8cb1c7d8d0deaf83316389ffcf550710d0ede2dd..a529490a9b1d8987ce4ff4833f3efdeb8d67febe 100644 --- a/examples/bts/264_destruct_if.mlw +++ b/examples/bts/264_destruct_if.mlw @@ -1,19 +1,22 @@ +use list.List +use list.Length +use int.Int constant x: int predicate p int +(**********************) +(* Simple destruction *) +(**********************) + axiom H: if x = 42 then p 1 else p 2 -goal g: p 3 - -use list.List -use list.Length -use int.Int +goal g: p 0 constant l: list int -axiom H': match l with +axiom H1: match l with | Nil -> p 4 | Cons x y -> p (x+length y) | Cons _ (Cons y Nil) -> p y @@ -21,19 +24,64 @@ axiom H': match l with | Cons _ (Cons _ (Cons _ _)) -> p 5 end -goal g': p 6 +goal g1: p 1 + +(**********************) +(* As and or patterns *) +(**********************) -axiom H'': match l with +axiom H2: match l with | Nil -> p 1 | Cons x Nil | Cons _ (Cons x Nil) -> p x -| Cons _ (Cons _ _ as l') -> p (length l') +| Cons _ (Cons _ _ as l1) -> p (length l1) end -goal g'': p 7 +goal g2: p 2 -axiom H''': match l with -| Cons _ (Cons _ _ as l') as l'' -> p (length l'+length l'') +axiom H3: match l with +| Cons _ (Cons _ _ as l1) as l2 -> p (length l1+length l2) | _ -> p 0 end -goal g''': p 8 \ No newline at end of file +goal g3: p 3 + +(*************************) +(* Recursive destruction *) +(*************************) + +axiom H4: + if p x then + (if p (x+1) then + p 1 + else + p 2) + else p 3 + +goal g4: p 4 + +axiom H5: match l with +| Cons x (Cons y _) -> + if x = y then + p 1 \/ p 2 + else + p 3 /\ p 4 +| _ -> true +end + +(*********************************************************************************) +(* Interaction between recursive destruction of conditionals and of implications *) +(*********************************************************************************) + +goal g5: p 5 + +axiom H6: p 1 -> if p 2 then p 3 else p 4 + +goal g6: p 6 + +axiom H7: if p 1 then p 2 -> p 3 else p 4 + +goal g7: p 7 + +axiom H8: if p 1 then if p 2 then (p 3 -> p 4) else p 5 else p 6 + +goal g8: p 8 \ No newline at end of file diff --git a/examples/bts/264_destruct_if/why3session.xml b/examples/bts/264_destruct_if/why3session.xml index cf490b6cee4d39b85198a6e647bcbee5f01df594..9b9c4ae7096c048794e591fe6e6d2c7ced6f3262 100644 --- a/examples/bts/264_destruct_if/why3session.xml +++ b/examples/bts/264_destruct_if/why3session.xml @@ -14,37 +14,117 @@ - - - + + + - + - + - + - + - - - + + + - + - + - + - - - + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/examples/bts/264_destruct_if/why3shapes.gz b/examples/bts/264_destruct_if/why3shapes.gz index c4843c536d50c1c4565c1373dbdad007325e836e..adb5410659db4736e60b80fe40ed33bdb8a36569 100644 Binary files a/examples/bts/264_destruct_if/why3shapes.gz and b/examples/bts/264_destruct_if/why3shapes.gz differ