27 |
27 |
28 (** calculation data **) |
28 (** calculation data **) |
29 |
29 |
30 structure CalculationData = GenericDataFun |
30 structure CalculationData = GenericDataFun |
31 ( |
31 ( |
32 type T = (thm NetRules.T * thm list) * (thm list * int) option; |
32 type T = (thm Item_Net.T * thm list) * (thm list * int) option; |
33 val empty = ((NetRules.elim, []), NONE); |
33 val empty = ((Thm.elim_rules, []), NONE); |
34 val extend = I; |
34 val extend = I; |
35 |
35 |
36 fun merge _ (((trans1, sym1), _), ((trans2, sym2), _)) = |
36 fun merge _ (((trans1, sym1), _), ((trans2, sym2), _)) = |
37 ((NetRules.merge (trans1, trans2), Thm.merge_thms (sym1, sym2)), NONE); |
37 ((Item_Net.merge (trans1, trans2), Thm.merge_thms (sym1, sym2)), NONE); |
38 ); |
38 ); |
39 |
39 |
40 fun print_rules ctxt = |
40 fun print_rules ctxt = |
41 let val ((trans, sym), _) = CalculationData.get (Context.Proof ctxt) in |
41 let val ((trans, sym), _) = CalculationData.get (Context.Proof ctxt) in |
42 [Pretty.big_list "transitivity rules:" |
42 [Pretty.big_list "transitivity rules:" |
43 (map (ProofContext.pretty_thm ctxt) (NetRules.rules trans)), |
43 (map (ProofContext.pretty_thm ctxt) (Item_Net.content trans)), |
44 Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)] |
44 Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)] |
45 |> Pretty.chunks |> Pretty.writeln |
45 |> Pretty.chunks |> Pretty.writeln |
46 end; |
46 end; |
47 |
47 |
48 |
48 |
64 |
64 |
65 (** attributes **) |
65 (** attributes **) |
66 |
66 |
67 (* add/del rules *) |
67 (* add/del rules *) |
68 |
68 |
69 val trans_add = Thm.declaration_attribute (CalculationData.map o apfst o apfst o NetRules.insert); |
69 val trans_add = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.insert); |
70 val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o NetRules.delete); |
70 val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.delete); |
71 |
71 |
72 val sym_add = |
72 val sym_add = |
73 Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.add_thm) |
73 Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.add_thm) |
74 #> ContextRules.elim_query NONE; |
74 #> ContextRules.elim_query NONE; |
75 val sym_del = |
75 val sym_del = |
128 |
128 |
129 val opt_rules = Option.map (prep_rules state) raw_rules; |
129 val opt_rules = Option.map (prep_rules state) raw_rules; |
130 fun combine ths = |
130 fun combine ths = |
131 (case opt_rules of SOME rules => rules |
131 (case opt_rules of SOME rules => rules |
132 | NONE => |
132 | NONE => |
133 (case ths of [] => NetRules.rules (#1 (get_rules state)) |
133 (case ths of [] => Item_Net.content (#1 (get_rules state)) |
134 | th :: _ => NetRules.retrieve (#1 (get_rules state)) (strip_assums_concl th))) |
134 | th :: _ => Item_Net.retrieve (#1 (get_rules state)) (strip_assums_concl th))) |
135 |> Seq.of_list |> Seq.maps (Drule.multi_resolve ths) |
135 |> Seq.of_list |> Seq.maps (Drule.multi_resolve ths) |
136 |> Seq.filter (not o projection ths); |
136 |> Seq.filter (not o projection ths); |
137 |
137 |
138 val facts = Proof.the_facts (assert_sane final state); |
138 val facts = Proof.the_facts (assert_sane final state); |
139 val (initial, calculations) = |
139 val (initial, calculations) = |