src/Provers/ind.ML
author ballarin
Wed, 19 Jul 2006 19:25:58 +0200
changeset 20168 ed7bced29e1b
parent 19299 5f0610aafc48
child 20344 d02b43ea722e
permissions -rw-r--r--
Reimplemented algebra method; now controlled by attribute.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	Provers/ind
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Tobias Nipkow
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Generic induction package -- for use with simplifier
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
signature IND_DATA =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
  sig
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
  val spec: thm (* All(?P) ==> ?P(?a) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
signature IND =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
  sig
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
  val all_frees_tac: string -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
  val ALL_IND_TAC: thm -> (int -> tactic) -> (int -> tactic)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
  val IND_TAC: thm -> (int -> tactic) -> string -> (int -> tactic)
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
functor InductionFun(Ind_Data: IND_DATA):IND =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
local open Ind_Data in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
val _$(_$Var(a_ixname,aT)) = concl_of spec;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
fun add_term_frees tsig =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
let fun add(tm, vars) = case tm of
14772
c52060b69a8c Type.typ_instance;
wenzelm
parents: 14643
diff changeset
    31
	Free(v,T) => if Type.typ_instance tsig (T,aT) then v ins vars
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
		     else vars
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
      | Abs (_,_,body) => add(body,vars)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
      | rator$rand => add(rator, add(rand, vars))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
      | _ => vars
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
in add end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
15462
b4208fbf9439 Eliminated hack for deleting leading question mark from induction
berghofe
parents: 14772
diff changeset
    39
fun qnt_tac i = fn (tac,var) => tac THEN Tactic.res_inst_tac' [(a_ixname,var)] spec i;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
(*Generalizes over all free variables, with the named var outermost.*)
1512
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 0
diff changeset
    42
fun all_frees_tac (var:string) i thm = 
14643
wenzelm
parents: 4452
diff changeset
    43
    let val tsig = Sign.tsig_of (Thm.sign_of_thm thm);
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15462
diff changeset
    44
        val frees = add_term_frees tsig (List.nth(prems_of thm,i-1),[var]);
19299
5f0610aafc48 remove (op =);
wenzelm
parents: 15570
diff changeset
    45
        val frees' = sort (rev_order o string_ord) (remove (op =) var frees) @ [var]
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15462
diff changeset
    46
    in Library.foldl (qnt_tac i) (all_tac,frees') thm end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
fun REPEAT_SIMP_TAC simp_tac n i =
1512
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 0
diff changeset
    49
let fun repeat thm = 
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 0
diff changeset
    50
        (COND (has_fewer_prems n) all_tac
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 0
diff changeset
    51
	 let val k = nprems_of thm
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 0
diff changeset
    52
	 in simp_tac i THEN COND (has_fewer_prems k) repeat all_tac end)
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 0
diff changeset
    53
	thm
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 0
diff changeset
    54
in repeat end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
1512
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 0
diff changeset
    56
fun ALL_IND_TAC sch simp_tac i thm = 
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 0
diff changeset
    57
	(resolve_tac [sch] i THEN
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 0
diff changeset
    58
	 REPEAT_SIMP_TAC simp_tac (nprems_of thm) i) thm;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
fun IND_TAC sch simp_tac var =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
	all_frees_tac var THEN' ALL_IND_TAC sch simp_tac;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
end;