58 val get_eqvts_raw_thms = eqvts_raw o Context.Proof; |
58 val get_eqvts_raw_thms = eqvts_raw o Context.Proof; |
59 |
59 |
60 val add_thm = EqvtData.map o Item_Net.update; |
60 val add_thm = EqvtData.map o Item_Net.update; |
61 val del_thm = EqvtData.map o Item_Net.remove; |
61 val del_thm = EqvtData.map o Item_Net.remove; |
62 |
62 |
63 fun is_equiv (Const ("==", _) $ _ $ _) = true |
|
64 | is_equiv _ = false |
|
65 |
|
66 fun add_raw_thm thm = |
63 fun add_raw_thm thm = |
67 case prop_of thm of |
64 case prop_of thm of |
68 Const ("==", _) $ _ $ _ => EqvtRawData.map (Item_Net.update thm) |
65 Const ("==", _) $ _ $ _ => EqvtRawData.map (Item_Net.update thm) |
69 | _ => raise THM ("Theorem must be a meta-equality", 0, [thm]) |
66 | _ => raise THM ("Theorem must be a meta-equality", 0, [thm]) |
70 |
67 |
71 val del_raw_thm = EqvtRawData.map o Item_Net.remove; |
68 val del_raw_thm = EqvtRawData.map o Item_Net.remove; |
72 |
|
73 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
|
74 | dest_perm t = raise TERM ("dest_perm", [t]) |
|
75 |
|
76 fun mk_perm p trm = |
|
77 let |
|
78 val ty = fastype_of trm |
|
79 in |
|
80 Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm |
|
81 end |
|
82 |
69 |
83 fun eq_transform_tac thm = REPEAT o FIRST' |
70 fun eq_transform_tac thm = REPEAT o FIRST' |
84 [CHANGED o simp_tac (HOL_basic_ss addsimps @{thms permute_minus_cancel}), |
71 [CHANGED o simp_tac (HOL_basic_ss addsimps @{thms permute_minus_cancel}), |
85 rtac (thm RS @{thm trans}), |
72 rtac (thm RS @{thm trans}), |
86 rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}] |
73 rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}] |
111 (* tests whether the lists of pis all agree, and that there is at least one p *) |
98 (* tests whether the lists of pis all agree, and that there is at least one p *) |
112 fun is_bad_list [] = true |
99 fun is_bad_list [] = true |
113 | is_bad_list [_] = false |
100 | is_bad_list [_] = false |
114 | is_bad_list (p::q::ps) = if p = q then is_bad_list (q::ps) else true |
101 | is_bad_list (p::q::ps) = if p = q then is_bad_list (q::ps) else true |
115 |
102 |
116 fun mk_minus p = |
|
117 Const (@{const_name "uminus"}, @{typ "perm => perm"}) $ p |
|
118 |
103 |
119 fun imp_transform_tac thy p p' thm = |
104 fun imp_transform_tac thy p p' thm = |
120 let |
105 let |
121 val cp = Thm.cterm_of thy p |
106 val cp = Thm.cterm_of thy p |
122 val cp' = Thm.cterm_of thy (mk_minus p') |
107 val cp' = Thm.cterm_of thy (mk_minus p') |
153 |> singleton (ProofContext.export ctxt' ctxt) |
138 |> singleton (ProofContext.export ctxt' ctxt) |
154 |> transform_eq ctxt |
139 |> transform_eq ctxt |
155 end |
140 end |
156 end |
141 end |
157 |
142 |
158 fun mk_equiv r = r RS @{thm eq_reflection}; |
|
159 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; |
|
160 |
|
161 fun transform addel_fun thm context = |
143 fun transform addel_fun thm context = |
162 let |
144 let |
163 val ctxt = Context.proof_of context |
145 val ctxt = Context.proof_of context |
164 in |
146 in |
165 case (prop_of thm) of |
147 case (prop_of thm) of |