equal
deleted
inserted
replaced
236 |
236 |
237 declare split_if [split] split_if_asm [split] |
237 declare split_if [split] split_if_asm [split] |
238 option.split [split] option.split_asm [split] |
238 option.split [split] option.split_asm [split] |
239 not_None_eq [simp] |
239 not_None_eq [simp] |
240 split_paired_All [simp] split_paired_Ex [simp] |
240 split_paired_All [simp] split_paired_Ex [simp] |
241 declaration {* K (Simplifier.map_ss (fn ss => ss addloop' ("split_all_tac", split_all_tac))) *} |
241 declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *} |
242 |
242 |
243 lemma evaln_Inj_elim: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w,s') \<Longrightarrow> case t of In1 ec \<Rightarrow> |
243 lemma evaln_Inj_elim: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w,s') \<Longrightarrow> case t of In1 ec \<Rightarrow> |
244 (case ec of Inl e \<Rightarrow> (\<exists>v. w = In1 v) | Inr c \<Rightarrow> w = \<diamondsuit>) |
244 (case ec of Inl e \<Rightarrow> (\<exists>v. w = In1 v) | Inr c \<Rightarrow> w = \<diamondsuit>) |
245 | In2 e \<Rightarrow> (\<exists>v. w = In2 v) | In3 e \<Rightarrow> (\<exists>v. w = In3 v)" |
245 | In2 e \<Rightarrow> (\<exists>v. w = In2 v) | In3 e \<Rightarrow> (\<exists>v. w = In3 v)" |
246 apply (erule evaln_cases , auto) |
246 apply (erule evaln_cases , auto) |