Introduction of rotate_rule
authorpaulson
Fri Feb 21 15:30:41 1997 +0100 (1997-02-21)
changeset 2671510d94c71dda
parent 2670 009798ca267b
child 2672 85d7e800d754
Introduction of rotate_rule
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Fri Feb 21 15:15:26 1997 +0100
     1.2 +++ b/src/Pure/thm.ML	Fri Feb 21 15:30:41 1997 +0100
     1.3 @@ -23,6 +23,7 @@
     1.4                                      maxidx: int}
     1.5    val term_of           : cterm -> term
     1.6    val cterm_of          : Sign.sg -> term -> cterm
     1.7 +  val ctyp_of_term      : cterm -> ctyp
     1.8    val read_cterm        : Sign.sg -> string * typ -> cterm
     1.9    val read_cterms       : Sign.sg -> string list * typ list -> cterm list
    1.10    val cterm_fun         : (term -> term) -> (cterm -> cterm)
    1.11 @@ -37,43 +38,44 @@
    1.12  
    1.13    (*theories*)
    1.14  
    1.15 -  (*proof terms [must duplicate declaration as a specification]*)
    1.16 +  (*proof terms [must DUPLICATE declaration as a specification]*)
    1.17    datatype deriv_kind = MinDeriv | ThmDeriv | FullDeriv;
    1.18    val keep_derivs       : deriv_kind ref
    1.19    datatype rule = 
    1.20        MinProof                          
    1.21      | Oracle of theory * Sign.sg * exn
    1.22 -    | Axiom             of theory * string
    1.23 -    | Theorem           of string       
    1.24 -    | Assume            of cterm
    1.25 -    | Implies_intr      of cterm
    1.26 +    | Axiom               of theory * string
    1.27 +    | Theorem             of string       
    1.28 +    | Assume              of cterm
    1.29 +    | Implies_intr        of cterm
    1.30      | Implies_intr_shyps
    1.31      | Implies_intr_hyps
    1.32      | Implies_elim 
    1.33 -    | Forall_intr       of cterm
    1.34 -    | Forall_elim       of cterm
    1.35 -    | Reflexive         of cterm
    1.36 +    | Forall_intr         of cterm
    1.37 +    | Forall_elim         of cterm
    1.38 +    | Reflexive           of cterm
    1.39      | Symmetric 
    1.40      | Transitive
    1.41 -    | Beta_conversion   of cterm
    1.42 +    | Beta_conversion     of cterm
    1.43      | Extensional
    1.44 -    | Abstract_rule     of string * cterm
    1.45 +    | Abstract_rule       of string * cterm
    1.46      | Combination
    1.47      | Equal_intr
    1.48      | Equal_elim
    1.49 -    | Trivial           of cterm
    1.50 -    | Lift_rule         of cterm * int 
    1.51 -    | Assumption        of int * Envir.env option
    1.52 -    | Instantiate       of (indexname * ctyp) list * (cterm * cterm) list
    1.53 -    | Bicompose         of bool * bool * int * int * Envir.env
    1.54 -    | Flexflex_rule     of Envir.env            
    1.55 -    | Class_triv        of theory * class       
    1.56 +    | Trivial             of cterm
    1.57 +    | Lift_rule           of cterm * int 
    1.58 +    | Assumption          of int * Envir.env option
    1.59 +    | Rotate_rule         of int * int
    1.60 +    | Instantiate         of (indexname * ctyp) list * (cterm * cterm) list
    1.61 +    | Bicompose           of bool * bool * int * int * Envir.env
    1.62 +    | Flexflex_rule       of Envir.env            
    1.63 +    | Class_triv          of theory * class       
    1.64      | VarifyT
    1.65      | FreezeT
    1.66 -    | RewriteC          of cterm
    1.67 -    | CongC             of cterm
    1.68 -    | Rewrite_cterm     of cterm
    1.69 -    | Rename_params_rule of string list * int;
    1.70 +    | RewriteC            of cterm
    1.71 +    | CongC               of cterm
    1.72 +    | Rewrite_cterm       of cterm
    1.73 +    | Rename_params_rule  of string list * int;
    1.74  
    1.75    type deriv   (* = rule mtree *)
    1.76  
    1.77 @@ -130,6 +132,7 @@
    1.78    val lift_rule         : (thm * int) -> thm -> thm
    1.79    val assumption        : int -> thm -> thm Sequence.seq
    1.80    val eq_assumption     : int -> thm -> thm
    1.81 +  val rotate_rule       : int -> int -> thm -> thm
    1.82    val rename_params_rule: string list * int -> thm -> thm
    1.83    val bicompose         : bool -> bool * thm * int ->
    1.84      int -> thm -> thm Sequence.seq
    1.85 @@ -192,6 +195,8 @@
    1.86  fun rep_cterm (Cterm args) = args;
    1.87  fun term_of (Cterm {t, ...}) = t;
    1.88  
    1.89 +fun ctyp_of_term (Cterm {sign, T, ...}) = Ctyp {sign=sign, T=T};
    1.90 +
    1.91  (*create a cterm by checking a "raw" term with respect to a signature*)
    1.92  fun cterm_of sign tm =
    1.93    let val (t, T, maxidx) = Sign.certify_term sign tm
    1.94 @@ -315,6 +320,7 @@
    1.95            Use cterm instead of thm to avoid mutual recursion.*)
    1.96    | Lift_rule           of cterm * int 
    1.97    | Assumption          of int * Envir.env option (*includes eq_assumption*)
    1.98 +  | Rotate_rule         of int * int
    1.99    | Instantiate         of (indexname * ctyp) list * (cterm * cterm) list
   1.100    | Bicompose           of bool * bool * int * int * Envir.env
   1.101    | Flexflex_rule       of Envir.env            (*identifies unifier chosen*)
   1.102 @@ -520,7 +526,7 @@
   1.103          val tfrees = map (TFree o rpair logicS) names;
   1.104  
   1.105          fun mk_insort (T, S) = map (Logic.mk_inclass o pair T) S;
   1.106 -        val sort_hyps = flat (map2 mk_insort (tfrees, xshyps));
   1.107 +        val sort_hyps = List.concat (map2 mk_insort (tfrees, xshyps));
   1.108        in
   1.109          Thm {sign = sign, 
   1.110               der = infer_derivs (Implies_intr_shyps, [der]), 
   1.111 @@ -1026,7 +1032,8 @@
   1.112    end
   1.113    handle TERM _ =>
   1.114             raise THM("instantiate: incompatible signatures",0,[th])
   1.115 -       | TYPE _ => raise THM("instantiate: type conflict", 0, [th]);
   1.116 +       | TYPE (msg,_,_) => raise THM("instantiate: type conflict: " ^ msg, 
   1.117 +				     0, [th]);
   1.118  
   1.119  (*The trivial implication A==>A, justified by assume and forall rules.
   1.120    A can contain Vars, not so for assume!   *)
   1.121 @@ -1160,6 +1167,31 @@
   1.122    end;
   1.123  
   1.124  
   1.125 +(*For rotate_tac: fast rotation of assumptions of subgoal i*)
   1.126 +fun rotate_rule k i state =
   1.127 +  let val Thm{sign,der,maxidx,hyps,prop,shyps} = state;
   1.128 +      val (tpairs, Bs, Bi, C) = dest_state(state,i)
   1.129 +      val params = Logic.strip_params Bi
   1.130 +      and asms   = Logic.strip_assums_hyp Bi
   1.131 +      and concl  = Logic.strip_assums_concl Bi
   1.132 +      val n      = length asms
   1.133 +      fun rot m  = if 0=m orelse m=n then Bi
   1.134 +		   else if 0<m andalso m<n 
   1.135 +		   then list_all 
   1.136 +			   (params, 
   1.137 +			    Logic.list_implies(List.drop(asms, m) @ 
   1.138 +					       List.take(asms, m),
   1.139 +					       concl))
   1.140 +		   else raise THM("rotate_rule", m, [state])
   1.141 +  in  Thm{sign = sign, 
   1.142 +	  der = infer_derivs (Rotate_rule (k,i), [der]),
   1.143 +	  maxidx = maxidx,
   1.144 +	  shyps = shyps,
   1.145 +	  hyps = hyps,
   1.146 +	  prop = Logic.rule_of(tpairs, Bs@[rot (if k<0 then n+k else k)], C)}
   1.147 +  end;
   1.148 +
   1.149 +
   1.150  (** User renaming of parameters in a subgoal **)
   1.151  
   1.152  (*Calls error rather than raising an exception because it is intended
   1.153 @@ -1486,7 +1518,7 @@
   1.154        andalso not (is_Var elhs);
   1.155    in
   1.156      if not ((term_vars erhs) subset
   1.157 -        (union_term (term_vars elhs, flat(map term_vars prems)))) then
   1.158 +        (union_term (term_vars elhs, List.concat(map term_vars prems)))) then
   1.159        (prtm_warning "extra Var(s) on rhs" sign prop; None)
   1.160      else if not perm andalso loops sign prems (elhs, erhs) then
   1.161        (prtm_warning "ignoring looping rewrite rule" sign prop; None)
   1.162 @@ -1662,8 +1694,8 @@
   1.163      val (elhs, erhs) = Logic.dest_equals econcl;
   1.164    in
   1.165      if not ((term_vars erhs) subset
   1.166 -        (union_term (term_vars elhs, flat(map term_vars prems)))) then
   1.167 -      (prtm_warning "extra Var(s) on rhs" sign prop; [])
   1.168 +        (union_term (term_vars elhs, List.concat(map term_vars prems)))) 
   1.169 +    then (prtm_warning "extra Var(s) on rhs" sign prop; [])
   1.170      else [{thm = thm, lhs = lhs, perm = false}]
   1.171    end;
   1.172