36 end; |
36 end; |
37 |
37 |
38 structure Nominal_ThmDecls: NOMINAL_THMDECLS = |
38 structure Nominal_ThmDecls: NOMINAL_THMDECLS = |
39 struct |
39 struct |
40 |
40 |
|
41 fun mk_equiv r = r RS @{thm eq_reflection}; |
|
42 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; |
41 |
43 |
42 structure EqvtData = Generic_Data |
44 structure EqvtData = Generic_Data |
43 ( type T = thm Item_Net.T; |
45 ( type T = thm Item_Net.T; |
44 val empty = Thm.full_rules; |
46 val empty = Thm.full_rules; |
45 val extend = I; |
47 val extend = I; |
64 | is_equiv _ = false |
66 | is_equiv _ = false |
65 |
67 |
66 fun add_raw_thm thm = |
68 fun add_raw_thm thm = |
67 let |
69 let |
68 val trm = prop_of thm |
70 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 |
71 in |
72 (EqvtRawData.map o Item_Net.update) thm |
72 if is_equiv trm |
|
73 then (EqvtRawData.map o Item_Net.update) thm |
|
74 else raise THM ("Theorem must be a meta-equality", 0, [thm]) |
73 end |
75 end |
74 |
76 |
75 val del_raw_thm = EqvtRawData.map o Item_Net.remove; |
77 val del_raw_thm = EqvtRawData.map o Item_Net.remove; |
76 |
78 |
77 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
79 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
78 | dest_perm t = raise TERM("dest_perm", [t]) |
80 | dest_perm t = raise TERM ("dest_perm", [t]) |
79 |
81 |
80 fun mk_perm p trm = |
82 fun mk_perm p trm = |
81 let |
83 let |
82 val ty = fastype_of trm |
84 val ty = fastype_of trm |
83 in |
85 in |
88 [CHANGED o simp_tac (HOL_basic_ss addsimps @{thms permute_minus_cancel}), |
90 [CHANGED o simp_tac (HOL_basic_ss addsimps @{thms permute_minus_cancel}), |
89 rtac (thm RS @{thm trans}), |
91 rtac (thm RS @{thm trans}), |
90 rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}] |
92 rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}] |
91 |
93 |
92 (* transform equations into the "p o c = c"-form *) |
94 (* transform equations into the "p o c = c"-form *) |
93 fun transform_eq ctxt thm lhs rhs = |
95 fun transform_eq ctxt thm = |
94 let |
96 let |
|
97 val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm)) |
95 val (p, t) = dest_perm lhs |
98 val (p, t) = dest_perm lhs |
96 val (c, args) = strip_comb t |
99 val (c, args) = strip_comb t |
97 val (c', args') = strip_comb rhs |
100 val (c', args') = strip_comb rhs |
98 val eargs = map Envir.eta_contract args |
101 val eargs = map Envir.eta_contract args |
99 val eargs' = map Envir.eta_contract args' |
102 val eargs' = map Envir.eta_contract args' |
100 val p_str = fst (fst (dest_Var p)) |
103 val p_str = fst (fst (dest_Var p)) |
101 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c)) |
104 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c)) |
102 in |
105 in |
111 end |
114 end |
112 |
115 |
113 fun transform addel_fun thm context = |
116 fun transform addel_fun thm context = |
114 let |
117 let |
115 val ctxt = Context.proof_of context |
118 val ctxt = Context.proof_of context |
116 val trm = HOLogic.dest_Trueprop (prop_of thm) |
|
117 in |
119 in |
118 case trm of |
120 case (prop_of thm) of |
119 Const (@{const_name "op ="}, _) $ lhs $ rhs => |
121 @{const "Trueprop"} $ (Const (@{const_name "op ="}, _) $ _ $ _) => |
120 let |
122 addel_fun (safe_mk_equiv (transform_eq ctxt thm)) context |
121 val thm' = transform_eq ctxt thm lhs rhs RS @{thm eq_reflection} |
123 | @{const "==>"} $ _ $ _ => |
122 in |
124 error ("not yet implemented") |
123 addel_fun thm' context |
|
124 end |
|
125 | _ => raise (error "only (op=) case implemented yet") |
125 | _ => raise (error "only (op=) case implemented yet") |
126 end |
126 end |
127 |
127 |
128 val eqvt_add = Thm.declaration_attribute (fn thm => (add_thm thm) o (transform add_raw_thm thm)); |
128 val eqvt_add = Thm.declaration_attribute (fn thm => (add_thm thm) o (transform add_raw_thm thm)); |
129 val eqvt_del = Thm.declaration_attribute (fn thm => (del_thm thm) o (transform del_raw_thm thm)); |
129 val eqvt_del = Thm.declaration_attribute (fn thm => (del_thm thm) o (transform del_raw_thm thm)); |