Commit 208569fe authored by Benedikt Becker's avatar Benedikt Becker

Update examples for recursive destruct of conditionals and matches

parent f8fa9b99
use list.List
use list.Length
use int.Int
constant x: int constant x: int
predicate p int predicate p int
(**********************)
(* Simple destruction *)
(**********************)
axiom H: if x = 42 then p 1 else p 2 axiom H: if x = 42 then p 1 else p 2
goal g: p 3 goal g: p 0
use list.List
use list.Length
use int.Int
constant l: list int constant l: list int
axiom H': match l with axiom H1: match l with
| Nil -> p 4 | Nil -> p 4
| Cons x y -> p (x+length y) | Cons x y -> p (x+length y)
| Cons _ (Cons y Nil) -> p y | Cons _ (Cons y Nil) -> p y
...@@ -21,19 +24,64 @@ axiom H': match l with ...@@ -21,19 +24,64 @@ axiom H': match l with
| Cons _ (Cons _ (Cons _ _)) -> p 5 | Cons _ (Cons _ (Cons _ _)) -> p 5
end 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 | Nil -> p 1
| Cons x Nil | Cons _ (Cons x Nil) -> p x | Cons x Nil | Cons _ (Cons x Nil) -> p x
| Cons _ (Cons _ _ as l') -> p (length l') | Cons _ (Cons _ _ as l1) -> p (length l1)
end end
goal g'': p 7 goal g2: p 2
axiom H''': match l with axiom H3: match l with
| Cons _ (Cons _ _ as l') as l'' -> p (length l'+length l'') | Cons _ (Cons _ _ as l1) as l2 -> p (length l1+length l2)
| _ -> p 0 | _ -> p 0
end end
goal g''': p 8 goal g3: p 3
\ No newline at end of file
(*************************)
(* 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
...@@ -14,37 +14,117 @@ ...@@ -14,37 +14,117 @@
</goal> </goal>
</transf> </transf>
</goal> </goal>
<goal name="g&#39;"> <goal name="g1">
<transf name="destruct" arg1="H&#39;"> <transf name="destruct" arg1="H1">
<goal name="g&#39;.0"> <goal name="g1.0">
</goal> </goal>
<goal name="g&#39;.1"> <goal name="g1.1">
</goal> </goal>
<goal name="g&#39;.2"> <goal name="g1.2">
</goal> </goal>
<goal name="g&#39;.3"> <goal name="g1.3">
</goal> </goal>
<goal name="g&#39;.4"> <goal name="g1.4">
</goal> </goal>
</transf> </transf>
</goal> </goal>
<goal name="g&#39;&#39;"> <goal name="g2">
<transf name="destruct" arg1="H&#39;&#39;"> <transf name="destruct" arg1="H2">
<goal name="g&#39;&#39;.0"> <goal name="g2.0">
</goal> </goal>
<goal name="g&#39;&#39;.1"> <goal name="g2.1">
</goal> </goal>
<goal name="g&#39;&#39;.2"> <goal name="g2.2">
</goal> </goal>
<goal name="g&#39;&#39;.3"> <goal name="g2.3">
</goal> </goal>
</transf> </transf>
</goal> </goal>
<goal name="g&#39;&#39;&#39;"> <goal name="g3">
<transf name="destruct" arg1="H&#39;&#39;&#39;"> <transf name="destruct" arg1="H3">
<goal name="g&#39;&#39;&#39;.0"> <goal name="g3.0">
</goal> </goal>
<goal name="g&#39;&#39;&#39;.1"> <goal name="g3.1">
</goal>
</transf>
</goal>
<goal name="g4">
<transf name="destruct" arg1="H4">
<goal name="g4.0">
</goal>
<goal name="g4.1">
</goal>
</transf>
<transf name="destruct_rec" arg1="H4">
<goal name="g4.0">
</goal>
<goal name="g4.1">
</goal>
<goal name="g4.2">
</goal>
</transf>
</goal>
<goal name="g5">
<transf name="destruct" arg1="H5">
<goal name="g5.0">
</goal>
<goal name="g5.1">
</goal>
</transf>
<transf name="destruct_rec" arg1="H5">
<goal name="g5.0">
</goal>
<goal name="g5.1">
</goal>
<goal name="g5.2">
</goal>
<goal name="g5.3">
</goal>
</transf>
</goal>
<goal name="g6">
<transf name="destruct" arg1="H6">
<goal name="g6.0" expl="destruct premise">
</goal>
<goal name="g6.1">
</goal>
</transf>
<transf name="destruct_rec" arg1="H6">
<goal name="g6.0" expl="destruct premise">
</goal>
<goal name="g6.1">
</goal>
<goal name="g6.2">
</goal>
</transf>
</goal>
<goal name="g7">
<transf name="destruct" arg1="H7">
<goal name="g7.0">
</goal>
<goal name="g7.1">
</goal>
</transf>
<transf name="destruct_rec" arg1="H7">
<goal name="g7.0">
</goal>
<goal name="g7.1">
</goal>
</transf>
</goal>
<goal name="g8">
<transf name="destruct" arg1="H8">
<goal name="g8.0">
</goal>
<goal name="g8.1">
</goal>
</transf>
<transf name="destruct_rec" arg1="H8">
<goal name="g8.0">
</goal>
<goal name="g8.1">
</goal>
<goal name="g8.2">
</goal> </goal>
</transf> </transf>
</goal> </goal>
......
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