equal
deleted
inserted
replaced
71 qed |
71 qed |
72 |
72 |
73 lemma imp_conjunction [unfolded prop_def]: |
73 lemma imp_conjunction [unfolded prop_def]: |
74 includes meta_conjunction_syntax |
74 includes meta_conjunction_syntax |
75 shows "(PROP A ==> PROP prop (PROP B && PROP C)) == (PROP A ==> PROP B) && (PROP A ==> PROP C)" |
75 shows "(PROP A ==> PROP prop (PROP B && PROP C)) == (PROP A ==> PROP B) && (PROP A ==> PROP C)" |
76 proof (unfold prop_def, rule) |
76 unfolding prop_def |
|
77 proof |
77 assume conj: "PROP A ==> PROP B && PROP C" |
78 assume conj: "PROP A ==> PROP B && PROP C" |
78 fix X assume r: "(PROP A ==> PROP B) ==> (PROP A ==> PROP C) ==> PROP X" |
79 fix X assume r: "(PROP A ==> PROP B) ==> (PROP A ==> PROP C) ==> PROP X" |
79 show "PROP X" |
80 show "PROP X" |
80 proof (rule r) |
81 proof (rule r) |
81 assume "PROP A" |
82 assume "PROP A" |
119 qed |
120 qed |
120 |
121 |
121 lemma conjunction_assoc: |
122 lemma conjunction_assoc: |
122 includes meta_conjunction_syntax |
123 includes meta_conjunction_syntax |
123 shows "((PROP A && PROP B) && PROP C) == (PROP A && (PROP B && PROP C))" |
124 shows "((PROP A && PROP B) && PROP C) == (PROP A && (PROP B && PROP C))" |
124 by (rule equal_intr_rule) (unfold imp_conjunction conjunction_imp) |
125 unfolding conjunction_imp . |
125 |
126 |
126 end |
127 end |