src/HOL/Nominal/nominal_permeq.ML
changeset 17870 c35381811d5c
child 18012 23e6cfda8c4b
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Mon Oct 17 12:30:57 2005 +0200
     1.3 @@ -0,0 +1,109 @@
     1.4 +(* $Id$ *)
     1.5 +
     1.6 +(* METHOD FOR ANALYSING EQUATION INVOLVING PERMUTATION *)
     1.7 +
     1.8 +local
     1.9 +
    1.10 +(* applies the expand_fun_eq rule to the first goal and strips off all universal quantifiers *)
    1.11 +val Expand_Fun_Eq_tac =    
    1.12 +    ("extensionality on functions",
    1.13 +    EVERY [simp_tac (HOL_basic_ss addsimps [expand_fun_eq]) 1, REPEAT_DETERM (rtac allI 1)]);
    1.14 +
    1.15 +(* applies the perm_compose rule - this rule would loop in the simplifier *)
    1.16 +fun Apply_Perm_Compose_tac ctxt = 
    1.17 +    let 
    1.18 +	val perm_compose = PureThy.get_thm (ProofContext.theory_of ctxt) (Name ("perm_compose"));
    1.19 +    in ("analysing permutation compositions",rtac (perm_compose RS trans)  1)
    1.20 +    end;
    1.21 +
    1.22 +(* unfolds the definition of permutations applied to functions *)
    1.23 +fun Unfold_Perm_Fun_Def_tac ctxt = 
    1.24 +    let 
    1.25 +	val perm_fun_def = PureThy.get_thm (ProofContext.theory_of ctxt) (Name ("nominal.perm_fun_def"))
    1.26 +    in ("unfolding of perms on functions", simp_tac (HOL_basic_ss addsimps [perm_fun_def]) 1)
    1.27 +    end
    1.28 +    
    1.29 +(* applies the perm_eq_lam and perm_eq_app simplifications *)
    1.30 +fun Apply_SimProc_tac ctxt = 
    1.31 +    let
    1.32 +        val thy = ProofContext.theory_of ctxt;
    1.33 +	val perm_app_eq = PureThy.get_thm thy (Name ("perm_app_eq"));
    1.34 +        val perm_lam_eq = PureThy.get_thm thy (Name ("perm_eq_lam"));
    1.35 +    in
    1.36 +	("simplification of permutation on applications and lambdas", 
    1.37 +	 asm_full_simp_tac (HOL_basic_ss addsimps [perm_app_eq,perm_lam_eq]) 1)
    1.38 +    end;
    1.39 +
    1.40 +(* applying Stefan's smart congruence tac *)
    1.41 +val Apply_Cong_tac = ("application of congruence",
    1.42 +                     (fn st => DatatypeAux.cong_tac  1 st handle Subscript => no_tac st));
    1.43 +
    1.44 +(* initial simplification step in the tactic *)
    1.45 +fun Initial_Simp_tac thms ctxt =
    1.46 +    let
    1.47 +	val thy = ProofContext.theory_of ctxt;
    1.48 +	val perm_swap  = PureThy.get_thm thy (Name ("perm_swap"));
    1.49 +        val perm_fresh = PureThy.get_thm thy (Name ("perm_fresh_fresh"));
    1.50 +        val perm_bij   = PureThy.get_thm thy (Name ("perm_bij"));
    1.51 +        val simps = (local_simpset_of ctxt) addsimps (thms @ [perm_swap,perm_fresh,perm_bij])
    1.52 +    in
    1.53 +      ("general simplification step", FIRST [rtac conjI 1, asm_full_simp_tac simps 1])
    1.54 +    end;
    1.55 +
    1.56 +
    1.57 +(* debugging *)
    1.58 +fun DEBUG_tac (msg,tac) = 
    1.59 +    EVERY [print_tac ("before application of "^msg), CHANGED tac, print_tac ("after "^msg)]; 
    1.60 +fun NO_DEBUG_tac (_,tac) = CHANGED tac; 
    1.61 +
    1.62 +(* Main Tactic *)
    1.63 +(* "repeating"-depth is set to 40 - this seems sufficient *)
    1.64 +fun perm_simp_tac tactical thms ctxt = 
    1.65 +    REPEAT_DETERM_N 40 
    1.66 +      (FIRST[tactical (Initial_Simp_tac thms ctxt),
    1.67 +             tactical (Apply_Perm_Compose_tac ctxt),
    1.68 +             tactical (Apply_SimProc_tac ctxt),
    1.69 +             tactical Apply_Cong_tac, 
    1.70 +             tactical (Unfold_Perm_Fun_Def_tac ctxt),
    1.71 +             tactical Expand_Fun_Eq_tac]);
    1.72 +
    1.73 +(* tactic that unfolds first the support definition *)
    1.74 +(* and then applies perm_simp                       *)
    1.75 +fun supports_tac tactical thms ctxt =
    1.76 +  let
    1.77 +    val thy = ProofContext.theory_of ctxt;
    1.78 +    val supports_def = PureThy.get_thm thy (Name ("nominal.op supports_def"));
    1.79 +    val fresh_def    = PureThy.get_thm thy (Name ("nominal.fresh_def"));
    1.80 +    val fresh_prod   = PureThy.get_thm thy (Name ("nominal.fresh_prod"));
    1.81 +    val simps        = [supports_def,symmetric fresh_def,fresh_prod];
    1.82 +
    1.83 +  in
    1.84 +      EVERY [tactical ("unfolding of supports",simp_tac (HOL_basic_ss addsimps simps) 1),
    1.85 +             tactical ("stripping of foralls " ,REPEAT_DETERM (rtac allI 1)),
    1.86 +             tactical ("geting rid of the imp",rtac impI 1),
    1.87 +             tactical ("eliminating conjuncts",REPEAT_DETERM (etac  conjE 1)),
    1.88 +             tactical ("applying perm_simp   ",perm_simp_tac tactical thms ctxt)]
    1.89 +  end;
    1.90 +
    1.91 +in             
    1.92 +
    1.93 +val perm_eq_meth = 
    1.94 +    Method.thms_ctxt_args 
    1.95 +	(fn thms => fn ctxt => Method.SIMPLE_METHOD (DETERM (perm_simp_tac NO_DEBUG_tac thms ctxt)));
    1.96 +
    1.97 +val perm_eq_meth_debug = 
    1.98 +    Method.thms_ctxt_args 
    1.99 +	(fn thms => fn ctxt => Method.SIMPLE_METHOD (DETERM (perm_simp_tac DEBUG_tac thms ctxt)));
   1.100 +
   1.101 +val supports_meth = 
   1.102 +    Method.thms_ctxt_args 
   1.103 +	(fn thms => fn ctxt => Method.SIMPLE_METHOD (DETERM (supports_tac NO_DEBUG_tac thms ctxt)));
   1.104 +
   1.105 +val supports_meth_debug = 
   1.106 +    Method.thms_ctxt_args 
   1.107 +	(fn thms => fn ctxt => Method.SIMPLE_METHOD (DETERM (supports_tac DEBUG_tac thms ctxt)));
   1.108 +
   1.109 +end
   1.110 +
   1.111 +
   1.112 +