commit by user ricciott

[helm.git] / weblib / ricciott / cpp2012.ma

diff --git a/weblib/ricciott/cpp2012.ma b/weblib/ricciott/cpp2012.ma
new file mode 100644 (file)
index 0000000..bac60d2
--- /dev/null
+++ b/weblib/ricciott/cpp2012.ma
@@ -0,0 +1,43 @@
+(* new script *)
+
+include "basics/logic.ma".
+include "basics/types.ma".
+include "basics/bool.ma".
+include "arithmetics/nat.ma".
+include "basics/list.ma".
+
+axiom Vector : Type[0] → nat → Type[0].
+axiom tape : Type[0] → Type[0].
+axiom current : ∀T:Type[0]. tape T → option T.
+axiom vec : ∀T:Type[0].∀n:nat.Vector T n → list T.
+coercion vec : ∀T:Type[0].∀n:nat.∀v:Vector T n.list T ≝ vec on _v:Vector ?? to list ?.
+axiom niltape : ∀T.tape T.
+axiom midtape : ∀T.list T → T → list T → tape T.
+axiom change_vec : ∀T,n.Vector T n → T → nat → Vector T n.
+axiom move : Type[0].
+axiom R : move.
+axiom tape_move : ∀T.tape T → option (T × move) → tape T.
+axiom memb: ∀T.T → list T → bool.
+interpretation "boolean membership" 'mem a l = (memb ? a l).
+axiom right : ∀T.tape T → list T.
+
+
+definition R_match_step_true ≝ 
+  λsrc,dst,sig,n,is_startc,is_endc.λint,outt: Vector (tape sig) (S n).
+  ∀s.current sig (nth src (tape sig) int (niltape sig)) = Some ? s → 
+  current sig (nth dst (tape sig) int (niltape sig)) ≠ None ? ∧
+  (is_startc s = true → 
+   (∀c.c ∈ right ? (nth src (tape sig) int (niltape sig)) = true → is_startc c = false) →
+   (∀s1.current sig (nth dst (tape sig) int (niltape sig)) = Some ? s1 → s ≠ s1 →  
+    outt = change_vec ?? int 
+          (tape_move … (nth dst ? int (niltape ?)) (Some ? 〈s1,R〉)) dst ∧ is_endc s = false) ∧  
+   (∀ls,x,xs,ci,rs,ls0,rs0. 
+     nth src ? int (niltape ?) = midtape ls x (xs@ci::rs) →
+     nth dst ? int (niltape ?) = midtape sig ls0 x (xs@rs0) →
+     (∀c0. memb ? c0 (x::xs) = true → is_endc c0 = false) → 
+     is_endc ci = false ∧ rs0 ≠ [] ∧
+     ∀cj,rs1.rs0 = cj::rs1 → 
+      ci ≠ cj →
+      (outt = change_vec ?? int 
+          (tape_move … (nth dst ? int (niltape ?)) (Some ? 〈x,R〉)) dst ∧ is_endc ci = false))). 
+