# HG changeset patch
# User urbanc
# Date 1189269002 -7200
# Node ID 419f7cde7f592b004ccd5b61fedc1e88984bd944
# Parent  57e2a5fbde86102899f21b5f53312fece1211232
some cleaning up

diff -r 57e2a5fbde86 -r 419f7cde7f59 src/HOL/Nominal/nominal_fresh_fun.ML
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Fri Sep 07 22:13:49 2007 +0200
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Sat Sep 08 18:30:02 2007 +0200
@@ -2,28 +2,29 @@
     ID:         $Id$
     Authors:    Stefan Berghofer, Julien Narboux, TU Muenchen
 
-A tactic to generate fresh names.
-A tactic to get rid of the fresh_fun.
+Provides a tactic to generate fresh names and
+a tactic to analyse instances of the fresh_fun.
+
 *)
 
-(* First some functions that could be in the library *)
+(* First some functions that should be in the library *)
 
-(* A tactical which applies a list of int -> tactic to the corresponding subgoals present after the application of another tactic. 
-T THENL [A,B,C] is equivalent to T THEN (C 3 THEN B 2 THEN A 1) 
-*)
+(* A tactical which applies a list of int -> tactic to the          *) 
+(* corresponding subgoals present after the application of          *) 
+(* another tactic.                                                  *)
+(*                                                                  *)
+(*  T THENL [A,B,C] is equivalent to T THEN (C 3 THEN B 2 THEN A 1) *) 
 
 infix 1 THENL
-
 fun tac THENL tacs =
  tac THEN
   (EVERY (map  (fn (tac,i) => tac i) (rev tacs ~~ (length tacs downto 1))))
 
-(* A tactical to test if a tactic completly solve a subgoal *)
-
+(* A tactic which only succeeds when the argument *)
+(* tactic solves completely the specified subgoal *)
 fun SOLVEI t = t THEN_ALL_NEW (fn i => no_tac);
 
 (* A version of TRY for int -> tactic *)
-
 fun TRY' tac i =  TRY (tac i);
 
 fun gen_res_inst_tac_term instf tyinst tinst elim th i st =
@@ -55,20 +56,18 @@
 fun cut_inst_tac_term' tinst th =
   res_inst_tac_term' tinst false (Tactic.make_elim_preserve th);
 
-fun get_dyn_thm thy name atom_name = (PureThy.get_thm thy (Name name)) handle _ => raise ERROR ("The atom type "^atom_name^" is not defined."); 
+fun get_dyn_thm thy name atom_name = (PureThy.get_thm thy (Name name)) handle _ => 
+                                          raise ERROR ("The atom type "^atom_name^" is not defined."); 
 
-(* End of function waiting to be
- in the library *)
+(* End of function waiting to be in the library :o) *)
 
-(* The theorems needed that are known at
-compile time. *)
+(* The theorems needed that are known at compile time. *)
+val at_exists_fresh' = @{thm "at_exists_fresh'"};
+val fresh_fun_app'   = @{thm "fresh_fun_app'"};
+val fresh_prod       = @{thm "fresh_prod"};
 
-val at_exists_fresh' = thm "at_exists_fresh'";
-val fresh_fun_app' = thm "fresh_fun_app'";
-val fresh_prod = thm "fresh_prod";
-
-(* A tactic to generate a name fresh for 
-all the free variables and parameters of the goal *)
+(* A tactic to generate a name fresh for  all the free *) 
+(* variables and parameters of the goal                *)
 
 fun generate_fresh_tac atom_name i thm =
  let 
@@ -104,14 +103,15 @@
   | get_inner_fresh_fun (v as Var _)  = NONE
   | get_inner_fresh_fun (Const _) = NONE
   | get_inner_fresh_fun (Abs (_, _, t)) = get_inner_fresh_fun t 
-  | get_inner_fresh_fun (Const ("Nominal.fresh_fun",Type("fun",[Type ("fun",[Type (T,_),_]),_])) $ u) = SOME T 
+  | get_inner_fresh_fun (Const ("Nominal.fresh_fun",Type("fun",[Type ("fun",[Type (T,_),_]),_])) $ u) 
+                           = SOME T 
   | get_inner_fresh_fun (t $ u) = 
      let val a = get_inner_fresh_fun u in
      if a = NONE then get_inner_fresh_fun t else a 
      end;
 
-(* This tactic generates a fresh name 
-of the atom type given by the inner most fresh_fun *)
+(* This tactic generates a fresh name of the atom type *) 
+(* given by the innermost fresh_fun                    *)
 
 fun generate_fresh_fun_tac i thm =
   let
@@ -123,7 +123,7 @@
   | SOME atom_name  => generate_fresh_tac atom_name i thm               
   end
 
-(* Two substitution tactics which looks for the inner most occurence in 
+(* Two substitution tactics which looks for the innermost occurence in 
    one assumption or in the conclusion *)
 
 val search_fun     = curry (Seq.flat o (uncurry EqSubst.searchf_bt_unify_valid));
@@ -135,7 +135,9 @@
 (* A tactic to substitute in the first assumption 
    which contains an occurence. *)
 
-fun subst_inner_asm_tac ctx th =  curry (curry (FIRST' (map uncurry (map uncurry (map subst_inner_asm_tac_aux (1 upto Thm.nprems_of th)))))) ctx th;
+fun subst_inner_asm_tac ctx th =  
+   curry (curry (FIRST' (map uncurry (map uncurry (map subst_inner_asm_tac_aux 
+                                                             (1 upto Thm.nprems_of th)))))) ctx th;
 
 fun fresh_fun_tac no_asm i thm = 
   (* Find the variable we instantiate *)
@@ -151,7 +153,8 @@
     val goal = nth (prems_of thm) (i-1);
     val atom_name_opt = get_inner_fresh_fun goal;
     val n = List.length (Logic.strip_params goal);
-    (* Here we rely on the fact that the variable introduced by generate_fresh_tac is the last one in the list, the inner one *)
+    (* Here we rely on the fact that the variable introduced by generate_fresh_tac *)
+    (* is the last one in the list, the inner one *)
   in
   case atom_name_opt of 
     NONE => all_tac thm