theory Solution06_2 imports "HOL-IMP.BExp" begin section "Nondeterminism" 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) | Or com com ("_ OR/ _" [60, 61] 60) | ASSUME bexp inductive big_step :: "com \ state \ state \ bool" (infix "\" 55) where Skip: "(SKIP,s) \ s" | Assign: "(x ::= a,s) \ s(x := aval a s)" | Seq: "\ (c\<^sub>1,s\<^sub>1) \ s\<^sub>2; (c\<^sub>2,s\<^sub>2) \ s\<^sub>3 \ \ (c\<^sub>1;;c\<^sub>2, s\<^sub>1) \ s\<^sub>3" | IfTrue: "\ bval b s; (c\<^sub>1,s) \ t \ \ (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \ t" | IfFalse: "\ \bval b s; (c\<^sub>2,s) \ t \ \ (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \ t" | WhileFalse: "\bval b s \ (WHILE b DO c,s) \ s" | WhileTrue: "\ bval b s\<^sub>1; (c,s\<^sub>1) \ s\<^sub>2; (WHILE b DO c, s\<^sub>2) \ s\<^sub>3 \ \ (WHILE b DO c, s\<^sub>1) \ s\<^sub>3" | Or1: "(c\<^sub>1,s) \ s' \ (c\<^sub>1 OR c\<^sub>2, s) \ s'" | Or2: "(c\<^sub>2,s) \ s' \ (c\<^sub>1 OR c\<^sub>2, s) \ s'" | Assume: "bval b s \ (ASSUME b, s) \ s" abbreviation equiv_c :: "com \ com \ bool" (infix "\" 50) where "c \ c' \ (\s t. (c,s) \ t = (c',s) \ t)" inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \ t" inductive_cases AssumeE[elim!]: "(ASSUME b, s) \ t" inductive_cases SeqE[elim!]: "(c1;;c2,s1) \ s3" inductive_cases OrE[elim!]: "(c1 OR c2, s) \ t" declare big_step.intros[intro] lemma or_commute: "c1 OR c2 \ c2 OR c1" by auto lemma if_then_else_assume: "(IF b THEN c1 ELSE c2) \ ((ASSUME b;; c1 ) OR (ASSUME (Not b);; c2 ))" by fastforce end