theory CoSemantics imports "../Projekt/Semantics" begin coinductive eval :: "com \ state \ state \ bool" ("((1\_,/_\) \/ _)" [0,0,50] 26) where EvalSkip: "\Skip,s\ \ s" | EvalLAss: "\x::=e,s\ \ s(x := \e\s)" | EvalSeq: "\\c\<^sub>1,s\ \ s''; \c\<^sub>2,s''\ \ s'\ \ \c\<^sub>1;;c\<^sub>2,s\ \ s'" | EvalCondTrue: "\\b\ s = Some true; \c\<^sub>1,s\ \ s'\ \ \IF (b) c\<^sub>1 ELSE c\<^sub>2,s\ \ s'" | EvalCondFalse: "\\b\ s = Some false; \c\<^sub>2,s\ \ s'\ \ \IF (b) c\<^sub>1 ELSE c\<^sub>2,s\ \ s'" | EvalWhileTrue: "\\b\ s = Some true; \c,s\ \ s''; \WHILE (b) c,s''\ \ s'\ \ \WHILE (b) c,s\ \ s'" | EvalWhileFalse: "\b\ s = Some false \ \WHILE (b) c,s\ \ s" parseWhileString prog = " while (0 < 1) { x := x + 1; } " lemma "\ (\prog, s\ \ s' : t)" by (rule notI) (induction "prog" s s' t rule: Semantics.eval.induct; simp add: prog_def) lemma "\prog, s\ \ s'" (* apply (rule eval.coinduct [where X="\p t t'. p = prog \ (t = s \ t = s(''x'' := None) \ (\k. t = s(''x'' := \Var ''x'' \Add\ Val (Intg k)\ s))) \ t' = s'"]) apply simp apply (clarsimp simp: prog_def) apply (rule_tac x="xa(''x'' := \Var ''x'' \Add\ Val (Intg 1)\ xa)" in exI) apply (rule conjI) apply (rule EvalLAss) apply (clarsimp split: option.splits) apply (case_tac x2; clarsimp) apply force[1] apply auto apply (case_tac y; auto) by (force simp: ac_simps) *) proof - consider (bool) b where "s ''x'' = Some (Bool b)" | (intg) k where "s ''x'' = Some (Intg k)" | (none) "s ''x'' = None" by (cases "s ''x''") (auto intro: val.exhaust) then show ?thesis proof cases case [simp]: bool show ?thesis apply (rule eval.coinduct [where X="\p t t'. p = prog \ (t = s \ t = s(''x'' := None)) \ t' = s'"]) apply simp apply (clarsimp simp: prog_def) apply (rule_tac x="xa(''x'' := \ Var ''x'' \Add\ Val (Intg 1)\ xa)" in exI) apply (rule conjI) apply (rule EvalLAss) by auto next case [simp]: intg show ?thesis apply (rule eval.coinduct [where X="\p t t'. p = prog \ (\k. t = s(''x'' := \Var ''x'' \Add\ Val (Intg k)\ s)) \ t' = s'"]) apply simp apply (rule_tac x=0 in exI) apply simp apply (rule ext) apply (clarsimp simp: fun_upd_def) apply (clarsimp simp: prog_def) apply (rule_tac x="(s(''x'' \ Intg (k + ka)))(''x'' := \Var ''x'' \Add\ Val (Intg 1)\ s(''x'' \ Intg (k + ka)))" in exI) apply (rule conjI) apply (rule EvalLAss) apply clarsimp apply (rule_tac x="ka + 1" in exI) by (clarsimp simp: ac_simps) next case [simp]: none show ?thesis apply (coinduction rule: eval.coinduct; simp add: prog_def) apply (rule_tac x="s(''x'' := None)" in exI) apply auto by (rule EvalLAss [where x="''x''" and e="Var ''x'' \Add\ Val (Intg 1)", of s, simplified]) qed qed end