| DISP | com_df |  == |
| ABS | com | == rec(C.Unit + C  C + Atom Exp +  exp C C + exp C) |
| THM | com_wf |   |
| DISP | skip_df | SKIP== SKIP |
| ABS | skip | SKIP == inl  |
| THM | skip_wf | SKIP |
| DISP | seq_df | {[SOFT}{->0}<c1:com:*> {\\}<c2:com:*>{<-}{]}== <c1> <c2> |
| ABS | seq | c1; c2 == inr (inl <c1, c2> ) |
| THM | seq_wf |  c1,c2:. c1; c2 |
| DISP | assig_df | <v:atom:*> := <e:exp:*>== <v> := <e> |
| ABS | assig | v := e == inr inr (inl <v, e> ) |
| THM | assig_wf | v:Atom. e:Exp. v := e |
| DISP | as_df | <a:tok> := <e:exp:*>== <a> := <e> |
| ABS | as | $a := e == "$a" := e |
| ML | as_tac | add_soft_abs ``as``;;
let asC = UnfoldC `as`;;
add_AbReduce_conv `as` asC;; |
| DISP | if_df | {[SOFT}{->0}IF {->0}<b:bexp:*> THEN {\\}<c1:com:*> {<-}{\\}ELS{->0}E
{\\}<c2:com:*> {<-}{\\}{<-}{]}
== IF <b> THEN <c1> ELSE <c2> |
| ABS | if | IF b THEN c1 ELSE c2 == inr inr inr (inl <b, c1, c2> ) |
| THM | if_wf | b:exp. c1,c2:. IF b THEN c1 ELSE c2 |
| DISP | while_df | {[SOFT}{->0}WHI{->0}LE <b:bexp:*> DO {\\}<c:com:*> {<-}{\\}OD{<-}{\\}
{]}
== WHILE <b> DO <c> OD |
| ABS | while | WHILE b DO c OD == inr inr inr inr <b, c> |
| THM | while_wf | b:exp. c:. WHILE b DO c OD |
| DISP | com_cases_df | {[SOFT}{->0}case <c:com:*> {\\}of {->0}SKIP   <skip_case:skip_case:*>
{\\}<c1:var><c2:var> <seq_case:seq_case:*> {\\}<v:var> := <e:var>
<assig_case:assig_case:*> {\\}IF (<b1:var>) <c3:var> ELSE <c4:var>
<if_case:if_case:*> {\\}WHILE (<b2:var>) <c5:var>
<while_case:while_case:*>{<-}{<-}{\\}{]}
== case <c>
of SKIP <skip_case>
<c1><c2> <seq_case>
<v> := <e> <assig_case>
IF (<b1>) <c3> ELSE <c4> <if_case>
WHILE (<b2>) <c5> <while_case>
|
| ABS | com_cases | case c
of SKIP skip_case
c1;c2 seq_case[c1; c2]
v := e assig_case[v; e]
IF (b1) c3 ELSE c4 if_case[b1; c3; c4]
WHILE (b2) c5 while_case[b2; c5]
==
case c
of inl(sk) => skip_case
| inr(nsk) => case nsk
of inl(se) => let <c1,c2> = se in seq_case[c1; c2]
| inr(nse) => case nse
of inl(as) => let <v,e> = as
in
assig_case[v; e]
| inr(nas) => case nas
of inl(i) => let <b1,c3
c4> = i
in
let <c3,c4
> = c3c4
in
if_case[b1
; c3; c4]
| inr(wh) => let <b2,c
5> = wh
in
while_cas
e[b2; c5] |
| THM | com_cases_wf | T:. skip_case:T. seq_case: T. assig_case:Atom
Exp
T.
if_case:exp T. while_case:exp T. c:.
case c
of SKIP skip_case
c1;c2 seq_case[c1;c2]
v := e assig_case[v;e]
IF (b1) c3 ELSE c4 if_case[b1;c3;c4]
WHILE (b2) c5 while_case[b2;c5]
T |
| THM | com_cases_wf1 | T:'. skip_case:T. seq_case: T. assig_case:Atom
Exp
T.
if_case:exp T. while_case:exp T. c:.
case c
of SKIP skip_case
c1;c2 seq_case[c1;c2]
v := e assig_case[v;e]
IF (b1) c3 ELSE c4 if_case[b1;c3;c4]
WHILE (b2) c5 while_case[b2;c5]
T |
| ML | com_cases_eval1 | let com_cases_skipC =
SimpleMacroC `com_cases_skip`
 case SKIP
of SKIP skip_case
c1;c2 seq_case[c1; c2]
v := e assig_case[v; e]
IF (b) c1 ELSE c2 if_case[b; c1; c2]
WHILE (b) c while_case[b; c]
skip_case ``com_cases skip``
;;
let com_cases_seqC =
SimpleMacroC `com_cases_seq`
case x; y
of SKIP skip_case
c1;c2 seq_case[c1; c2]
v := e assig_case[v; e]
IF (b) c1 ELSE c2 if_case[b; c1; c2]
WHILE (b) c while_case[b; c]
seq_case[x; y] ``com_cases seq``
;;
let com_cases_assigC =
SimpleMacroC `com_cases_assig`
case x := y
of SKIP skip_case
c1;c2 seq_case[c1; c2]
v := e assig_case[v; e]
IF (b) c1 ELSE c2 if_case[b; c1; c2]
WHILE (b) c while_case[b; c]
assig_case[x; y] ``com_cases assig``
;;
let com_cases_ifC =
SimpleMacroC `com_cases_if`
case IF x THEN y ELSE z
of SKIP skip_case
c1;c2 seq_case[c1; c2]
v := e assig_case[v; e]
IF (b) c1 ELSE c2 if_case[b; c1; c2]
WHILE (b) c while_case[b; c]
if_case[x; y; z] ``com_cases if``
;; |
| ML | com_cases_eval2 | let com_cases_whileC =
SimpleMacroC `com_cases_while`
case WHILE x DO y OD
of SKIP skip_case
c1;c2 seq_case[c1; c2]
v := e assig_case[v; e]
IF (b) c1 ELSE c2 if_case[b; c1; c2]
WHILE (b) c while_case[b; c]
while_case[x; y] ``com_cases while``
;;
let com_casesC =
FirstC [com_cases_skipC;
com_cases_seqC;
com_cases_assigC;
com_cases_ifC;
com_cases_whileC]
;;
add_AbReduce_conv `com_cases` com_casesC
;; |
| THM | com_ind_tp | T:. P:  .
P[SKIP]
  (c1,c2:. P[c1] P[c2] P[c1; c2])
(v:Atom. e:Exp. P[v := e])
(b:exp. c1,c2:. P[c1] P[c2] P[IF b THEN c1 ELSE c2 ])
(b:exp. c:. P[c] P[WHILE b DO c OD])
{c:. P[c]} |
| ML | com_ind_tac | let ComInd i p = ByAnalogyWith1 `com_ind_tp` [`hr`, int_to_arg i] p;; |
| DISP | is_skip_df | is_skip(<c:com:*>)== is_skip(<c>) |
| ABS | is_skip | is_skip(c) ==
case c
of SKIP tt
c1;c2 ff
e1 := e2 ff
IF (b) c1 ELSE c2 ff
WHILE (b) c ff
|
| THM | is_skip_wf | c:. is_skip(c) |
| ML | is_skip_eval | let is_skip_skipC =
MacroC `is_skip_skip`
(EvalC ``is_skip``) is_skip(SKIP) IdC tt;;
let is_skip_seqC =
MacroC `is_skip_seq`
(EvalC ``is_skip``) is_skip(c1; c2) IdC ff;;
let is_skip_assigC =
MacroC `is_skip_assig`
(EvalC ``is_skip``) is_skip(e1 := e2) IdC ff;;
let is_skip_ifC =
MacroC `is_skip_if`
(EvalC ``is_skip``) is_skip(IF b THEN c1 ELSE c2 ) IdC ff;;
let is_skip_whileC =
MacroC `is_skip_while`
(EvalC ``is_skip``) is_skip(WHILE b DO c OD) IdC ff;;
add_AbReduce_conv `is_skip`
(FirstC [is_skip_skipC;
is_skip_seqC;
is_skip_assigC;
is_skip_ifC;
is_skip_whileC])
;; |
| THM | is_skip_eq_skip | c:.  is_skip(c) c = SKIP |