equal
deleted
inserted
replaced
105 |
105 |
106 end |
106 end |
107 |
107 |
108 thm add_assoc |
108 thm add_assoc |
109 |
109 |
110 lemma plus_raw_rsp[quotient_rsp]: |
110 lemma plus_raw_rsp[quot_respect]: |
111 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw" |
111 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw" |
112 by auto |
112 by auto |
113 |
113 |
114 lemma minus_raw_rsp[quotient_rsp]: |
114 lemma minus_raw_rsp[quot_respect]: |
115 shows "(op \<approx> ===> op \<approx>) minus_raw minus_raw" |
115 shows "(op \<approx> ===> op \<approx>) minus_raw minus_raw" |
116 by auto |
116 by auto |
117 |
117 |
118 lemma mult_raw_rsp[quotient_rsp]: |
118 lemma mult_raw_rsp[quot_respect]: |
119 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw" |
119 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw" |
120 apply(auto) |
120 apply(auto) |
121 apply(simp add: algebra_simps) |
121 apply(simp add: algebra_simps) |
122 sorry |
122 sorry |
123 |
123 |
124 lemma le_raw_rsp[quotient_rsp]: |
124 lemma le_raw_rsp[quot_respect]: |
125 shows "(op \<approx> ===> op \<approx> ===> op =) le_raw le_raw" |
125 shows "(op \<approx> ===> op \<approx> ===> op =) le_raw le_raw" |
126 by auto |
126 by auto |
127 |
127 |
128 lemma plus_assoc_raw: |
128 lemma plus_assoc_raw: |
129 shows "plus_raw (plus_raw i j) k \<approx> plus_raw i (plus_raw j k)" |
129 shows "plus_raw (plus_raw i j) k \<approx> plus_raw i (plus_raw j k)" |