src/CTT/CTT.ML

--- a/src/CTT/CTT.ML	Fri Sep 16 21:02:15 2005 +0200
+++ b/src/CTT/CTT.ML	Fri Sep 16 23:01:29 2005 +0200
@@ -10,7 +10,7 @@
 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]
@@ -42,7 +42,7 @@
 
 val intrL2_rls = [NI_succL, ProdIL, SumIL2, PlusI_inlL, PlusI_inrL];
 
-(*Exploit p:Prod(A,B) to create the assumption z:B(a).  
+(*Exploit p:Prod(A,B) to create the assumption z:B(a).
   A more natural form of product elimination. *)
 val prems = Goal "[| p: Prod(A,B);  a: A;  !!z. z: B(a) ==> c(z): C(z) \
 \    |] ==> c(p`a): C(p`a)";
@@ -56,7 +56,7 @@
   | is_rigid_elem (Const("CTT.Type",_) $ a) = not(is_Var (head_of a))
   | is_rigid_elem _ = false;
 
-(*Try solving a:A or a=b:A by assumption provided a is rigid!*) 
+(*Try solving a:A or a=b: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);
@@ -81,7 +81,7 @@
   in  REPEAT_FIRST (ASSUME tac)  end;
 
 
-(*Solve a:A (a flexible, A rigid) by introduction rules. 
+(*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 =
@@ -125,22 +125,22 @@
 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! 
+    Vars in the given terms will be incremented!
     The (rtac EqE i) lets them apply to equality judgements. **)
 
-fun NE_tac (sp: string) i = 
+fun NE_tac (sp: string) i =
   TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] NE i;
 
-fun SumE_tac (sp: string) i = 
+fun SumE_tac (sp: string) i =
   TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] SumE i;
 
-fun PlusE_tac (sp: string) i = 
+fun PlusE_tac (sp: string) i =
   TRY (rtac 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 = 
+fun add_mp_tac i =
     rtac subst_prodE i  THEN  assume_tac i  THEN  assume_tac i;
 
 (*Finds P-->Q and P in the assumptions, replaces implication by Q *)
@@ -148,11 +148,11 @@
 
 (*"safe" when regarded as predicate calculus rules*)
 val safe_brls = sort (make_ord lessb)
-    [ (true,FE), (true,asm_rl), 
+    [ (true,FE), (true,asm_rl),
       (false,ProdI), (true,SumE), (true,PlusE) ];
 
 val unsafe_brls =
-    [ (false,PlusI_inl), (false,PlusI_inr), (false,SumI), 
+    [ (false,PlusI_inl), (false,PlusI_inr), (false,SumI),
       (true,subst_prodE) ];
 
 (*0 subgoals vs 1 or more*)
@@ -160,12 +160,12 @@
     List.partition (apl(0,op=) o subgoals_of_brl) safe_brls;
 
 fun safestep_tac thms i =
-    form_tac  ORELSE  
+    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 safe_tac thms i = DEPTH_SOLVE_1 (safestep_tac thms i);
 
 fun step_tac thms = safestep_tac thms  ORELSE'  biresolve_tac unsafe_brls;