src/HOL/Nominal/nominal_permeq.ML
changeset 18012 23e6cfda8c4b
parent 17870 c35381811d5c
child 18046 b7389981170b
     1.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Fri Oct 28 16:35:40 2005 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Fri Oct 28 16:43:46 2005 +0200
     1.3 @@ -2,106 +2,121 @@
     1.4  
     1.5  (* METHOD FOR ANALYSING EQUATION INVOLVING PERMUTATION *)
     1.6  
     1.7 +(* tries until depth 40 the following (in that order):                     *)
     1.8 +(*                                                                         *)
     1.9 +(*  - simplification plus analysing perm_swaps, perm_fresh_fresh, perm_bij *)
    1.10 +(*  - permutation compositions (on the left hand side of =)                *)
    1.11 +(*  - simplification of permutation on applications and abstractions       *)
    1.12 +(*  - analysing congruences (from Stefan Berghofer's datatype pkg)         *)
    1.13 +(*  - unfolding permutation on functions                                   *)
    1.14 +(*  - expanding equalities of functions                                    *)
    1.15 +(*                                                                         *)
    1.16 +(*  for supports - it first unfolds the definitions and strips of intros   *)
    1.17 +
    1.18  local
    1.19  
    1.20 -(* applies the expand_fun_eq rule to the first goal and strips off all universal quantifiers *)
    1.21 -val Expand_Fun_Eq_tac =    
    1.22 -    ("extensionality on functions",
    1.23 -    EVERY [simp_tac (HOL_basic_ss addsimps [expand_fun_eq]) 1, REPEAT_DETERM (rtac allI 1)]);
    1.24 +(* pulls out dynamically a thm via the simpset *)
    1.25 +fun dynamic_thm ss name = 
    1.26 +    ProofContext.get_thm (Simplifier.the_context ss) (Name name);
    1.27 +
    1.28 +(* initial simplification step in the tactic *)
    1.29 +fun initial_simp_tac ss i =
    1.30 +    let
    1.31 +	val perm_swap  = dynamic_thm ss "perm_swap";
    1.32 +        val perm_fresh = dynamic_thm ss "perm_fresh_fresh";
    1.33 +        val perm_bij   = dynamic_thm ss "perm_bij";
    1.34 +        val ss' = ss addsimps [perm_swap,perm_fresh,perm_bij]
    1.35 +    in
    1.36 +      ("general simplification step", FIRST [rtac conjI i, asm_full_simp_tac ss' i])
    1.37 +    end;
    1.38  
    1.39  (* applies the perm_compose rule - this rule would loop in the simplifier *)
    1.40 -fun Apply_Perm_Compose_tac ctxt = 
    1.41 +fun apply_perm_compose_tac ss i = 
    1.42 +    let
    1.43 +	val perm_compose = dynamic_thm ss "perm_compose"; 
    1.44 +    in
    1.45 +	("analysing permutation compositions on the lhs",rtac (perm_compose RS trans)  i)
    1.46 +    end
    1.47 +
    1.48 +
    1.49 +(* applies the perm_eq_lam and perm_eq_app simplifications *)
    1.50 +fun apply_app_lam_simp_tac ss i =
    1.51      let 
    1.52 -	val perm_compose = PureThy.get_thm (ProofContext.theory_of ctxt) (Name ("perm_compose"));
    1.53 -    in ("analysing permutation compositions",rtac (perm_compose RS trans)  1)
    1.54 -    end;
    1.55 +	val perm_app_eq  = dynamic_thm ss "perm_app_eq";
    1.56 +        val perm_lam_eq  = dynamic_thm ss "perm_eq_lam"
    1.57 +    in
    1.58 +     ("simplification of permutations on applications and lambdas", 
    1.59 +      asm_full_simp_tac (HOL_basic_ss addsimps [perm_app_eq,perm_lam_eq]) i)
    1.60 +    end
    1.61 +
    1.62 +(* applying Stefan's smart congruence tac *)
    1.63 +fun apply_cong_tac i = 
    1.64 +    ("application of congruence",
    1.65 +     (fn st => DatatypeAux.cong_tac  i st handle Subscript => no_tac st));
    1.66  
    1.67  (* unfolds the definition of permutations applied to functions *)
    1.68 -fun Unfold_Perm_Fun_Def_tac ctxt = 
    1.69 -    let 
    1.70 -	val perm_fun_def = PureThy.get_thm (ProofContext.theory_of ctxt) (Name ("nominal.perm_fun_def"))
    1.71 -    in ("unfolding of perms on functions", simp_tac (HOL_basic_ss addsimps [perm_fun_def]) 1)
    1.72 +fun unfold_perm_fun_def_tac i = 
    1.73 +    let
    1.74 +	val perm_fun_def = thm "nominal.perm_fun_def"
    1.75 +    in
    1.76 +	("unfolding of permutations on functions", 
    1.77 +	 simp_tac (HOL_basic_ss addsimps [perm_fun_def]) i)
    1.78      end
    1.79 -    
    1.80 -(* applies the perm_eq_lam and perm_eq_app simplifications *)
    1.81 -fun Apply_SimProc_tac ctxt = 
    1.82 -    let
    1.83 -        val thy = ProofContext.theory_of ctxt;
    1.84 -	val perm_app_eq = PureThy.get_thm thy (Name ("perm_app_eq"));
    1.85 -        val perm_lam_eq = PureThy.get_thm thy (Name ("perm_eq_lam"));
    1.86 -    in
    1.87 -	("simplification of permutation on applications and lambdas", 
    1.88 -	 asm_full_simp_tac (HOL_basic_ss addsimps [perm_app_eq,perm_lam_eq]) 1)
    1.89 -    end;
    1.90  
    1.91 -(* applying Stefan's smart congruence tac *)
    1.92 -val Apply_Cong_tac = ("application of congruence",
    1.93 -                     (fn st => DatatypeAux.cong_tac  1 st handle Subscript => no_tac st));
    1.94 -
    1.95 -(* initial simplification step in the tactic *)
    1.96 -fun Initial_Simp_tac thms ctxt =
    1.97 -    let
    1.98 -	val thy = ProofContext.theory_of ctxt;
    1.99 -	val perm_swap  = PureThy.get_thm thy (Name ("perm_swap"));
   1.100 -        val perm_fresh = PureThy.get_thm thy (Name ("perm_fresh_fresh"));
   1.101 -        val perm_bij   = PureThy.get_thm thy (Name ("perm_bij"));
   1.102 -        val simps = (local_simpset_of ctxt) addsimps (thms @ [perm_swap,perm_fresh,perm_bij])
   1.103 -    in
   1.104 -      ("general simplification step", FIRST [rtac conjI 1, asm_full_simp_tac simps 1])
   1.105 -    end;
   1.106 -
   1.107 +(* applies the expand_fun_eq rule to the first goal and strips off all universal quantifiers *)
   1.108 +fun expand_fun_eq_tac i =    
   1.109 +    ("extensionality expansion of functions",
   1.110 +    EVERY [simp_tac (HOL_basic_ss addsimps [expand_fun_eq]) i, REPEAT_DETERM (rtac allI i)]);
   1.111  
   1.112  (* debugging *)
   1.113  fun DEBUG_tac (msg,tac) = 
   1.114 -    EVERY [print_tac ("before application of "^msg), CHANGED tac, print_tac ("after "^msg)]; 
   1.115 +    EVERY [CHANGED tac, print_tac ("after "^msg)]; 
   1.116  fun NO_DEBUG_tac (_,tac) = CHANGED tac; 
   1.117  
   1.118  (* Main Tactic *)
   1.119 +
   1.120  (* "repeating"-depth is set to 40 - this seems sufficient *)
   1.121 -fun perm_simp_tac tactical thms ctxt = 
   1.122 -    REPEAT_DETERM_N 40 
   1.123 -      (FIRST[tactical (Initial_Simp_tac thms ctxt),
   1.124 -             tactical (Apply_Perm_Compose_tac ctxt),
   1.125 -             tactical (Apply_SimProc_tac ctxt),
   1.126 -             tactical Apply_Cong_tac, 
   1.127 -             tactical (Unfold_Perm_Fun_Def_tac ctxt),
   1.128 -             tactical Expand_Fun_Eq_tac]);
   1.129 +fun perm_simp_tac tactical ss i = 
   1.130 +    DETERM (REPEAT_DETERM_N 40 
   1.131 +      (FIRST[tactical (initial_simp_tac ss i),
   1.132 +             tactical (apply_perm_compose_tac ss i),
   1.133 +             tactical (apply_app_lam_simp_tac ss i),
   1.134 +             tactical (apply_cong_tac i), 
   1.135 +             tactical (unfold_perm_fun_def_tac i),
   1.136 +             tactical (expand_fun_eq_tac i)]));
   1.137  
   1.138 -(* tactic that unfolds first the support definition *)
   1.139 -(* and then applies perm_simp                       *)
   1.140 -fun supports_tac tactical thms ctxt =
   1.141 -  let
   1.142 -    val thy = ProofContext.theory_of ctxt;
   1.143 -    val supports_def = PureThy.get_thm thy (Name ("nominal.op supports_def"));
   1.144 -    val fresh_def    = PureThy.get_thm thy (Name ("nominal.fresh_def"));
   1.145 -    val fresh_prod   = PureThy.get_thm thy (Name ("nominal.fresh_prod"));
   1.146 -    val simps        = [supports_def,symmetric fresh_def,fresh_prod];
   1.147 -
   1.148 +(* tactic that first unfolds the support definition *)
   1.149 +(* and strips of intros, then applies perm_simp_tac *)
   1.150 +fun supports_tac tactical ss i =
   1.151 +  let 
   1.152 +      val supports_def = thm "nominal.op supports_def";
   1.153 +      val fresh_def    = thm "nominal.fresh_def";
   1.154 +      val fresh_prod   = thm "nominal.fresh_prod";
   1.155 +      val simps        = [supports_def,symmetric fresh_def,fresh_prod]
   1.156    in
   1.157 -      EVERY [tactical ("unfolding of supports",simp_tac (HOL_basic_ss addsimps simps) 1),
   1.158 -             tactical ("stripping of foralls " ,REPEAT_DETERM (rtac allI 1)),
   1.159 -             tactical ("geting rid of the imp",rtac impI 1),
   1.160 -             tactical ("eliminating conjuncts",REPEAT_DETERM (etac  conjE 1)),
   1.161 -             tactical ("applying perm_simp   ",perm_simp_tac tactical thms ctxt)]
   1.162 +      EVERY [tactical ("unfolding of supports ",simp_tac (HOL_basic_ss addsimps simps) i),
   1.163 +             tactical ("stripping of foralls  " ,REPEAT_DETERM (rtac allI i)),
   1.164 +             tactical ("geting rid of the imps",rtac impI i),
   1.165 +             tactical ("eliminating conjuncts ",REPEAT_DETERM (etac  conjE i)),
   1.166 +             tactical ("applying perm_simp    ",perm_simp_tac tactical ss i)]
   1.167    end;
   1.168  
   1.169  in             
   1.170  
   1.171 -val perm_eq_meth = 
   1.172 -    Method.thms_ctxt_args 
   1.173 -	(fn thms => fn ctxt => Method.SIMPLE_METHOD (DETERM (perm_simp_tac NO_DEBUG_tac thms ctxt)));
   1.174 +(* FIXME simp_modifiers' 
   1.175  
   1.176 -val perm_eq_meth_debug = 
   1.177 -    Method.thms_ctxt_args 
   1.178 -	(fn thms => fn ctxt => Method.SIMPLE_METHOD (DETERM (perm_simp_tac DEBUG_tac thms ctxt)));
   1.179 +(Markus needs to commit this)
   1.180 +*)
   1.181 +
   1.182  
   1.183 -val supports_meth = 
   1.184 -    Method.thms_ctxt_args 
   1.185 -	(fn thms => fn ctxt => Method.SIMPLE_METHOD (DETERM (supports_tac NO_DEBUG_tac thms ctxt)));
   1.186 +fun simp_meth_setup tac =
   1.187 +  Method.only_sectioned_args (Simplifier.simp_modifiers @ Splitter.split_modifiers)
   1.188 +  (Method.SIMPLE_METHOD' HEADGOAL o tac o local_simpset_of);
   1.189  
   1.190 -val supports_meth_debug = 
   1.191 -    Method.thms_ctxt_args 
   1.192 -	(fn thms => fn ctxt => Method.SIMPLE_METHOD (DETERM (supports_tac DEBUG_tac thms ctxt)));
   1.193 +val perm_eq_meth        = simp_meth_setup (perm_simp_tac NO_DEBUG_tac);
   1.194 +val perm_eq_meth_debug  = simp_meth_setup (perm_simp_tac DEBUG_tac);
   1.195 +val supports_meth       = simp_meth_setup (supports_tac NO_DEBUG_tac);
   1.196 +val supports_meth_debug = simp_meth_setup (supports_tac DEBUG_tac);
   1.197  
   1.198  end
   1.199