equal
deleted
inserted
replaced
18 |
18 |
19 judgment |
19 judgment |
20 Trueprop :: "o \<Rightarrow> prop" ("_" 5) |
20 Trueprop :: "o \<Rightarrow> prop" ("_" 5) |
21 |
21 |
22 text {* |
22 text {* |
23 \noindent Note that the object-logic judgement is implicit in the |
23 \noindent Note that the object-logic judgment is implicit in the |
24 syntax: writing @{prop A} produces @{term "Trueprop A"} internally. |
24 syntax: writing @{prop A} produces @{term "Trueprop A"} internally. |
25 From the Pure perspective this means ``@{prop A} is derivable in the |
25 From the Pure perspective this means ``@{prop A} is derivable in the |
26 object-logic''. |
26 object-logic''. |
27 *} |
27 *} |
28 |
28 |
143 |
143 |
144 (*<*) |
144 (*<*) |
145 theorem "\<And>A. PROP A \<Longrightarrow> PROP A" |
145 theorem "\<And>A. PROP A \<Longrightarrow> PROP A" |
146 proof - |
146 proof - |
147 assume [symmetric, defn]: "\<And>x y. (x \<equiv> y) \<equiv> Trueprop (x = y)" |
147 assume [symmetric, defn]: "\<And>x y. (x \<equiv> y) \<equiv> Trueprop (x = y)" |
|
148 fix x |
148 (*>*) |
149 (*>*) |
149 have "x \<circ> 1 = x \<circ> (x\<inverse> \<circ> x)" unfolding left_inv .. |
150 have "x \<circ> 1 = x \<circ> (x\<inverse> \<circ> x)" unfolding left_inv .. |
150 also have "\<dots> = (x \<circ> x\<inverse>) \<circ> x" unfolding assoc .. |
151 also have "\<dots> = (x \<circ> x\<inverse>) \<circ> x" unfolding assoc .. |
151 also have "\<dots> = 1 \<circ> x" unfolding right_inv .. |
152 also have "\<dots> = 1 \<circ> x" unfolding right_inv .. |
152 also have "\<dots> = x" unfolding left_unit .. |
153 also have "\<dots> = x" unfolding left_unit .. |