equal
deleted
inserted
replaced
80 axioms |
80 axioms |
81 |
81 |
82 (* Equality *) |
82 (* Equality *) |
83 |
83 |
84 refl: "a=a" |
84 refl: "a=a" |
85 subst: "[| a=b; P(a) |] ==> P(b)" |
|
86 |
85 |
87 (* Propositional logic *) |
86 (* Propositional logic *) |
88 |
87 |
89 conjI: "[| P; Q |] ==> P&Q" |
88 conjI: "[| P; Q |] ==> P&Q" |
90 conjunct1: "P&Q ==> P" |
89 conjunct1: "P&Q ==> P" |
109 |
108 |
110 (* Reflection *) |
109 (* Reflection *) |
111 |
110 |
112 eq_reflection: "(x=y) ==> (x==y)" |
111 eq_reflection: "(x=y) ==> (x==y)" |
113 iff_reflection: "(P<->Q) ==> (P==Q)" |
112 iff_reflection: "(P<->Q) ==> (P==Q)" |
|
113 |
|
114 |
|
115 text{*Thanks to Stephan Merz*} |
|
116 theorem subst: |
|
117 assumes eq: "a = b" and p: "P(a)" |
|
118 shows "P(b)" |
|
119 proof - |
|
120 from eq have meta: "a \<equiv> b" |
|
121 by (rule eq_reflection) |
|
122 from p show ?thesis |
|
123 by (unfold meta) |
|
124 qed |
114 |
125 |
115 |
126 |
116 defs |
127 defs |
117 (* Definitions *) |
128 (* Definitions *) |
118 |
129 |