src/ZF/intr_elim.ML
author lcp
Thu Aug 18 17:41:40 1994 +0200 (1994-08-18 ago)
changeset 543 e961b2092869
parent 516 1957113f0d7d
child 578 efc648d29dd0
permissions -rw-r--r--
ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
ZF/ind_syntax/prove_term: deleted

ZF/constructor, indrule, intr_elim: now call prove_goalw_cterm and
Logic.unvarify
clasohm@0
     1
(*  Title: 	ZF/intr-elim.ML
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@516
     4
    Copyright   1994  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Introduction/elimination rule module -- for Inductive/Coinductive Definitions
clasohm@0
     7
*)
clasohm@0
     8
lcp@516
     9
signature INDUCTIVE_ARG =	(** Description of a (co)inductive def **)
clasohm@0
    10
  sig
lcp@516
    11
  val thy        : theory               (*new theory with inductive defs*)
clasohm@0
    12
  val monos      : thm list		(*monotonicity of each M operator*)
clasohm@0
    13
  val con_defs   : thm list		(*definitions of the constructors*)
clasohm@0
    14
  val type_intrs : thm list		(*type-checking intro rules*)
clasohm@0
    15
  val type_elims : thm list		(*type-checking elim rules*)
clasohm@0
    16
  end;
clasohm@0
    17
lcp@516
    18
(*internal items*)
lcp@516
    19
signature INDUCTIVE_I =
lcp@516
    20
  sig
lcp@516
    21
  val rec_tms    : term list		(*the recursive sets*)
lcp@516
    22
  val domts      : term list		(*their domains*)
lcp@516
    23
  val intr_tms   : term list		(*terms for the introduction rules*)
lcp@516
    24
  end;
lcp@516
    25
clasohm@0
    26
signature INTR_ELIM =
clasohm@0
    27
  sig
lcp@516
    28
  val thy        : theory               (*copy of input theory*)
clasohm@0
    29
  val defs	 : thm list		(*definitions made in thy*)
clasohm@0
    30
  val bnd_mono   : thm			(*monotonicity for the lfp definition*)
clasohm@0
    31
  val unfold     : thm			(*fixed-point equation*)
clasohm@0
    32
  val dom_subset : thm			(*inclusion of recursive set in dom*)
clasohm@0
    33
  val intrs      : thm list		(*introduction rules*)
clasohm@0
    34
  val elim       : thm			(*case analysis theorem*)
clasohm@0
    35
  val raw_induct : thm			(*raw induction rule from Fp.induct*)
clasohm@0
    36
  val mk_cases : thm list -> string -> thm	(*generates case theorems*)
lcp@516
    37
  val rec_names  : string list		(*names of recursive sets*)
clasohm@0
    38
  val sumprod_free_SEs : thm list       (*destruct rules for Su and Pr*)
clasohm@0
    39
  end;
clasohm@0
    40
lcp@516
    41
(*prove intr/elim rules for a fixedpoint definition*)
lcp@516
    42
functor Intr_elim_Fun
lcp@516
    43
    (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end  
lcp@516
    44
     and Fp: FP and Pr : PR and Su : SU) : INTR_ELIM =
clasohm@0
    45
struct
lcp@516
    46
open Logic Inductive Ind_Syntax;
clasohm@0
    47
lcp@516
    48
val rec_names = map (#1 o dest_Const o head_of) rec_tms;
clasohm@0
    49
val big_rec_name = space_implode "_" rec_names;
clasohm@0
    50
lcp@516
    51
(*fetch fp definitions from the theory*)
lcp@516
    52
val big_rec_def::part_rec_defs = 
lcp@516
    53
  map (get_def thy)
lcp@516
    54
      (case rec_names of [_] => rec_names | _ => big_rec_name::rec_names);
clasohm@0
    55
clasohm@0
    56
lcp@516
    57
val sign = sign_of thy;
clasohm@0
    58
clasohm@0
    59
(********)
lcp@516
    60
val _ = writeln "  Proving monotonicity...";
lcp@516
    61
lcp@516
    62
val Const("==",_) $ _ $ (_ $ dom_sum $ fp_abs) =
lcp@543
    63
    big_rec_def |> rep_thm |> #prop |> Logic.unvarify;
clasohm@0
    64
clasohm@0
    65
val bnd_mono = 
lcp@543
    66
    prove_goalw_cterm [] 
lcp@543
    67
      (cterm_of sign (mk_tprop (Fp.bnd_mono $ dom_sum $ fp_abs)))
lcp@543
    68
      (fn _ =>
clasohm@0
    69
       [rtac (Collect_subset RS bnd_monoI) 1,
clasohm@0
    70
	REPEAT (ares_tac (basic_monos @ monos) 1)]);
clasohm@0
    71
clasohm@0
    72
val dom_subset = standard (big_rec_def RS Fp.subs);
clasohm@0
    73
clasohm@0
    74
val unfold = standard (bnd_mono RS (big_rec_def RS Fp.Tarski));
clasohm@0
    75
clasohm@0
    76
(********)
lcp@516
    77
val _ = writeln "  Proving the introduction rules...";
clasohm@0
    78
clasohm@0
    79
(*Mutual recursion: Needs subset rules for the individual sets???*)
clasohm@0
    80
val rec_typechecks = [dom_subset] RL (asm_rl::monos) RL [subsetD];
clasohm@0
    81
clasohm@0
    82
(*Type-checking is hardest aspect of proof;
clasohm@0
    83
  disjIn selects the correct disjunct after unfolding*)
clasohm@0
    84
fun intro_tacsf disjIn prems = 
clasohm@0
    85
  [(*insert prems and underlying sets*)
lcp@55
    86
   cut_facts_tac prems 1,
clasohm@0
    87
   rtac (unfold RS ssubst) 1,
clasohm@0
    88
   REPEAT (resolve_tac [Part_eqI,CollectI] 1),
clasohm@0
    89
   (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
clasohm@0
    90
   rtac disjIn 2,
clasohm@0
    91
   REPEAT (ares_tac [refl,exI,conjI] 2),
clasohm@0
    92
   rewrite_goals_tac con_defs,
clasohm@0
    93
   (*Now can solve the trivial equation*)
clasohm@0
    94
   REPEAT (rtac refl 2),
lcp@516
    95
   REPEAT (FIRSTGOAL (        dresolve_tac rec_typechecks
lcp@516
    96
		      ORELSE' eresolve_tac (asm_rl::PartE::SigmaE2::type_elims)
lcp@516
    97
		      ORELSE' hyp_subst_tac)),
lcp@495
    98
   DEPTH_SOLVE (swap_res_tac (SigmaI::type_intrs) 1)];
clasohm@0
    99
clasohm@0
   100
(*combines disjI1 and disjI2 to access the corresponding nested disjunct...*)
clasohm@0
   101
val mk_disj_rls = 
clasohm@0
   102
    let fun f rl = rl RS disjI1
lcp@516
   103
	and g rl = rl RS disjI2
clasohm@0
   104
    in  accesses_bal(f, g, asm_rl)  end;
clasohm@0
   105
lcp@543
   106
val intrs = map (uncurry (prove_goalw_cterm part_rec_defs))
lcp@543
   107
            (map (cterm_of sign) intr_tms ~~ 
lcp@543
   108
	     map intro_tacsf (mk_disj_rls(length intr_tms)));
clasohm@0
   109
clasohm@0
   110
(********)
lcp@516
   111
val _ = writeln "  Proving the elimination rule...";
clasohm@0
   112
lcp@55
   113
(*Includes rules for succ and Pair since they are common constructions*)
lcp@55
   114
val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0, 
lcp@70
   115
		Pair_neq_0, sym RS Pair_neq_0, make_elim succ_inject, 
lcp@70
   116
		refl_thin, conjE, exE, disjE];
clasohm@0
   117
clasohm@0
   118
val sumprod_free_SEs = 
clasohm@0
   119
    map (gen_make_elim [conjE,FalseE])
lcp@516
   120
	([Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff] 
clasohm@0
   121
	 RL [iffD1]);
clasohm@0
   122
clasohm@0
   123
(*Breaks down logical connectives in the monotonic function*)
clasohm@0
   124
val basic_elim_tac =
clasohm@0
   125
    REPEAT (SOMEGOAL (eresolve_tac (elim_rls@sumprod_free_SEs)
lcp@516
   126
	      ORELSE' bound_hyp_subst_tac))
clasohm@0
   127
    THEN prune_params_tac;
clasohm@0
   128
clasohm@0
   129
val elim = rule_by_tactic basic_elim_tac (unfold RS equals_CollectD);
clasohm@0
   130
lcp@14
   131
(*Applies freeness of the given constructors, which *must* be unfolded by
lcp@14
   132
  the given defs.  Cannot simply use the local con_defs because con_defs=[] 
lcp@14
   133
  for inference systems. *)
clasohm@0
   134
fun con_elim_tac defs =
lcp@70
   135
    rewrite_goals_tac defs THEN basic_elim_tac THEN fold_tac defs;
clasohm@0
   136
clasohm@0
   137
(*String s should have the form t:Si where Si is an inductive set*)
clasohm@0
   138
fun mk_cases defs s = 
clasohm@0
   139
    rule_by_tactic (con_elim_tac defs)
clasohm@0
   140
      (assume_read thy s  RS  elim);
clasohm@0
   141
clasohm@0
   142
val defs = big_rec_def::part_rec_defs;
clasohm@0
   143
clasohm@0
   144
val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct);
lcp@516
   145
end;
clasohm@0
   146