equal
deleted
inserted
replaced
42 qed auto |
42 qed auto |
43 |
43 |
44 abbreviation Big_step :: "com \<Rightarrow> com_den" where |
44 abbreviation Big_step :: "com \<Rightarrow> com_den" where |
45 "Big_step c \<equiv> {(s,t). (c,s) \<Rightarrow> t}" |
45 "Big_step c \<equiv> {(s,t). (c,s) \<Rightarrow> t}" |
46 |
46 |
47 lemma Big_step_if_D: "(s,t) \<in> D(c) \<Longrightarrow> (s,t) : Big_step c" |
47 lemma Big_step_if_D: "(s,t) \<in> D(c) \<Longrightarrow> (s,t) \<in> Big_step c" |
48 proof (induction c arbitrary: s t) |
48 proof (induction c arbitrary: s t) |
49 case Seq thus ?case by fastforce |
49 case Seq thus ?case by fastforce |
50 next |
50 next |
51 case (While b c) |
51 case (While b c) |
52 let ?B = "Big_step (WHILE b DO c)" let ?f = "W (bval b) (D c)" |
52 let ?B = "Big_step (WHILE b DO c)" let ?f = "W (bval b) (D c)" |