src/Pure/Isar/calculation.ML
changeset 6877 3d5e5e6f9e20
parent 6787 25265c6807c3
child 6903 682f8a9ec75d
equal deleted inserted replaced
6876:4ae9c47f2b6b 6877:3d5e5e6f9e20
    11   val print_local_rules: Proof.context -> unit
    11   val print_local_rules: Proof.context -> unit
    12   val trans_add_global: theory attribute
    12   val trans_add_global: theory attribute
    13   val trans_del_global: theory attribute
    13   val trans_del_global: theory attribute
    14   val trans_add_local: Proof.context attribute
    14   val trans_add_local: Proof.context attribute
    15   val trans_del_local: Proof.context attribute
    15   val trans_del_local: Proof.context attribute
    16   val also: (thm -> unit) -> Proof.state -> Proof.state Seq.seq
    16   val also: thm list option -> (thm -> unit) -> Proof.state -> Proof.state Seq.seq
    17   val finally: (thm -> unit) -> Proof.state -> Proof.state Seq.seq
    17   val finally: thm list option -> (thm -> unit) -> Proof.state -> Proof.state Seq.seq
    18   val setup: (theory -> theory) list
    18   val setup: (theory -> theory) list
    19 end;
    19 end;
    20 
    20 
    21 structure Calculation: CALCULATION =
    21 structure Calculation: CALCULATION =
    22 struct
    22 struct
    24 
    24 
    25 (** global and local calculation data **)
    25 (** global and local calculation data **)
    26 
    26 
    27 fun print_rules ths =
    27 fun print_rules ths =
    28   Pretty.writeln (Pretty.big_list "calculation rules:" (map Display.pretty_thm ths));
    28   Pretty.writeln (Pretty.big_list "calculation rules:" (map Display.pretty_thm ths));
    29 
       
    30 
    29 
    31 (* theory data kind 'Isar/calculation' *)
    30 (* theory data kind 'Isar/calculation' *)
    32 
    31 
    33 structure GlobalCalculationArgs =
    32 structure GlobalCalculationArgs =
    34 struct
    33 struct
   115 
   114 
   116 
   115 
   117 
   116 
   118 (** proof commands **)
   117 (** proof commands **)
   119 
   118 
   120 fun have_thms name thms = Proof.have_thmss name [] [(thms, [])];
       
   121 
       
   122 val calculationN = "calculation";
   119 val calculationN = "calculation";
   123 
   120 
   124 fun calculate final print state =
   121 fun calculate final opt_rules print state =
   125   let
   122   let
   126     val fact = Proof.the_fact state;
   123     val fact = Proof.the_fact state;
   127     val rules = Seq.of_list (get_local_rules state);
   124     val rules = Seq.of_list (case opt_rules of None => get_local_rules state | Some thms => thms);
   128     val calculations =
   125     val calculations =
   129       (case get_calculation state of
   126       (case get_calculation state of
   130         None => Seq.single fact
   127         None => Seq.single fact
   131       | Some thm => Seq.flat (Seq.map (Method.multi_resolve [thm, fact]) rules));
   128       | Some thm => Seq.flat (Seq.map (Method.multi_resolve [thm, fact]) rules));
   132   in
   129   in
   133     calculations |> Seq.map (fn calc =>
   130     calculations |> Seq.map (fn calc =>
   134       (print calc;
   131       (print calc;
   135         (if final then
   132         (if final then
   136           state
   133           state
   137           |> reset_calculation
   134           |> reset_calculation
   138           |> have_thms calculationN []
   135           |> Proof.simple_have_thms calculationN []
   139           |> have_thms "" [calc]
   136           |> Proof.simple_have_thms "" [calc]
   140           |> Proof.chain
   137           |> Proof.chain
   141         else
   138         else
   142           state
   139           state
   143           |> put_calculation calc
   140           |> put_calculation calc
   144           |> have_thms calculationN [calc]
   141           |> Proof.simple_have_thms calculationN [calc]
   145           |> Proof.reset_facts)))
   142           |> Proof.reset_facts)))
   146   end;
   143   end;
   147 
   144 
   148 fun also print = calculate false print;
   145 fun also print = calculate false print;
   149 fun finally print = calculate true print;
   146 fun finally print = calculate true print;