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 

7475

128 
fun differ thms thms' = not (Library.equal_lists Thm.eq_thm (thms, thms'));

7414

129 
fun combine thms =


130 
Seq.map Library.single (Seq.flat (Seq.map (Method.multi_resolve (thms @ facts)) rules));


131 

6903

132 
val (initial, calculations) =

6778

133 
(case get_calculation state of

7414

134 
None => (true, Seq.single facts)


135 
 Some thms => (false, Seq.filter (differ thms) (combine thms)))

6778

136 
in

6903

137 
err_if (initial andalso final) "No calculation yet";


138 
err_if (initial andalso is_some opt_rules) "Initial calculation  no rules to be given";

6782

139 
calculations > Seq.map (fn calc =>


140 
(print calc;

6787

141 
(if final then


142 
state


143 
> reset_calculation

6877

144 
> Proof.simple_have_thms calculationN []

7414

145 
> Proof.simple_have_thms "" calc

6787

146 
> Proof.chain


147 
else


148 
state


149 
> put_calculation calc

7414

150 
> Proof.simple_have_thms calculationN calc

6787

151 
> Proof.reset_facts)))

6778

152 
end;


153 

6782

154 
fun also print = calculate false print;


155 
fun finally print = calculate true print;

6778

156 


157 


158 


159 
(** theory setup **)


160 


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


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


163 


164 


165 
end;
