document syntax change: meta on propositions

doc/manual.tex

@@ -315,6 +315,8 @@ egalite sur les type algebriques ? engendrees automatiquement ?
 \hline
 \texttt{"attribute"} & \texttt{[@attribute]} \\
 \hline
+\texttt{meta M prop P} & \texttt{meta M lemma P} or \texttt{meta M axiom P} or \texttt{meta M goal P} \\
+\hline
 \end{tabular}
 \end{center}
 

tests/demo-itp.mlw

@@ -12,15 +12,15 @@ module ApplyRewrite
 
   use HighOrd
 
-  axiom H: forall x. (\z: int. x + z) =  f x
+  axiom H: forall x. (fun (z: int) -> x + z) =  f x
 
-  goal g1: (\toto. 42 + toto) = f 42
+  goal g1: (fun toto -> 42 + toto) = f 42
   
-  axiom Ha: forall x. (\z: int. x + z) 2 = 2
+  axiom Ha: forall x. (fun (z: int) -> x + z) 2 = 2
   
-  goal g3: (\toto. 42 + toto) 2 = 2 
+  goal g3: (fun toto -> 42 + toto) 2 = 2 
     
-  goal g2: (\y. y + y) = f 24
+  goal g2: (fun y -> y + y) = f 24
 end
 
 module A
@@ -34,7 +34,7 @@ module A
   
   goal g1: exists x. f x = x + 42
   
-  goal g: (\y. f y) 0 = 3
+  goal g: (fun y -> f y) 0 = 3
 
   constant b: bool
 
@@ -52,9 +52,9 @@ module Soundness
   function f0 (x y z:int) : int = x * y + z
   predicate p (f:int -> int) =
     f (-1) = 0 && forall n:int. f n = f 0 + (f 1 - f 0) * n
-  lemma A : forall y z:int. p (\x. f0 x y z) <-> y = z
-  meta rewrite prop A
-  lemma Fail : 0 = 0 /\ p (\x. f0 x x x)
+  lemma A : forall y z:int. p (fun x -> f0 x y z) <-> y = z
+  meta rewrite lemma A
+  lemma Fail : 0 = 0 /\ p (fun x -> f0 x x x)
   lemma Absurd : false
 end
 
@@ -62,7 +62,7 @@ module TestCEX
 
   use import int.Int
   
-  goal g: forall x "model". x=0
+  goal g: forall x. x=0
   
 end
 

tests/demo-itp/why3session.xml

@@ -8,13 +8,13 @@
 <prover id="3" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="4" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="5" name="Eprover" version="2.0" timelimit="5" steplimit="0" memlimit="1000"/>
-<prover id="6" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="6" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <file name="../demo-itp.mlw">
-<theory name="Naming" sum="887148d0be0266efa5001ad2fedbe72e">
+<theory name="Naming">
  <goal name="G">
  </goal>
 </theory>
-<theory name="ApplyRewrite" sum="a5d903eba2570fb4645483c4ff500ebb">
+<theory name="ApplyRewrite">
  <goal name="g1" proved="true">
  <transf name="apply" proved="true" arg1="H">
  </transf>
@@ -36,7 +36,7 @@
  </transf>
  </goal>
 </theory>
-<theory name="A" sum="1abc5293356c4003ce35806f735459dc">
+<theory name="A">
  <goal name="g1" proved="true">
  <transf name="apply" proved="true" arg1="H">
  </transf>
@@ -50,72 +50,75 @@
  <goal name="gb">
  </goal>
 </theory>
-<theory name="Soundness" sum="aa1c41b51a76f536179c52b8dcf8a473">
- <goal name="A" proved="true">
- <proof prover="2" timelimit="5"><result status="valid" time="0.24"/></proof>
+<theory name="Soundness">
+ <goal name="A">
+ <proof prover="2" timelimit="5" obsolete="true"><result status="valid" time="0.24"/></proof>
  </goal>
  <goal name="Fail">
- <transf name="assert" arg1="(forall y:int, z:int. y = z -&gt; p (\ x:int. f0 x y z))">
+ <transf name="assert" arg1="(forall y:int, z:int. y = z -&gt; p (fun (x:int) -&gt; f0 x y z))">
   <goal name="Fail.0" proved="true">
-  <proof prover="2" timelimit="5"><result status="valid" time="0.21"/></proof>
+  <proof prover="2"><result status="valid" time="0.10"/></proof>
   </goal>
   <goal name="Fail.1">
   <transf name="compute_specified" >
    <goal name="Fail.1.0">
+   <proof prover="2"><result status="unknown" time="0.01"/></proof>
+   <proof prover="4"><result status="timeout" time="1.00"/></proof>
+   <proof prover="6"><result status="timeout" time="1.01"/></proof>
    </goal>
   </transf>
   </goal>
  </transf>
  </goal>
- <goal name="Absurd" proved="true">
- <proof prover="2" timelimit="5"><result status="valid" time="0.02"/></proof>
+ <goal name="Absurd">
+ <proof prover="2" timelimit="5" obsolete="true"><result status="valid" time="0.02"/></proof>
  </goal>
 </theory>
-<theory name="TestCEX" sum="55ceea8b24a88c1829a53af2c814f1a6">
+<theory name="TestCEX">
  <goal name="g">
- <proof prover="2" timelimit="5"><result status="unknown" time="0.00"/></proof>
+ <proof prover="2" timelimit="5" obsolete="true"><result status="unknown" time="0.00"/></proof>
  </goal>
 </theory>
-<theory name="TestCopyPaste" sum="22d35cc9b3a5547f481892208f0547bc">
+<theory name="TestCopyPaste">
  <goal name="g1">
  <transf name="split_goal_wp" >
   <goal name="g1.0">
-  <proof prover="6"><result status="unknown" time="0.00"/></proof>
+  <proof prover="6" timelimit="5" obsolete="true"><result status="unknown" time="0.00"/></proof>
   </goal>
   <goal name="g1.1">
-  <proof prover="2"><result status="unknown" time="0.00"/></proof>
-  <proof prover="3"><result status="unknown" time="0.00"/></proof>
-  <proof prover="4"><result status="unknown" time="0.01"/></proof>
-  <proof prover="6" timelimit="1"><result status="unknown" time="0.01"/></proof>
+  <proof prover="2" obsolete="true"><result status="unknown" time="0.00"/></proof>
+  <proof prover="3" obsolete="true"><result status="unknown" time="0.00"/></proof>
+  <proof prover="4" obsolete="true"><result status="unknown" time="0.01"/></proof>
+  <proof prover="6" obsolete="true"><result status="unknown" time="0.01"/></proof>
   </goal>
  </transf>
  </goal>
  <goal name="g2">
  <transf name="split_goal_wp" >
   <goal name="g2.0">
-  <proof prover="6"><result status="unknown" time="0.01"/></proof>
+  <proof prover="6" timelimit="5" obsolete="true"><result status="unknown" time="0.01"/></proof>
   </goal>
   <goal name="g2.1">
-  <proof prover="2"><result status="unknown" time="0.00"/></proof>
-  <proof prover="3"><result status="unknown" time="0.00"/></proof>
-  <proof prover="4"><result status="unknown" time="0.01"/></proof>
-  <proof prover="6" timelimit="1"><result status="unknown" time="0.01"/></proof>
+  <proof prover="2" obsolete="true"><result status="unknown" time="0.00"/></proof>
+  <proof prover="3" obsolete="true"><result status="unknown" time="0.00"/></proof>
+  <proof prover="4" obsolete="true"><result status="unknown" time="0.01"/></proof>
+  <proof prover="6" obsolete="true"><result status="unknown" time="0.01"/></proof>
   </goal>
   <goal name="g2.2">
-  <proof prover="5"><result status="timeout" time="4.89"/></proof>
+  <proof prover="5" obsolete="true"><result status="timeout" time="4.89"/></proof>
   </goal>
  </transf>
  </goal>
 </theory>
-<theory name="M" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
+<theory name="M" proved="true">
 </theory>
-<theory name="TestWarnings" sum="aeca3388f2e65d42f78feba3152450b6">
+<theory name="TestWarnings">
  <goal name="g1">
  </goal>
  <goal name="g2">
  </goal>
 </theory>
-<theory name="TestTaskPrinting" sum="01fbd777d08f356d2f390e335249eeb9">
+<theory name="TestTaskPrinting">
  <goal name="g1">
  </goal>
  <goal name="g2">
@@ -133,25 +136,35 @@
  <goal name="g8">
  </goal>
 </theory>
-<theory name="TestAutomaticIntro" sum="6566463f1ee0314d808add53aa21307c">
+<theory name="TestAutomaticIntro">
  <goal name="g">
  </goal>
 </theory>
-<theory name="TestInduction" sum="7cd4f889593553a3efe96040db1cbe94">
+<theory name="TestInduction">
  <goal name="g">
- <transf name="induction" arg1="n">
-  <goal name="g.0" expl="base case">
-  </goal>
-  <goal name="g.1" expl="recursive case">
+ <transf name="introduce_premises" >
+  <goal name="g.0">
+  <transf name="induction" arg1="n">
+   <goal name="g.0.0" expl="base case">
+   <proof prover="2"><result status="unknown" time="0.01"/></proof>
+   <proof prover="4"><result status="unknown" time="0.02"/></proof>
+   <proof prover="6"><result status="unknown" time="0.01"/></proof>
+   </goal>
+   <goal name="g.0.1" expl="recursive case">
+   <proof prover="2"><result status="unknown" time="0.00"/></proof>
+   <proof prover="4"><result status="unknown" time="0.02"/></proof>
+   <proof prover="6"><result status="unknown" time="0.01"/></proof>
+   </goal>
+  </transf>
   </goal>
  </transf>
  </goal>
 </theory>
-<theory name="TestInfixSymbols" sum="1e2101112f2c37523da345d6bab356e6">
+<theory name="TestInfixSymbols">
  <goal name="g">
  </goal>
 </theory>
-<theory name="TestAutoFocus" sum="bd282d677ea02bff5e05e03fd51a598a">
+<theory name="TestAutoFocus">
  <goal name="g0">
  </goal>
  <goal name="g1">
@@ -159,7 +172,7 @@
  <goal name="g2">
  </goal>
 </theory>
-<theory name="TestRewritePoly" sum="f0130f227c41947e0998709cc1c49883">
+<theory name="TestRewritePoly">
  <goal name="g">
  <transf name="rewrite" arg1="Append_assoc">
   <goal name="g.0">
@@ -167,51 +180,52 @@
  </transf>
  </goal>
 </theory>
-<theory name="Power" sum="53cae56d1419c17b838380453eb24720">
- <goal name="power_1" proved="true">
- <proof prover="1"><result status="valid" time="0.17"/></proof>
+<theory name="Power">
+ <goal name="power_1">
+ <proof prover="1" obsolete="true"><result status="valid" time="0.17"/></proof>
  </goal>
  <goal name="sqrt4_256" proved="true">
  <transf name="exists" proved="true" arg1="4">
   <goal name="sqrt4_256.0" proved="true">
-  <proof prover="1"><result status="valid" time="0.04"/></proof>
-  <proof prover="2"><result status="unknown" time="1.00"/></proof>
+  <proof prover="4"><result status="valid" time="0.05"/></proof>
   </goal>
  </transf>
  </goal>
  <goal name="power_sum" proved="true">
- <transf name="induction" proved="true" arg1="n">
-  <goal name="power_sum.0" expl="base case" proved="true">
-  <proof prover="1"><result status="valid" time="0.01"/></proof>
-  <proof prover="2"><result status="unknown" time="1.00"/></proof>
-  </goal>
-  <goal name="power_sum.1" expl="recursive case" proved="true">
-  <proof prover="0"><result status="valid" time="0.87" steps="15"/></proof>
-  <proof prover="1"><result status="timeout" time="1.00"/></proof>
-  <proof prover="2"><result status="unknown" time="1.01"/></proof>
-  <transf name="case" proved="true" arg1="(n=0)">
-   <goal name="power_sum.1.0" expl="true case (recursive case)" proved="true">
-   <proof prover="1"><result status="valid" time="0.01"/></proof>
-   <proof prover="2"><result status="unknown" time="1.00"/></proof>
+ <transf name="introduce_premises" proved="true" >
+  <goal name="power_sum.0" proved="true">
+  <transf name="induction" proved="true" arg1="n">
+   <goal name="power_sum.0.0" expl="base case" proved="true">
+   <proof prover="1"><result status="valid" time="0.02"/></proof>
    </goal>
-   <goal name="power_sum.1.1" expl="false case (recursive case)" proved="true">
-   <proof prover="0"><result status="timeout" time="1.00"/></proof>
-   <proof prover="1"><result status="timeout" time="1.00"/></proof>
-   <proof prover="2"><result status="unknown" time="1.10"/></proof>
-   <proof prover="3"><result status="unknown" time="0.00"/></proof>
+   <goal name="power_sum.0.1" expl="recursive case" proved="true">
+   <transf name="case" proved="true" arg1="(n=0)">
+    <goal name="power_sum.0.1.0" expl="true case (recursive case)" proved="true">
+    <proof prover="1"><result status="valid" time="0.01"/></proof>
+    <proof prover="2"><result status="valid" time="0.00"/></proof>
+    </goal>
+    <goal name="power_sum.0.1.1" expl="false case (recursive case)" proved="true">
+    <transf name="instantiate" proved="true" arg1="Hrec" arg2="(n-1)">
+     <goal name="power_sum.0.1.1.0" expl="false case (recursive case)" proved="true">
+     <transf name="replace" proved="true" arg1="(n+m)" arg2="((n-1)+m+1)">
+      <goal name="power_sum.0.1.1.0.0" expl="false case (recursive case)" proved="true">
+      <proof prover="0"><result status="valid" time="0.09" steps="15"/></proof>
+      </goal>
+      <goal name="power_sum.0.1.1.0.1" proved="true">
+      <proof prover="2"><result status="valid" time="0.00"/></proof>
+      </goal>
+     </transf>
+     </goal>
+    </transf>
+    </goal>
+   </transf>
    <transf name="instantiate" proved="true" arg1="Hrec" arg2="(n-1)">
-    <goal name="power_sum.1.1.0" expl="false case (recursive case)" proved="true">
-    <proof prover="0"><result status="timeout" time="1.01"/></proof>
-    <proof prover="1"><result status="timeout" time="1.00"/></proof>
-    <proof prover="2"><result status="timeout" time="1.00"/></proof>
-    <proof prover="3"><result status="unknown" time="0.00"/></proof>
+    <goal name="power_sum.0.1.0" expl="recursive case" proved="true">
     <transf name="replace" proved="true" arg1="(n+m)" arg2="((n-1)+m+1)">
-     <goal name="power_sum.1.1.0.0" expl="false case (recursive case)" proved="true">
-     <proof prover="0"><result status="valid" time="0.08" steps="14"/></proof>
-     <proof prover="1"><result status="timeout" time="1.00"/></proof>
-     <proof prover="2"><result status="timeout" time="1.00"/></proof>
+     <goal name="power_sum.0.1.0.0" expl="recursive case" proved="true">
+     <proof prover="0"><result status="valid" time="0.11" steps="14"/></proof>
      </goal>
-     <goal name="power_sum.1.1.0.1" proved="true">
+     <goal name="power_sum.0.1.0.1" proved="true">
      <proof prover="2"><result status="valid" time="0.00"/></proof>
      </goal>
     </transf>
@@ -219,43 +233,20 @@
    </transf>
    </goal>
   </transf>
-  <transf name="instantiate" proved="true" arg1="Hrec" arg2="(n-1)">
-   <goal name="power_sum.1.0" expl="recursive case" proved="true">
-   <transf name="replace" proved="true" arg1="(n+m)" arg2="((n-1)+m+1)">
-    <goal name="power_sum.1.0.0" expl="recursive case" proved="true">
-    <proof prover="0"><result status="valid" time="0.22" steps="29"/></proof>
-    <proof prover="1"><result status="timeout" time="1.00"/></proof>
-    <proof prover="2"><result status="timeout" time="1.00"/></proof>
-    </goal>
-    <goal name="power_sum.1.0.1" proved="true">
-    <proof prover="2"><result status="valid" time="0.00"/></proof>
-    </goal>
-   </transf>
-   </goal>
-  </transf>
-  <transf name="replace" arg1="(n+m)" arg2="((n-1)+m+1)">
-   <goal name="power_sum.1.0" expl="recursive case">
-   <proof prover="0"><result status="timeout" time="1.00"/></proof>
-   <proof prover="1"><result status="timeout" time="1.00"/></proof>
-   <proof prover="2"><result status="unknown" time="1.74"/></proof>
-   <proof prover="3"><result status="unknown" time="0.01"/></proof>
-   </goal>
-   <goal name="power_sum.1.1" proved="true">
-   <proof prover="2"><result status="valid" time="0.00"/></proof>
-   </goal>
-  </transf>
   </goal>
  </transf>
  </goal>
  <goal name="power_0_left" proved="true">
- <transf name="replace" proved="true" arg1="n" arg2="(n-1+1)">
+ <transf name="introduce_premises" proved="true" >
   <goal name="power_0_left.0" proved="true">
-  <proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
-  <proof prover="1"><result status="timeout" time="1.00"/></proof>
-  <proof prover="2"><result status="unknown" time="0.98"/></proof>
-  </goal>
-  <goal name="power_0_left.1" proved="true">
-  <proof prover="2"><result status="valid" time="0.00"/></proof>
+  <transf name="replace" proved="true" arg1="n" arg2="(n-1+1)">
+   <goal name="power_0_left.0.0" proved="true">
+   <proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
+   </goal>
+   <goal name="power_0_left.0.1" proved="true">
+   <proof prover="2"><result status="valid" time="0.00"/></proof>
+   </goal>
+  </transf>
   </goal>
  </transf>
  </goal>