85 proof - |
85 proof - |
86 have "x * 1 = x * (inverse x * x)" |
86 have "x * 1 = x * (inverse x * x)" |
87 by (simp only: group_left_inverse) |
87 by (simp only: group_left_inverse) |
88 |
88 |
89 note calculation = this |
89 note calculation = this |
90 -- \<open>first calculational step: init calculation register\<close> |
90 \<comment> \<open>first calculational step: init calculation register\<close> |
91 |
91 |
92 have "\<dots> = x * inverse x * x" |
92 have "\<dots> = x * inverse x * x" |
93 by (simp only: group_assoc) |
93 by (simp only: group_assoc) |
94 |
94 |
95 note calculation = trans [OF calculation this] |
95 note calculation = trans [OF calculation this] |
96 -- \<open>general calculational step: compose with transitivity rule\<close> |
96 \<comment> \<open>general calculational step: compose with transitivity rule\<close> |
97 |
97 |
98 have "\<dots> = 1 * x" |
98 have "\<dots> = 1 * x" |
99 by (simp only: group_right_inverse) |
99 by (simp only: group_right_inverse) |
100 |
100 |
101 note calculation = trans [OF calculation this] |
101 note calculation = trans [OF calculation this] |
102 -- \<open>general calculational step: compose with transitivity rule\<close> |
102 \<comment> \<open>general calculational step: compose with transitivity rule\<close> |
103 |
103 |
104 have "\<dots> = x" |
104 have "\<dots> = x" |
105 by (simp only: group_left_one) |
105 by (simp only: group_left_one) |
106 |
106 |
107 note calculation = trans [OF calculation this] |
107 note calculation = trans [OF calculation this] |
108 -- \<open>final calculational step: compose with transitivity rule \dots\<close> |
108 \<comment> \<open>final calculational step: compose with transitivity rule \dots\<close> |
109 from calculation |
109 from calculation |
110 -- \<open>\dots\ and pick up the final result\<close> |
110 \<comment> \<open>\dots\ and pick up the final result\<close> |
111 |
111 |
112 show ?thesis . |
112 show ?thesis . |
113 qed |
113 qed |
114 |
114 |
115 text \<open>Note that this scheme of calculations is not restricted to plain |
115 text \<open>Note that this scheme of calculations is not restricted to plain |