src/HOL/HoareParallel/OG_Syntax.thy
changeset 28524 644b62cf678f
parent 25706 45d090186bbe
child 31723 f5cafe803b55
equal deleted inserted replaced
28523:5818d9cfb2e7 28524:644b62cf678f
    43   "c_1,, c_2" \<rightleftharpoons> "Seq c_1 c_2"
    43   "c_1,, c_2" \<rightleftharpoons> "Seq c_1 c_2"
    44 
    44 
    45   "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "Cond .{b}. c1 c2"
    45   "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "Cond .{b}. c1 c2"
    46   "IF b THEN c FI" \<rightleftharpoons> "IF b THEN c ELSE SKIP FI"
    46   "IF b THEN c FI" \<rightleftharpoons> "IF b THEN c ELSE SKIP FI"
    47   "WHILE b INV i DO c OD" \<rightharpoonup> "While .{b}. i c"
    47   "WHILE b INV i DO c OD" \<rightharpoonup> "While .{b}. i c"
    48   "WHILE b DO c OD" \<rightleftharpoons> "WHILE b INV arbitrary DO c OD"
    48   "WHILE b DO c OD" \<rightleftharpoons> "WHILE b INV CONST undefined DO c OD"
    49 
    49 
    50   "r SKIP" \<rightleftharpoons> "AnnBasic r id"
    50   "r SKIP" \<rightleftharpoons> "AnnBasic r id"
    51   "c_1;; c_2" \<rightleftharpoons> "AnnSeq c_1 c_2" 
    51   "c_1;; c_2" \<rightleftharpoons> "AnnSeq c_1 c_2" 
    52   "r IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "AnnCond1 r .{b}. c1 c2"
    52   "r IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "AnnCond1 r .{b}. c1 c2"
    53   "r IF b THEN c FI" \<rightharpoonup> "AnnCond2 r .{b}. c"
    53   "r IF b THEN c FI" \<rightharpoonup> "AnnCond2 r .{b}. c"