1open preamble lprefix_lubTheory 2 3val _ = new_theory "while_lang"; 4 5Type nat[pp] = ���:num���; 6 7(* -- AST and other types -- *) 8 9Type name = ���: string ��� 10Type value = ���: nat ��� 11Type store = ���: name -> value ��� 12Type exp = ���: store -> value ��� 13 14Datatype: 15 prog = Skip 16 | Assign name exp 17 | Print exp 18 | Seq prog prog 19 | If exp prog prog 20 | While exp prog 21End 22 23 24(* -- small-step semantics -- *) 25 26Type output = ���: value list ��� 27Type state[pp] = ���: store # output ��� 28 29Definition output_of_def: 30 output_of ((s,out):state) = out 31End 32 33Definition subst_def: 34 subst n e (s,out) = ((n =+ e s) s,out:value list) 35End 36 37Definition print_def: 38 print e ((s,out):state) = (s,out ++ [e s]) 39End 40 41Definition guard_def: 42 guard x ((s,out):state) = (x s ��� 0) 43End 44 45Inductive step: 46 (���s:state. 47 step (Skip,s) (Skip,s)) 48 ��� 49 (���s n x. 50 step (Assign n x,s) (Skip, subst n x s)) 51 ��� 52 (���s x. 53 step (Print x,s) (Skip, print x s)) 54 ��� 55 (���s q. 56 step (Seq Skip q,s) (q,s)) 57 ��� 58 (���p0 p1 q s0 s1. 59 step (p0,s0) (p1,s1) ��� p0 ��� Skip ��� 60 step (Seq p0 q,s0) (Seq p1 q,s1)) 61 ��� 62 (���x p q s. 63 step (If x p q, s) ((if guard x s then p else q), s)) 64 ��� 65 (���x p s. 66 step (While x p, s) (If x (Seq p (While x p)) Skip, s)) 67End 68 69Inductive terminates: 70 ���s p t. RTC step (p,s) (Skip,t) ��� terminates s p t 71End 72 73Inductive diverges: 74 ���s p output. 75 (���t. ~(terminates s p t)) ��� 76 output = LUB { fromList out | ���q t. RTC step (p,s) (q,t,out) } 77 ��� 78 diverges s p output 79End 80 81val _ = export_theory(); 82