equal
deleted
inserted
replaced
1227 lemma (in UP_pre_univ_prop) eval_monom: |
1227 lemma (in UP_pre_univ_prop) eval_monom: |
1228 assumes R: "r \<in> carrier R" and S: "s \<in> carrier S" |
1228 assumes R: "r \<in> carrier R" and S: "s \<in> carrier S" |
1229 shows "eval R S h s (monom P r n) = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n" |
1229 shows "eval R S h s (monom P r n) = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n" |
1230 proof - |
1230 proof - |
1231 interpret UP_univ_prop [R S h P s _] |
1231 interpret UP_univ_prop [R S h P s _] |
1232 by (auto! intro: UP_univ_prop.intro UP_univ_prop_axioms.intro) |
1232 using `UP_pre_univ_prop R S h` P_def R S |
|
1233 by (auto intro: UP_univ_prop.intro UP_univ_prop_axioms.intro) |
1233 from R |
1234 from R |
1234 show ?thesis by (rule Eval_monom) |
1235 show ?thesis by (rule Eval_monom) |
1235 qed |
1236 qed |
1236 |
1237 |
1237 lemma (in UP_univ_prop) Eval_smult: |
1238 lemma (in UP_univ_prop) Eval_smult: |