src/HOL/Nominal/nominal_fresh_fun.ML
changeset 24558 419f7cde7f59
parent 24271 499608101177
child 26337 44473c957672
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Fri Sep 07 22:13:49 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Sat Sep 08 18:30:02 2007 +0200
     1.3 @@ -2,28 +2,29 @@
     1.4      ID:         $Id$
     1.5      Authors:    Stefan Berghofer, Julien Narboux, TU Muenchen
     1.6  
     1.7 -A tactic to generate fresh names.
     1.8 -A tactic to get rid of the fresh_fun.
     1.9 +Provides a tactic to generate fresh names and
    1.10 +a tactic to analyse instances of the fresh_fun.
    1.11 +
    1.12  *)
    1.13  
    1.14 -(* First some functions that could be in the library *)
    1.15 +(* First some functions that should be in the library *)
    1.16  
    1.17 -(* A tactical which applies a list of int -> tactic to the corresponding subgoals present after the application of another tactic. 
    1.18 -T THENL [A,B,C] is equivalent to T THEN (C 3 THEN B 2 THEN A 1) 
    1.19 -*)
    1.20 +(* A tactical which applies a list of int -> tactic to the          *) 
    1.21 +(* corresponding subgoals present after the application of          *) 
    1.22 +(* another tactic.                                                  *)
    1.23 +(*                                                                  *)
    1.24 +(*  T THENL [A,B,C] is equivalent to T THEN (C 3 THEN B 2 THEN A 1) *) 
    1.25  
    1.26  infix 1 THENL
    1.27 -
    1.28  fun tac THENL tacs =
    1.29   tac THEN
    1.30    (EVERY (map  (fn (tac,i) => tac i) (rev tacs ~~ (length tacs downto 1))))
    1.31  
    1.32 -(* A tactical to test if a tactic completly solve a subgoal *)
    1.33 -
    1.34 +(* A tactic which only succeeds when the argument *)
    1.35 +(* tactic solves completely the specified subgoal *)
    1.36  fun SOLVEI t = t THEN_ALL_NEW (fn i => no_tac);
    1.37  
    1.38  (* A version of TRY for int -> tactic *)
    1.39 -
    1.40  fun TRY' tac i =  TRY (tac i);
    1.41  
    1.42  fun gen_res_inst_tac_term instf tyinst tinst elim th i st =
    1.43 @@ -55,20 +56,18 @@
    1.44  fun cut_inst_tac_term' tinst th =
    1.45    res_inst_tac_term' tinst false (Tactic.make_elim_preserve th);
    1.46  
    1.47 -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."); 
    1.48 +fun get_dyn_thm thy name atom_name = (PureThy.get_thm thy (Name name)) handle _ => 
    1.49 +                                          raise ERROR ("The atom type "^atom_name^" is not defined."); 
    1.50  
    1.51 -(* End of function waiting to be
    1.52 - in the library *)
    1.53 +(* End of function waiting to be in the library :o) *)
    1.54  
    1.55 -(* The theorems needed that are known at
    1.56 -compile time. *)
    1.57 +(* The theorems needed that are known at compile time. *)
    1.58 +val at_exists_fresh' = @{thm "at_exists_fresh'"};
    1.59 +val fresh_fun_app'   = @{thm "fresh_fun_app'"};
    1.60 +val fresh_prod       = @{thm "fresh_prod"};
    1.61  
    1.62 -val at_exists_fresh' = thm "at_exists_fresh'";
    1.63 -val fresh_fun_app' = thm "fresh_fun_app'";
    1.64 -val fresh_prod = thm "fresh_prod";
    1.65 -
    1.66 -(* A tactic to generate a name fresh for 
    1.67 -all the free variables and parameters of the goal *)
    1.68 +(* A tactic to generate a name fresh for  all the free *) 
    1.69 +(* variables and parameters of the goal                *)
    1.70  
    1.71  fun generate_fresh_tac atom_name i thm =
    1.72   let 
    1.73 @@ -104,14 +103,15 @@
    1.74    | get_inner_fresh_fun (v as Var _)  = NONE
    1.75    | get_inner_fresh_fun (Const _) = NONE
    1.76    | get_inner_fresh_fun (Abs (_, _, t)) = get_inner_fresh_fun t 
    1.77 -  | get_inner_fresh_fun (Const ("Nominal.fresh_fun",Type("fun",[Type ("fun",[Type (T,_),_]),_])) $ u) = SOME T 
    1.78 +  | get_inner_fresh_fun (Const ("Nominal.fresh_fun",Type("fun",[Type ("fun",[Type (T,_),_]),_])) $ u) 
    1.79 +                           = SOME T 
    1.80    | get_inner_fresh_fun (t $ u) = 
    1.81       let val a = get_inner_fresh_fun u in
    1.82       if a = NONE then get_inner_fresh_fun t else a 
    1.83       end;
    1.84  
    1.85 -(* This tactic generates a fresh name 
    1.86 -of the atom type given by the inner most fresh_fun *)
    1.87 +(* This tactic generates a fresh name of the atom type *) 
    1.88 +(* given by the innermost fresh_fun                    *)
    1.89  
    1.90  fun generate_fresh_fun_tac i thm =
    1.91    let
    1.92 @@ -123,7 +123,7 @@
    1.93    | SOME atom_name  => generate_fresh_tac atom_name i thm               
    1.94    end
    1.95  
    1.96 -(* Two substitution tactics which looks for the inner most occurence in 
    1.97 +(* Two substitution tactics which looks for the innermost occurence in 
    1.98     one assumption or in the conclusion *)
    1.99  
   1.100  val search_fun     = curry (Seq.flat o (uncurry EqSubst.searchf_bt_unify_valid));
   1.101 @@ -135,7 +135,9 @@
   1.102  (* A tactic to substitute in the first assumption 
   1.103     which contains an occurence. *)
   1.104  
   1.105 -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;
   1.106 +fun subst_inner_asm_tac ctx th =  
   1.107 +   curry (curry (FIRST' (map uncurry (map uncurry (map subst_inner_asm_tac_aux 
   1.108 +                                                             (1 upto Thm.nprems_of th)))))) ctx th;
   1.109  
   1.110  fun fresh_fun_tac no_asm i thm = 
   1.111    (* Find the variable we instantiate *)
   1.112 @@ -151,7 +153,8 @@
   1.113      val goal = nth (prems_of thm) (i-1);
   1.114      val atom_name_opt = get_inner_fresh_fun goal;
   1.115      val n = List.length (Logic.strip_params goal);
   1.116 -    (* Here we rely on the fact that the variable introduced by generate_fresh_tac is the last one in the list, the inner one *)
   1.117 +    (* Here we rely on the fact that the variable introduced by generate_fresh_tac *)
   1.118 +    (* is the last one in the list, the inner one *)
   1.119    in
   1.120    case atom_name_opt of 
   1.121      NONE => all_tac thm