# HG changeset patch
# User berghofe
# Date 1214398485 -7200
# Node ID 8adeff7fd4bc9e317594f2acc326cb70efa6af0f
# Parent  6b120fb452785f3435ec0c12cbe3df436fb5258c
- Equivariance simpset used in proofs of strong induction and inversion
  rules now contains perm_simproc_app and perm_simproc_fun as well
- first_order_matchs now eta-contracts terms before matching
- Rewrote code for proving strong inversion rule to avoid failure when
  one of the arguments of the inductive predicate has an atom type

diff -r 6b120fb45278 -r 8adeff7fd4bc src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Wed Jun 25 12:15:05 2008 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Jun 25 14:54:45 2008 +0200
@@ -136,9 +136,11 @@
           REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))])
   in Option.map prove (map_term f prop (the_default prop opt)) end;
 
+val eta_contract_cterm = Thm.dest_arg o Thm.cprop_of o Thm.eta_conversion;
+
 fun first_order_matchs pats objs = Thm.first_order_match
-  (Conjunction.mk_conjunction_balanced pats,
-   Conjunction.mk_conjunction_balanced objs);
+  (eta_contract_cterm (Conjunction.mk_conjunction_balanced pats),
+   eta_contract_cterm (Conjunction.mk_conjunction_balanced objs));
 
 fun first_order_mrs ths th = ths MRS
   Thm.instantiate (first_order_matchs (cprems_of th) (map cprop_of ths)) th;
@@ -274,8 +276,10 @@
     val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
     val pt2_atoms = map (fn aT => PureThy.get_thm thy
       ("pt_" ^ Sign.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
-    val eqvt_ss = HOL_basic_ss addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
-      addsimprocs [mk_perm_bool_simproc ["Fun.id"]];
+    val eqvt_ss = Simplifier.theory_context thy HOL_basic_ss
+      addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
+      addsimprocs [mk_perm_bool_simproc ["Fun.id"],
+        NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
     val fresh_bij = PureThy.get_thms thy "fresh_bij";
     val perm_bij = PureThy.get_thms thy "perm_bij";
     val fs_atoms = map (fn aT => PureThy.get_thm thy
@@ -452,7 +456,13 @@
                    concl))
           in map mk_prem prems end) cases_prems;
 
-    val cases_eqvt_ss = HOL_ss addsimps eqvt_thms @ calc_atm delsplits [split_if];
+    val cases_eqvt_ss = Simplifier.theory_context thy HOL_ss
+      addsimps eqvt_thms @ fresh_atm @ perm_pi_simp delsplits [split_if]
+      addsimprocs [NominalPermeq.perm_simproc_app,
+        NominalPermeq.perm_simproc_fun];
+
+    val simp_fresh_atm = map
+      (Simplifier.simplify (HOL_basic_ss addsimps fresh_atm));
 
     fun mk_cases_proof thy ((((name, thss), elim), (prem, args, concl, prems)),
         prems') =
@@ -514,16 +524,20 @@
                        SUBPROOF (fn {prems = fresh_hyps, ...} =>
                          let
                            val fresh_hyps' = NominalPackage.mk_not_sym fresh_hyps;
-                           val case_ss = cases_eqvt_ss addsimps
-                             vc_compat_ths' @ freshs2' @ fresh_hyps'
+                           val case_ss = cases_eqvt_ss addsimps freshs2' @
+                             simp_fresh_atm (vc_compat_ths' @ fresh_hyps');
                            val fresh_fresh_ss = case_ss addsimps perm_fresh_fresh;
+                           val calc_atm_ss = case_ss addsimps calc_atm;
                            val hyps1' = map
                              (mk_pis #> Simplifier.simplify fresh_fresh_ss) hyps1;
                            val hyps2' = map
                              (mk_pis #> Simplifier.simplify case_ss) hyps2;
-                           val case_hyps' = hyps1' @ hyps2'
+                           (* calc_atm must be applied last, since *)
+                           (* it may interfere with other rules    *)
+                           val case_hyps' = map
+                             (Simplifier.simplify calc_atm_ss) (hyps1' @ hyps2')
                          in
-                           simp_tac case_ss 1 THEN
+                           simp_tac calc_atm_ss 1 THEN
                            REPEAT_DETERM (TRY (rtac conjI 1) THEN
                              resolve_tac case_hyps' 1)
                          end) ctxt4 1)