Tidying of signature. More robust renaming in freeze_thaw.
authorpaulson
Thu Jun 05 13:52:43 1997 +0200 (1997-06-05)
changeset 3409c0466958df5d
parent 3408 98a2d517cabe
child 3410 98f59f455d57
Tidying of signature. More robust renaming in freeze_thaw.
New tactic distinct_subgoals_tac
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Thu Jun 05 13:30:24 1997 +0200
     1.2 +++ b/src/Pure/tactic.ML	Thu Jun 05 13:52:43 1997 +0200
     1.3 @@ -8,82 +8,84 @@
     1.4  
     1.5  signature TACTIC =
     1.6    sig
     1.7 -  val ares_tac: thm list -> int -> tactic
     1.8 +  val ares_tac		: thm list -> int -> tactic
     1.9    val asm_rewrite_goal_tac:
    1.10          bool*bool -> (meta_simpset -> tactic) -> meta_simpset -> int -> tactic
    1.11 -  val assume_tac: int -> tactic
    1.12 -  val atac: int ->tactic
    1.13 +  val assume_tac	: int -> tactic
    1.14 +  val atac	: int ->tactic
    1.15    val bimatch_from_nets_tac: 
    1.16        (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic
    1.17 -  val bimatch_tac: (bool*thm)list -> int -> tactic
    1.18 +  val bimatch_tac	: (bool*thm)list -> int -> tactic
    1.19    val biresolve_from_nets_tac: 
    1.20        (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic
    1.21 -  val biresolve_tac: (bool*thm)list -> int -> tactic
    1.22 -  val build_net: thm list -> (int*thm) Net.net
    1.23 +  val biresolve_tac	: (bool*thm)list -> int -> tactic
    1.24 +  val build_net	: thm list -> (int*thm) Net.net
    1.25    val build_netpair:    (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net ->
    1.26        (bool*thm)list -> (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net
    1.27 -  val compose_inst_tac: (string*string)list -> (bool*thm*int) -> int -> tactic
    1.28 -  val compose_tac: (bool * thm * int) -> int -> tactic 
    1.29 -  val cut_facts_tac: thm list -> int -> tactic
    1.30 -  val cut_inst_tac: (string*string)list -> thm -> int -> tactic   
    1.31 -  val defer_tac : int -> tactic
    1.32 -  val dmatch_tac: thm list -> int -> tactic
    1.33 -  val dresolve_tac: thm list -> int -> tactic
    1.34 -  val dres_inst_tac: (string*string)list -> thm -> int -> tactic   
    1.35 -  val dtac: thm -> int ->tactic
    1.36 -  val etac: thm -> int ->tactic
    1.37 -  val eq_assume_tac: int -> tactic   
    1.38 -  val ematch_tac: thm list -> int -> tactic
    1.39 -  val eresolve_tac: thm list -> int -> tactic
    1.40 -  val eres_inst_tac: (string*string)list -> thm -> int -> tactic   
    1.41 -  val filter_thms: (term*term->bool) -> int*term*thm list -> thm list
    1.42 -  val filt_resolve_tac: thm list -> int -> int -> tactic
    1.43 -  val flexflex_tac: tactic
    1.44 -  val fold_goals_tac: thm list -> tactic
    1.45 -  val fold_tac: thm list -> tactic
    1.46 -  val forward_tac: thm list -> int -> tactic   
    1.47 -  val forw_inst_tac: (string*string)list -> thm -> int -> tactic
    1.48 -  val freeze_thaw: thm -> thm * (thm -> thm)
    1.49 -  val insert_tagged_brl:  ('a*(bool*thm)) * 
    1.50 -                    (('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) ->
    1.51 -                    ('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net
    1.52 -  val delete_tagged_brl:  (bool*thm) * 
    1.53 -                    ((int*(bool*thm))Net.net * (int*(bool*thm))Net.net) ->
    1.54 +  val compose_inst_tac	: (string*string)list -> (bool*thm*int) -> 
    1.55 +                          int -> tactic
    1.56 +  val compose_tac	: (bool * thm * int) -> int -> tactic 
    1.57 +  val cut_facts_tac	: thm list -> int -> tactic
    1.58 +  val cut_inst_tac	: (string*string)list -> thm -> int -> tactic   
    1.59 +  val defer_tac 	: int -> tactic
    1.60 +  val distinct_subgoals_tac	: tactic
    1.61 +  val dmatch_tac	: thm list -> int -> tactic
    1.62 +  val dresolve_tac	: thm list -> int -> tactic
    1.63 +  val dres_inst_tac	: (string*string)list -> thm -> int -> tactic   
    1.64 +  val dtac		: thm -> int ->tactic
    1.65 +  val etac		: thm -> int ->tactic
    1.66 +  val eq_assume_tac	: int -> tactic   
    1.67 +  val ematch_tac	: thm list -> int -> tactic
    1.68 +  val eresolve_tac	: thm list -> int -> tactic
    1.69 +  val eres_inst_tac	: (string*string)list -> thm -> int -> tactic   
    1.70 +  val filter_thms	: (term*term->bool) -> int*term*thm list -> thm list
    1.71 +  val filt_resolve_tac	: thm list -> int -> int -> tactic
    1.72 +  val flexflex_tac	: tactic
    1.73 +  val fold_goals_tac	: thm list -> tactic
    1.74 +  val fold_tac		: thm list -> tactic
    1.75 +  val forward_tac	: thm list -> int -> tactic   
    1.76 +  val forw_inst_tac	: (string*string)list -> thm -> int -> tactic
    1.77 +  val freeze_thaw	: thm -> thm * (thm -> thm)
    1.78 +  val insert_tagged_brl : ('a*(bool*thm)) * 
    1.79 +                          (('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) ->
    1.80 +                          ('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net
    1.81 +  val delete_tagged_brl	: (bool*thm) * 
    1.82 +                         ((int*(bool*thm))Net.net * (int*(bool*thm))Net.net) ->
    1.83                      (int*(bool*thm))Net.net * (int*(bool*thm))Net.net
    1.84 -  val is_fact: thm -> bool
    1.85 -  val lessb: (bool * thm) * (bool * thm) -> bool
    1.86 -  val lift_inst_rule: thm * int * (string*string)list * thm -> thm
    1.87 -  val make_elim: thm -> thm
    1.88 -  val match_from_net_tac: (int*thm) Net.net -> int -> tactic
    1.89 -  val match_tac: thm list -> int -> tactic
    1.90 -  val metacut_tac: thm -> int -> tactic   
    1.91 -  val net_bimatch_tac: (bool*thm) list -> int -> tactic
    1.92 -  val net_biresolve_tac: (bool*thm) list -> int -> tactic
    1.93 -  val net_match_tac: thm list -> int -> tactic
    1.94 -  val net_resolve_tac: thm list -> int -> tactic
    1.95 -  val orderlist: (int * 'a) list -> 'a list
    1.96 -  val PRIMITIVE: (thm -> thm) -> tactic  
    1.97 -  val PRIMSEQ: (thm -> thm Sequence.seq) -> tactic  
    1.98 -  val prune_params_tac: tactic
    1.99 -  val rename_tac: string -> int -> tactic
   1.100 -  val rename_last_tac: string -> string list -> int -> tactic
   1.101 -  val resolve_from_net_tac: (int*thm) Net.net -> int -> tactic
   1.102 -  val resolve_tac: thm list -> int -> tactic
   1.103 -  val res_inst_tac: (string*string)list -> thm -> int -> tactic   
   1.104 -  val rewrite_goals_tac: thm list -> tactic
   1.105 -  val rewrite_tac: thm list -> tactic
   1.106 -  val rewtac: thm -> tactic
   1.107 -  val rotate_tac: int -> int -> tactic
   1.108 -  val rtac: thm -> int -> tactic
   1.109 -  val rule_by_tactic: tactic -> thm -> thm
   1.110 -  val subgoal_tac: string -> int -> tactic
   1.111 -  val subgoals_tac: string list -> int -> tactic
   1.112 -  val subgoals_of_brl: bool * thm -> int
   1.113 -  val term_lift_inst_rule:
   1.114 +  val is_fact		: thm -> bool
   1.115 +  val lessb		: (bool * thm) * (bool * thm) -> bool
   1.116 +  val lift_inst_rule	: thm * int * (string*string)list * thm -> thm
   1.117 +  val make_elim		: thm -> thm
   1.118 +  val match_from_net_tac	: (int*thm) Net.net -> int -> tactic
   1.119 +  val match_tac	: thm list -> int -> tactic
   1.120 +  val metacut_tac	: thm -> int -> tactic   
   1.121 +  val net_bimatch_tac	: (bool*thm) list -> int -> tactic
   1.122 +  val net_biresolve_tac	: (bool*thm) list -> int -> tactic
   1.123 +  val net_match_tac	: thm list -> int -> tactic
   1.124 +  val net_resolve_tac	: thm list -> int -> tactic
   1.125 +  val orderlist		: (int * 'a) list -> 'a list
   1.126 +  val PRIMITIVE		: (thm -> thm) -> tactic  
   1.127 +  val PRIMSEQ		: (thm -> thm Sequence.seq) -> tactic  
   1.128 +  val prune_params_tac	: tactic
   1.129 +  val rename_tac	: string -> int -> tactic
   1.130 +  val rename_last_tac	: string -> string list -> int -> tactic
   1.131 +  val resolve_from_net_tac	: (int*thm) Net.net -> int -> tactic
   1.132 +  val resolve_tac	: thm list -> int -> tactic
   1.133 +  val res_inst_tac	: (string*string)list -> thm -> int -> tactic   
   1.134 +  val rewrite_goals_tac	: thm list -> tactic
   1.135 +  val rewrite_tac	: thm list -> tactic
   1.136 +  val rewtac		: thm -> tactic
   1.137 +  val rotate_tac	: int -> int -> tactic
   1.138 +  val rtac		: thm -> int -> tactic
   1.139 +  val rule_by_tactic	: tactic -> thm -> thm
   1.140 +  val subgoal_tac	: string -> int -> tactic
   1.141 +  val subgoals_tac	: string list -> int -> tactic
   1.142 +  val subgoals_of_brl	: bool * thm -> int
   1.143 +  val term_lift_inst_rule	:
   1.144        thm * int * (indexname*typ)list * ((indexname*typ)*term)list  * thm
   1.145        -> thm
   1.146 -  val thin_tac: string -> int -> tactic
   1.147 -  val trace_goalno_tac: (int -> tactic) -> int -> tactic
   1.148 +  val thin_tac		: string -> int -> tactic
   1.149 +  val trace_goalno_tac	: (int -> tactic) -> int -> tactic
   1.150    end;
   1.151  
   1.152  
   1.153 @@ -99,24 +101,25 @@
   1.154  
   1.155  
   1.156  (*Convert all Vars in a theorem to Frees.  Also return a function for 
   1.157 -  reversing that operation.  DOES NOT WORK FOR TYPE VARIABLES.*)
   1.158 -local
   1.159 -    fun string_of (a,0) = a
   1.160 -      | string_of (a,i) = a ^ "_" ^ string_of_int i;
   1.161 -in
   1.162 -  fun freeze_thaw th =
   1.163 -    let val fth = freezeT th
   1.164 -	val vary = variant (add_term_names (#prop(rep_thm fth), []))
   1.165 -	val {prop,sign,...} = rep_thm fth
   1.166 -	fun mk_inst (Var(v,T)) = 
   1.167 -	    (cterm_of sign (Var(v,T)),
   1.168 -	     cterm_of sign (Free(vary (string_of v), T)))
   1.169 -	val insts = map mk_inst (term_vars prop)
   1.170 -	fun thaw th' = 
   1.171 -	    th' |> forall_intr_list (map #2 insts)
   1.172 -		|> forall_elim_list (map #1 insts)
   1.173 -    in  (instantiate ([],insts) fth, thaw)  end;
   1.174 -end;
   1.175 +  reversing that operation.  DOES NOT WORK FOR TYPE VARIABLES.
   1.176 +  Similar code in type/freeze_thaw*)
   1.177 +fun freeze_thaw th =
   1.178 +  let val fth = freezeT th
   1.179 +      val {prop,sign,...} = rep_thm fth
   1.180 +      val used = add_term_names (prop, [])
   1.181 +      and vars = term_vars prop
   1.182 +      fun newName (Var(ix,_), (pairs,used)) = 
   1.183 +	    let val v = variant used (string_of_indexname ix)
   1.184 +	    in  ((ix,v)::pairs, v::used)  end;
   1.185 +      val (alist, _) = foldr newName (vars, ([], used))
   1.186 +      fun mk_inst (Var(v,T)) = 
   1.187 +	  (cterm_of sign (Var(v,T)),
   1.188 +	   cterm_of sign (Free(the (assoc(alist,v)), T)))
   1.189 +      val insts = map mk_inst vars
   1.190 +      fun thaw th' = 
   1.191 +	  th' |> forall_intr_list (map #2 insts)
   1.192 +	      |> forall_elim_list (map #1 insts)
   1.193 +  in  (instantiate ([],insts) fth, thaw)  end;
   1.194  
   1.195  
   1.196  (*Rotates the given subgoal to be the last.  Useful when re-playing
   1.197 @@ -202,6 +205,21 @@
   1.198  (*Smash all flex-flex disagreement pairs in the proof state.*)
   1.199  val flexflex_tac = PRIMSEQ flexflex_rule;
   1.200  
   1.201 +
   1.202 +(*Remove duplicate subgoals.  By Mark Staples*)
   1.203 +local
   1.204 +fun cterm_aconv (a,b) = #t (rep_cterm a) aconv #t (rep_cterm b);
   1.205 +in
   1.206 +fun distinct_subgoals_tac state = 
   1.207 +    let val (frozth,thawfn) = freeze_thaw state
   1.208 +	val froz_prems = cprems_of frozth
   1.209 +	val assumed = implies_elim_list frozth (map assume froz_prems)
   1.210 +	val implied = implies_intr_list (gen_distinct cterm_aconv froz_prems)
   1.211 +					assumed;
   1.212 +    in  Sequence.single (thawfn implied)  end
   1.213 +end; 
   1.214 +
   1.215 +
   1.216  (*Lift and instantiate a rule wrt the given state and subgoal number *)
   1.217  fun lift_inst_rule (st, i, sinsts, rule) =
   1.218  let val {maxidx,sign,...} = rep_thm st