28 |
28 |
29 (** calculation data **) |
29 (** calculation data **) |
30 |
30 |
31 structure CalculationData = GenericDataFun |
31 structure CalculationData = GenericDataFun |
32 ( |
32 ( |
33 val name = "Isar/calculation"; |
|
34 type T = (thm NetRules.T * thm list) * (thm list * int) option; |
33 type T = (thm NetRules.T * thm list) * (thm list * int) option; |
35 val empty = ((NetRules.elim, []), NONE); |
34 val empty = ((NetRules.elim, []), NONE); |
36 val extend = I; |
35 val extend = I; |
37 |
36 |
38 fun merge _ (((trans1, sym1), _), ((trans2, sym2), _)) = |
37 fun merge _ (((trans1, sym1), _), ((trans2, sym2), _)) = |
39 ((NetRules.merge (trans1, trans2), Drule.merge_rules (sym1, sym2)), NONE); |
38 ((NetRules.merge (trans1, trans2), Drule.merge_rules (sym1, sym2)), NONE); |
40 |
|
41 fun print generic ((trans, sym), _) = |
|
42 let val ctxt = Context.proof_of generic in |
|
43 [Pretty.big_list "transitivity rules:" |
|
44 (map (ProofContext.pretty_thm ctxt) (NetRules.rules trans)), |
|
45 Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)] |
|
46 |> Pretty.chunks |> Pretty.writeln |
|
47 end; |
|
48 ); |
39 ); |
49 |
40 |
50 val _ = Context.add_setup CalculationData.init; |
41 fun print_rules ctxt = |
51 val print_rules = CalculationData.print o Context.Proof; |
42 let val ((trans, sym), _) = CalculationData.get (Context.Proof ctxt) in |
|
43 [Pretty.big_list "transitivity rules:" |
|
44 (map (ProofContext.pretty_thm ctxt) (NetRules.rules trans)), |
|
45 Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)] |
|
46 |> Pretty.chunks |> Pretty.writeln |
|
47 end; |
52 |
48 |
53 |
49 |
54 (* access calculation *) |
50 (* access calculation *) |
55 |
51 |
56 fun get_calculation state = |
52 fun get_calculation state = |