equal
deleted
inserted
replaced
274 apply (simp only: upper_unit_Rep_compact_basis [symmetric] |
274 apply (simp only: upper_unit_Rep_compact_basis [symmetric] |
275 upper_plus_principal [symmetric]) |
275 upper_plus_principal [symmetric]) |
276 apply (erule insert [OF unit]) |
276 apply (erule insert [OF unit]) |
277 done |
277 done |
278 |
278 |
279 lemma upper_pd_induct: |
279 lemma upper_pd_induct |
|
280 [case_names adm upper_unit upper_plus, induct type: upper_pd]: |
280 assumes P: "adm P" |
281 assumes P: "adm P" |
281 assumes unit: "\<And>x. P {x}\<sharp>" |
282 assumes unit: "\<And>x. P {x}\<sharp>" |
282 assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<sharp> ys)" |
283 assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<sharp> ys)" |
283 shows "P (xs::'a upper_pd)" |
284 shows "P (xs::'a upper_pd)" |
284 apply (induct xs rule: upper_pd.principal_induct, rule P) |
285 apply (induct xs rule: upper_pd.principal_induct, rule P) |