src/ZF/intr_elim.ML
author clasohm
Thu, 16 Sep 1993 12:20:38 +0200
changeset 0 a5a9c433f639
child 14 1c0926788772
permissions -rw-r--r--
Initial revision
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/intr-elim.ML
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Introduction/elimination rule module -- for Inductive/Coinductive Definitions
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
Features:
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
* least or greatest fixedpoints
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
* user-specified product and sum constructions
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
* mutually recursive definitions
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
* definitions involving arbitrary monotone operators
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
* automatically proves introduction and elimination rules
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
The recursive sets must *already* be declared as constants in parent theory!
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
  Introduction rules have the form
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
  [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk |]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
  where M is some monotone operator (usually the identity)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
  P(x) is any (non-conjunctive) side condition on the free variables
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
  ti, t are any terms
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
  Sj, Sk are two of the sets being defiend in mutual recursion
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
Sums are used only for mutual recursion;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
Products are used only to derive "streamlined" induction rules for relations
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
signature FP =		(** Description of a fixed point operator **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
  sig
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
  val oper	: term			(*fixed point operator*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
  val bnd_mono	: term			(*monotonicity predicate*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
  val bnd_monoI	: thm			(*intro rule for bnd_mono*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
  val subs	: thm			(*subset theorem for fp*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
  val Tarski	: thm			(*Tarski's fixed point theorem*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
  val induct	: thm			(*induction/coinduction rule*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
signature PR =			(** Description of a Cartesian product **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
  sig
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
  val sigma	: term			(*Cartesian product operator*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
  val pair	: term			(*pairing operator*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
  val split_const  : term		(*splitting operator*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
  val fsplit_const : term		(*splitting operator for formulae*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
  val pair_iff	: thm			(*injectivity of pairing, using <->*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
  val split_eq	: thm			(*equality rule for split*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
  val fsplitI	: thm			(*intro rule for fsplit*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
  val fsplitD	: thm			(*destruct rule for fsplit*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
  val fsplitE	: thm			(*elim rule for fsplit*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
signature SU =			(** Description of a disjoint sum **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
  sig
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
  val sum	: term			(*disjoint sum operator*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
  val inl	: term			(*left injection*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
  val inr	: term			(*right injection*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
  val elim	: term			(*case operator*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
  val case_inl	: thm			(*inl equality rule for case*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
  val case_inr	: thm			(*inr equality rule for case*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
  val inl_iff	: thm			(*injectivity of inl, using <->*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
  val inr_iff	: thm			(*injectivity of inr, using <->*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
  val distinct	: thm			(*distinctness of inl, inr using <->*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
  val distinct'	: thm			(*distinctness of inr, inl using <->*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
signature INDUCTIVE =		(** Description of a (co)inductive defn **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
  sig
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
  val thy        : theory		(*parent theory*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
  val rec_doms   : (string*string) list	(*recursion ops and their domains*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
  val sintrs     : string list		(*desired introduction rules*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
  val monos      : thm list		(*monotonicity of each M operator*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
  val con_defs   : thm list		(*definitions of the constructors*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
  val type_intrs : thm list		(*type-checking intro rules*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
  val type_elims : thm list		(*type-checking elim rules*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
signature INTR_ELIM =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
  sig
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
  val thy        : theory		(*new theory*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
  val defs	 : thm list		(*definitions made in thy*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
  val bnd_mono   : thm			(*monotonicity for the lfp definition*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
  val unfold     : thm			(*fixed-point equation*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
  val dom_subset : thm			(*inclusion of recursive set in dom*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
  val intrs      : thm list		(*introduction rules*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
  val elim       : thm			(*case analysis theorem*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
  val raw_induct : thm			(*raw induction rule from Fp.induct*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
  val mk_cases : thm list -> string -> thm	(*generates case theorems*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
  (*internal items...*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
  val big_rec_tm : term			(*the lhs of the fixedpoint defn*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
  val rec_tms    : term list		(*the mutually recursive sets*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
  val domts      : term list		(*domains of the recursive sets*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
  val intr_tms   : term list		(*terms for the introduction rules*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
  val rec_params : term list		(*parameters of the recursion*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
  val sumprod_free_SEs : thm list       (*destruct rules for Su and Pr*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
functor Intr_elim_Fun (structure Ind: INDUCTIVE and 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
		       Fp: FP and Pr : PR and Su : SU) : INTR_ELIM =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
open Logic Ind;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
(*** Extract basic information from arguments ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
val sign = sign_of Ind.thy;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
fun rd T a = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
    Sign.read_cterm sign (a,T)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
    handle ERROR => error ("The error above occurred for " ^ a);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
val rec_names = map #1 rec_doms
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
and domts     = map (Sign.term_of o rd iT o #2) rec_doms;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
val dummy = assert_all Syntax.is_identifier rec_names
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
   (fn a => "Name of recursive set not an identifier: " ^ a);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
val dummy = assert_all (is_some o lookup_const sign) rec_names
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
   (fn a => "Name of recursive set not declared as constant: " ^ a);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
val intr_tms = map (Sign.term_of o rd propT) sintrs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
val (Const(_,recT),rec_params) = strip_comb (#2 (rule_concl(hd intr_tms)))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
val rec_hds = map (fn a=> Const(a,recT)) rec_names;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
val rec_tms = map (fn rec_hd=> list_comb(rec_hd,rec_params)) rec_hds;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
val dummy = assert_all is_Free rec_params
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
    (fn t => "Param in recursion term not a free variable: " ^
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
             Sign.string_of_term sign t);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
(*** Construct the lfp definition ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
val mk_variant = variant (foldr add_term_names (intr_tms,[]));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
val z' = mk_variant"z"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
and X' = mk_variant"X"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
and w' = mk_variant"w";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
(*simple error-checking in the premises*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
fun chk_prem rec_hd (Const("op &",_) $ _ $ _) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
	error"Premises may not be conjuctive"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
  | chk_prem rec_hd (Const("op :",_) $ t $ X) = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
	deny (rec_hd occs t) "Recursion term on left of member symbol"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
  | chk_prem rec_hd t = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
	deny (rec_hd occs t) "Recursion term in side formula";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
(*Makes a disjunct from an introduction rule*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
fun lfp_part intr = (*quantify over rule's free vars except parameters*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
  let val prems = map dest_tprop (strip_imp_prems intr)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
      val dummy = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
      val exfrees = term_frees intr \\ rec_params
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
      val zeq = eq_const $ (Free(z',iT)) $ (#1 (rule_concl intr))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
  in foldr mk_exists (exfrees, fold_bal (app conj) (zeq::prems)) end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
val dom_sum = fold_bal (app Su.sum) domts;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
(*The Part(A,h) terms -- compose injections to make h*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
fun mk_Part (Bound 0) = Free(X',iT)	(*no mutual rec, no Part needed*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
  | mk_Part h         = Part_const $ Free(X',iT) $ Abs(w',iT,h);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
(*Access to balanced disjoint sums via injections*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
val parts = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
    map mk_Part (accesses_bal (ap Su.inl, ap Su.inr, Bound 0) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
		              (length rec_doms));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
(*replace each set by the corresponding Part(A,h)*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
val lfp_abs = absfree(X', iT, 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
	         mk_Collect(z', dom_sum, fold_bal (app disj) part_intrs));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
val lfp_rhs = Fp.oper $ dom_sum $ lfp_abs
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
val dummy = seq (fn rec_hd => deny (rec_hd occs lfp_rhs) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
			   "Illegal occurrence of recursion operator")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
	 rec_hds;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
(*** Make the new theory ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
(*A key definition:
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
  If no mutual recursion then it equals the one recursive set.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
  If mutual recursion then it differs from all the recursive sets. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
val big_rec_name = space_implode "_" rec_names;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
(*Big_rec... is the union of the mutually recursive sets*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
(*The individual sets must already be declared*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
val axpairs = map (mk_defpair sign) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
      ((big_rec_tm, lfp_rhs) ::
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
       (case parts of 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
	   [_] => [] 			(*no mutual recursion*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
	 | _ => rec_tms ~~		(*define the sets as Parts*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
		map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
val thy = extend_theory Ind.thy (big_rec_name ^ "_Inductive")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
    ([], [], [], [], [], None) axpairs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
val defs = map (get_axiom thy o #1) axpairs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
val big_rec_def::part_rec_defs = defs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
val prove = prove_term (sign_of thy);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
(********)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
val dummy = writeln "Proving monotonocity...";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
val bnd_mono = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
    prove [] (mk_tprop (Fp.bnd_mono $ dom_sum $ lfp_abs), 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
       fn _ =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
       [rtac (Collect_subset RS bnd_monoI) 1,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
	REPEAT (ares_tac (basic_monos @ monos) 1)]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
val dom_subset = standard (big_rec_def RS Fp.subs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
val unfold = standard (bnd_mono RS (big_rec_def RS Fp.Tarski));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
(********)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
val dummy = writeln "Proving the introduction rules...";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   217
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   218
(*Mutual recursion: Needs subset rules for the individual sets???*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
val rec_typechecks = [dom_subset] RL (asm_rl::monos) RL [subsetD];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
(*Type-checking is hardest aspect of proof;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
  disjIn selects the correct disjunct after unfolding*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
fun intro_tacsf disjIn prems = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   224
  [(*insert prems and underlying sets*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
   cut_facts_tac (prems @ (prems RL [PartD1])) 1,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   226
   rtac (unfold RS ssubst) 1,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   227
   REPEAT (resolve_tac [Part_eqI,CollectI] 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
   (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   229
   rtac disjIn 2,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
   REPEAT (ares_tac [refl,exI,conjI] 2),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   231
   rewrite_goals_tac con_defs,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   232
   (*Now can solve the trivial equation*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   233
   REPEAT (rtac refl 2),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
   REPEAT (FIRSTGOAL (eresolve_tac (asm_rl::type_elims)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
		      ORELSE' dresolve_tac rec_typechecks)),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   236
   DEPTH_SOLVE (ares_tac type_intrs 1)];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   237
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   238
(*combines disjI1 and disjI2 to access the corresponding nested disjunct...*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   239
val mk_disj_rls = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   240
    let fun f rl = rl RS disjI1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   241
        and g rl = rl RS disjI2
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   242
    in  accesses_bal(f, g, asm_rl)  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   243
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   244
val intrs = map (prove part_rec_defs) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   245
	       (intr_tms ~~ map intro_tacsf (mk_disj_rls(length intr_tms)));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   246
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   247
(********)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   248
val dummy = writeln "Proving the elimination rule...";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   249
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   250
val elim_rls = [asm_rl, FalseE, conjE, exE, disjE];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   251
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   252
val sumprod_free_SEs = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   253
    map (gen_make_elim [conjE,FalseE])
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   254
        ([Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff] 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   255
	 RL [iffD1]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   256
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   257
(*Breaks down logical connectives in the monotonic function*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   258
val basic_elim_tac =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   259
    REPEAT (SOMEGOAL (eresolve_tac (elim_rls@sumprod_free_SEs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   260
              ORELSE' bound_hyp_subst_tac))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   261
    THEN prune_params_tac;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   262
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   263
val elim = rule_by_tactic basic_elim_tac (unfold RS equals_CollectD);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   264
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   265
(*Applies freeness of the given constructors.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   266
  NB for datatypes, defs=con_defs; for inference systems, con_defs=[]! *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   267
fun con_elim_tac defs =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   268
    rewrite_goals_tac defs THEN basic_elim_tac THEN fold_con_tac defs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   269
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   270
(*String s should have the form t:Si where Si is an inductive set*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   271
fun mk_cases defs s = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   272
    rule_by_tactic (con_elim_tac defs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   273
      (assume_read thy s  RS  elim);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   274
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   275
val defs = big_rec_def::part_rec_defs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   276
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   277
val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   278
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   279
end;