264_destruct_if.mlw 1.47 KB
Newer Older
1 2 3
use list.List
use list.Length
use int.Int
4 5 6 7 8

constant x: int

predicate p int

9 10 11 12
(**********************)
(* Simple destruction *)
(**********************)

13 14
axiom H: if x = 42 then p 1 else p 2

15
goal g: p 0
16 17 18

constant l: list int

19
axiom H1: match l with
20 21 22 23 24 25 26
| Nil -> p 4
| Cons x y -> p (x+length y)
| Cons _ (Cons y Nil) -> p y
| Cons x (Cons y z) -> p (x+y+length z)
| Cons _ (Cons _ (Cons _ _)) -> p 5
end

27 28 29 30 31
goal g1: p 1

(**********************)
(* As and or patterns *)
(**********************)
32

33
axiom H2: match l with
34 35
| Nil -> p 1
| Cons x Nil | Cons _ (Cons x Nil) -> p x
36
| Cons _ (Cons _ _ as l1) -> p (length l1)
37 38
end

39
goal g2: p 2
40

41 42
axiom H3: match l with
| Cons _ (Cons _ _ as l1) as l2 -> p (length l1+length l2)
43 44 45
| _ -> p 0
end

46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87
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