equal
deleted
inserted
replaced
10 |
10 |
11 text {* |
11 text {* |
12 Lifting beta-reduction to lists of terms, reducing exactly one element. |
12 Lifting beta-reduction to lists of terms, reducing exactly one element. |
13 *} |
13 *} |
14 |
14 |
15 syntax |
15 abbreviation (output) |
16 "_list_beta" :: "dB => dB => bool" (infixl "=>" 50) |
16 list_beta :: "dB list => dB list => bool" (infixl "=>" 50) |
17 translations |
17 "(rs => ss) = ((rs, ss) : step1 beta)" |
18 "rs => ss" == "(rs, ss) : step1 beta" |
|
19 |
18 |
20 lemma head_Var_reduction: |
19 lemma head_Var_reduction: |
21 "Var n \<degree>\<degree> rs -> v \<Longrightarrow> \<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss" |
20 "Var n \<degree>\<degree> rs -> v \<Longrightarrow> \<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss" |
22 apply (induct u == "Var n \<degree>\<degree> rs" v fixing: rs set: beta) |
21 apply (induct u == "Var n \<degree>\<degree> rs" v fixing: rs set: beta) |
23 apply simp |
22 apply simp |