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


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


17 
val finally: (thm > unit) > Proof.state > Proof.state Seq.seq


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 


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";


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


55 


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


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


58 
end;


59 


60 
structure LocalCalculation = ProofDataFun(LocalCalculationArgs);


61 
val get_local_rules = #1 o LocalCalculation.get o Proof.context_of;


62 
val print_local_rules = LocalCalculation.print;


63 


64 


65 
(* access calculation *)


66 


67 
fun get_calculation state =


68 
(case #2 (LocalCalculation.get (Proof.context_of state)) of


69 
None => None


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


71 


72 
fun put_calculation thm state =


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


74 


75 


76 


77 
(** attributes **)


78 


79 
(* trans add/del *)


80 


81 
local


82 


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


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


85 


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


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


88 


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


90 


91 
in


92 


93 
val trans_add_global = mk_att map_rules_global add_trans;


94 
val trans_del_global = mk_att map_rules_global del_trans;


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


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


97 


98 
end;


99 


100 


101 
(* concrete syntax *)


102 


103 
val transN = "trans";


104 
val addN = "add";


105 
val delN = "del";


106 


107 
fun trans_att add del =


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


109 


110 
val trans_attr =


111 
(trans_att trans_add_global trans_del_global, trans_att trans_add_local trans_del_local);


112 


113 


114 
(** proof commands **)


115 


116 
val calculationN = "calculation";


117 


118 
fun calculate final prt state =


119 
let


120 
val fact = Proof.the_fact state;


121 
val dddot = ObjectLogic.dest_main_statement (#prop (Thm.rep_thm fact)) handle TERM _ =>


122 
raise Proof.STATE ("Unable to bind '...' pattern from current fact", state);


123 


124 
val name = if final then "" else calculationN;


125 
fun have_thm thm = Proof.have_thmss name [] [([thm], [])];


126 


127 
val rules = Seq.of_list (get_local_rules state);


128 
val calculations =


129 
(case get_calculation state of


130 
None => Seq.single fact


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


132 
in


133 
calculations


134 
> Seq.map (fn calc =>


135 
(prt calc;


136 
state


137 
> Proof.bind_i [(Syntax.dddot_indexname, dddot)]

6781

138 
> put_calculation calc

6778

139 
> have_thm calc

6781

140 
> (if final then Proof.chain else Proof.reset_facts)))

6778

141 
end;


142 

6781

143 
fun also prt = calculate false prt;


144 
fun finally prt = calculate true prt;

6778

145 


146 


147 


148 
(** theory setup **)


149 


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


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


152 


153 


154 
end;
