equal
deleted
inserted
replaced
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 val add_raw_thm = EqvtRawData.map o Item_Net.update; |
63 fun is_equiv (Const ("==", _) $ _ $ _) = true |
|
64 | is_equiv _ = false |
|
65 |
|
66 fun add_raw_thm thm = |
|
67 let |
|
68 val trm = prop_of thm |
|
69 val _ = if is_equiv trm then () |
|
70 else raise THM ("Theorem must be a meta-equality", 0, [thm]) |
|
71 in |
|
72 (EqvtRawData.map o Item_Net.update) thm |
|
73 end |
|
74 |
64 val del_raw_thm = EqvtRawData.map o Item_Net.remove; |
75 val del_raw_thm = EqvtRawData.map o Item_Net.remove; |
65 |
76 |
66 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
77 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
67 | dest_perm t = raise TERM("dest_perm", [t]) |
78 | dest_perm t = raise TERM("dest_perm", [t]) |
68 |
79 |
76 fun eqvt_transform_tac thm = REPEAT o FIRST' |
87 fun eqvt_transform_tac thm = REPEAT o FIRST' |
77 [CHANGED o simp_tac (HOL_basic_ss addsimps @{thms permute_minus_cancel}), |
88 [CHANGED o simp_tac (HOL_basic_ss addsimps @{thms permute_minus_cancel}), |
78 rtac (thm RS @{thm trans}), |
89 rtac (thm RS @{thm trans}), |
79 rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}] |
90 rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}] |
80 |
91 |
81 (* transform equations into the required form *) |
92 (* transform equations into the "p o c = c"-form *) |
82 fun transform_eq ctxt thm lhs rhs = |
93 fun transform_eq ctxt thm lhs rhs = |
83 let |
94 let |
84 val (p, t) = dest_perm lhs |
95 val (p, t) = dest_perm lhs |
85 val (c, args) = strip_comb t |
96 val (c, args) = strip_comb t |
86 val (c', args') = strip_comb rhs |
97 val (c', args') = strip_comb rhs |