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

6877

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


17 
val finally: thm list option > (thm > 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 


30 
(* theory data kind 'Isar/calculation' *)


31 


32 
structure GlobalCalculationArgs =


33 
struct


34 
val name = "Isar/calculation";


35 
type T = thm list;


36 


37 
val empty = [];


38 
val copy = I;


39 
val prep_ext = I;


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


41 
fun print _ = print_rules;


42 
end;


43 


44 
structure GlobalCalculation = TheoryDataFun(GlobalCalculationArgs);


45 
val print_global_rules = GlobalCalculation.print;


46 


47 


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


49 


50 
structure LocalCalculationArgs =


51 
struct


52 
val name = "Isar/calculation";


53 
type T = thm list * (thm * int) option;


54 


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


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


57 
end;


58 


59 
structure LocalCalculation = ProofDataFun(LocalCalculationArgs);

6787

60 
val get_local_rules = #1 o LocalCalculation.get_st;

6778

61 
val print_local_rules = LocalCalculation.print;


62 


63 


64 
(* access calculation *)


65 


66 
fun get_calculation state =

6787

67 
(case #2 (LocalCalculation.get_st state) of

6778

68 
None => None


69 
 Some (thm, lev) => if lev = Proof.level state then Some thm else None);


70 


71 
fun put_calculation thm state =


72 
LocalCalculation.put_st (get_local_rules state, Some (thm, Proof.level state)) state;


73 

6787

74 
fun reset_calculation state =


75 
LocalCalculation.put_st (get_local_rules state, None) state;


76 

6778

77 


78 


79 
(** attributes **)


80 


81 
(* trans add/del *)


82 


83 
local


84 


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


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


87 


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


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


90 


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


92 


93 
in


94 


95 
val trans_add_global = mk_att map_rules_global add_trans;


96 
val trans_del_global = mk_att map_rules_global del_trans;


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


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


99 


100 
end;


101 


102 


103 
(* concrete syntax *)


104 


105 
val transN = "trans";


106 
val addN = "add";


107 
val delN = "del";


108 


109 
fun trans_att add del =


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


111 


112 
val trans_attr =


113 
(trans_att trans_add_global trans_del_global, trans_att trans_add_local trans_del_local);


114 


115 

6787

116 

6778

117 
(** proof commands **)


118 


119 
val calculationN = "calculation";


120 

6877

121 
fun calculate final opt_rules print state =

6778

122 
let


123 
val fact = Proof.the_fact state;

6877

124 
val rules = Seq.of_list (case opt_rules of None => get_local_rules state  Some thms => thms);

6778

125 
val calculations =


126 
(case get_calculation state of


127 
None => Seq.single fact


128 
 Some thm => Seq.flat (Seq.map (Method.multi_resolve [thm, fact]) rules));


129 
in

6782

130 
calculations > Seq.map (fn calc =>


131 
(print calc;

6787

132 
(if final then


133 
state


134 
> reset_calculation

6877

135 
> Proof.simple_have_thms calculationN []


136 
> Proof.simple_have_thms "" [calc]

6787

137 
> Proof.chain


138 
else


139 
state


140 
> put_calculation calc

6877

141 
> Proof.simple_have_thms calculationN [calc]

6787

142 
> Proof.reset_facts)))

6778

143 
end;


144 

6782

145 
fun also print = calculate false print;


146 
fun finally print = calculate true print;

6778

147 


148 


149 


150 
(** theory setup **)


151 


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


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


154 


155 


156 
end;
