32 val eqvt_raw_del: attribute |
32 val eqvt_raw_del: attribute |
33 val setup: theory -> theory |
33 val setup: theory -> theory |
34 val get_eqvts_thms: Proof.context -> thm list |
34 val get_eqvts_thms: Proof.context -> thm list |
35 val get_eqvts_raw_thms: Proof.context -> thm list |
35 val get_eqvts_raw_thms: Proof.context -> thm list |
36 val eqvt_transform: Proof.context -> thm -> thm |
36 val eqvt_transform: Proof.context -> thm -> thm |
|
37 val is_eqvt: Proof.context -> term -> bool |
37 |
38 |
38 (* TEMPORARY FIX *) |
39 (* TEMPORARY FIX *) |
39 val add_thm: thm -> Context.generic -> Context.generic |
40 val add_thm: thm -> Context.generic -> Context.generic |
40 val add_raw_thm: thm -> Context.generic -> Context.generic |
41 val add_raw_thm: thm -> Context.generic -> Context.generic |
41 end; |
42 end; |
42 |
43 |
43 structure Nominal_ThmDecls: NOMINAL_THMDECLS = |
44 structure Nominal_ThmDecls: NOMINAL_THMDECLS = |
44 struct |
45 struct |
45 |
46 |
46 fun get_ps trm = |
47 structure EqvtData = Generic_Data |
|
48 ( type T = thm Item_Net.T; |
|
49 val empty = Thm.full_rules; |
|
50 val extend = I; |
|
51 val merge = Item_Net.merge); |
|
52 |
|
53 structure EqvtRawData = Generic_Data |
|
54 ( type T = thm Symtab.table; |
|
55 val empty = Symtab.empty; |
|
56 val extend = I; |
|
57 val merge = Symtab.merge (K true)); |
|
58 |
|
59 val eqvts = Item_Net.content o EqvtData.get; |
|
60 val eqvts_raw = map snd o Symtab.dest o EqvtRawData.get; |
|
61 |
|
62 val get_eqvts_thms = eqvts o Context.Proof; |
|
63 val get_eqvts_raw_thms = eqvts_raw o Context.Proof; |
|
64 |
|
65 val add_thm = EqvtData.map o Item_Net.update; |
|
66 val del_thm = EqvtData.map o Item_Net.remove; |
|
67 |
|
68 fun add_raw_thm thm = |
|
69 case prop_of thm of |
|
70 Const ("==", _) $ _ $ Const (c, _) => EqvtRawData.map (Symtab.update (c, thm)) |
|
71 | _ => raise THM ("Theorem must be a meta-equality where the right-hand side is a constant.", 0, [thm]) |
|
72 |
|
73 fun del_raw_thm thm = |
|
74 case prop_of thm of |
|
75 Const ("==", _) $ _ $ Const (c, _) => EqvtRawData.map (Symtab.delete c) |
|
76 | _ => raise THM ("Theorem must be a meta-equality where the right-hand side is a constant.", 0, [thm]) |
|
77 |
|
78 fun is_eqvt ctxt trm = |
47 case trm of |
79 case trm of |
48 Const (@{const_name permute}, _) $ p $ (Bound _) => |
80 Const (c, _) => Symtab.defined (EqvtRawData.get (Context.Proof ctxt)) c |
49 raise TERM ("get_ps called on bound", [trm]) |
81 | _ => raise TERM ("Term must be a constsnt.", [trm]) |
|
82 |
|
83 |
|
84 |
|
85 (** transformation of eqvt lemmas **) |
|
86 |
|
87 fun get_perms trm = |
|
88 case trm of |
|
89 Const (@{const_name permute}, _) $ _ $ (Bound _) => |
|
90 raise TERM ("get_perms called on bound", [trm]) |
50 | Const (@{const_name permute}, _) $ p $ _ => [p] |
91 | Const (@{const_name permute}, _) $ p $ _ => [p] |
51 | t $ u => get_ps t @ get_ps u |
92 | t $ u => get_perms t @ get_perms u |
52 | Abs (_, _, t) => get_ps t |
93 | Abs (_, _, t) => get_perms t |
53 | _ => [] |
94 | _ => [] |
54 |
95 |
55 fun put_p p trm = |
96 fun put_perm p trm = |
56 case trm of |
97 case trm of |
57 Bound _ => trm |
98 Bound _ => trm |
58 | Const _ => trm |
99 | Const _ => trm |
59 | t $ u => put_p p t $ put_p p u |
100 | t $ u => put_perm p t $ put_perm p u |
60 | Abs (x, ty, t) => Abs (x, ty, put_p p t) |
101 | Abs (x, ty, t) => Abs (x, ty, put_perm p t) |
61 | _ => mk_perm p trm |
102 | _ => mk_perm p trm |
62 |
103 |
63 (* tests whether there is a disagreement between the permutations, |
104 (* tests whether there is a disagreement between the permutations, |
64 and that there is at least one permutation *) |
105 and that there is at least one permutation *) |
65 fun is_bad_list [] = true |
106 fun is_bad_list [] = true |
66 | is_bad_list [_] = false |
107 | is_bad_list [_] = false |
67 | is_bad_list (p::q::ps) = if p = q then is_bad_list (q::ps) else true |
108 | is_bad_list (p::q::ps) = if p = q then is_bad_list (q::ps) else true |
68 |
109 |
69 |
110 |
70 structure EqvtData = Generic_Data |
|
71 ( type T = thm Item_Net.T; |
|
72 val empty = Thm.full_rules; |
|
73 val extend = I; |
|
74 val merge = Item_Net.merge ); |
|
75 |
|
76 structure EqvtRawData = Generic_Data |
|
77 ( type T = thm Item_Net.T; |
|
78 val empty = Thm.full_rules; |
|
79 val extend = I; |
|
80 val merge = Item_Net.merge ); |
|
81 |
|
82 val eqvts = Item_Net.content o EqvtData.get; |
|
83 val eqvts_raw = Item_Net.content o EqvtRawData.get; |
|
84 |
|
85 val get_eqvts_thms = eqvts o Context.Proof; |
|
86 val get_eqvts_raw_thms = eqvts_raw o Context.Proof; |
|
87 |
|
88 val add_thm = EqvtData.map o Item_Net.update; |
|
89 val del_thm = EqvtData.map o Item_Net.remove; |
|
90 |
|
91 fun add_raw_thm thm = |
|
92 case prop_of thm of |
|
93 Const ("==", _) $ _ $ _ => (EqvtRawData.map o Item_Net.update) thm |
|
94 | _ => raise THM ("Theorem must be a meta-equality", 0, [thm]) |
|
95 |
|
96 val del_raw_thm = EqvtRawData.map o Item_Net.remove; |
|
97 |
|
98 |
|
99 (** transformation of eqvt lemmas **) |
|
100 |
|
101 |
|
102 (* transforms equations into the "p o c == c"-form |
111 (* transforms equations into the "p o c == c"-form |
103 from p o (c x1 ...xn) = c (p o x1) ... (p o xn) *) |
112 from p o (c x1 ...xn) = c (p o x1) ... (p o xn) *) |
104 |
113 |
105 fun eqvt_transform_eq_tac thm = |
114 fun eqvt_transform_eq_tac thm = |
106 let |
115 let |
117 val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm)) |
126 val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm)) |
118 handle TERM _ => error "Equivariance lemma must be an equality." |
127 handle TERM _ => error "Equivariance lemma must be an equality." |
119 val (p, t) = dest_perm lhs |
128 val (p, t) = dest_perm lhs |
120 handle TERM _ => error "Equivariance lemma is not of the form p \<bullet> c... = c..." |
129 handle TERM _ => error "Equivariance lemma is not of the form p \<bullet> c... = c..." |
121 |
130 |
122 val ps = get_ps rhs handle TERM _ => [] |
131 val ps = get_perms rhs handle TERM _ => [] |
123 val (c, c') = (head_of t, head_of rhs) |
132 val (c, c') = (head_of t, head_of rhs) |
124 val msg = "Equivariance lemma is not of the right form " |
133 val msg = "Equivariance lemma is not of the right form " |
125 in |
134 in |
126 if c <> c' |
135 if c <> c' |
127 then error (msg ^ "(constants do not agree).") |
136 then error (msg ^ "(constants do not agree).") |
128 else if is_bad_list (p::ps) |
137 else if is_bad_list (p :: ps) |
129 then error (msg ^ "(permutations do not agree).") |
138 then error (msg ^ "(permutations do not agree).") |
130 else if not (rhs aconv (put_p p t)) |
139 else if not (rhs aconv (put_perm p t)) |
131 then error (msg ^ "(arguments do not agree).") |
140 then error (msg ^ "(arguments do not agree).") |
132 else if is_Const t |
141 else if is_Const t |
133 then safe_mk_equiv thm |
142 then safe_mk_equiv thm |
134 else |
143 else |
135 let |
144 let |
160 |
169 |
161 fun eqvt_transform_imp ctxt thm = |
170 fun eqvt_transform_imp ctxt thm = |
162 let |
171 let |
163 val (prem, concl) = pairself HOLogic.dest_Trueprop (Logic.dest_implies (prop_of thm)) |
172 val (prem, concl) = pairself HOLogic.dest_Trueprop (Logic.dest_implies (prop_of thm)) |
164 val (c, c') = (head_of prem, head_of concl) |
173 val (c, c') = (head_of prem, head_of concl) |
165 val ps = get_ps concl handle TERM _ => [] |
174 val ps = get_perms concl handle TERM _ => [] |
166 val p = try hd ps |
175 val p = try hd ps |
167 val msg = "Equivariance lemma is not of the right form " |
176 val msg = "Equivariance lemma is not of the right form " |
168 in |
177 in |
169 if c <> c' |
178 if c <> c' |
170 then error (msg ^ "(constants do not agree).") |
179 then error (msg ^ "(constants do not agree).") |
171 else if is_bad_list ps |
180 else if is_bad_list ps |
172 then error (msg ^ "(permutations do not agree).") |
181 then error (msg ^ "(permutations do not agree).") |
173 else if not (concl aconv (put_p (the p) prem)) |
182 else if not (concl aconv (put_perm (the p) prem)) |
174 then error (msg ^ "(arguments do not agree).") |
183 then error (msg ^ "(arguments do not agree).") |
175 else |
184 else |
176 let |
185 let |
177 val prem' = mk_perm (the p) prem |
186 val prem' = mk_perm (the p) prem |
178 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (prem', concl)) |
187 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (prem', concl)) |
179 val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt |
188 val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt |
180 in |
189 in |
181 Goal.prove ctxt' [] [] goal' |
190 Goal.prove ctxt' [] [] goal' |
182 (fn _ => eqvt_transform_imp_tac ctxt' (the p) p' thm 1) |
191 (fn _ => eqvt_transform_imp_tac ctxt' (the p) p' thm 1) |
183 |> singleton (ProofContext.export ctxt' ctxt) |
192 |> singleton (ProofContext.export ctxt' ctxt) |
184 |> eqvt_transform_eq ctxt |
|
185 end |
193 end |
186 end |
194 end |
187 |
195 |
188 fun eqvt_transform ctxt thm = |
196 fun eqvt_transform ctxt thm = |
189 case (prop_of thm) of |
197 case (prop_of thm) of |
190 @{const "Trueprop"} $ (Const (@{const_name "op ="}, _) $ |
198 @{const "Trueprop"} $ (Const (@{const_name "op ="}, _) $ |
191 (Const (@{const_name "permute"}, _) $ _ $ _) $ _) => |
199 (Const (@{const_name "permute"}, _) $ _ $ _) $ _) => |
192 eqvt_transform_eq ctxt thm |
200 eqvt_transform_eq ctxt thm |
193 | @{const "==>"} $ (@{const "Trueprop"} $ _) $ (@{const "Trueprop"} $ _) => |
201 | @{const "==>"} $ (@{const "Trueprop"} $ _) $ (@{const "Trueprop"} $ _) => |
194 eqvt_transform_imp ctxt thm |
202 eqvt_transform_imp ctxt thm |> eqvt_transform_eq ctxt |
195 | _ => raise error "Only _ = _ and _ ==> _ cases are implemented." |
203 | _ => raise error "Only _ = _ and _ ==> _ cases are implemented." |
196 |
204 |
197 |
205 |
198 (** attributes **) |
206 (** attributes **) |
199 |
207 |