Demostración automática de teoremas (2014-15) Demostración automática de teoremas (2014-15)

header "IMP: sintaxis de un lenguaje imperativo simple"

theory Com_b imports BExp_b begin

text{*
Definimos un lenguaje imperativo con las instrucciones básicas
siguientes: asignación, composición secuencial, condicional,
bucle mientras y SKIP (para representar una instrucción sin 
ninguna acción a realizar). 

Las instrucciones del lenguaje son:
- Assign x e: asignar la expresión aritmética e a la variable x
- Seq c1 c2: realizar la instrucción cs y, a continuación, c2
- If b c1 c2: si la expresión booleana b es verdadera, realiizar c2;
              en caso contrario, realizar c2
- WHILE b c1 c2: mientras la expresión booleana b sea verdadera,
                 realizar c1; después, realizar c2
- SKIP: no hacer nada

*}

text{*
Representamos el lenguaje mediante el siguiente tipo:
*}

datatype
  com = SKIP 
      | Assign vname aexp       ("_ ::= _" [1000, 61] 61)
      | Seq    com  com         ("_;;/ _"  [60, 61] 60)
      | If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
      | While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)


text{*
Observaciones:

- Escribiremos Assign x a como x::= e
- Escribiremos Seq c1 c2 como c1 ;; c2
- Escribiremos if b c1 c2 como IF b THEN c1 ELSE c2
- Escribiremos While b c como WHILE b DO c
- La instrucción ;; asocia por la izquierda. Es decir,
  c1 ;; c2 ;; c3  es (c1 ;; c2) ;; c3
- Las instrucciones IF y WHILE tienen prelación sobre ;;.  
  Es decir, WHILE b DO c1 ;; c2 es (WHILE b DO c1) ;; c2.
*}

text{*
Ejemplo:
*}

value "Assign ''y'' (N 2)"
value "''y'' ::= (N 2)"
value "''x'' ::= Plus (V ''y'') (N 1) ;; ''y''::= N 2"


end