author  wenzelm 
Tue, 21 Sep 1999 17:07:28 +0200  
changeset 7554  30327f9f6b4a 
parent 7475  dc4f8d6ee0d2 
child 7600  73f91da46230 
permissions  rwrr 
6778  1 
(* Title: Pure/Isar/calculation.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

4 

5 
Support for calculational proofs. 

6 
*) 

7 

8 
signature CALCULATION = 

9 
sig 

10 
val print_global_rules: theory > unit 

11 
val print_local_rules: Proof.context > unit 

12 
val trans_add_global: theory attribute 

13 
val trans_del_global: theory attribute 

14 
val trans_add_local: Proof.context attribute 

15 
val trans_del_local: Proof.context attribute 

7414  16 
val also: thm list option > (thm list > unit) > Proof.state > Proof.state Seq.seq 
17 
val finally: thm list option > (thm list > unit) > Proof.state > Proof.state Seq.seq 

6778  18 
val setup: (theory > theory) list 
19 
end; 

20 

21 
structure Calculation: CALCULATION = 

22 
struct 

23 

24 

25 
(** global and local calculation data **) 

26 

27 
fun print_rules ths = 

28 
Pretty.writeln (Pretty.big_list "calculation rules:" (map Display.pretty_thm ths)); 

29 

7414  30 

6778  31 
(* theory data kind 'Isar/calculation' *) 
32 

33 
structure GlobalCalculationArgs = 

34 
struct 

35 
val name = "Isar/calculation"; 

36 
type T = thm list; 

37 

38 
val empty = []; 

39 
val copy = I; 

40 
val prep_ext = I; 

41 
fun merge (ths1, ths2) = Library.generic_merge Thm.eq_thm I I ths1 ths2; 

42 
fun print _ = print_rules; 

43 
end; 

44 

45 
structure GlobalCalculation = TheoryDataFun(GlobalCalculationArgs); 

46 
val print_global_rules = GlobalCalculation.print; 

47 

48 

49 
(* proof data kind 'Isar/calculation' *) 

50 

51 
structure LocalCalculationArgs = 

52 
struct 

53 
val name = "Isar/calculation"; 

7414  54 
type T = thm list * (thm list * int) option; 
6778  55 

56 
fun init thy = (GlobalCalculation.get thy, None); 

57 
fun print _ (ths, _) = print_rules ths; 

58 
end; 

59 

60 
structure LocalCalculation = ProofDataFun(LocalCalculationArgs); 

6787  61 
val get_local_rules = #1 o LocalCalculation.get_st; 
6778  62 
val print_local_rules = LocalCalculation.print; 
63 

64 

65 
(* access calculation *) 

66 

67 
fun get_calculation state = 

6787  68 
(case #2 (LocalCalculation.get_st state) of 
6778  69 
None => None 
7414  70 
 Some (thms, lev) => if lev = Proof.level state then Some thms else None); 
6778  71 

7414  72 
fun put_calculation thms state = 
73 
LocalCalculation.put_st (get_local_rules state, Some (thms, Proof.level state)) state; 

6778  74 

6787  75 
fun reset_calculation state = 
76 
LocalCalculation.put_st (get_local_rules state, None) state; 

77 

6778  78 

79 

80 
(** attributes **) 

81 

82 
(* trans add/del *) 

83 

84 
local 

85 

86 
fun map_rules_global f thy = GlobalCalculation.put (f (GlobalCalculation.get thy)) thy; 

87 
fun map_rules_local f ctxt = LocalCalculation.put (f (LocalCalculation.get ctxt)) ctxt; 

88 

89 
fun add_trans thm rules = Library.gen_ins Thm.eq_thm (thm, rules); 

90 
fun del_trans thm rules = Library.gen_rem Thm.eq_thm (rules, thm); 

91 

92 
fun mk_att f g (x, thm) = (f (g thm) x, thm); 

93 

94 
in 

95 

96 
val trans_add_global = mk_att map_rules_global add_trans; 

97 
val trans_del_global = mk_att map_rules_global del_trans; 

98 
val trans_add_local = mk_att map_rules_local (Library.apfst o add_trans); 

99 
val trans_del_local = mk_att map_rules_local (Library.apfst o del_trans); 

100 

101 
end; 

102 

103 

104 
(* concrete syntax *) 

105 

106 
val transN = "trans"; 

107 
val addN = "add"; 

108 
val delN = "del"; 

109 

110 
fun trans_att add del = 

111 
Attrib.syntax (Scan.lift (Args.$$$ addN >> K add  Args.$$$ delN >> K del  Scan.succeed add)); 

112 

113 
val trans_attr = 

114 
(trans_att trans_add_global trans_del_global, trans_att trans_add_local trans_del_local); 

115 

116 

6787  117 

6778  118 
(** proof commands **) 
119 

120 
val calculationN = "calculation"; 

121 

6877  122 
fun calculate final opt_rules print state = 
6778  123 
let 
6903  124 
fun err_if b msg = if b then raise Proof.STATE (msg, state) else (); 
7414  125 
val facts = Proof.the_facts state; 
7197  126 
val rules = Seq.of_list (if_none opt_rules [] @ get_local_rules state); 
7414  127 

7554
30327f9f6b4a
differ: compare actual props only (hyps may changed due to trivial steps involving assumptions);
wenzelm
parents:
7475
diff
changeset

128 
val eq_prop = op aconv o pairself (#prop o Thm.rep_thm); 
30327f9f6b4a
differ: compare actual props only (hyps may changed due to trivial steps involving assumptions);
wenzelm
parents:
7475
diff
changeset

129 
fun differ thms thms' = not (Library.equal_lists eq_prop (thms, thms')); 
7414  130 
fun combine thms = 
131 
Seq.map Library.single (Seq.flat (Seq.map (Method.multi_resolve (thms @ facts)) rules)); 

132 

6903  133 
val (initial, calculations) = 
6778  134 
(case get_calculation state of 
7414  135 
None => (true, Seq.single facts) 
136 
 Some thms => (false, Seq.filter (differ thms) (combine thms))) 

6778  137 
in 
6903  138 
err_if (initial andalso final) "No calculation yet"; 
139 
err_if (initial andalso is_some opt_rules) "Initial calculation  no rules to be given"; 

6782  140 
calculations > Seq.map (fn calc => 
141 
(print calc; 

6787  142 
(if final then 
143 
state 

144 
> reset_calculation 

6877  145 
> Proof.simple_have_thms calculationN [] 
7414  146 
> Proof.simple_have_thms "" calc 
6787  147 
> Proof.chain 
148 
else 

149 
state 

150 
> put_calculation calc 

7414  151 
> Proof.simple_have_thms calculationN calc 
6787  152 
> Proof.reset_facts))) 
6778  153 
end; 
154 

6782  155 
fun also print = calculate false print; 
156 
fun finally print = calculate true print; 

6778  157 

158 

159 

160 
(** theory setup **) 

161 

162 
val setup = [GlobalCalculation.init, LocalCalculation.init, 

163 
Attrib.add_attributes [(transN, trans_attr, "transitivity rule")]]; 

164 

165 

166 
end; 