equal
deleted
inserted
replaced
132 in |
132 in |
133 Local_Theory.exit_global lthy'' |
133 Local_Theory.exit_global lthy'' |
134 end |
134 end |
135 *} |
135 *} |
136 |
136 |
|
137 ML {* |
|
138 fun neq_to_rel r neq = |
|
139 let |
|
140 val neq = HOLogic.dest_Trueprop (prop_of neq) |
|
141 val eq = HOLogic.dest_not neq |
|
142 val (lhs, rhs) = HOLogic.dest_eq eq |
|
143 val rel = r $ lhs $ rhs |
|
144 val nrel = HOLogic.mk_not rel |
|
145 in |
|
146 HOLogic.mk_Trueprop nrel |
|
147 end |
|
148 *} |
|
149 |
|
150 ML {* |
|
151 fun neq_to_rel_tac cases distinct = |
|
152 rtac notI THEN' eresolve_tac cases THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct) |
|
153 *} |
|
154 |
|
155 ML {* |
|
156 fun distinct_rel ctxt cases (dists, rel) = |
|
157 let |
|
158 val ((_, thms), ctxt') = Variable.import false dists ctxt |
|
159 val terms = map (neq_to_rel rel) thms |
|
160 val nrels = map (fn t => Goal.prove ctxt' [] [] t (fn _ => neq_to_rel_tac cases dists 1)) terms |
|
161 in |
|
162 Variable.export ctxt' ctxt nrels |
|
163 end |
|
164 *} |
|
165 |
|
166 |
|
167 |
137 (* Test |
168 (* Test |
138 atom_decl name |
169 atom_decl name |
139 |
170 |
140 datatype rtrm1 = |
171 datatype rtrm1 = |
141 rVr1 "name" |
172 rVr1 "name" |