calculation: thm list;
authorwenzelm
Wed Sep 01 21:14:23 1999 +0200 (1999-09-01)
changeset 74149bc7797d1249
parent 7413 e25ad9ab0b50
child 7415 bd819d0255e1
calculation: thm list;
filter differ;
src/Pure/Isar/calculation.ML
     1.1 --- a/src/Pure/Isar/calculation.ML	Wed Sep 01 21:13:12 1999 +0200
     1.2 +++ b/src/Pure/Isar/calculation.ML	Wed Sep 01 21:14:23 1999 +0200
     1.3 @@ -13,8 +13,8 @@
     1.4    val trans_del_global: theory attribute
     1.5    val trans_add_local: Proof.context attribute
     1.6    val trans_del_local: Proof.context attribute
     1.7 -  val also: thm list option -> (thm -> unit) -> Proof.state -> Proof.state Seq.seq
     1.8 -  val finally: thm list option -> (thm -> unit) -> Proof.state -> Proof.state Seq.seq
     1.9 +  val also: thm list option -> (thm list -> unit) -> Proof.state -> Proof.state Seq.seq
    1.10 +  val finally: thm list option -> (thm list -> unit) -> Proof.state -> Proof.state Seq.seq
    1.11    val setup: (theory -> theory) list
    1.12  end;
    1.13  
    1.14 @@ -27,6 +27,7 @@
    1.15  fun print_rules ths =
    1.16    Pretty.writeln (Pretty.big_list "calculation rules:" (map Display.pretty_thm ths));
    1.17  
    1.18 +
    1.19  (* theory data kind 'Isar/calculation' *)
    1.20  
    1.21  structure GlobalCalculationArgs =
    1.22 @@ -50,7 +51,7 @@
    1.23  structure LocalCalculationArgs =
    1.24  struct
    1.25    val name = "Isar/calculation";
    1.26 -  type T = thm list * (thm * int) option;
    1.27 +  type T = thm list * (thm list * int) option;
    1.28  
    1.29    fun init thy = (GlobalCalculation.get thy, None);
    1.30    fun print _ (ths, _) = print_rules ths;
    1.31 @@ -66,10 +67,10 @@
    1.32  fun get_calculation state =
    1.33    (case #2 (LocalCalculation.get_st state) of
    1.34      None => None
    1.35 -  | Some (thm, lev) => if lev = Proof.level state then Some thm else None);
    1.36 +  | Some (thms, lev) => if lev = Proof.level state then Some thms else None);
    1.37  
    1.38 -fun put_calculation thm state =
    1.39 -  LocalCalculation.put_st (get_local_rules state, Some (thm, Proof.level state)) state;
    1.40 +fun put_calculation thms state =
    1.41 +  LocalCalculation.put_st (get_local_rules state, Some (thms, Proof.level state)) state;
    1.42  
    1.43  fun reset_calculation state =
    1.44    LocalCalculation.put_st (get_local_rules state, None) state;
    1.45 @@ -121,12 +122,18 @@
    1.46  fun calculate final opt_rules print state =
    1.47    let
    1.48      fun err_if b msg = if b then raise Proof.STATE (msg, state) else ();
    1.49 -    val fact = Proof.the_fact state;
    1.50 +    val facts = Proof.the_facts state;
    1.51      val rules = Seq.of_list (if_none opt_rules [] @ get_local_rules state);
    1.52 +
    1.53 +    fun differ thms thms' =
    1.54 +      length thms <> length thms' orelse exists2 (not o Thm.eq_thm) (thms, thms');
    1.55 +    fun combine thms =
    1.56 +      Seq.map Library.single (Seq.flat (Seq.map (Method.multi_resolve (thms @ facts)) rules));
    1.57 +
    1.58      val (initial, calculations) =
    1.59        (case get_calculation state of
    1.60 -        None => (true, Seq.single fact)
    1.61 -      | Some thm => (false, Seq.flat (Seq.map (Method.multi_resolve [thm, fact]) rules)));
    1.62 +        None => (true, Seq.single facts)
    1.63 +      | Some thms => (false, Seq.filter (differ thms) (combine thms)))
    1.64    in
    1.65      err_if (initial andalso final) "No calculation yet";
    1.66      err_if (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
    1.67 @@ -136,12 +143,12 @@
    1.68            state
    1.69            |> reset_calculation
    1.70            |> Proof.simple_have_thms calculationN []
    1.71 -          |> Proof.simple_have_thms "" [calc]
    1.72 +          |> Proof.simple_have_thms "" calc
    1.73            |> Proof.chain
    1.74          else
    1.75            state
    1.76            |> put_calculation calc
    1.77 -          |> Proof.simple_have_thms calculationN [calc]
    1.78 +          |> Proof.simple_have_thms calculationN calc
    1.79            |> Proof.reset_facts)))
    1.80    end;
    1.81