equal
deleted
inserted
replaced
72 | _ => raise THM ("Theorem must be a meta-equality where the right-hand side is a constant.", 0, [thm]) |
72 | _ => raise THM ("Theorem must be a meta-equality where the right-hand side is a constant.", 0, [thm]) |
73 |
73 |
74 fun is_eqvt ctxt trm = |
74 fun is_eqvt ctxt trm = |
75 case trm of |
75 case trm of |
76 (c as Const _) => Termtab.defined (EqvtRawData.get (Context.Proof ctxt)) c |
76 (c as Const _) => Termtab.defined (EqvtRawData.get (Context.Proof ctxt)) c |
77 | _ => raise TERM ("Term must be a constsnt.", [trm]) |
77 | _ => false (* raise TERM ("Term must be a constant.", [trm]) *) |
78 |
78 |
79 |
79 |
80 |
80 |
81 (** transformation of eqvt lemmas **) |
81 (** transformation of eqvt lemmas **) |
82 |
82 |
87 | Const (@{const_name permute}, _) $ p $ _ => [p] |
87 | Const (@{const_name permute}, _) $ p $ _ => [p] |
88 | t $ u => get_perms t @ get_perms u |
88 | t $ u => get_perms t @ get_perms u |
89 | Abs (_, _, t) => get_perms t |
89 | Abs (_, _, t) => get_perms t |
90 | _ => [] |
90 | _ => [] |
91 |
91 |
92 fun put_perm p trm = |
92 fun add_perm p trm = |
93 case trm of |
93 let |
94 Bound _ => trm |
94 fun aux trm = |
95 | Const _ => trm |
95 case trm of |
96 | t $ u => put_perm p t $ put_perm p u |
96 Bound _ => trm |
97 | Abs (x, ty, t) => Abs (x, ty, put_perm p t) |
97 | Const _ => trm |
98 | _ => mk_perm p trm |
98 | t $ u => aux t $ aux u |
|
99 | Abs (x, ty, t) => Abs (x, ty, aux t) |
|
100 | _ => mk_perm p trm |
|
101 in |
|
102 strip_comb trm |
|
103 ||> map aux |
|
104 |> list_comb |
|
105 end |
|
106 |
99 |
107 |
100 (* tests whether there is a disagreement between the permutations, |
108 (* tests whether there is a disagreement between the permutations, |
101 and that there is at least one permutation *) |
109 and that there is at least one permutation *) |
102 fun is_bad_list [] = true |
110 fun is_bad_list [] = true |
103 | is_bad_list [_] = false |
111 | is_bad_list [_] = false |
130 in |
138 in |
131 if c <> c' |
139 if c <> c' |
132 then error (msg ^ "(constants do not agree).") |
140 then error (msg ^ "(constants do not agree).") |
133 else if is_bad_list (p :: ps) |
141 else if is_bad_list (p :: ps) |
134 then error (msg ^ "(permutations do not agree).") |
142 then error (msg ^ "(permutations do not agree).") |
135 else if not (rhs aconv (put_perm p t)) |
143 else if not (rhs aconv (add_perm p t)) |
136 then error (msg ^ "(arguments do not agree).") |
144 then error (msg ^ "(arguments do not agree).") |
137 else if is_Const t |
145 else if is_Const t |
138 then safe_mk_equiv thm |
146 then safe_mk_equiv thm |
139 else |
147 else |
140 let |
148 let |
173 in |
181 in |
174 if c <> c' |
182 if c <> c' |
175 then error (msg ^ "(constants do not agree).") |
183 then error (msg ^ "(constants do not agree).") |
176 else if is_bad_list ps |
184 else if is_bad_list ps |
177 then error (msg ^ "(permutations do not agree).") |
185 then error (msg ^ "(permutations do not agree).") |
178 else if not (concl aconv (put_perm (the p) prem)) |
186 else if not (concl aconv (add_perm (the p) prem)) |
179 then error (msg ^ "(arguments do not agree).") |
187 then error (msg ^ "(arguments do not agree).") |
180 else |
188 else |
181 let |
189 let |
182 val prem' = mk_perm (the p) prem |
190 val prem' = mk_perm (the p) prem |
183 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (prem', concl)) |
191 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (prem', concl)) |