- Equivariance simpset used in proofs of strong induction and inversion
authorberghofe
Wed Jun 25 14:54:45 2008 +0200 (2008-06-25)
changeset 273528adeff7fd4bc
parent 27351 6b120fb45278
child 27353 71c4dd53d4cb
- 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
src/HOL/Nominal/nominal_inductive.ML
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Wed Jun 25 12:15:05 2008 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Jun 25 14:54:45 2008 +0200
     1.3 @@ -136,9 +136,11 @@
     1.4            REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))])
     1.5    in Option.map prove (map_term f prop (the_default prop opt)) end;
     1.6  
     1.7 +val eta_contract_cterm = Thm.dest_arg o Thm.cprop_of o Thm.eta_conversion;
     1.8 +
     1.9  fun first_order_matchs pats objs = Thm.first_order_match
    1.10 -  (Conjunction.mk_conjunction_balanced pats,
    1.11 -   Conjunction.mk_conjunction_balanced objs);
    1.12 +  (eta_contract_cterm (Conjunction.mk_conjunction_balanced pats),
    1.13 +   eta_contract_cterm (Conjunction.mk_conjunction_balanced objs));
    1.14  
    1.15  fun first_order_mrs ths th = ths MRS
    1.16    Thm.instantiate (first_order_matchs (cprems_of th) (map cprop_of ths)) th;
    1.17 @@ -274,8 +276,10 @@
    1.18      val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
    1.19      val pt2_atoms = map (fn aT => PureThy.get_thm thy
    1.20        ("pt_" ^ Sign.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
    1.21 -    val eqvt_ss = HOL_basic_ss addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
    1.22 -      addsimprocs [mk_perm_bool_simproc ["Fun.id"]];
    1.23 +    val eqvt_ss = Simplifier.theory_context thy HOL_basic_ss
    1.24 +      addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
    1.25 +      addsimprocs [mk_perm_bool_simproc ["Fun.id"],
    1.26 +        NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
    1.27      val fresh_bij = PureThy.get_thms thy "fresh_bij";
    1.28      val perm_bij = PureThy.get_thms thy "perm_bij";
    1.29      val fs_atoms = map (fn aT => PureThy.get_thm thy
    1.30 @@ -452,7 +456,13 @@
    1.31                     concl))
    1.32            in map mk_prem prems end) cases_prems;
    1.33  
    1.34 -    val cases_eqvt_ss = HOL_ss addsimps eqvt_thms @ calc_atm delsplits [split_if];
    1.35 +    val cases_eqvt_ss = Simplifier.theory_context thy HOL_ss
    1.36 +      addsimps eqvt_thms @ fresh_atm @ perm_pi_simp delsplits [split_if]
    1.37 +      addsimprocs [NominalPermeq.perm_simproc_app,
    1.38 +        NominalPermeq.perm_simproc_fun];
    1.39 +
    1.40 +    val simp_fresh_atm = map
    1.41 +      (Simplifier.simplify (HOL_basic_ss addsimps fresh_atm));
    1.42  
    1.43      fun mk_cases_proof thy ((((name, thss), elim), (prem, args, concl, prems)),
    1.44          prems') =
    1.45 @@ -514,16 +524,20 @@
    1.46                         SUBPROOF (fn {prems = fresh_hyps, ...} =>
    1.47                           let
    1.48                             val fresh_hyps' = NominalPackage.mk_not_sym fresh_hyps;
    1.49 -                           val case_ss = cases_eqvt_ss addsimps
    1.50 -                             vc_compat_ths' @ freshs2' @ fresh_hyps'
    1.51 +                           val case_ss = cases_eqvt_ss addsimps freshs2' @
    1.52 +                             simp_fresh_atm (vc_compat_ths' @ fresh_hyps');
    1.53                             val fresh_fresh_ss = case_ss addsimps perm_fresh_fresh;
    1.54 +                           val calc_atm_ss = case_ss addsimps calc_atm;
    1.55                             val hyps1' = map
    1.56                               (mk_pis #> Simplifier.simplify fresh_fresh_ss) hyps1;
    1.57                             val hyps2' = map
    1.58                               (mk_pis #> Simplifier.simplify case_ss) hyps2;
    1.59 -                           val case_hyps' = hyps1' @ hyps2'
    1.60 +                           (* calc_atm must be applied last, since *)
    1.61 +                           (* it may interfere with other rules    *)
    1.62 +                           val case_hyps' = map
    1.63 +                             (Simplifier.simplify calc_atm_ss) (hyps1' @ hyps2')
    1.64                           in
    1.65 -                           simp_tac case_ss 1 THEN
    1.66 +                           simp_tac calc_atm_ss 1 THEN
    1.67                             REPEAT_DETERM (TRY (rtac conjI 1) THEN
    1.68                               resolve_tac case_hyps' 1)
    1.69                           end) ctxt4 1)