43 structure Nominal_ThmDecls: NOMINAL_THMDECLS = |
43 structure Nominal_ThmDecls: NOMINAL_THMDECLS = |
44 struct |
44 struct |
45 |
45 |
46 fun get_ps trm = |
46 fun get_ps trm = |
47 case trm of |
47 case trm of |
48 Const (@{const_name permute}, _) $ p $ (Bound _) => raise TERM ("get_ps", [trm]) |
48 Const (@{const_name permute}, _) $ p $ (Bound _) => |
|
49 raise TERM ("get_ps called on bound", [trm]) |
49 | Const (@{const_name permute}, _) $ p $ _ => [p] |
50 | Const (@{const_name permute}, _) $ p $ _ => [p] |
50 | t $ u => get_ps t @ get_ps u |
51 | t $ u => get_ps t @ get_ps u |
51 | Abs (_, _, t) => get_ps t |
52 | Abs (_, _, t) => get_ps t |
52 | _ => [] |
53 | _ => [] |
53 |
54 |
57 | Const _ => trm |
58 | Const _ => trm |
58 | t $ u => put_p p t $ put_p p u |
59 | t $ u => put_p p t $ put_p p u |
59 | Abs (x, ty, t) => Abs (x, ty, put_p p t) |
60 | Abs (x, ty, t) => Abs (x, ty, put_p p t) |
60 | _ => mk_perm p trm |
61 | _ => mk_perm p trm |
61 |
62 |
62 (* tests whether the lists of ps all agree, and that there is at least one p *) |
63 (* tests whether there is a disagreement between the permutations, |
|
64 and that there is at least one permutation *) |
63 fun is_bad_list [] = true |
65 fun is_bad_list [] = true |
64 | is_bad_list [_] = false |
66 | is_bad_list [_] = false |
65 | is_bad_list (p::q::ps) = if p = q then is_bad_list (q::ps) else true |
67 | is_bad_list (p::q::ps) = if p = q then is_bad_list (q::ps) else true |
66 |
68 |
67 |
69 |
86 val add_thm = EqvtData.map o Item_Net.update; |
88 val add_thm = EqvtData.map o Item_Net.update; |
87 val del_thm = EqvtData.map o Item_Net.remove; |
89 val del_thm = EqvtData.map o Item_Net.remove; |
88 |
90 |
89 fun add_raw_thm thm = |
91 fun add_raw_thm thm = |
90 case prop_of thm of |
92 case prop_of thm of |
91 Const ("==", _) $ _ $ _ => |
93 Const ("==", _) $ _ $ _ => (EqvtRawData.map o Item_Net.update) thm |
92 EqvtRawData.map (Item_Net.update (zero_var_indexes thm)) |
|
93 | _ => raise THM ("Theorem must be a meta-equality", 0, [thm]) |
94 | _ => raise THM ("Theorem must be a meta-equality", 0, [thm]) |
94 |
95 |
95 val del_raw_thm = EqvtRawData.map o Item_Net.remove; |
96 val del_raw_thm = EqvtRawData.map o Item_Net.remove; |
96 |
97 |
97 |
98 |
98 (** transformation of eqvt lemmas **) |
99 (** transformation of eqvt lemmas **) |
99 |
100 |
100 |
101 |
101 (* transforms equations into the "p o c = c"-form |
102 (* transforms equations into the "p o c == c"-form |
102 from p o (c x1 ...xn) = c (p o x1) ... (p o xn) *) |
103 from p o (c x1 ...xn) = c (p o x1) ... (p o xn) *) |
103 |
104 |
104 fun eqvt_transform_eq_tac thm = |
105 fun eqvt_transform_eq_tac thm = |
105 let |
106 let |
106 val ss_thms = @{thms permute_minus_cancel permute_prod.simps split_paired_all} |
107 val ss_thms = @{thms permute_minus_cancel permute_prod.simps split_paired_all} |
111 rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}] |
112 rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}] |
112 end |
113 end |
113 |
114 |
114 fun eqvt_transform_eq ctxt thm = |
115 fun eqvt_transform_eq ctxt thm = |
115 let |
116 let |
116 val ((p, t), rhs) = apfst dest_perm |
117 val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm)) |
117 (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))) |
118 handle TERM _ => error "Equivariance lemma must be an equality." |
118 handle TERM _ => error "Eqvt lemma is not of the form p \<bullet> c... = c..." |
119 val (p, t) = dest_perm lhs |
|
120 handle TERM _ => error "Equivariance lemma is not of the form p \<bullet> c... = c..." |
|
121 |
119 val ps = get_ps rhs handle TERM _ => [] |
122 val ps = get_ps rhs handle TERM _ => [] |
120 val (c, c') = (head_of t, head_of rhs) |
123 val (c, c') = (head_of t, head_of rhs) |
|
124 val msg = "Equivariance lemma is not of the right form " |
121 in |
125 in |
122 if c <> c' |
126 if c <> c' |
123 then error "Eqvt lemma is not of the right form (constants do not agree)" |
127 then error (msg ^ "(constants do not agree).") |
124 else if is_bad_list (p::ps) |
128 else if is_bad_list (p::ps) |
125 then error "Eqvt lemma is not of the right form (permutations do not agree)" |
129 then error (msg ^ "(permutations do not agree).") |
126 else if not (rhs aconv (put_p p t)) |
130 else if not (rhs aconv (put_p p t)) |
127 then error "Eqvt lemma is not of the right form (arguments do not agree)" |
131 then error (msg ^ "(arguments do not agree).") |
128 else if is_Const t |
132 else if is_Const t |
129 then safe_mk_equiv thm |
133 then safe_mk_equiv thm |
130 else |
134 else |
131 let |
135 let |
132 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c)) |
136 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c)) |
133 val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt |
137 val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt |
134 in |
138 in |
135 Goal.prove ctxt [] [] goal' (fn _ => eqvt_transform_eq_tac thm 1) |
139 Goal.prove ctxt [] [] goal' (fn _ => eqvt_transform_eq_tac thm 1) |
136 |> singleton (ProofContext.export ctxt' ctxt) |
140 |> singleton (ProofContext.export ctxt' ctxt) |
137 |> safe_mk_equiv |
141 |> safe_mk_equiv |
|
142 |> zero_var_indexes |
138 end |
143 end |
139 end |
144 end |
140 |
145 |
141 (* transforms equations into the "p o c = c"-form |
146 (* transforms equations into the "p o c == c"-form |
142 from R x1 ...xn ==> R (p o x1) ... (p o xn) *) |
147 from R x1 ...xn ==> R (p o x1) ... (p o xn) *) |
143 |
148 |
144 fun eqvt_transform_imp_tac thy p p' thm = |
149 fun eqvt_transform_imp_tac ctxt p p' thm = |
145 let |
150 let |
|
151 val thy = ProofContext.theory_of ctxt |
146 val cp = Thm.cterm_of thy p |
152 val cp = Thm.cterm_of thy p |
147 val cp' = Thm.cterm_of thy (mk_minus p') |
153 val cp' = Thm.cterm_of thy (mk_minus p') |
148 val thm' = Drule.cterm_instantiate [(cp, cp')] thm |
154 val thm' = Drule.cterm_instantiate [(cp, cp')] thm |
149 val simp = HOL_basic_ss addsimps @{thms permute_minus_cancel(2)} |
155 val simp = HOL_basic_ss addsimps @{thms permute_minus_cancel(2)} |
150 in |
156 in |
152 rtac @{thm permute_boolI}, dtac thm', full_simp_tac simp] |
158 rtac @{thm permute_boolI}, dtac thm', full_simp_tac simp] |
153 end |
159 end |
154 |
160 |
155 fun eqvt_transform_imp ctxt thm = |
161 fun eqvt_transform_imp ctxt thm = |
156 let |
162 let |
157 val thy = ProofContext.theory_of ctxt |
|
158 val (prem, concl) = pairself HOLogic.dest_Trueprop (Logic.dest_implies (prop_of thm)) |
163 val (prem, concl) = pairself HOLogic.dest_Trueprop (Logic.dest_implies (prop_of thm)) |
159 val (c, c') = (head_of prem, head_of concl) |
164 val (c, c') = (head_of prem, head_of concl) |
160 val ps = get_ps concl handle TERM _ => [] |
165 val ps = get_ps concl handle TERM _ => [] |
161 val p = try hd ps |
166 val p = try hd ps |
|
167 val msg = "Equivariance lemma is not of the right form " |
162 in |
168 in |
163 if c <> c' |
169 if c <> c' |
164 then error "Eqvt lemma is not of the right form (constants do not agree)" |
170 then error (msg ^ "(constants do not agree).") |
165 else if is_bad_list ps |
171 else if is_bad_list ps |
166 then error "Eqvt lemma is not of the right form (permutations do not agree)" |
172 then error (msg ^ "(permutations do not agree).") |
167 else if not (concl aconv (put_p (the p) prem)) |
173 else if not (concl aconv (put_p (the p) prem)) |
168 then error "Eqvt lemma is not of the right form (arguments do not agree)" |
174 then error (msg ^ "(arguments do not agree).") |
169 else |
175 else |
170 let |
176 let |
171 val prem' = mk_perm (the p) prem |
177 val prem' = mk_perm (the p) prem |
172 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (prem', concl)) |
178 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (prem', concl)) |
173 val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt |
179 val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt |
174 in |
180 in |
175 Goal.prove ctxt' [] [] goal' |
181 Goal.prove ctxt' [] [] goal' |
176 (fn _ => eqvt_transform_imp_tac thy (the p) p' thm 1) |
182 (fn _ => eqvt_transform_imp_tac ctxt' (the p) p' thm 1) |
177 |> singleton (ProofContext.export ctxt' ctxt) |
183 |> singleton (ProofContext.export ctxt' ctxt) |
178 |> eqvt_transform_eq ctxt |
184 |> eqvt_transform_eq ctxt |
179 end |
185 end |
180 end |
186 end |
181 |
187 |