45 val empty = Thm.full_rules; |
45 val empty = Thm.full_rules; |
46 val extend = I; |
46 val extend = I; |
47 val merge = Item_Net.merge); |
47 val merge = Item_Net.merge); |
48 |
48 |
49 structure EqvtRawData = Generic_Data |
49 structure EqvtRawData = Generic_Data |
50 ( type T = thm Symtab.table; |
50 ( type T = thm Termtab.table; |
51 val empty = Symtab.empty; |
51 val empty = Termtab.empty; |
52 val extend = I; |
52 val extend = I; |
53 val merge = Symtab.merge (K true)); |
53 val merge = Termtab.merge (K true)); |
54 |
54 |
55 val eqvts = Item_Net.content o EqvtData.get; |
55 val eqvts = Item_Net.content o EqvtData.get; |
56 val eqvts_raw = map snd o Symtab.dest o EqvtRawData.get; |
56 val eqvts_raw = map snd o Termtab.dest o EqvtRawData.get; |
57 |
57 |
58 val get_eqvts_thms = eqvts o Context.Proof; |
58 val get_eqvts_thms = eqvts o Context.Proof; |
59 val get_eqvts_raw_thms = eqvts_raw o Context.Proof; |
59 val get_eqvts_raw_thms = eqvts_raw o Context.Proof; |
60 |
60 |
61 val add_thm = EqvtData.map o Item_Net.update; |
61 val add_thm = EqvtData.map o Item_Net.update; |
62 val del_thm = EqvtData.map o Item_Net.remove; |
62 val del_thm = EqvtData.map o Item_Net.remove; |
63 |
63 |
64 fun add_raw_thm thm = |
64 fun add_raw_thm thm = |
65 case prop_of thm of |
65 case prop_of thm of |
66 Const ("==", _) $ _ $ Const (c, _) => EqvtRawData.map (Symtab.update (c, thm)) |
66 Const ("==", _) $ _ $ (c as Const _) => EqvtRawData.map (Termtab.update (c, thm)) |
67 | _ => raise THM ("Theorem must be a meta-equality where the right-hand side is a constant.", 0, [thm]) |
67 | _ => raise THM ("Theorem must be a meta-equality where the right-hand side is a constant.", 0, [thm]) |
68 |
68 |
69 fun del_raw_thm thm = |
69 fun del_raw_thm thm = |
70 case prop_of thm of |
70 case prop_of thm of |
71 Const ("==", _) $ _ $ Const (c, _) => EqvtRawData.map (Symtab.delete c) |
71 Const ("==", _) $ _ $ (c as Const _) => EqvtRawData.map (Termtab.delete c) |
72 | _ => raise THM ("Theorem must be a meta-equality where the right-hand side is a constant.", 0, [thm]) |
72 | _ => raise THM ("Theorem must be a meta-equality where the right-hand side is a constant.", 0, [thm]) |
73 |
73 |
74 fun is_eqvt ctxt trm = |
74 fun is_eqvt ctxt trm = |
75 case trm of |
75 case trm of |
76 Const (c, _) => Symtab.defined (EqvtRawData.get (Context.Proof ctxt)) c |
76 (c as Const _) => Termtab.defined (EqvtRawData.get (Context.Proof ctxt)) c |
77 | _ => raise TERM ("Term must be a constsnt.", [trm]) |
77 | _ => raise TERM ("Term must be a constsnt.", [trm]) |
78 |
78 |
79 |
79 |
80 |
80 |
81 (** transformation of eqvt lemmas **) |
81 (** transformation of eqvt lemmas **) |