src/ZF/intr_elim.ML
author lcp
Fri, 21 Oct 1994 09:58:05 +0100
changeset 652 ff4d4d7fcb7f
parent 634 8a5f6961250f
child 726 d703d1a1a2af
permissions -rw-r--r--
ZF/intr_elim/elim_rls: now includes Pair_inject, since coinductive definitions may involve ordinary pairs. (HOL/intr_elim does not require this change)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents: 543
diff changeset
     1
(*  Title: 	ZF/intr_elim.ML
0
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
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
     4
    Copyright   1994  University of Cambridge
0
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
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
     9
signature INDUCTIVE_ARG =	(** Description of a (co)inductive def **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
  sig
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    11
  val thy        : theory               (*new theory with inductive defs*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
  val monos      : thm list		(*monotonicity of each M operator*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
  val con_defs   : thm list		(*definitions of the constructors*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
  val type_intrs : thm list		(*type-checking intro rules*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
  val type_elims : thm list		(*type-checking elim rules*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    18
(*internal items*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    19
signature INDUCTIVE_I =
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    20
  sig
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    21
  val rec_tms    : term list		(*the recursive sets*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    22
  val domts      : term list		(*their domains*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    23
  val intr_tms   : term list		(*terms for the introduction rules*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    24
  end;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    25
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
signature INTR_ELIM =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
  sig
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    28
  val thy        : theory               (*copy of input theory*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
  val defs	 : thm list		(*definitions made in thy*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
  val bnd_mono   : thm			(*monotonicity for the lfp definition*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
  val unfold     : thm			(*fixed-point equation*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
  val dom_subset : thm			(*inclusion of recursive set in dom*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
  val intrs      : thm list		(*introduction rules*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
  val elim       : thm			(*case analysis theorem*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
  val raw_induct : thm			(*raw induction rule from Fp.induct*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
  val mk_cases : thm list -> string -> thm	(*generates case theorems*)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    37
  val rec_names  : string list		(*names of recursive sets*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
  val sumprod_free_SEs : thm list       (*destruct rules for Su and Pr*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    41
(*prove intr/elim rules for a fixedpoint definition*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    42
functor Intr_elim_Fun
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    43
    (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end  
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    44
     and Fp: FP and Pr : PR and Su : SU) : INTR_ELIM =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
struct
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    46
open Logic Inductive Ind_Syntax;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    48
val rec_names = map (#1 o dest_Const o head_of) rec_tms;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
val big_rec_name = space_implode "_" rec_names;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents: 543
diff changeset
    51
val _ = deny (big_rec_name  mem  map ! (stamps_of_thy thy))
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents: 543
diff changeset
    52
             ("Definition " ^ big_rec_name ^ 
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents: 543
diff changeset
    53
	      " would clash with the theory of the same name!");
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents: 543
diff changeset
    54
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    55
(*fetch fp definitions from the theory*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    56
val big_rec_def::part_rec_defs = 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    57
  map (get_def thy)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    58
      (case rec_names of [_] => rec_names | _ => big_rec_name::rec_names);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    61
val sign = sign_of thy;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
(********)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    64
val _ = writeln "  Proving monotonicity...";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    65
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    66
val Const("==",_) $ _ $ (_ $ dom_sum $ fp_abs) =
543
e961b2092869 ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents: 516
diff changeset
    67
    big_rec_def |> rep_thm |> #prop |> Logic.unvarify;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
val bnd_mono = 
543
e961b2092869 ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents: 516
diff changeset
    70
    prove_goalw_cterm [] 
e961b2092869 ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents: 516
diff changeset
    71
      (cterm_of sign (mk_tprop (Fp.bnd_mono $ dom_sum $ fp_abs)))
e961b2092869 ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents: 516
diff changeset
    72
      (fn _ =>
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
       [rtac (Collect_subset RS bnd_monoI) 1,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
	REPEAT (ares_tac (basic_monos @ monos) 1)]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
val dom_subset = standard (big_rec_def RS Fp.subs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
val unfold = standard (bnd_mono RS (big_rec_def RS Fp.Tarski));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
(********)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    81
val _ = writeln "  Proving the introduction rules...";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
(*Mutual recursion: Needs subset rules for the individual sets???*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
val rec_typechecks = [dom_subset] RL (asm_rl::monos) RL [subsetD];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
(*Type-checking is hardest aspect of proof;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
  disjIn selects the correct disjunct after unfolding*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
fun intro_tacsf disjIn prems = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
  [(*insert prems and underlying sets*)
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 25
diff changeset
    90
   cut_facts_tac prems 1,
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
   rtac (unfold RS ssubst) 1,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
   REPEAT (resolve_tac [Part_eqI,CollectI] 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
   (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
   rtac disjIn 2,
634
8a5f6961250f {HOL,ZF}/intr_elim/intro_tacsf: now calls DEPTH_SOLVE_1 instead of REPEAT to
lcp
parents: 590
diff changeset
    95
   (*Not ares_tac, since refl must be tried before any equality assumptions;
8a5f6961250f {HOL,ZF}/intr_elim/intro_tacsf: now calls DEPTH_SOLVE_1 instead of REPEAT to
lcp
parents: 590
diff changeset
    96
     backtracking may occur if the premises have extra variables!*)
8a5f6961250f {HOL,ZF}/intr_elim/intro_tacsf: now calls DEPTH_SOLVE_1 instead of REPEAT to
lcp
parents: 590
diff changeset
    97
   DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 2 ORELSE assume_tac 2),
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents: 543
diff changeset
    98
   (*Now solve the equations like Tcons(a,f) = Inl(?b4)*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
   rewrite_goals_tac con_defs,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
   REPEAT (rtac refl 2),
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents: 543
diff changeset
   101
   (*Typechecking; this can fail*)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
   102
   REPEAT (FIRSTGOAL (        dresolve_tac rec_typechecks
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
   103
		      ORELSE' eresolve_tac (asm_rl::PartE::SigmaE2::type_elims)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
   104
		      ORELSE' hyp_subst_tac)),
495
612888a07889 ZF/intr_elim/intro_tacsf: now uses SigmaI as a default intro rule and
lcp
parents: 477
diff changeset
   105
   DEPTH_SOLVE (swap_res_tac (SigmaI::type_intrs) 1)];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
(*combines disjI1 and disjI2 to access the corresponding nested disjunct...*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
val mk_disj_rls = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
    let fun f rl = rl RS disjI1
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
   110
	and g rl = rl RS disjI2
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
    in  accesses_bal(f, g, asm_rl)  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
543
e961b2092869 ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents: 516
diff changeset
   113
val intrs = map (uncurry (prove_goalw_cterm part_rec_defs))
e961b2092869 ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents: 516
diff changeset
   114
            (map (cterm_of sign) intr_tms ~~ 
e961b2092869 ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents: 516
diff changeset
   115
	     map intro_tacsf (mk_disj_rls(length intr_tms)));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
(********)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
   118
val _ = writeln "  Proving the elimination rule...";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 25
diff changeset
   120
(*Includes rules for succ and Pair since they are common constructions*)
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 25
diff changeset
   121
val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0, 
652
ff4d4d7fcb7f ZF/intr_elim/elim_rls: now includes Pair_inject, since coinductive
lcp
parents: 634
diff changeset
   122
		Pair_neq_0, sym RS Pair_neq_0, Pair_inject,
ff4d4d7fcb7f ZF/intr_elim/elim_rls: now includes Pair_inject, since coinductive
lcp
parents: 634
diff changeset
   123
		make_elim succ_inject, 
70
8a29f8b4aca1 ZF/ind-syntax/fold_con_tac: deleted, since fold_tac now works
lcp
parents: 55
diff changeset
   124
		refl_thin, conjE, exE, disjE];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
652
ff4d4d7fcb7f ZF/intr_elim/elim_rls: now includes Pair_inject, since coinductive
lcp
parents: 634
diff changeset
   126
(*Standard sum/products for datatypes, variant ones for codatatypes;
ff4d4d7fcb7f ZF/intr_elim/elim_rls: now includes Pair_inject, since coinductive
lcp
parents: 634
diff changeset
   127
  We always include Pair_inject above*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
val sumprod_free_SEs = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
    map (gen_make_elim [conjE,FalseE])
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
   130
	([Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff] 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
	 RL [iffD1]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
(*Breaks down logical connectives in the monotonic function*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
val basic_elim_tac =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
    REPEAT (SOMEGOAL (eresolve_tac (elim_rls@sumprod_free_SEs)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
   136
	      ORELSE' bound_hyp_subst_tac))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
    THEN prune_params_tac;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
val elim = rule_by_tactic basic_elim_tac (unfold RS equals_CollectD);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 0
diff changeset
   141
(*Applies freeness of the given constructors, which *must* be unfolded by
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 0
diff changeset
   142
  the given defs.  Cannot simply use the local con_defs because con_defs=[] 
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 0
diff changeset
   143
  for inference systems. *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
fun con_elim_tac defs =
70
8a29f8b4aca1 ZF/ind-syntax/fold_con_tac: deleted, since fold_tac now works
lcp
parents: 55
diff changeset
   145
    rewrite_goals_tac defs THEN basic_elim_tac THEN fold_tac defs;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
(*String s should have the form t:Si where Si is an inductive set*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
fun mk_cases defs s = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
    rule_by_tactic (con_elim_tac defs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
      (assume_read thy s  RS  elim);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
val defs = big_rec_def::part_rec_defs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct);
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
   155
end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156