author  lcp 
Fri, 21 Oct 1994 09:58:05 +0100  
changeset 652  ff4d4d7fcb7f 
parent 634  8a5f6961250f 
child 726  d703d1a1a2af 
permissions  rwrr 
578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
543
diff
changeset

1 
(* Title: ZF/intr_elim.ML 
0  2 
ID: $Id$ 
3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

516  4 
Copyright 1994 University of Cambridge 
0  5 

6 
Introduction/elimination rule module  for Inductive/Coinductive Definitions 

7 
*) 

8 

516  9 
signature INDUCTIVE_ARG = (** Description of a (co)inductive def **) 
0  10 
sig 
516  11 
val thy : theory (*new theory with inductive defs*) 
0  12 
val monos : thm list (*monotonicity of each M operator*) 
13 
val con_defs : thm list (*definitions of the constructors*) 

14 
val type_intrs : thm list (*typechecking intro rules*) 

15 
val type_elims : thm list (*typechecking elim rules*) 

16 
end; 

17 

516  18 
(*internal items*) 
19 
signature INDUCTIVE_I = 

20 
sig 

21 
val rec_tms : term list (*the recursive sets*) 

22 
val domts : term list (*their domains*) 

23 
val intr_tms : term list (*terms for the introduction rules*) 

24 
end; 

25 

0  26 
signature INTR_ELIM = 
27 
sig 

516  28 
val thy : theory (*copy of input theory*) 
0  29 
val defs : thm list (*definitions made in thy*) 
30 
val bnd_mono : thm (*monotonicity for the lfp definition*) 

31 
val unfold : thm (*fixedpoint equation*) 

32 
val dom_subset : thm (*inclusion of recursive set in dom*) 

33 
val intrs : thm list (*introduction rules*) 

34 
val elim : thm (*case analysis theorem*) 

35 
val raw_induct : thm (*raw induction rule from Fp.induct*) 

36 
val mk_cases : thm list > string > thm (*generates case theorems*) 

516  37 
val rec_names : string list (*names of recursive sets*) 
0  38 
val sumprod_free_SEs : thm list (*destruct rules for Su and Pr*) 
39 
end; 

40 

516  41 
(*prove intr/elim rules for a fixedpoint definition*) 
42 
functor Intr_elim_Fun 

43 
(structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end 

44 
and Fp: FP and Pr : PR and Su : SU) : INTR_ELIM = 

0  45 
struct 
516  46 
open Logic Inductive Ind_Syntax; 
0  47 

516  48 
val rec_names = map (#1 o dest_Const o head_of) rec_tms; 
0  49 
val big_rec_name = space_implode "_" rec_names; 
50 

578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding 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 rebuilding without
lcp
parents:
543
diff
changeset

52 
("Definition " ^ big_rec_name ^ 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding 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 rebuilding without
lcp
parents:
543
diff
changeset

54 

516  55 
(*fetch fp definitions from the theory*) 
56 
val big_rec_def::part_rec_defs = 

57 
map (get_def thy) 

58 
(case rec_names of [_] => rec_names  _ => big_rec_name::rec_names); 

0  59 

60 

516  61 
val sign = sign_of thy; 
0  62 

63 
(********) 

516  64 
val _ = writeln " Proving monotonicity..."; 
65 

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  68 

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  73 
[rtac (Collect_subset RS bnd_monoI) 1, 
74 
REPEAT (ares_tac (basic_monos @ monos) 1)]); 

75 

76 
val dom_subset = standard (big_rec_def RS Fp.subs); 

77 

78 
val unfold = standard (bnd_mono RS (big_rec_def RS Fp.Tarski)); 

79 

80 
(********) 

516  81 
val _ = writeln " Proving the introduction rules..."; 
0  82 

83 
(*Mutual recursion: Needs subset rules for the individual sets???*) 

84 
val rec_typechecks = [dom_subset] RL (asm_rl::monos) RL [subsetD]; 

85 

86 
(*Typechecking is hardest aspect of proof; 

87 
disjIn selects the correct disjunct after unfolding*) 

88 
fun intro_tacsf disjIn prems = 

89 
[(*insert prems and underlying sets*) 

55  90 
cut_facts_tac prems 1, 
0  91 
rtac (unfold RS ssubst) 1, 
92 
REPEAT (resolve_tac [Part_eqI,CollectI] 1), 

93 
(*Now 23 subgoals: typechecking, the disjunction, perhaps equality.*) 

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 rebuilding without
lcp
parents:
543
diff
changeset

98 
(*Now solve the equations like Tcons(a,f) = Inl(?b4)*) 
0  99 
rewrite_goals_tac con_defs, 
100 
REPEAT (rtac refl 2), 

578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
543
diff
changeset

101 
(*Typechecking; this can fail*) 
516  102 
REPEAT (FIRSTGOAL ( dresolve_tac rec_typechecks 
103 
ORELSE' eresolve_tac (asm_rl::PartE::SigmaE2::type_elims) 

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  106 

107 
(*combines disjI1 and disjI2 to access the corresponding nested disjunct...*) 

108 
val mk_disj_rls = 

109 
let fun f rl = rl RS disjI1 

516  110 
and g rl = rl RS disjI2 
0  111 
in accesses_bal(f, g, asm_rl) end; 
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  116 

117 
(********) 

516  118 
val _ = writeln " Proving the elimination rule..."; 
0  119 

55  120 
(*Includes rules for succ and Pair since they are common constructions*) 
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/indsyntax/fold_con_tac: deleted, since fold_tac now works
lcp
parents:
55
diff
changeset

124 
refl_thin, conjE, exE, disjE]; 
0  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  128 
val sumprod_free_SEs = 
129 
map (gen_make_elim [conjE,FalseE]) 

516  130 
([Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff] 
0  131 
RL [iffD1]); 
132 

133 
(*Breaks down logical connectives in the monotonic function*) 

134 
val basic_elim_tac = 

135 
REPEAT (SOMEGOAL (eresolve_tac (elim_rls@sumprod_free_SEs) 

516  136 
ORELSE' bound_hyp_subst_tac)) 
0  137 
THEN prune_params_tac; 
138 

139 
val elim = rule_by_tactic basic_elim_tac (unfold RS equals_CollectD); 

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  144 
fun con_elim_tac defs = 
70
8a29f8b4aca1
ZF/indsyntax/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  146 

147 
(*String s should have the form t:Si where Si is an inductive set*) 

148 
fun mk_cases defs s = 

149 
rule_by_tactic (con_elim_tac defs) 

150 
(assume_read thy s RS elim); 

151 

152 
val defs = big_rec_def::part_rec_defs; 

153 

154 
val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct); 

516  155 
end; 
0  156 