improved the decision-procedure for permutations;
authorurbanc
Sun Feb 26 22:24:05 2006 +0100 (2006-02-26)
changeset 19139af69e41eab5d
parent 19138 42ff710d432f
child 19140 5a98cdf99079
improved the decision-procedure for permutations;
now uses a simproc

FIXME:
the simproc still needs to be adapted for arbitrary
atom types
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_permeq.ML
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sat Feb 25 15:19:47 2006 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sun Feb 26 22:24:05 2006 +0100
     1.3 @@ -658,7 +658,8 @@
     1.4         val pt_fresh_fresh    = thm "nominal.pt_fresh_fresh";
     1.5         val pt_bij            = thm "nominal.pt_bij";
     1.6         val pt_perm_compose   = thm "nominal.pt_perm_compose";
     1.7 -       val perm_eq_app       = thm "nominal.perm_eq_app";
     1.8 +       val pt_perm_compose'  = thm "nominal.pt_perm_compose'";
     1.9 +       val perm_app          = thm "nominal.pt_fun_app_eq";
    1.10         val at_fresh          = thm "nominal.at_fresh";
    1.11         val at_calc           = thms "nominal.at_calc";
    1.12         val at_supp           = thm "nominal.at_supp";
    1.13 @@ -667,6 +668,8 @@
    1.14         val fresh_left        = thm "nominal.pt_fresh_left";
    1.15         val fresh_bij_ineq    = thm "nominal.pt_fresh_bij_ineq";
    1.16         val fresh_bij         = thm "nominal.pt_fresh_bij";
    1.17 +       val pt_pi_rev         = thm "nominal.pt_pi_rev";
    1.18 +       val pt_rev_pi         = thm "nominal.pt_rev_pi";
    1.19  
    1.20         (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
    1.21         (* types; this allows for example to use abs_perm (which is a      *)
    1.22 @@ -732,13 +735,18 @@
    1.23              thy32 
    1.24  	    |>   PureThy.add_thmss [(("alpha", inst_pt_at [abs_fun_eq]),[])]
    1.25              ||>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij]),[])]
    1.26 +            ||>> PureThy.add_thmss 
    1.27 +	      let val thms1 = inst_pt_at [pt_pi_rev];
    1.28 +		  val thms2 = inst_pt_at [pt_rev_pi];
    1.29 +              in [(("perm_pi_simp",thms1 @ thms2),[])] end
    1.30              ||>> PureThy.add_thmss [(("perm_fresh_fresh", inst_pt_at [pt_fresh_fresh]),[])]
    1.31              ||>> PureThy.add_thmss [(("perm_bij", inst_pt_at [pt_bij]),[])]
    1.32              ||>> PureThy.add_thmss 
    1.33  	      let val thms1 = inst_pt_at [pt_perm_compose];
    1.34  		  val thms2 = instR cp1 (Library.flat cps');
    1.35                in [(("perm_compose",thms1 @ thms2),[])] end
    1.36 -            ||>> PureThy.add_thmss [(("perm_app_eq", inst_pt_at [perm_eq_app]),[])]
    1.37 +            ||>> PureThy.add_thmss [(("perm_compose'",inst_pt_at [pt_perm_compose']),[])] 
    1.38 +            ||>> PureThy.add_thmss [(("perm_app", inst_pt_at [perm_app]),[])]
    1.39              ||>> PureThy.add_thmss [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])]
    1.40              ||>> PureThy.add_thmss [(("fresh_atm", inst_at [at_fresh]),[])]
    1.41              ||>> PureThy.add_thmss [(("calc_atm", inst_at at_calc),[])]
     2.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Sat Feb 25 15:19:47 2006 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Sun Feb 26 22:24:05 2006 +0100
     2.3 @@ -2,38 +2,72 @@
     2.4  
     2.5  (* METHOD FOR ANALYSING EQUATION INVOLVING PERMUTATION *)
     2.6  
     2.7 -(* tries until depth 40 the following (in that order):                     *)
     2.8 -(*                                                                         *)
     2.9 -(*  - simplification plus analysing perm_swaps, perm_fresh_fresh, perm_bij *)
    2.10 -(*  - permutation compositions (on the left hand side of =)                *)
    2.11 -(*  - simplification of permutation on applications and abstractions       *)
    2.12 -(*  - analysing congruences (from Stefan Berghofer's datatype pkg)         *)
    2.13 -(*  - unfolding permutation on functions                                   *)
    2.14 -(*  - expanding equalities of functions                                    *)
    2.15 -(*                                                                         *)
    2.16 -(*  for supports - it first unfolds the definitions and strips of intros   *)
    2.17 -
    2.18  local
    2.19  
    2.20  (* pulls out dynamically a thm via the simpset *)
    2.21  fun dynamic_thms ss name = 
    2.22      ProofContext.get_thms (Simplifier.the_context ss) (Name name);
    2.23 +fun dynamic_thm ss name = 
    2.24 +    ProofContext.get_thm (Simplifier.the_context ss) (Name name);
    2.25  
    2.26 +(* FIXME: make it usable for all atom-types *)
    2.27  (* initial simplification step in the tactic *)
    2.28 -fun initial_simp_tac ss i =
    2.29 +fun perm_eval_tac ss i =
    2.30      let
    2.31 +        val perm_eq_app   = thm "nominal.pt_fun_app_eq";
    2.32 +        val at_inst       = dynamic_thm ss "at_name_inst";
    2.33 +        val pt_inst       = dynamic_thm ss "pt_name_inst";
    2.34 +
    2.35 +        fun perm_eval_simproc sg ss redex =
    2.36 +        (case redex of 
    2.37 +        (* case pi o (f x) == (pi o f) (pi o x)    *)
    2.38 +        (* special treatment in cases of constants *)
    2.39 +        (Const("nominal.perm",Type("fun",[Type("List.list",[Type("*",[ty,_])]),_])) $ pi $ (f $ x)) 
    2.40 +        => let
    2.41 +             val _ = warning ("type: "^Sign.string_of_typ (sign_of (the_context())) ty)
    2.42 +           in
    2.43 +
    2.44 +           (case f of
    2.45 +                    (* nothing to do on constants *)
    2.46 +                    (* FIXME: proper treatment of constants *)
    2.47 +                      Const(_,_)                   => NONE
    2.48 +                    | (Const(_,_) $ _)             => NONE
    2.49 +                    | ((Const(_,_) $ _) $ _)       => NONE
    2.50 +                    | (((Const(_,_) $ _) $ _) $ _) => NONE
    2.51 +                    | _ => 
    2.52 +                       (* FIXME: analyse type here or at "pty"*)
    2.53 +		       SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection))
    2.54 +            end
    2.55 +
    2.56 +        (* case pi o (%x. f x) == (%x. pi o (f ((rev pi)o x))) *)
    2.57 +        | (Const("nominal.perm",_) $ pi $ (Abs _)) 
    2.58 +        => let 
    2.59 +             val perm_fun_def = thm "nominal.perm_fun_def"
    2.60 +           in SOME (perm_fun_def) end
    2.61 +
    2.62 +        (* no redex otherwise *) 
    2.63 +        | _ => NONE);
    2.64 +
    2.65 +	val perm_eval =
    2.66 +	    Simplifier.simproc (Theory.sign_of (the_context ())) "perm_eval" 
    2.67 +	    ["nominal.perm pi x"] perm_eval_simproc;
    2.68 +
    2.69          (* these lemmas are created dynamically according to the atom types *) 
    2.70 -	val perm_swap  = dynamic_thms ss "perm_swap";
    2.71 -        val perm_fresh = dynamic_thms ss "perm_fresh_fresh";
    2.72 -        val perm_bij   = dynamic_thms ss "perm_bij";
    2.73 -        val ss' = ss addsimps (perm_swap@perm_fresh@perm_bij)
    2.74 +	val perm_swap     = dynamic_thms ss "perm_swap";
    2.75 +        val perm_fresh    = dynamic_thms ss "perm_fresh_fresh";
    2.76 +        val perm_bij      = dynamic_thms ss "perm_bij";
    2.77 +        val perm_compose' = dynamic_thms ss "perm_compose'";
    2.78 +        val perm_pi_simp  = dynamic_thms ss "perm_pi_simp";
    2.79 +        val ss' = ss addsimps (perm_swap@perm_fresh@perm_bij@perm_compose'@perm_pi_simp)
    2.80 +                     addsimprocs [perm_eval];
    2.81 +                    
    2.82      in
    2.83        ("general simplification step", FIRST [rtac conjI i, asm_full_simp_tac ss' i])
    2.84      end;
    2.85  
    2.86  (* applies the perm_compose rule - this rule would loop in the simplifier     *)
    2.87  (* in case there are more atom-types we have to check every possible instance *)
    2.88 -(* of perm_compose *)
    2.89 +(* of perm_compose                                                            *)
    2.90  fun apply_perm_compose_tac ss i = 
    2.91      let
    2.92  	val perm_compose = dynamic_thms ss "perm_compose"; 
    2.93 @@ -42,18 +76,6 @@
    2.94  	("analysing permutation compositions on the lhs",FIRST (tacs))
    2.95      end
    2.96  
    2.97 -(* applies the perm_eq_lam and perm_eq_app simplifications     *)
    2.98 -(* FIXME: it seems the order of perm_app_eq and perm_lam_eq is *)
    2.99 -(* significant                                                 *)   
   2.100 -fun apply_app_lam_simp_tac ss i =
   2.101 -    let 
   2.102 -	val perm_app_eq  = dynamic_thms ss "perm_app_eq";
   2.103 -        val perm_lam_eq  = thm "nominal.perm_eq_lam"
   2.104 -    in
   2.105 -     ("simplification of permutations on applications and lambdas", 
   2.106 -      asm_full_simp_tac (HOL_basic_ss addsimps (perm_app_eq@[perm_lam_eq])) i)
   2.107 -    end
   2.108 -
   2.109  (* applying Stefan's smart congruence tac *)
   2.110  fun apply_cong_tac i = 
   2.111      ("application of congruence",
   2.112 @@ -80,18 +102,22 @@
   2.113  
   2.114  (* Main Tactic *)
   2.115  
   2.116 -(* "repeating"-depth is set to 40 - this seems sufficient *)
   2.117  fun perm_simp_tac tactical ss i = 
   2.118 +    DETERM (tactical (perm_eval_tac ss i));
   2.119 +
   2.120 +(* perm_simp_tac plus additional tactics to decide            *)
   2.121 +(* support problems                                           *)
   2.122 +(* the "repeating"-depth is set to 40 - this seems sufficient *)
   2.123 +fun perm_supports_tac tactical ss i = 
   2.124      DETERM (REPEAT_DETERM_N 40 
   2.125 -      (FIRST[tactical (initial_simp_tac ss i),
   2.126 +      (FIRST[tactical (perm_eval_tac ss i),
   2.127               tactical (apply_perm_compose_tac ss i),
   2.128 -             tactical (apply_app_lam_simp_tac ss i),
   2.129               tactical (apply_cong_tac i), 
   2.130               tactical (unfold_perm_fun_def_tac i),
   2.131               tactical (expand_fun_eq_tac i)]));
   2.132  
   2.133 -(* tactic that first unfolds the support definition *)
   2.134 -(* and strips of intros, then applies perm_simp_tac *)
   2.135 +(* tactic that first unfolds the support definition          *)
   2.136 +(* and strips off the intros, then applies perm_supports_tac *)
   2.137  fun supports_tac tactical ss i =
   2.138    let 
   2.139        val supports_def = thm "nominal.op supports_def";
   2.140 @@ -103,7 +129,7 @@
   2.141               tactical ("stripping of foralls  " ,REPEAT_DETERM (rtac allI i)),
   2.142               tactical ("geting rid of the imps",rtac impI i),
   2.143               tactical ("eliminating conjuncts ",REPEAT_DETERM (etac  conjE i)),
   2.144 -             tactical ("applying perm_simp    ",perm_simp_tac tactical ss i)]
   2.145 +             tactical ("applying perm_simp    ",perm_supports_tac tactical ss i)]
   2.146    end;
   2.147  
   2.148  in