weblib/ricciott/cpp2012.ma

   1 (* new script *)
   2
   3 include "basics/logic.ma".
   4 include "basics/types.ma".
   5 include "basics/bool.ma".
   6 include "arithmetics/nat.ma".
   7 include "basics/list.ma".
   8
   9 axiom Vector : Type[0] → nat → Type[0].
  10 axiom tape : Type[0] → Type[0].
  11 axiom current : ∀T:Type[0]. tape T → option T.
  12 axiom vec : ∀T:Type[0].∀n:nat.Vector T n → list T.
  13 coercion vec : ∀T:Type[0].∀n:nat.∀v:Vector T n.list T ≝ vec on _v:Vector ?? to list ?.
  14 axiom niltape : ∀T.tape T.
  15 axiom midtape : ∀T.list T → T → list T → tape T.
  16 axiom change_vec : ∀T,n.Vector T n → T → nat → Vector T n.
  17 axiom move : Type[0].
  18 axiom R : move.
  19 axiom tape_move : ∀T.tape T → option (T × move) → tape T.
  20 axiom memb: ∀T.T → list T → bool.
  21 interpretation "boolean membership" 'mem a l = (memb ? a l).
  22 axiom right : ∀T.tape T → list T.
  23
  24
  25 definition R_match_step_true ≝
  26   λsrc,dst,sig,n,is_startc,is_endc.λint,outt: Vector (tape sig) (S n).
  27   ∀s.current sig (nth src (tape sig) int (niltape sig)) = Some ? s →
  28   current sig (nth dst (tape sig) int (niltape sig)) ≠ None ? ∧
  29   (is_startc s = true →
  30    (∀c.c ∈ right ? (nth src (tape sig) int (niltape sig)) = true → is_startc c = false) →
  31    (∀s1.current sig (nth dst (tape sig) int (niltape sig)) = Some ? s1 → s ≠ s1 →
  32     outt = change_vec ?? int
  33           (tape_move … (nth dst ? int (niltape ?)) (Some ? 〈s1,R〉)) dst ∧ is_endc s = false) ∧
  34    (∀ls,x,xs,ci,rs,ls0,rs0.
  35      nth src ? int (niltape ?) = midtape ls x (xs@ci::rs) →
  36      nth dst ? int (niltape ?) = midtape sig ls0 x (xs@rs0) →
  37      (∀c0. memb ? c0 (x::xs) = true → is_endc c0 = false) →
  38      is_endc ci = false ∧ rs0 ≠ [] ∧
  39      ∀cj,rs1.rs0 = cj::rs1 →
  40       ci ≠ cj →
  41       (outt = change_vec ?? int
  42           (tape_move … (nth dst ? int (niltape ?)) (Some ? 〈x,R〉)) dst ∧ is_endc ci = false))).
  43