1078 using lin |
1078 using lin |
1079 proof (induct p rule: iszlfm.induct) |
1079 proof (induct p rule: iszlfm.induct) |
1080 case (1 p q) |
1080 case (1 p q) |
1081 let ?d = "\<delta> (And p q)" |
1081 let ?d = "\<delta> (And p q)" |
1082 from prems ilcm_pos have dp: "?d >0" by simp |
1082 from prems ilcm_pos have dp: "?d >0" by simp |
1083 have d1: "\<delta> p dvd \<delta> (And p q)" using prems ilcm_dvd1 by simp |
1083 have d1: "\<delta> p dvd \<delta> (And p q)" using prems ilcm_dvd1 by simp |
1084 hence th: "d\<delta> p ?d" using delta_mono prems by auto |
1084 hence th: "d\<delta> p ?d" using delta_mono prems(3-4) by(simp del:dvd_ilcm_self1) |
1085 have "\<delta> q dvd \<delta> (And p q)" using prems ilcm_dvd2 by simp |
1085 have "\<delta> q dvd \<delta> (And p q)" using prems ilcm_dvd2 by simp |
1086 hence th': "d\<delta> q ?d" using delta_mono prems by auto |
1086 hence th': "d\<delta> q ?d" using delta_mono prems by(simp del:dvd_ilcm_self2) |
1087 from th th' dp show ?case by simp |
1087 from th th' dp show ?case by simp |
1088 next |
1088 next |
1089 case (2 p q) |
1089 case (2 p q) |
1090 let ?d = "\<delta> (And p q)" |
1090 let ?d = "\<delta> (And p q)" |
1091 from prems ilcm_pos have dp: "?d >0" by simp |
1091 from prems ilcm_pos have dp: "?d >0" by simp |
1092 have "\<delta> p dvd \<delta> (And p q)" using prems ilcm_dvd1 by simp hence th: "d\<delta> p ?d" using delta_mono prems by auto |
1092 have "\<delta> p dvd \<delta> (And p q)" using prems ilcm_dvd1 by simp |
1093 have "\<delta> q dvd \<delta> (And p q)" using prems ilcm_dvd2 by simp hence th': "d\<delta> q ?d" using delta_mono prems by auto |
1093 hence th: "d\<delta> p ?d" using delta_mono prems by(simp del:dvd_ilcm_self1) |
1094 from th th' dp show ?case by simp |
1094 have "\<delta> q dvd \<delta> (And p q)" using prems ilcm_dvd2 by simp |
|
1095 hence th': "d\<delta> q ?d" using delta_mono prems by(simp del:dvd_ilcm_self2) |
|
1096 from th th' dp show ?case by simp |
1095 qed simp_all |
1097 qed simp_all |
1096 |
1098 |
1097 |
1099 |
1098 consts |
1100 consts |
1099 a\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" (* adjusts the coeffitients of a formula *) |
1101 a\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" (* adjusts the coeffitients of a formula *) |