--- a/src/CTT/ctt.ML Sat Apr 05 16:00:00 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,249 +0,0 @@
-(* Title: CTT/ctt.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1991 University of Cambridge
-
-Tactics and lemmas for ctt.thy (Constructive Type Theory)
-*)
-
-open CTT;
-
-signature CTT_RESOLVE =
- sig
- val add_mp_tac: int -> tactic
- val ASSUME: (int -> tactic) -> int -> tactic
- val basic_defs: thm list
- val comp_rls: thm list
- val element_rls: thm list
- val elimL_rls: thm list
- val elim_rls: thm list
- val eqintr_tac: tactic
- val equal_tac: thm list -> tactic
- val formL_rls: thm list
- val form_rls: thm list
- val form_tac: tactic
- val intrL2_rls: thm list
- val intrL_rls: thm list
- val intr_rls: thm list
- val intr_tac: thm list -> tactic
- val mp_tac: int -> tactic
- val NE_tac: string -> int -> tactic
- val pc_tac: thm list -> int -> tactic
- val PlusE_tac: string -> int -> tactic
- val reduction_rls: thm list
- val replace_type: thm
- val routine_rls: thm list
- val routine_tac: thm list -> thm list -> int -> tactic
- val safe_brls: (bool * thm) list
- val safestep_tac: thm list -> int -> tactic
- val safe_tac: thm list -> int -> tactic
- val step_tac: thm list -> int -> tactic
- val subst_eqtyparg: thm
- val subst_prodE: thm
- val SumE_fst: thm
- val SumE_snd: thm
- val SumE_tac: string -> int -> tactic
- val SumIL2: thm
- val test_assume_tac: int -> tactic
- val typechk_tac: thm list -> tactic
- val unsafe_brls: (bool * thm) list
- end;
-
-
-structure CTT_Resolve : CTT_RESOLVE =
-struct
-
-(*Formation rules*)
-val form_rls = [NF, ProdF, SumF, PlusF, EqF, FF, TF]
-and formL_rls = [ProdFL, SumFL, PlusFL, EqFL];
-
-
-(*Introduction rules
- OMITTED: EqI, because its premise is an eqelem, not an elem*)
-val intr_rls = [NI0, NI_succ, ProdI, SumI, PlusI_inl, PlusI_inr, TI]
-and intrL_rls = [NI_succL, ProdIL, SumIL, PlusI_inlL, PlusI_inrL];
-
-
-(*Elimination rules
- OMITTED: EqE, because its conclusion is an eqelem, not an elem
- TE, because it does not involve a constructor *)
-val elim_rls = [NE, ProdE, SumE, PlusE, FE]
-and elimL_rls = [NEL, ProdEL, SumEL, PlusEL, FEL];
-
-(*OMITTED: eqC are TC because they make rewriting loop: p = un = un = ... *)
-val comp_rls = [NC0, NC_succ, ProdC, SumC, PlusC_inl, PlusC_inr];
-
-(*rules with conclusion a:A, an elem judgement*)
-val element_rls = intr_rls @ elim_rls;
-
-(*Definitions are (meta)equality axioms*)
-val basic_defs = [fst_def,snd_def];
-
-(*Compare with standard version: B is applied to UNSIMPLIFIED expression! *)
-val SumIL2 = prove_goal CTT.thy
- "[| c=a : A; d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)"
- (fn prems=>
- [ (resolve_tac [sym_elem] 1),
- (resolve_tac [SumIL] 1),
- (ALLGOALS (resolve_tac [sym_elem])),
- (ALLGOALS (resolve_tac prems)) ]);
-
-val intrL2_rls = [NI_succL, ProdIL, SumIL2, PlusI_inlL, PlusI_inrL];
-
-(*Exploit p:Prod(A,B) to create the assumption z:B(a).
- A more natural form of product elimination. *)
-val subst_prodE = prove_goal CTT.thy
- "[| p: Prod(A,B); a: A; !!z. z: B(a) ==> c(z): C(z) \
-\ |] ==> c(p`a): C(p`a)"
- (fn prems=>
- [ (REPEAT (resolve_tac (prems@[ProdE]) 1)) ]);
-
-(** Tactics for type checking **)
-
-fun is_rigid_elem (Const("Elem",_) $ a $ _) = not (is_Var (head_of a))
- | is_rigid_elem _ = false;
-
-(*Try solving a:A by assumption provided a is rigid!*)
-val test_assume_tac = SUBGOAL(fn (prem,i) =>
- if is_rigid_elem (Logic.strip_assums_concl prem)
- then assume_tac i else no_tac);
-
-fun ASSUME tf i = test_assume_tac i ORELSE tf i;
-
-
-(*For simplification: type formation and checking,
- but no equalities between terms*)
-val routine_rls = form_rls @ formL_rls @ [refl_type] @ element_rls;
-
-fun routine_tac rls prems = ASSUME (filt_resolve_tac (prems @ rls) 4);
-
-
-(*Solve all subgoals "A type" using formation rules. *)
-val form_tac = REPEAT_FIRST (filt_resolve_tac(form_rls) 1);
-
-
-(*Type checking: solve a:A (a rigid, A flexible) by intro and elim rules. *)
-fun typechk_tac thms =
- let val tac = filt_resolve_tac (thms @ form_rls @ element_rls) 3
- in REPEAT_FIRST (ASSUME tac) end;
-
-
-(*Solve a:A (a flexible, A rigid) by introduction rules.
- Cannot use stringtrees (filt_resolve_tac) since
- goals like ?a:SUM(A,B) have a trivial head-string *)
-fun intr_tac thms =
- let val tac = filt_resolve_tac(thms@form_rls@intr_rls) 1
- in REPEAT_FIRST (ASSUME tac) end;
-
-
-(*Equality proving: solve a=b:A (where a is rigid) by long rules. *)
-fun equal_tac thms =
- let val rls = thms @ form_rls @ element_rls @ intrL_rls @
- elimL_rls @ [refl_elem]
- in REPEAT_FIRST (ASSUME (filt_resolve_tac rls 3)) end;
-
-(*** Simplification ***)
-
-(*To simplify the type in a goal*)
-val replace_type = prove_goal CTT.thy
- "[| B = A; a : A |] ==> a : B"
- (fn prems=>
- [ (resolve_tac [equal_types] 1),
- (resolve_tac [sym_type] 2),
- (ALLGOALS (resolve_tac prems)) ]);
-
-(*Simplify the parameter of a unary type operator.*)
-val subst_eqtyparg = prove_goal CTT.thy
- "a=c : A ==> (!!z.z:A ==> B(z) type) ==> B(a)=B(c)"
- (fn prems=>
- [ (resolve_tac [subst_typeL] 1),
- (resolve_tac [refl_type] 2),
- (ALLGOALS (resolve_tac prems)),
- (assume_tac 1) ]);
-
-(*Make a reduction rule for simplification.
- A goal a=c becomes b=c, by virtue of a=b *)
-fun resolve_trans rl = rl RS trans_elem;
-
-(*Simplification rules for Constructive Type Theory*)
-val reduction_rls = map resolve_trans comp_rls;
-
-(*Converts each goal "e : Eq(A,a,b)" into "a=b:A" for simplification.
- Uses other intro rules to avoid changing flexible goals.*)
-val eqintr_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac(EqI::intr_rls) 1));
-
-(** Tactics that instantiate CTT-rules.
- Vars in the given terms will be incremented!
- The (resolve_tac [EqE] i) lets them apply to equality judgements. **)
-
-fun NE_tac (sp: string) i =
- TRY (resolve_tac [EqE] i) THEN res_inst_tac [ ("p",sp) ] NE i;
-
-fun SumE_tac (sp: string) i =
- TRY (resolve_tac [EqE] i) THEN res_inst_tac [ ("p",sp) ] SumE i;
-
-fun PlusE_tac (sp: string) i =
- TRY (resolve_tac [EqE] i) THEN res_inst_tac [ ("p",sp) ] PlusE i;
-
-(** Predicate logic reasoning, WITH THINNING!! Procedures adapted from NJ. **)
-
-(*Finds f:Prod(A,B) and a:A in the assumptions, concludes there is z:B(a) *)
-fun add_mp_tac i =
- resolve_tac [subst_prodE] i THEN assume_tac i THEN assume_tac i;
-
-(*Finds P-->Q and P in the assumptions, replaces implication by Q *)
-fun mp_tac i = eresolve_tac [subst_prodE] i THEN assume_tac i;
-
-(*"safe" when regarded as predicate calculus rules*)
-val safe_brls = sort lessb
- [ (true,FE), (true,asm_rl),
- (false,ProdI), (true,SumE), (true,PlusE) ];
-
-val unsafe_brls =
- [ (false,PlusI_inl), (false,PlusI_inr), (false,SumI),
- (true,subst_prodE) ];
-
-(*0 subgoals vs 1 or more*)
-val (safe0_brls, safep_brls) =
- partition (apl(0,op=) o subgoals_of_brl) safe_brls;
-
-fun safestep_tac thms i =
- form_tac ORELSE
- resolve_tac thms i ORELSE
- biresolve_tac safe0_brls i ORELSE mp_tac i ORELSE
- DETERM (biresolve_tac safep_brls i);
-
-fun safe_tac thms i = DEPTH_SOLVE_1 (safestep_tac thms i);
-
-fun step_tac thms = safestep_tac thms ORELSE' biresolve_tac unsafe_brls;
-
-(*Fails unless it solves the goal!*)
-fun pc_tac thms = DEPTH_SOLVE_1 o (step_tac thms);
-
-(** The elimination rules for fst/snd **)
-
-val SumE_fst = prove_goal CTT.thy
- "p : Sum(A,B) ==> fst(p) : A"
- (fn prems=>
- [ (rewrite_goals_tac basic_defs),
- (resolve_tac elim_rls 1),
- (REPEAT (pc_tac prems 1)),
- (fold_tac basic_defs) ]);
-
-(*The first premise must be p:Sum(A,B) !!*)
-val SumE_snd = prove_goal CTT.thy
- "[| p: Sum(A,B); A type; !!x. x:A ==> B(x) type \
-\ |] ==> snd(p) : B(fst(p))"
- (fn prems=>
- [ (rewrite_goals_tac basic_defs),
- (resolve_tac elim_rls 1),
- (resolve_tac prems 1),
- (resolve_tac [replace_type] 1),
- (resolve_tac [subst_eqtyparg] 1), (*like B(x) equality formation?*)
- (resolve_tac comp_rls 1),
- (typechk_tac prems),
- (fold_tac basic_defs) ]);
-
-end;
-
-open CTT_Resolve;