Re: [isabelle] Introducing a variable from a constant



Am 25.12.2011 20:12, schrieb Lars Hupel:
> I'm trying to formalize that for a particular grammar, there is no
> production which accepts the empty word. Thus, I wrote the following lemma:
> 
> lemma empty_unaccepted_helper:
> 	"⟦ accepted prods nt bs; bs = [] ⟧ ⟹ False"
> by (induction rule: accepted.induct) auto
> 
> Now I want to make that fact explicit:
> 
> lemma empty_unaccepted[simp]: "¬ (accepted prods nt [])"
> 
> My idea is the following:
> 
> proof
>   assume "accepted prods nt []"
>   hence "accepted prods nt bs ∧ bs = []" (* and now? *)
> 
> I know that this is a rather naive approach and as expected it didn't
> work. Any idea on how I could do that?
> 
> 
> 

lemma empty_unaccepted[simp]: "¬ (accepted prods nt [])"
proof (rule notI)
  assume "accepted prods nt []"
  with empty_unaccepted_helper[OF this] show "False" by simp
qed

- René

-- 
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.