equal
deleted
inserted
replaced
7 header {* Application of a term to a list of terms *} |
7 header {* Application of a term to a list of terms *} |
8 |
8 |
9 theory ListApplication imports Lambda begin |
9 theory ListApplication imports Lambda begin |
10 |
10 |
11 abbreviation |
11 abbreviation |
12 list_application :: "dB => dB list => dB" (infixl "\<degree>\<degree>" 150) |
12 list_application :: "dB => dB list => dB" (infixl "\<degree>\<degree>" 150) where |
13 "t \<degree>\<degree> ts == foldl (op \<degree>) t ts" |
13 "t \<degree>\<degree> ts == foldl (op \<degree>) t ts" |
14 |
14 |
15 lemma apps_eq_tail_conv [iff]: "(r \<degree>\<degree> ts = s \<degree>\<degree> ts) = (r = s)" |
15 lemma apps_eq_tail_conv [iff]: "(r \<degree>\<degree> ts = s \<degree>\<degree> ts) = (r = s)" |
16 by (induct ts rule: rev_induct) auto |
16 by (induct ts rule: rev_induct) auto |
17 |
17 |