src/FOL/IFOL.thy
 changeset 15377 3d99eea28a9b parent 14854 61bdf2ae4dc5 child 15481 fc075ae929e4
equal inserted replaced
15376:302ef111b621 15377:3d99eea28a9b
`    80 axioms`
`    80 axioms`
`    81 `
`    81 `
`    82   (* Equality *)`
`    82   (* Equality *)`
`    83 `
`    83 `
`    84   refl:         "a=a"`
`    84   refl:         "a=a"`
`    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 `