equal
deleted
inserted
replaced
68 Const ("==", _) $ _ $ _ => EqvtRawData.map (Item_Net.update thm) |
68 Const ("==", _) $ _ $ _ => EqvtRawData.map (Item_Net.update thm) |
69 | _ => raise THM ("Theorem must be a meta-equality", 0, [thm]) |
69 | _ => raise THM ("Theorem must be a meta-equality", 0, [thm]) |
70 |
70 |
71 val del_raw_thm = EqvtRawData.map o Item_Net.remove; |
71 val del_raw_thm = EqvtRawData.map o Item_Net.remove; |
72 |
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 |
|
83 fun eq_transform_tac thm = REPEAT o FIRST' |
73 fun eq_transform_tac thm = REPEAT o FIRST' |
84 [CHANGED o simp_tac (HOL_basic_ss addsimps @{thms permute_minus_cancel}), |
74 [CHANGED o simp_tac (HOL_basic_ss addsimps @{thms permute_minus_cancel}), |
85 rtac (thm RS @{thm trans}), |
75 rtac (thm RS @{thm trans}), |
86 rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}] |
76 rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}] |
87 |
77 |
111 (* tests whether the lists of pis all agree, and that there is at least one p *) |
101 (* tests whether the lists of pis all agree, and that there is at least one p *) |
112 fun is_bad_list [] = true |
102 fun is_bad_list [] = true |
113 | is_bad_list [_] = false |
103 | is_bad_list [_] = false |
114 | is_bad_list (p::q::ps) = if p = q then is_bad_list (q::ps) else true |
104 | is_bad_list (p::q::ps) = if p = q then is_bad_list (q::ps) else true |
115 |
105 |
116 fun mk_minus p = |
|
117 Const (@{const_name "uminus"}, @{typ "perm => perm"}) $ p |
|
118 |
106 |
119 fun imp_transform_tac thy p p' thm = |
107 fun imp_transform_tac thy p p' thm = |
120 let |
108 let |
121 val cp = Thm.cterm_of thy p |
109 val cp = Thm.cterm_of thy p |
122 val cp' = Thm.cterm_of thy (mk_minus p') |
110 val cp' = Thm.cterm_of thy (mk_minus p') |
153 |> singleton (ProofContext.export ctxt' ctxt) |
141 |> singleton (ProofContext.export ctxt' ctxt) |
154 |> transform_eq ctxt |
142 |> transform_eq ctxt |
155 end |
143 end |
156 end |
144 end |
157 |
145 |
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 = |
146 fun transform addel_fun thm context = |
162 let |
147 let |
163 val ctxt = Context.proof_of context |
148 val ctxt = Context.proof_of context |
164 in |
149 in |
165 case (prop_of thm) of |
150 case (prop_of thm) of |