src/Provers/simp.ML
author lcp
Tue, 18 Jan 1994 16:37:12 +0100
changeset 231 cb6a24451544
parent 1 c6a6e3db5353
child 611 11098f505bfe
permissions -rw-r--r--
Updated refs to old Sign functions
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title:      Provers/simp
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    Author:     Tobias Nipkow
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
Generic simplifier, suitable for most logics.  The only known exception is
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Constructive Type Theory.  The reflexivity axiom must be unconditional,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
namely a=a not a:A ==> a=a:A.  Used typedsimp.ML otherwise.  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
signature SIMP_DATA =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
sig
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
  val dest_red     : term -> term * term * term
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
  val mk_rew_rules : thm -> thm list
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
  val norm_thms    : (thm*thm) list (* [(?x>>norm(?x), norm(?x)>>?x), ...] *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
  val red1         : thm        (*  ?P>>?Q  ==>  ?P  ==>  ?Q  *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
  val red2         : thm        (*  ?P>>?Q  ==>  ?Q  ==>  ?P  *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
  val refl_thms    : thm list
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
  val subst_thms   : thm list   (* [ ?a>>?b ==> ?P(?a) ==> ?P(?b), ...] *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
  val trans_thms   : thm list
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
infix 4 addrews addcongs addsplits delrews delcongs setauto;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
signature SIMP =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
sig
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
  type simpset
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
  val empty_ss  : simpset
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
  val addcongs  : simpset * thm list -> simpset
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
  val addrews   : simpset * thm list -> simpset
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
  val addsplits : simpset * thm list -> simpset
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
  val delcongs  : simpset * thm list -> simpset
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
  val delrews   : simpset * thm list -> simpset
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
  val dest_ss   : simpset -> thm list * thm list
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
  val print_ss  : simpset -> unit
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
  val setauto   : simpset * (thm list -> int -> tactic) -> simpset
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
  val ASM_SIMP_TAC      : simpset -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
  val SPLIT_TAC          : simpset -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
  val SIMP_SPLIT2_TAC    : simpset -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
  val SIMP_THM          : simpset -> thm -> thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
  val SIMP_TAC          : simpset -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
  val mk_congs          : theory -> string list -> thm list
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
  val mk_typed_congs    : theory -> (string * string) list -> thm list
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
(* temporarily disabled:
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
  val extract_free_congs        : unit -> thm list
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
  val tracing   : bool ref
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
functor SimpFun (Simp_data: SIMP_DATA) : SIMP = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
local open Simp_data Logic in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
(*For taking apart reductions into left, right hand sides*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
val lhs_of = #2 o dest_red;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
val rhs_of = #3 o dest_red;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
(*** Indexing and filtering of theorems ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
fun eq_brl ((b1,th1),(b2,th2)) = b1=b2 andalso eq_thm(th1,th2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
(*insert a thm in a discrimination net by its lhs*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
fun lhs_insert_thm (th,net) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
    Net.insert_term((lhs_of (concl_of th), (false,th)), net, eq_brl)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
    handle  Net.INSERT => net;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
(*match subgoal i against possible theorems in the net.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
  Similar to match_from_nat_tac, but the net does not contain numbers;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
  rewrite rules are not ordered.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
fun net_tac net =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
  SUBGOAL(fn (prem,i) => 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
	  match_tac (Net.match_term net (strip_assums_concl prem)) i);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
(*match subgoal i against possible theorems indexed by lhs in the net*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
fun lhs_net_tac net =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
  SUBGOAL(fn (prem,i) => 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
	  bimatch_tac (Net.match_term net
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
		       (lhs_of (strip_assums_concl prem))) i);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
fun nth_subgoal i thm = nth_elem(i-1,prems_of thm);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
fun goal_concl i thm = strip_assums_concl(nth_subgoal i thm);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
fun lhs_of_eq i thm = lhs_of(goal_concl i thm)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
and rhs_of_eq i thm = rhs_of(goal_concl i thm);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
fun var_lhs(thm,i) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
let fun var(Var _) = true
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
      | var(Abs(_,_,t)) = var t
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
      | var(f$_) = var f
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
      | var _ = false;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
in var(lhs_of_eq i thm) end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
fun contains_op opns =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
    let fun contains(Const(s,_)) = s mem opns |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
            contains(s$t) = contains s orelse contains t |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
            contains(Abs(_,_,t)) = contains t |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
            contains _ = false;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
    in contains end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
fun may_match(match_ops,i) = contains_op match_ops o lhs_of_eq i;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
val (normI_thms,normE_thms) = split_list norm_thms;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
(*Get the norm constants from norm_thms*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
val norms =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
  let fun norm thm = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
      case lhs_of(concl_of thm) of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
	  Const(n,_)$_ => n
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
	| _ => (prths normE_thms; error"No constant in lhs of a norm_thm")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
  in map norm normE_thms end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
fun lhs_is_NORM(thm,i) = case lhs_of_eq i thm of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
	Const(s,_)$_ => s mem norms | _ => false;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
val refl_tac = resolve_tac refl_thms;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
fun find_res thms thm =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
    let fun find [] = (prths thms; error"Check Simp_Data")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
          | find(th::thms) = thm RS th handle _ => find thms
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
    in find thms end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
val mk_trans = find_res trans_thms;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
fun mk_trans2 thm =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
let fun mk[] = error"Check transitivity"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
      | mk(t::ts) = (thm RSN (2,t))  handle _  => mk ts
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
in mk trans_thms end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
(*Applies tactic and returns the first resulting state, FAILS if none!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
fun one_result(tac,thm) = case Sequence.pull(tapply(tac,thm)) of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
	Some(thm',_) => thm'
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
      | None => raise THM("Simplifier: could not continue", 0, [thm]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
fun res1(thm,thms,i) = one_result(resolve_tac thms i,thm);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
(**** Adding "NORM" tags ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
(*get name of the constant from conclusion of a congruence rule*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
fun cong_const cong = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
    case head_of (lhs_of (concl_of cong)) of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
	Const(c,_) => c
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
      | _ => ""			(*a placeholder distinct from const names*);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
(*true if the term is an atomic proposition (no ==> signs) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
val atomic = null o strip_assums_hyp;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
(*ccs contains the names of the constants possessing congruence rules*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
fun add_hidden_vars ccs =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
  let fun add_hvars(tm,hvars) = case tm of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
	      Abs(_,_,body) => add_term_vars(body,hvars)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
	    | _$_ => let val (f,args) = strip_comb tm 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
		     in case f of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
			    Const(c,T) => 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
				if c mem ccs
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
				then foldr add_hvars (args,hvars)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
				else add_term_vars(tm,hvars)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
			  | _ => add_term_vars(tm,hvars)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
		     end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
	    | _ => hvars;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
  in add_hvars end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
fun add_new_asm_vars new_asms =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
    let fun itf((tm,at),vars) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
		if at then vars else add_term_vars(tm,vars)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
	fun add_list(tm,al,vars) = let val (_,tml) = strip_comb tm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
		in if length(tml)=length(al)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
		   then foldr itf (tml~~al,vars)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
		   else vars
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
		end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
	fun add_vars (tm,vars) = case tm of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
		  Abs (_,_,body) => add_vars(body,vars)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
		| r$s => (case head_of tm of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
			  Const(c,T) => (case assoc(new_asms,c) of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
				  None => add_vars(r,add_vars(s,vars))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
				| Some(al) => add_list(tm,al,vars))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
			| _ => add_vars(r,add_vars(s,vars)))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
		| _ => vars
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
    in add_vars end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
fun add_norms(congs,ccs,new_asms) thm =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
let val thm' = mk_trans2 thm;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
(* thm': [?z -> l; Prems; r -> ?t] ==> ?z -> ?t *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
    val nops = nprems_of thm'
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
    val lhs = rhs_of_eq 1 thm'
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
    val rhs = lhs_of_eq nops thm'
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
    val asms = tl(rev(tl(prems_of thm')))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
    val hvars = foldr (add_hidden_vars ccs) (lhs::rhs::asms,[])
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
    val hvars = add_new_asm_vars new_asms (rhs,hvars)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
    fun it_asms (asm,hvars) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
	if atomic asm then add_new_asm_vars new_asms (asm,hvars)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
	else add_term_frees(asm,hvars)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
    val hvars = foldr it_asms (asms,hvars)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
    val hvs = map (#1 o dest_Var) hvars
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
    val refl1_tac = refl_tac 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
    val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
	      (STATE(fn thm =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
		case head_of(rhs_of_eq 1 thm) of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
		  Var(ixn,_) => if ixn mem hvs then refl1_tac
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
				else resolve_tac normI_thms 1 ORELSE refl1_tac
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
		| Const _ => resolve_tac normI_thms 1 ORELSE
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
			     resolve_tac congs 1 ORELSE refl1_tac
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
		| Free _ => resolve_tac congs 1 ORELSE refl1_tac
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
		| _ => refl1_tac))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
    val Some(thm'',_) = Sequence.pull(tapply(add_norm_tac,thm'))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
in thm'' end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
fun add_norm_tags congs =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
    let val ccs = map cong_const congs
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
	val new_asms = filter (exists not o #2)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
		(ccs ~~ (map (map atomic o prems_of) congs));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
    in add_norms(congs,ccs,new_asms) end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   217
fun normed_rews congs =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   218
  let val add_norms = add_norm_tags congs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
  in fn thm => map (varifyT o add_norms o mk_trans) (mk_rew_rules(freezeT thm))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
fun NORM norm_lhs_tac = EVERY'[resolve_tac [red2], norm_lhs_tac, refl_tac];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   224
val trans_norms = map mk_trans normE_thms;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   226
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   227
(* SIMPSET *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   229
datatype simpset =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
	SS of {auto_tac: thm list -> int -> tactic,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   231
	       congs: thm list,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   232
	       cong_net: thm Net.net,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   233
	       mk_simps: thm -> thm list,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
	       simps: (thm * thm list) list,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
	       simp_net: thm Net.net,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   236
               splits: thm list,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   237
               split_consts: string list}
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   238
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   239
val empty_ss = SS{auto_tac= K (K no_tac), congs=[], cong_net=Net.empty,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   240
		  mk_simps=normed_rews[], simps=[], simp_net=Net.empty,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   241
                  splits=[], split_consts=[]};
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   242
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   243
(** Insertion of congruences, rewrites and case splits **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   244
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   245
(*insert a thm in a thm net*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   246
fun insert_thm_warn (th,net) = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   247
  Net.insert_term((concl_of th, th), net, eq_thm)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   248
  handle Net.INSERT => 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   249
    (writeln"\nDuplicate rewrite or congruence rule:"; print_thm th;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   250
     net);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   251
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   252
val insert_thms = foldr insert_thm_warn;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   253
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   254
fun addrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   255
              splits,split_consts}, thm) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   256
let val thms = mk_simps thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   257
in SS{auto_tac=auto_tac,congs=congs, cong_net=cong_net, mk_simps=mk_simps,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   258
      simps = (thm,thms)::simps, simp_net = insert_thms(thms,simp_net),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   259
      splits=splits,split_consts=split_consts}
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   260
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   261
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   262
val op addrews = foldl addrew;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   263
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   264
fun op addcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   265
                   splits,split_consts}, thms) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   266
let val congs' = thms @ congs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   267
in SS{auto_tac=auto_tac, congs= congs',
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   268
      cong_net= insert_thms (map mk_trans thms,cong_net),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   269
      mk_simps= normed_rews congs', simps=simps, simp_net=simp_net,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   270
      splits=splits,split_consts=split_consts}
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   271
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   272
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   273
fun split_err() = error("split rule not of the form ?P(c(...)) = ...");
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   274
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   275
fun split_const(_ $ t) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   276
       (case head_of t of Const(a,_) => a | _ => split_err())
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   277
  | split_const _ = split_err();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   278
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   279
fun addsplit(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   280
                splits,split_consts}, thm) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   281
let val a = split_const(lhs_of(concl_of thm))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   282
in SS{auto_tac=auto_tac,congs=congs,cong_net=cong_net,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   283
      mk_simps=mk_simps,simps=simps,simp_net=simp_net,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   284
      splits=splits@[mk_trans thm],split_consts=split_consts@[a]} end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   285
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   286
val op addsplits = foldl addsplit;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   287
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   288
(** Deletion of congruences and rewrites **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   289
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   290
(*delete a thm from a thm net*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   291
fun delete_thm_warn (th,net) = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   292
  Net.delete_term((concl_of th, th), net, eq_thm)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   293
  handle Net.DELETE => 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   294
    (writeln"\nNo such rewrite or congruence rule:";  print_thm th;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   295
     net);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   296
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   297
val delete_thms = foldr delete_thm_warn;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   298
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   299
fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   300
                   splits,split_consts}, thms) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   301
let val congs' = foldl (gen_rem eq_thm) (congs,thms)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   302
in SS{auto_tac=auto_tac, congs= congs',
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   303
      cong_net= delete_thms(map mk_trans thms,cong_net),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   304
      mk_simps= normed_rews congs', simps=simps, simp_net=simp_net,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   305
      splits=splits,split_consts=split_consts}
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   306
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   307
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   308
fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   309
              splits,split_consts}, thm) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   310
let fun find((p as (th,ths))::ps',ps) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   311
	  if eq_thm(thm,th) then (ths,ps@ps') else find(ps',p::ps)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   312
      | find([],simps') = (writeln"\nNo such rewrite or congruence rule:";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   313
			   print_thm thm;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   314
			   ([],simps'))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   315
    val (thms,simps') = find(simps,[])
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   316
in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   317
      simps = simps', simp_net = delete_thms(thms,simp_net),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   318
      splits=splits,split_consts=split_consts}
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   319
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   320
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   321
val op delrews = foldl delrew;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   322
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   323
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   324
fun op setauto(SS{congs,cong_net,mk_simps,simps,simp_net,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   325
                  splits,split_consts,...}, auto_tac) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   326
    SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   327
       simps=simps, simp_net=simp_net,splits=splits,split_consts=split_consts};
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   328
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   329
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   330
(** Inspection of a simpset **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   331
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   332
fun dest_ss(SS{congs,simps,...}) = (congs, map #1 simps);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   333
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   334
fun print_ss(SS{congs,simps,splits,...}) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   335
	(writeln"Congruences:"; prths congs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   336
         writeln"Case Splits"; prths splits;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   337
	 writeln"Rewrite Rules:"; prths (map #1 simps); ());
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   338
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   339
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   340
(* Rewriting with case splits *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   341
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   342
fun splittable a i thm =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   343
    let val tm = goal_concl i thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   344
	fun nobound(Abs(_,_,tm),j,k) = nobound(tm,j,k+1)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   345
	  | nobound(s$t,j,k) = nobound(s,j,k) andalso nobound(t,j,k)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   346
	  | nobound(Bound n,j,k) = n < k orelse k+j <= n
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   347
	  | nobound(_) = true;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   348
	fun check_args(al,j) = forall (fn t => nobound(t,j,0)) al
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   349
	fun find_if(Abs(_,_,tm),j) = find_if(tm,j+1)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   350
	  | find_if(tm as s$t,j) = let val (f,al) = strip_comb tm in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   351
		case f of Const(c,_) =>	if c=a then check_args(al,j)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   352
			else find_if(s,j) orelse find_if(t,j)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   353
		| _ => find_if(s,j) orelse find_if(t,j) end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   354
	  | find_if(_) = false;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   355
    in find_if(tm,0) end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   356
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   357
fun split_tac (cong_tac,splits,split_consts) i =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   358
    let fun seq_try (split::splits,a::bs) thm = tapply(
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   359
		COND (splittable a i) (DETERM(resolve_tac[split]i))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   360
			(Tactic(seq_try(splits,bs))), thm)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   361
	      | seq_try([],_) thm = tapply(no_tac,thm)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   362
	and try_rew thm = tapply(Tactic(seq_try(splits,split_consts))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   363
				 ORELSE Tactic one_subt, thm)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   364
	and one_subt thm =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   365
		let val test = has_fewer_prems (nprems_of thm + 1)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   366
		    fun loop thm = tapply(COND test no_tac
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   367
			((Tactic try_rew THEN DEPTH_FIRST test (refl_tac i))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   368
			 ORELSE (refl_tac i THEN Tactic loop)), thm)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   369
		in tapply(cong_tac THEN Tactic loop, thm) end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   370
    in if null splits then no_tac
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   371
       else COND (may_match(split_consts,i)) (Tactic try_rew) no_tac
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   372
    end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   373
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   374
fun SPLIT_TAC (SS{cong_net,splits,split_consts,...}) i =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   375
let val cong_tac = net_tac cong_net i
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   376
in NORM (split_tac (cong_tac,splits,split_consts)) i end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   377
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   378
(* Rewriting Automaton *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   379
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   380
datatype cntrl = STOP | MK_EQ | ASMS of int | SIMP_LHS | REW | REFL | TRUE
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   381
	       | PROVE | POP_CS | POP_ARTR | SPLIT;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   382
(*
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   383
fun pr_cntrl c = case c of STOP => prs("STOP") | MK_EQ => prs("MK_EQ") |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   384
ASMS i => print_int i | POP_ARTR => prs("POP_ARTR") |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   385
SIMP_LHS => prs("SIMP_LHS") | REW => prs("REW") | REFL => prs("REFL") |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   386
TRUE => prs("TRUE") | PROVE => prs("PROVE") | POP_CS => prs("POP_CS") | SPLIT
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   387
=> prs("SPLIT");
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   388
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   389
fun simp_refl([],_,ss) = ss
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   390
  | simp_refl(a'::ns,a,ss) = if a'=a then simp_refl(ns,a,SIMP_LHS::REFL::ss)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   391
	else simp_refl(ns,a,ASMS(a)::SIMP_LHS::REFL::POP_ARTR::ss);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   392
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   393
(** Tracing **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   394
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   395
val tracing = ref false;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   396
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   397
(*Replace parameters by Free variables in P*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   398
fun variants_abs ([],P) = P
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   399
  | variants_abs ((a,T)::aTs, P) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   400
      variants_abs (aTs, #2 (variant_abs(a,T,P)));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   401
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   402
(*Select subgoal i from proof state; substitute parameters, for printing*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   403
fun prepare_goal i st =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   404
    let val subgi = nth_subgoal i st
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   405
	val params = rev(strip_params subgi)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   406
    in variants_abs (params, strip_assums_concl subgi) end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   407
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   408
(*print lhs of conclusion of subgoal i*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   409
fun pr_goal_lhs i st =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   410
    writeln (Sign.string_of_term (#sign(rep_thm st)) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   411
	     (lhs_of (prepare_goal i st)));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   412
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   413
(*print conclusion of subgoal i*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   414
fun pr_goal_concl i st =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   415
    writeln (Sign.string_of_term (#sign(rep_thm st)) (prepare_goal i st)) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   416
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   417
(*print subgoals i to j (inclusive)*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   418
fun pr_goals (i,j) st =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   419
    if i>j then ()
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   420
    else (pr_goal_concl i st;  pr_goals (i+1,j) st);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   421
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   422
(*Print rewrite for tracing; i=subgoal#, n=number of new subgoals,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   423
  thm=old state, thm'=new state *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   424
fun pr_rew (i,n,thm,thm',not_asms) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   425
    if !tracing
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   426
    then (if not_asms then () else writeln"Assumption used in";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   427
          pr_goal_lhs i thm; writeln"->"; pr_goal_lhs (i+n) thm';
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   428
	  if n>0 then (writeln"Conditions:"; pr_goals (i, i+n-1) thm')
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   429
          else ();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   430
          writeln"" )
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   431
    else ();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   432
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   433
(* Skip the first n hyps of a goal, and return the rest in generalized form *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   434
fun strip_varify(Const("==>", _) $ H $ B, n, vs) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   435
	if n=0 then subst_bounds(vs,H)::strip_varify(B,0,vs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   436
	else strip_varify(B,n-1,vs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   437
  | strip_varify(Const("all",_)$Abs(_,T,t), n, vs) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   438
	strip_varify(t,n,Var(("?",length vs),T)::vs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   439
  | strip_varify  _  = [];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   440
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   441
fun execute(ss,if_fl,auto_tac,cong_tac,splits,split_consts,net,i) thm = let
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   442
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   443
fun simp_lhs(thm,ss,anet,ats,cs) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   444
    if var_lhs(thm,i) then (ss,thm,anet,ats,cs) else
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   445
    if lhs_is_NORM(thm,i) then (ss, res1(thm,trans_norms,i), anet,ats,cs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   446
    else case Sequence.pull(tapply(cong_tac i,thm)) of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   447
	    Some(thm',_) =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   448
		    let val ps = prems_of thm and ps' = prems_of thm';
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   449
			val n = length(ps')-length(ps);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   450
			val a = length(strip_assums_hyp(nth_elem(i-1,ps)))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   451
			val l = map (fn p => length(strip_assums_hyp(p)))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   452
				    (take(n,drop(i-1,ps')));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   453
		    in (simp_refl(rev(l),a,REW::ss),thm',anet,ats,cs) end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   454
	  | None => (REW::ss,thm,anet,ats,cs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   455
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   456
(*NB: the "Adding rewrites:" trace will look strange because assumptions
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   457
      are represented by rules, generalized over their parameters*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   458
fun add_asms(ss,thm,a,anet,ats,cs) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   459
    let val As = strip_varify(nth_subgoal i thm, a, []);
231
cb6a24451544 Updated refs to old Sign functions
lcp
parents: 1
diff changeset
   460
	val thms = map (trivial o cterm_of(#sign(rep_thm(thm))))As;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   461
	val new_rws = flat(map mk_rew_rules thms);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   462
	val rwrls = map mk_trans (flat(map mk_rew_rules thms));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   463
	val anet' = foldr lhs_insert_thm (rwrls,anet)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   464
    in  if !tracing andalso not(null new_rws)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   465
	then (writeln"Adding rewrites:";  prths new_rws;  ())
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   466
	else ();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   467
	(ss,thm,anet',anet::ats,cs) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   468
    end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   469
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   470
fun rew(seq,thm,ss,anet,ats,cs, more) = case Sequence.pull seq of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   471
      Some(thm',seq') =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   472
	    let val n = (nprems_of thm') - (nprems_of thm)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   473
	    in pr_rew(i,n,thm,thm',more);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   474
	       if n=0 then (SIMP_LHS::ss, thm', anet, ats, cs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   475
	       else ((replicate n PROVE) @ (POP_CS::SIMP_LHS::ss),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   476
		     thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   477
	    end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   478
    | None => if more
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   479
	    then rew(tapply(lhs_net_tac anet i THEN assume_tac i,thm),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   480
		     thm,ss,anet,ats,cs,false)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   481
	    else (ss,thm,anet,ats,cs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   482
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   483
fun try_true(thm,ss,anet,ats,cs) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   484
    case Sequence.pull(tapply(auto_tac i,thm)) of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   485
      Some(thm',_) => (ss,thm',anet,ats,cs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   486
    | None => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   487
	      in if !tracing
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   488
		 then (writeln"*** Failed to prove precondition. Normal form:";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   489
		       pr_goal_concl i thm;  writeln"")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   490
		 else ();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   491
		 rew(seq,thm0,ss0,anet0,ats0,cs0,more)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   492
	      end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   493
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   494
fun split(thm,ss,anet,ats,cs) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   495
	case Sequence.pull(tapply(split_tac
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   496
                                  (cong_tac i,splits,split_consts) i,thm)) of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   497
		Some(thm',_) => (SIMP_LHS::SPLIT::ss,thm',anet,ats,cs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   498
	      | None => (ss,thm,anet,ats,cs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   499
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   500
fun step(s::ss, thm, anet, ats, cs) = case s of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   501
	  MK_EQ => (ss, res1(thm,[red2],i), anet, ats, cs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   502
	| ASMS(a) => add_asms(ss,thm,a,anet,ats,cs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   503
	| SIMP_LHS => simp_lhs(thm,ss,anet,ats,cs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   504
	| REW => rew(tapply(net_tac net i,thm),thm,ss,anet,ats,cs,true)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   505
	| REFL => (ss, res1(thm,refl_thms,i), anet, ats, cs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   506
	| TRUE => try_true(res1(thm,refl_thms,i),ss,anet,ats,cs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   507
	| PROVE => (if if_fl then MK_EQ::SIMP_LHS::SPLIT::TRUE::ss
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   508
		    else MK_EQ::SIMP_LHS::TRUE::ss, thm, anet, ats, cs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   509
	| POP_ARTR => (ss,thm,hd ats,tl ats,cs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   510
	| POP_CS => (ss,thm,anet,ats,tl cs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   511
	| SPLIT => split(thm,ss,anet,ats,cs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   512
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   513
fun exec(state as (s::ss, thm, _, _, _)) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   514
	if s=STOP then thm else exec(step(state));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   515
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   516
in exec(ss, thm, Net.empty, [], []) end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   517
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   518
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   519
(*ss = list of commands (not simpset!); 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   520
  fl = even use case splits to solve conditional rewrite rules;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   521
  addhyps = add hyps to simpset*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   522
fun EXEC_TAC (ss,fl,addhyps) simpset = METAHYPS 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   523
 (fn hyps => 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   524
     case (if addhyps then simpset addrews hyps else simpset) of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   525
         (SS{auto_tac,cong_net,simp_net,splits,split_consts,...}) =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   526
	     PRIMITIVE(execute(ss,fl,auto_tac hyps,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   527
			       net_tac cong_net,splits,split_consts,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   528
                               simp_net, 1))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   529
	     THEN TRY(auto_tac hyps 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   530
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   531
val SIMP_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,SPLIT,REFL,STOP],false,false);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   532
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   533
val ASM_SIMP_TAC = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   534
    EXEC_TAC([ASMS(0),MK_EQ,SIMP_LHS,SPLIT,REFL,STOP],false,true);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   535
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   536
val SIMP_SPLIT2_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,SPLIT,REFL,STOP],true,false);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   537
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   538
fun REWRITE (ss,fl) (SS{auto_tac,cong_net,simp_net,splits,split_consts,...}) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   539
let val cong_tac = net_tac cong_net
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   540
in fn thm =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   541
   let val state = thm RSN (2,red1)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   542
   in execute(ss,fl,auto_tac[],cong_tac,splits,split_consts,simp_net,1)state
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   543
   end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   544
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   545
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   546
val SIMP_THM = REWRITE ([ASMS(0),SIMP_LHS,SPLIT,REFL,STOP],false);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   547
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   548
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   549
(* Compute Congruence rules for individual constants using the substition
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   550
   rules *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   551
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   552
val subst_thms = map standard subst_thms;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   553
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   554
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   555
fun exp_app(0,t) = t
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   556
  | exp_app(i,t) = exp_app(i-1,t $ Bound (i-1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   557
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   558
fun exp_abs(Type("fun",[T1,T2]),t,i) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   559
	Abs("x"^string_of_int i,T1,exp_abs(T2,t,i+1))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   560
  | exp_abs(T,t,i) = exp_app(i,t);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   561
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   562
fun eta_Var(ixn,T) = exp_abs(T,Var(ixn,T),0);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   563
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   564
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   565
fun Pinst(f,fT,(eq,eqT),k,i,T,yik,Ts) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   566
let fun xn_list(x,n) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   567
	let val ixs = map (fn i => (x^(radixstring(26,"a",i)),0)) (0 upto n);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   568
	in map eta_Var (ixs ~~ (take(n+1,Ts))) end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   569
    val lhs = list_comb(f,xn_list("X",k-1))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   570
    val rhs = list_comb(f,xn_list("X",i-1) @ [Bound 0] @ yik)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   571
in Abs("", T, Const(eq,[fT,fT]--->eqT) $ lhs $ rhs) end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   572
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   573
fun find_subst tsig T =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   574
let fun find (thm::thms) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   575
	let val (Const(_,cT), va, vb) =	dest_red(hd(prems_of thm));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   576
	    val [P] = term_vars(concl_of thm) \\ [va,vb]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   577
	    val eqT::_ = binder_types cT
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   578
        in if Type.typ_instance(tsig,T,eqT) then Some(thm,va,vb,P)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   579
	   else find thms
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   580
	end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   581
      | find [] = None
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   582
in find subst_thms end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   583
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   584
fun mk_cong sg (f,aTs,rT) (refl,eq) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   585
let val tsig = #tsig(Sign.rep_sg sg);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   586
    val k = length aTs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   587
    fun ri((subst,va as Var(_,Ta),vb as Var(_,Tb),P),i,si,T,yik) =
231
cb6a24451544 Updated refs to old Sign functions
lcp
parents: 1
diff changeset
   588
	let val ca = cterm_of sg va
cb6a24451544 Updated refs to old Sign functions
lcp
parents: 1
diff changeset
   589
	    and cx = cterm_of sg (eta_Var(("X"^si,0),T))
cb6a24451544 Updated refs to old Sign functions
lcp
parents: 1
diff changeset
   590
	    val cb = cterm_of sg vb
cb6a24451544 Updated refs to old Sign functions
lcp
parents: 1
diff changeset
   591
	    and cy = cterm_of sg (eta_Var(("Y"^si,0),T))
cb6a24451544 Updated refs to old Sign functions
lcp
parents: 1
diff changeset
   592
	    val cP = cterm_of sg P
cb6a24451544 Updated refs to old Sign functions
lcp
parents: 1
diff changeset
   593
	    and cp = cterm_of sg (Pinst(f,rT,eq,k,i,T,yik,aTs))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   594
	in cterm_instantiate [(ca,cx),(cb,cy),(cP,cp)] subst end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   595
    fun mk(c,T::Ts,i,yik) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   596
	let val si = radixstring(26,"a",i)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   597
	in case find_subst tsig T of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   598
	     None => mk(c,Ts,i-1,eta_Var(("X"^si,0),T)::yik)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   599
	   | Some s => let val c' = c RSN (2,ri(s,i,si,T,yik))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   600
		       in mk(c',Ts,i-1,eta_Var(("Y"^si,0),T)::yik) end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   601
	end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   602
      | mk(c,[],_,_) = c;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   603
in mk(refl,rev aTs,k-1,[]) end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   604
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   605
fun mk_cong_type sg (f,T) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   606
let val (aTs,rT) = strip_type T;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   607
    val tsig = #tsig(Sign.rep_sg sg);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   608
    fun find_refl(r::rs) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   609
	let val (Const(eq,eqT),_,_) = dest_red(concl_of r)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   610
	in if Type.typ_instance(tsig, rT, hd(binder_types eqT))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   611
	   then Some(r,(eq,body_type eqT)) else find_refl rs
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   612
	end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   613
      | find_refl([]) = None;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   614
in case find_refl refl_thms of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   615
     None => []  |  Some(refl) => [mk_cong sg (f,aTs,rT) refl]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   616
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   617
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   618
fun mk_cong_thy thy f =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   619
let val sg = sign_of thy;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   620
    val T = case Sign.Symtab.lookup(#const_tab(Sign.rep_sg sg),f) of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   621
		None => error(f^" not declared") | Some(T) => T;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   622
    val T' = incr_tvar 9 T;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   623
in mk_cong_type sg (Const(f,T'),T') end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   624
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   625
fun mk_congs thy = filter_out is_fact o flat o map (mk_cong_thy thy);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   626
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   627
fun mk_typed_congs thy =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   628
let val sg = sign_of thy;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   629
    val S0 = Type.defaultS(#tsig(Sign.rep_sg sg))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   630
    fun readfT(f,s) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   631
	let val T = incr_tvar 9 (Sign.read_typ(sg,K(Some(S0))) s);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   632
	    val t = case Sign.Symtab.lookup(#const_tab(Sign.rep_sg sg),f) of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   633
		      Some(_) => Const(f,T) | None => Free(f,T)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   634
	in (t,T) end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   635
in flat o map (mk_cong_type sg o readfT) end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   636
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   637
(* This code is fishy, esp the "let val T' = ..." 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   638
fun extract_free_congs() =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   639
let val {prop,sign,...} = rep_thm(topthm());
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   640
    val frees = add_term_frees(prop,[]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   641
    fun filter(Free(a,T as Type("fun",_))) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   642
	  let val T' = incr_tvar 9 (Type.varifyT T)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   643
	  in [(Free(a,T),T)] end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   644
      | filter _ = []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   645
in flat(map (mk_cong_type sign) (flat (map filter frees))) end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   646
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   647
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   648
end (* local *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   649
end (* SIMP *);