src/Provers/clasimp.ML
changeset 9860 5c5efed691b9
parent 9805 10b617bdd028
child 9893 93d2fde0306c
equal deleted inserted replaced
9859:2cd338998b53 9860:5c5efed691b9
     4 
     4 
     5 Combination of classical reasoner and simplifier (depends on
     5 Combination of classical reasoner and simplifier (depends on
     6 simplifier.ML, splitter.ML classical.ML, blast.ML).
     6 simplifier.ML, splitter.ML classical.ML, blast.ML).
     7 *)
     7 *)
     8 
     8 
     9 infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2 addsimps2 delsimps2;
     9 infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2 addsimps2 delsimps2
    10 infix 4 addSss addss;
    10   addSss addss addIffs delIffs;
    11 
    11 
    12 signature CLASIMP_DATA =
    12 signature CLASIMP_DATA =
    13 sig
    13 sig
    14   structure Simplifier: SIMPLIFIER
    14   structure Simplifier: SIMPLIFIER
    15   structure Splitter: SPLITTER
    15   structure Splitter: SPLITTER
    16   structure Classical: CLASSICAL
    16   structure Classical: CLASSICAL
    17   structure Blast: BLAST
    17   structure Blast: BLAST
    18   sharing type Classical.claset = Blast.claset
    18   sharing type Classical.claset = Blast.claset
       
    19   val dest_Trueprop: term -> term
       
    20   val not_const: term
       
    21   val iff_const: term
       
    22   val notE: thm
       
    23   val iffD1: thm
       
    24   val iffD2: thm
       
    25   val cla_make_elim: thm -> thm
    19 end
    26 end
    20 
    27 
    21 signature CLASIMP =
    28 signature CLASIMP =
    22 sig
    29 sig
    23   include CLASIMP_DATA
    30   include CLASIMP_DATA
    24   type claset
    31   type claset
    25   type simpset
    32   type simpset
    26   type clasimpset
    33   type clasimpset
    27   val addSIs2   : clasimpset * thm list -> clasimpset
    34   val addSIs2: clasimpset * thm list -> clasimpset
    28   val addSEs2   : clasimpset * thm list -> clasimpset
    35   val addSEs2: clasimpset * thm list -> clasimpset
    29   val addSDs2   : clasimpset * thm list -> clasimpset
    36   val addSDs2: clasimpset * thm list -> clasimpset
    30   val addIs2    : clasimpset * thm list -> clasimpset
    37   val addIs2: clasimpset * thm list -> clasimpset
    31   val addEs2    : clasimpset * thm list -> clasimpset
    38   val addEs2: clasimpset * thm list -> clasimpset
    32   val addDs2    : clasimpset * thm list -> clasimpset
    39   val addDs2: clasimpset * thm list -> clasimpset
    33   val addsimps2 : clasimpset * thm list -> clasimpset
    40   val addsimps2: clasimpset * thm list -> clasimpset
    34   val delsimps2 : clasimpset * thm list -> clasimpset
    41   val delsimps2: clasimpset * thm list -> clasimpset
    35   val addSss    : claset * simpset -> claset
    42   val addSss: claset * simpset -> claset
    36   val addss     : claset * simpset -> claset
    43   val addss: claset * simpset -> claset
    37   val CLASIMPSET  :(clasimpset -> tactic) -> tactic
    44   val addIffs: clasimpset * thm list -> clasimpset
    38   val CLASIMPSET' :(clasimpset -> 'a -> tactic) -> 'a -> tactic
    45   val delIffs: clasimpset * thm list -> clasimpset
       
    46   val AddIffs: thm list -> unit
       
    47   val DelIffs: thm list -> unit
       
    48   val CLASIMPSET: (clasimpset -> tactic) -> tactic
       
    49   val CLASIMPSET': (clasimpset -> 'a -> tactic) -> 'a -> tactic
    39   val clarsimp_tac: clasimpset -> int -> tactic
    50   val clarsimp_tac: clasimpset -> int -> tactic
    40   val Clarsimp_tac:               int -> tactic
    51   val Clarsimp_tac: int -> tactic
    41   val mk_auto_tac : clasimpset -> int -> int -> tactic
    52   val mk_auto_tac: clasimpset -> int -> int -> tactic
    42   val auto_tac    : clasimpset -> tactic
    53   val auto_tac: clasimpset -> tactic
    43   val Auto_tac    : tactic
    54   val Auto_tac: tactic
    44   val auto        : unit -> unit
    55   val auto: unit -> unit
    45   val force_tac   : clasimpset  -> int -> tactic
    56   val force_tac: clasimpset  -> int -> tactic
    46   val Force_tac   : int -> tactic
    57   val Force_tac: int -> tactic
    47   val force       : int -> unit
    58   val force: int -> unit
    48   val fast_simp_tac : clasimpset -> int -> tactic
    59   val fast_simp_tac: clasimpset -> int -> tactic
    49   val slow_simp_tac : clasimpset -> int -> tactic
    60   val slow_simp_tac: clasimpset -> int -> tactic
    50   val best_simp_tac : clasimpset -> int -> tactic
    61   val best_simp_tac: clasimpset -> int -> tactic
    51   val change_global_css: (clasimpset * thm list -> clasimpset) -> theory attribute
    62   val change_global_css: (clasimpset * thm list -> clasimpset) -> theory attribute
    52   val change_local_css: (clasimpset * thm list -> clasimpset) -> Proof.context attribute
    63   val change_local_css: (clasimpset * thm list -> clasimpset) -> Proof.context attribute
    53   val get_local_clasimpset: Proof.context -> clasimpset
    64   val get_local_clasimpset: Proof.context -> clasimpset
       
    65   val iff_add_global: theory attribute
       
    66   val iff_del_global: theory attribute
       
    67   val iff_add_local: Proof.context attribute
       
    68   val iff_del_local: Proof.context attribute
       
    69   val iff_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
    54   val clasimp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
    70   val clasimp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
    55   val setup       : (theory -> theory) list
    71   val setup: (theory -> theory) list
    56 end;
    72 end;
    57 
    73 
    58 functor ClasimpFun(Data: CLASIMP_DATA): CLASIMP =
    74 functor ClasimpFun(Data: CLASIMP_DATA): CLASIMP =
    59 struct
    75 struct
    60 
    76 
    89 (*Caution: only one simpset added can be added by each of addSss and addss*)
   105 (*Caution: only one simpset added can be added by each of addSss and addss*)
    90 fun cs addSss ss = Classical.addSaltern (cs, ("safe_asm_full_simp_tac",
   106 fun cs addSss ss = Classical.addSaltern (cs, ("safe_asm_full_simp_tac",
    91                             CHANGED o safe_asm_full_simp_tac ss));
   107                             CHANGED o safe_asm_full_simp_tac ss));
    92 fun cs addss  ss = Classical.addbefore  (cs, ("asm_full_simp_tac",
   108 fun cs addss  ss = Classical.addbefore  (cs, ("asm_full_simp_tac",
    93                             CHANGED o Simplifier.asm_full_simp_tac ss));
   109                             CHANGED o Simplifier.asm_full_simp_tac ss));
       
   110 
       
   111 
       
   112 (* iffs: addition of rules to simpsets and clasets simultaneously *)
       
   113 
       
   114 (*Takes UNCONDITIONAL theorems of the form A<->B to
       
   115         the Safe Intr     rule B==>A and
       
   116         the Safe Destruct rule A==>B.
       
   117   Also ~A goes to the Safe Elim rule A ==> ?R
       
   118   Failing other cases, A is added as a Safe Intr rule*)
       
   119 local
       
   120 
       
   121 fun addIff ((cla, simp), th) =
       
   122   (case dest_Trueprop (#prop (rep_thm th)) of
       
   123     con $ _ $ _ =>
       
   124       if con = Data.iff_const then
       
   125         Classical.addSDs (Classical.addSIs (cla, [zero_var_indexes (th RS Data.iffD2)]),
       
   126           [zero_var_indexes (th RS Data.iffD1)])
       
   127       else Classical.addSIs (cla, [th])
       
   128   | con $ A =>
       
   129       if con = Data.not_const then Classical.addSEs (cla, [zero_var_indexes (th RS Data.notE)])
       
   130       else Classical.addSIs (cla, [th])
       
   131   | _ => Classical.addSIs (cla, [th]), Simplifier.addsimps (simp, [th]))
       
   132   handle TERM _ => error ("iff add: theorem must be unconditional\n" ^ Display.string_of_thm th);
       
   133 
       
   134 fun delIff ((cla, simp), th) =
       
   135   (case dest_Trueprop (#prop (rep_thm th)) of
       
   136     con $ _ $ _ =>
       
   137       if con = Data.iff_const then
       
   138         Classical.delrules (cla, [zero_var_indexes (th RS Data.iffD2),
       
   139           Data.cla_make_elim (zero_var_indexes (th RS Data.iffD1))])
       
   140       else Classical.delrules (cla, [th])
       
   141   | con $ A =>
       
   142       if con = Data.not_const then Classical.delrules (cla, [zero_var_indexes (th RS Data.notE)])
       
   143       else Classical.delrules (cla, [th])
       
   144   | _ => Classical.delrules (cla, [th]), Simplifier.delsimps (simp, [th]))
       
   145   handle TERM _ =>
       
   146     (warning ("iff del: ignoring conditional theorem\n" ^ string_of_thm th); (cla, simp));
       
   147 
       
   148 fun store_clasimp (cla, simp) =
       
   149   (Classical.claset_ref () := cla; Simplifier.simpset_ref () := simp);
       
   150 
       
   151 in
       
   152 
       
   153 val op addIffs = foldl addIff;
       
   154 val op delIffs = foldl delIff;
       
   155 fun AddIffs thms = store_clasimp ((Classical.claset (), Simplifier.simpset ()) addIffs thms);
       
   156 fun DelIffs thms = store_clasimp ((Classical.claset (), Simplifier.simpset ()) delIffs thms);
       
   157 
       
   158 end;
       
   159 
    94 
   160 
    95 (* tacticals *)
   161 (* tacticals *)
    96 
   162 
    97 fun CLASIMPSET tacf state =
   163 fun CLASIMPSET tacf state =
    98   Classical.CLASET (fn cs => Simplifier.SIMPSET (fn ss => tacf (cs, ss))) state;
   164   Classical.CLASET (fn cs => Simplifier.SIMPSET (fn ss => tacf (cs, ss))) state;
   165 val fast_simp_tac = ADDSS Classical.fast_tac;
   231 val fast_simp_tac = ADDSS Classical.fast_tac;
   166 val slow_simp_tac = ADDSS Classical.slow_tac;
   232 val slow_simp_tac = ADDSS Classical.slow_tac;
   167 val best_simp_tac = ADDSS Classical.best_tac;
   233 val best_simp_tac = ADDSS Classical.best_tac;
   168 
   234 
   169 
   235 
   170 (* change clasimpset *)
   236 (* access clasimpset *)
   171 
   237 
   172 fun change_global_css f (thy, th) =
   238 fun change_global_css f (thy, th) =
   173   let
   239   let
   174     val cs_ref = Classical.claset_ref_of thy;
   240     val cs_ref = Classical.claset_ref_of thy;
   175     val ss_ref = Simplifier.simpset_ref_of thy;
   241     val ss_ref = Simplifier.simpset_ref_of thy;
   185       ctxt
   251       ctxt
   186       |> Classical.put_local_claset cs'
   252       |> Classical.put_local_claset cs'
   187       |> Simplifier.put_local_simpset ss';
   253       |> Simplifier.put_local_simpset ss';
   188   in (ctxt', th) end;
   254   in (ctxt', th) end;
   189 
   255 
   190 
       
   191 (* methods *)
       
   192 
       
   193 fun get_local_clasimpset ctxt =
   256 fun get_local_clasimpset ctxt =
   194   (Classical.get_local_claset ctxt, Simplifier.get_local_simpset ctxt);
   257   (Classical.get_local_claset ctxt, Simplifier.get_local_simpset ctxt);
   195 
   258 
       
   259 
       
   260 (* attributes *)
       
   261 
       
   262 val iff_add_global = change_global_css (op addIffs);
       
   263 val iff_del_global = change_global_css (op delIffs);
       
   264 val iff_add_local = change_local_css (op addIffs);
       
   265 val iff_del_local = change_local_css (op delIffs);
       
   266 
       
   267 val iff_attr =
       
   268  (Attrib.add_del_args iff_add_global iff_del_global,
       
   269   Attrib.add_del_args iff_add_local iff_del_local);
       
   270 
       
   271 
       
   272 (* method modifiers *)
       
   273 
       
   274 val iffN = "iff";
       
   275 val addN = "add";
       
   276 val delN = "del";
       
   277 
       
   278 val iff_modifiers =
       
   279  [Args.$$$ iffN -- Args.colon >> K ((I, iff_add_local): Method.modifier),
       
   280   Args.$$$ iffN -- Args.$$$ addN -- Args.colon >> K (I, iff_add_local),
       
   281   Args.$$$ iffN -- Args.$$$ delN -- Args.colon >> K (I, iff_del_local)];
       
   282 
   196 val clasimp_modifiers =
   283 val clasimp_modifiers =
   197   Simplifier.simp_modifiers @ Splitter.split_modifiers @ Classical.cla_modifiers;
   284   Simplifier.simp_modifiers @ Splitter.split_modifiers @
       
   285   Classical.cla_modifiers @ iff_modifiers;
       
   286 
       
   287 
       
   288 (* methods *)
   198 
   289 
   199 fun clasimp_meth tac prems ctxt = Method.METHOD (fn facts =>
   290 fun clasimp_meth tac prems ctxt = Method.METHOD (fn facts =>
   200   ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_clasimpset ctxt));
   291   ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_clasimpset ctxt));
   201 
   292 
   202 fun clasimp_meth' tac prems ctxt = Method.METHOD (fn facts =>
   293 fun clasimp_meth' tac prems ctxt = Method.METHOD (fn facts =>
   214 
   305 
   215 
   306 
   216 (* theory setup *)
   307 (* theory setup *)
   217 
   308 
   218 val setup =
   309 val setup =
   219  [Method.add_methods
   310  [Attrib.add_attributes
       
   311   [("iff", iff_attr, "declare simplifier / classical rules")],
       
   312   Method.add_methods
   220    [("fastsimp", clasimp_method' fast_simp_tac, "combined fast and simp"),
   313    [("fastsimp", clasimp_method' fast_simp_tac, "combined fast and simp"),
   221     ("slowsimp", clasimp_method' slow_simp_tac, "combined slow and simp"),
   314     ("slowsimp", clasimp_method' slow_simp_tac, "combined slow and simp"),
   222     ("bestsimp", clasimp_method' best_simp_tac, "combined best and simp"),
   315     ("bestsimp", clasimp_method' best_simp_tac, "combined best and simp"),
   223     ("force", clasimp_method' force_tac, "force"),
   316     ("force", clasimp_method' force_tac, "force"),
   224     ("auto", auto_args auto_meth, "auto"),
   317     ("auto", auto_args auto_meth, "auto"),
   225     ("clarsimp", clasimp_method' (CHANGED oo clarsimp_tac), "clarify simplified goal")]];
   318     ("clarsimp", clasimp_method' (CHANGED oo clarsimp_tac), "clarify simplified goal")]];
   226 
   319 
   227 
       
   228 end;
   320 end;