src/HOL/Lambda/ListBeta.thy
changeset 9827 ce6e22ff89c3
parent 9811 39ffdb8cab03
child 9906 5c027cca6262
equal deleted inserted replaced
9826:5b5d9ee742ca 9827:ce6e22ff89c3
    13 *}
    13 *}
    14 
    14 
    15 syntax
    15 syntax
    16   "_list_beta" :: "dB => dB => bool"   (infixl "=>" 50)
    16   "_list_beta" :: "dB => dB => bool"   (infixl "=>" 50)
    17 translations
    17 translations
    18   "rs => ss" == "(rs,ss) : step1 beta"
    18   "rs => ss" == "(rs, ss) : step1 beta"
    19 
    19 
    20 lemma head_Var_reduction_aux:
    20 lemma head_Var_reduction_aux:
    21   "v -> v' ==> \<forall>rs. v = Var n $$ rs --> (\<exists>ss. rs => ss \<and> v' = Var n $$ ss)"
    21   "v -> v' ==> \<forall>rs. v = Var n $$ rs --> (\<exists>ss. rs => ss \<and> v' = Var n $$ ss)"
    22   apply (erule beta.induct)
    22   apply (erule beta.induct)
    23      apply simp
    23      apply simp