--- a/intr_elim.ML Tue Oct 24 14:59:17 1995 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,141 +0,0 @@
-(* Title: HOL/intr_elim.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Introduction/elimination rule module -- for Inductive/Coinductive Definitions
-*)
-
-signature INDUCTIVE_ARG = (** Description of a (co)inductive def **)
- sig
- val thy : theory (*new theory with inductive defs*)
- val monos : thm list (*monotonicity of each M operator*)
- val con_defs : thm list (*definitions of the constructors*)
- end;
-
-(*internal items*)
-signature INDUCTIVE_I =
- sig
- val rec_tms : term list (*the recursive sets*)
- val intr_tms : term list (*terms for the introduction rules*)
- end;
-
-signature INTR_ELIM =
- sig
- val thy : theory (*copy of input theory*)
- val defs : thm list (*definitions made in thy*)
- val mono : thm (*monotonicity for the lfp definition*)
- val unfold : thm (*fixed-point equation*)
- val intrs : thm list (*introduction rules*)
- val elim : thm (*case analysis theorem*)
- val raw_induct : thm (*raw induction rule from Fp.induct*)
- val mk_cases : thm list -> string -> thm (*generates case theorems*)
- val rec_names : string list (*names of recursive sets*)
- end;
-
-(*prove intr/elim rules for a fixedpoint definition*)
-functor Intr_elim_Fun
- (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end
- and Fp: FP) : INTR_ELIM =
-struct
-open Logic Inductive Ind_Syntax;
-
-val rec_names = map (#1 o dest_Const o head_of) rec_tms;
-val big_rec_name = space_implode "_" rec_names;
-
-val _ = deny (big_rec_name mem map ! (stamps_of_thy thy))
- ("Definition " ^ big_rec_name ^
- " would clash with the theory of the same name!");
-
-(*fetch fp definitions from the theory*)
-val big_rec_def::part_rec_defs =
- map (get_def thy)
- (case rec_names of [_] => rec_names | _ => big_rec_name::rec_names);
-
-
-val sign = sign_of thy;
-
-(********)
-val _ = writeln " Proving monotonicity...";
-
-val Const("==",_) $ _ $ (Const(_,fpT) $ fp_abs) =
- big_rec_def |> rep_thm |> #prop |> unvarify;
-
-(*For the type of the argument of mono*)
-val [monoT] = binder_types fpT;
-
-val mono =
- prove_goalw_cterm []
- (cterm_of sign (mk_Trueprop (Const("mono", monoT-->boolT) $ fp_abs)))
- (fn _ =>
- [rtac monoI 1,
- REPEAT (ares_tac (basic_monos @ monos) 1)]);
-
-val unfold = standard (mono RS (big_rec_def RS Fp.Tarski));
-
-(********)
-val _ = writeln " Proving the introduction rules...";
-
-fun intro_tacsf disjIn prems =
- [(*insert prems and underlying sets*)
- cut_facts_tac prems 1,
- rtac (unfold RS ssubst) 1,
- REPEAT (resolve_tac [Part_eqI,CollectI] 1),
- (*Now 1-2 subgoals: the disjunction, perhaps equality.*)
- rtac disjIn 1,
- (*Not ares_tac, since refl must be tried before any equality assumptions;
- backtracking may occur if the premises have extra variables!*)
- DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 1 ORELSE assume_tac 1)];
-
-(*combines disjI1 and disjI2 to access the corresponding nested disjunct...*)
-val mk_disj_rls =
- let fun f rl = rl RS disjI1
- and g rl = rl RS disjI2
- in accesses_bal(f, g, asm_rl) end;
-
-val intrs = map (uncurry (prove_goalw_cterm part_rec_defs))
- (map (cterm_of sign) intr_tms ~~
- map intro_tacsf (mk_disj_rls(length intr_tms)));
-
-(********)
-val _ = writeln " Proving the elimination rule...";
-
-(*Includes rules for Suc and Pair since they are common constructions*)
-val elim_rls = [asm_rl, FalseE, Suc_neq_Zero, Zero_neq_Suc,
- make_elim Suc_inject,
- refl_thin, conjE, exE, disjE];
-
-(*Breaks down logical connectives in the monotonic function*)
-val basic_elim_tac =
- REPEAT (SOMEGOAL (eresolve_tac (elim_rls@sumprod_free_SEs)
- ORELSE' bound_hyp_subst_tac))
- THEN prune_params_tac;
-
-val elim = rule_by_tactic basic_elim_tac (unfold RS equals_CollectD);
-
-(*Applies freeness of the given constructors, which *must* be unfolded by
- the given defs. Cannot simply use the local con_defs because con_defs=[]
- for inference systems.
-fun con_elim_tac defs =
- rewrite_goals_tac defs THEN basic_elim_tac THEN fold_tac defs;
- *)
-fun con_elim_tac simps =
- let val elim_tac = REPEAT o (eresolve_tac (elim_rls@sumprod_free_SEs))
- in ALLGOALS(EVERY'[elim_tac,
- asm_full_simp_tac (nat_ss addsimps simps),
- elim_tac,
- REPEAT o bound_hyp_subst_tac])
- THEN prune_params_tac
- end;
-
-
-(*String s should have the form t:Si where Si is an inductive set*)
-fun mk_cases defs s =
- rule_by_tactic (con_elim_tac defs)
- (assume_read thy s RS elim);
-
-val defs = big_rec_def::part_rec_defs;
-
-val raw_induct = standard ([big_rec_def, mono] MRS Fp.induct);
-end;
-