src/Provers/classical.ML
changeset 1073 b3f190995bc9
parent 1010 a7693f30065d
child 1231 91d2c1bb5803
equal deleted inserted replaced
1072:0140ff702b23 1073:b3f190995bc9
    31 
    31 
    32 
    32 
    33 signature CLASSICAL =
    33 signature CLASSICAL =
    34   sig
    34   sig
    35   type claset
    35   type claset
       
    36   type netpair
    36   val empty_cs		: claset
    37   val empty_cs		: claset
    37   val addDs 		: claset * thm list -> claset
    38   val addDs 		: claset * thm list -> claset
    38   val addEs 		: claset * thm list -> claset
    39   val addEs 		: claset * thm list -> claset
    39   val addIs 		: claset * thm list -> claset
    40   val addIs 		: claset * thm list -> claset
    40   val addSDs		: claset * thm list -> claset
    41   val addSDs		: claset * thm list -> claset
    44   val compwrapper 	: claset * (tactic->tactic) -> claset
    45   val compwrapper 	: claset * (tactic->tactic) -> claset
    45   val addbefore 	: claset * tactic -> claset
    46   val addbefore 	: claset * tactic -> claset
    46   val addafter 		: claset * tactic -> claset
    47   val addafter 		: claset * tactic -> claset
    47 
    48 
    48   val print_cs		: claset -> unit
    49   val print_cs		: claset -> unit
    49   val rep_claset	: claset -> {safeIs: thm list, safeEs: thm list, 
    50   val rep_claset	: 
    50 				     hazIs: thm list, hazEs: thm list,
    51       claset -> {safeIs: thm list, safeEs: thm list, 
    51 				     wrapper: tactic -> tactic}
    52 		 hazIs: thm list, hazEs: thm list,
       
    53 		 wrapper: tactic -> tactic,
       
    54 		 safe0_netpair: netpair, safep_netpair: netpair,
       
    55 		 haz_netpair: netpair, dup_netpair: netpair}
    52   val getwrapper	: claset -> tactic -> tactic
    56   val getwrapper	: claset -> tactic -> tactic
    53   val THEN_MAYBE	: tactic * tactic -> tactic
    57   val THEN_MAYBE	: tactic * tactic -> tactic
    54 
    58 
    55   val best_tac 		: claset -> int -> tactic
    59   val best_tac 		: claset -> int -> tactic
    56   val contr_tac 	: int -> tactic
    60   val contr_tac 	: int -> tactic
   116 fun dup_intr th = standard (th RS classical);
   120 fun dup_intr th = standard (th RS classical);
   117 
   121 
   118 fun dup_elim th = th RSN (2, revcut_rl) |> assumption 2 |> Sequence.hd |> 
   122 fun dup_elim th = th RSN (2, revcut_rl) |> assumption 2 |> Sequence.hd |> 
   119                   rule_by_tactic (TRYALL (etac revcut_rl));
   123                   rule_by_tactic (TRYALL (etac revcut_rl));
   120 
   124 
       
   125 
   121 (*** Classical rule sets ***)
   126 (*** Classical rule sets ***)
   122 
   127 
   123 type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net;
   128 type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net;
   124 
   129 
   125 datatype claset =
   130 datatype claset =
   131 	 safe0_netpair	: netpair,		(*nets for trivial cases*)
   136 	 safe0_netpair	: netpair,		(*nets for trivial cases*)
   132 	 safep_netpair	: netpair,		(*nets for >0 subgoals*)
   137 	 safep_netpair	: netpair,		(*nets for >0 subgoals*)
   133 	 haz_netpair  	: netpair,		(*nets for unsafe rules*)
   138 	 haz_netpair  	: netpair,		(*nets for unsafe rules*)
   134 	 dup_netpair	: netpair};		(*nets for duplication*)
   139 	 dup_netpair	: netpair};		(*nets for duplication*)
   135 
   140 
   136 fun rep_claset (CS{safeIs,safeEs,hazIs,hazEs,wrapper,...}) = 
   141 (*Desired invariants are
   137     {safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs, wrapper=wrapper};
       
   138 
       
   139 fun getwrapper (CS{wrapper,...}) = wrapper;
       
   140 
       
   141 (*For use with biresolve_tac.  Combines intr rules with swap to handle negated
       
   142   assumptions.  Pairs elim rules with true.  Sorts the list of pairs by 
       
   143   the number of new subgoals generated. *)
       
   144 fun joinrules (intrs,elims) =  
       
   145   sort lessb 
       
   146     (map (pair true) (elims @ swapify intrs)  @
       
   147      map (pair false) intrs);
       
   148 
       
   149 val build = build_netpair(Net.empty,Net.empty);
       
   150 
       
   151 (*Make a claset from the four kinds of rules*)
       
   152 fun make_cs {safeIs,safeEs,hazIs,hazEs,wrapper} =
       
   153   let val (safe0_brls, safep_brls) = (*0 subgoals vs 1 or more*)
       
   154           take_prefix (fn brl => subgoals_of_brl brl=0)
       
   155              (joinrules(safeIs, safeEs))
       
   156   in CS{safeIs = safeIs, 
       
   157         safeEs = safeEs,
       
   158 	hazIs = hazIs,
       
   159 	hazEs = hazEs,
       
   160 	wrapper = wrapper,
       
   161 	safe0_netpair = build safe0_brls,
   142 	safe0_netpair = build safe0_brls,
   162 	safep_netpair = build safep_brls,
   143 	safep_netpair = build safep_brls,
   163 	haz_netpair = build (joinrules(hazIs, hazEs)),
   144 	haz_netpair = build (joinrules(hazIs, hazEs)),
   164 	dup_netpair = build (joinrules(map dup_intr hazIs, 
   145 	dup_netpair = build (joinrules(map dup_intr hazIs, 
   165 				       map dup_elim hazEs))}
   146 				       map dup_elim hazEs))}
   166   end;
   147 
   167 
   148 where build = build_netpair(Net.empty,Net.empty), 
   168 (*** Manipulation of clasets ***)
   149       safe0_brls contains all brules that solve the subgoal, and
   169 
   150       safep_brls contains all brules that generate 1 or more new subgoals.
   170 val empty_cs = make_cs{safeIs=[], safeEs=[], hazIs=[], hazEs=[], wrapper=I};
   151 Nets must be built incrementally, to save space and time.
       
   152 *)
       
   153 
       
   154 val empty_cs = 
       
   155   CS{safeIs	= [],
       
   156      safeEs	= [],
       
   157      hazIs	= [],
       
   158      hazEs	= [],
       
   159      wrapper 	= I,
       
   160      safe0_netpair = (Net.empty,Net.empty),
       
   161      safep_netpair = (Net.empty,Net.empty),
       
   162      haz_netpair   = (Net.empty,Net.empty),
       
   163      dup_netpair   = (Net.empty,Net.empty)};
   171 
   164 
   172 fun print_cs (CS{safeIs,safeEs,hazIs,hazEs,...}) =
   165 fun print_cs (CS{safeIs,safeEs,hazIs,hazEs,...}) =
   173  (writeln"Introduction rules";  prths hazIs;
   166  (writeln"Introduction rules";  	prths hazIs;
   174   writeln"Safe introduction rules";  prths safeIs;
   167   writeln"Safe introduction rules";  	prths safeIs;
   175   writeln"Elimination rules";  prths hazEs;
   168   writeln"Elimination rules";  		prths hazEs;
   176   writeln"Safe elimination rules";  prths safeEs;
   169   writeln"Safe elimination rules";  	prths safeEs;
   177   ());
   170   ());
   178 
   171 
   179 (** Adding new (un)safe introduction or elimination rules 
   172 fun rep_claset (CS args) = args;
   180     In case of overlap, new rules are tried BEFORE old ones
   173 
       
   174 fun getwrapper (CS{wrapper,...}) = wrapper;
       
   175 
       
   176 
       
   177 (** Adding (un)safe introduction or elimination rules.
       
   178 
       
   179     In case of overlap, new rules are tried BEFORE old ones!!
   181 **)
   180 **)
   182 
   181 
   183 fun (CS{safeIs,safeEs,hazIs,hazEs,wrapper,...}) addSIs ths =
   182 (*For use with biresolve_tac.  Combines intr rules with swap to handle negated
   184   make_cs {safeIs=ths@safeIs, 
   183   assumptions.  Pairs elim rules with true. *)
   185 	   safeEs=safeEs, hazIs=hazIs, hazEs=hazEs, wrapper=wrapper};
   184 fun joinrules (intrs,elims) =  
   186 
   185     (map (pair true) (elims @ swapify intrs)  @
   187 fun (CS{safeIs,safeEs,hazIs,hazEs,wrapper,...}) addSEs ths =
   186      map (pair false) intrs);
   188   make_cs {safeEs=ths@safeEs, 
   187 
   189 	   safeIs=safeIs, hazIs=hazIs, hazEs=hazEs, wrapper=wrapper};
   188 (*Priority: prefer rules with fewest subgoals, 
       
   189               then rules added most recently.*)
       
   190 fun tag_brls k [] = []
       
   191   | tag_brls k (brl::brls) =
       
   192       (1000000*subgoals_of_brl brl + k, brl) :: 
       
   193       tag_brls (k+1) brls;
       
   194 
       
   195 fun insert_tagged_list kbrls np = foldr insert_tagged_brl (kbrls, np);
       
   196 
       
   197 (*Insert into netpair that already has nI intr rules and nE elim rules.
       
   198   Count the intr rules double (to account for swapify).  Negate to give the
       
   199   new insertions the lowest priority.*)
       
   200 fun insert (nI,nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules;
       
   201 
       
   202 
       
   203 (** Safe rules **)
       
   204 
       
   205 fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
       
   206 	safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) 
       
   207     addSIs  ths  =
       
   208   let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
       
   209           take_prefix (fn rl => nprems_of rl=0) ths
       
   210       val nI = length safeIs + length ths
       
   211       and nE = length safeEs
       
   212   in CS{safeIs	= ths@safeIs,
       
   213         safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair,
       
   214 	safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair,
       
   215 	safeEs	= safeEs,
       
   216 	hazIs	= hazIs,
       
   217 	hazEs	= hazEs,
       
   218 	wrapper = wrapper,
       
   219 	haz_netpair = haz_netpair,
       
   220 	dup_netpair = dup_netpair}
       
   221   end;
       
   222 
       
   223 fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
       
   224 	safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) 
       
   225     addSEs  ths  =
       
   226   let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
       
   227           take_prefix (fn rl => nprems_of rl=1) ths
       
   228       val nI = length safeIs
       
   229       and nE = length safeEs + length ths
       
   230   in 
       
   231      CS{safeEs	= ths@safeEs,
       
   232         safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair,
       
   233 	safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair,
       
   234 	safeIs	= safeIs,
       
   235 	hazIs	= hazIs,
       
   236 	hazEs	= hazEs,
       
   237 	wrapper = wrapper,
       
   238 	haz_netpair = haz_netpair,
       
   239 	dup_netpair = dup_netpair}
       
   240   end;
   190 
   241 
   191 fun cs addSDs ths = cs addSEs (map make_elim ths);
   242 fun cs addSDs ths = cs addSEs (map make_elim ths);
   192 
   243 
   193 fun (CS{safeIs,safeEs,hazIs,hazEs,wrapper,...}) addIs ths =
   244 
   194   make_cs {hazIs=ths@hazIs, 
   245 (** Hazardous (unsafe) rules **)
   195 	   safeIs=safeIs, safeEs=safeEs, hazEs=hazEs, wrapper=wrapper};
   246 
   196 
   247 fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
   197 fun (CS{safeIs,safeEs,hazIs,hazEs,wrapper,...}) addEs ths =
   248 	safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) 
   198   make_cs {hazEs=ths@hazEs,
   249     addIs  ths  =
   199 	   safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, wrapper=wrapper};
   250   let val nI = length hazIs + length ths
       
   251       and nE = length hazEs
       
   252   in 
       
   253      CS{hazIs	= ths@hazIs,
       
   254 	haz_netpair = insert (nI,nE) (ths, []) haz_netpair,
       
   255 	dup_netpair = insert (nI,nE) (map dup_intr ths, []) dup_netpair,
       
   256 	safeIs 	= safeIs, 
       
   257 	safeEs	= safeEs,
       
   258 	hazEs	= hazEs,
       
   259 	wrapper 	= wrapper,
       
   260 	safe0_netpair = safe0_netpair,
       
   261 	safep_netpair = safep_netpair}
       
   262   end;
       
   263 
       
   264 fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
       
   265 	safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) 
       
   266     addEs  ths  =
       
   267   let val nI = length hazIs 
       
   268       and nE = length hazEs + length ths
       
   269   in 
       
   270      CS{hazEs	= ths@hazEs,
       
   271 	haz_netpair = insert (nI,nE) ([], ths) haz_netpair,
       
   272 	dup_netpair = insert (nI,nE) ([], map dup_elim ths) dup_netpair,
       
   273 	safeIs	= safeIs, 
       
   274 	safeEs	= safeEs,
       
   275 	hazIs	= hazIs,
       
   276 	wrapper	= wrapper,
       
   277 	safe0_netpair = safe0_netpair,
       
   278 	safep_netpair = safep_netpair}
       
   279   end;
   200 
   280 
   201 fun cs addDs ths = cs addEs (map make_elim ths);
   281 fun cs addDs ths = cs addEs (map make_elim ths);
   202 
   282 
       
   283 
   203 (** Setting or modifying the wrapper tactical **)
   284 (** Setting or modifying the wrapper tactical **)
   204 
   285 
   205 (*Set a new wrapper*)
   286 (*Set a new wrapper*)
   206 fun (CS{safeIs,safeEs,hazIs,hazEs,...}) setwrapper wrapper =
   287 fun (CS{safeIs, safeEs, hazIs, hazEs, 
   207   make_cs {wrapper=wrapper,
   288 	safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...}) 
   208 	   safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs};
   289     setwrapper new_wrapper  =
       
   290   CS{wrapper 	= new_wrapper,
       
   291      safeIs	= safeIs,
       
   292      safeEs	= safeEs,
       
   293      hazIs	= hazIs,
       
   294      hazEs	= hazEs,
       
   295      safe0_netpair = safe0_netpair,
       
   296      safep_netpair = safep_netpair,
       
   297      haz_netpair = haz_netpair,
       
   298      dup_netpair = dup_netpair};
   209 
   299 
   210 (*Compose a tactical with the existing wrapper*)
   300 (*Compose a tactical with the existing wrapper*)
   211 fun cs compwrapper wrapper' = cs setwrapper (wrapper' o getwrapper cs);
   301 fun cs compwrapper wrapper' = cs setwrapper (wrapper' o getwrapper cs);
   212 
   302 
   213 (*Execute tac1, but only execute tac2 if there are at least as many subgoals
   303 (*Execute tac1, but only execute tac2 if there are at least as many subgoals