151 (case (distinct (op =) (get_pi_aux t)) of |
151 (case (distinct (op =) (get_pi_aux t)) of |
152 [(pi,typi)] => (pi,typi) |
152 [(pi,typi)] => (pi,typi) |
153 | _ => raise EQVT_FORM "All permutation should be the same") |
153 | _ => raise EQVT_FORM "All permutation should be the same") |
154 end; |
154 end; |
155 |
155 |
156 fun tactic_eqvt_simple_form thy orig_thm = |
|
157 let val perm_pi_simp = dynamic_thms thy "perm_pi_simp" |
|
158 val _ = (warning "perm_pi_simp :";map print_thm perm_pi_simp) |
|
159 in |
|
160 tactic ("Try to prove simple eqvt form.", |
|
161 asm_full_simp_tac (HOL_basic_ss addsimps [perm_fun_def,orig_thm]@perm_pi_simp) 1) |
|
162 end |
|
163 |
|
164 fun derive_simple_statement thy oldlhs orig_thm pi typi typrm = |
|
165 let val goal_term = |
|
166 case (strip_comb oldlhs) of |
|
167 (Const (f,t),args) => |
|
168 let val lhs = Const ("Nominal.perm",Type ("fun",[typi,Type ("fun",[t,t])])) $ Var(pi,typi) $ Const (f,t) |
|
169 in Logic.unvarify (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,Const(f,t)))) end |
|
170 | _ => raise EQVT_FORM "Error deriving simple version." |
|
171 val _ = Display.print_cterm (cterm_of thy goal_term) |
|
172 in |
|
173 Goal.prove_global thy [] [] goal_term (fn _ => tactic_eqvt_simple_form thy orig_thm) |
|
174 end |
|
175 |
|
176 (* Either adds a theorem (orig_thm) to or deletes one from the equivaraince *) |
156 (* Either adds a theorem (orig_thm) to or deletes one from the equivaraince *) |
177 (* lemma list depending on flag. To be added the lemma has to satisfy a *) |
157 (* lemma list depending on flag. To be added the lemma has to satisfy a *) |
178 (* certain form. *) |
158 (* certain form. *) |
179 fun eqvt_add_del_aux flag orig_thm context = |
159 fun eqvt_add_del_aux flag orig_thm context = |
180 let |
160 let |
192 else raise EQVT_FORM "Type Implication" |
172 else raise EQVT_FORM "Type Implication" |
193 end |
173 end |
194 (* case: eqvt-lemma is of the equational form *) |
174 (* case: eqvt-lemma is of the equational form *) |
195 | (Const ("Trueprop", _) $ (Const ("op =", _) $ |
175 | (Const ("Trueprop", _) $ (Const ("op =", _) $ |
196 (Const ("Nominal.perm",typrm) $ Var (pi,typi) $ lhs) $ rhs)) => |
176 (Const ("Nominal.perm",typrm) $ Var (pi,typi) $ lhs) $ rhs)) => |
197 let val optth = ([derive_simple_statement thy lhs orig_thm pi typi typrm] |
|
198 handle (ERROR s) => (warning ("Couldn't prove the simple version:\n"^s);[]) |
|
199 | _ => (warning "Couldn't prove the simple version";[]) |
|
200 ) |
|
201 in |
|
202 (if (apply_pi lhs (pi,typi)) = rhs |
177 (if (apply_pi lhs (pi,typi)) = rhs |
203 then orig_thm::optth |
178 then [orig_thm] |
204 else raise EQVT_FORM "Type Equality") |
179 else raise EQVT_FORM "Type Equality") |
205 end |
|
206 | _ => raise EQVT_FORM "Type unknown") |
180 | _ => raise EQVT_FORM "Type unknown") |
207 in |
181 in |
208 update_context flag thms_to_be_added context |
182 update_context flag thms_to_be_added context |
209 end |
183 end |
210 handle EQVT_FORM s => |
184 handle EQVT_FORM s => |