Added lemmas for normalizing freshness results involving fresh_star.
authorberghofe
Wed Feb 25 19:34:00 2009 +0100 (2009-02-25)
changeset 300929c3b1c136d1f
parent 30091 2fb0b721e9c2
child 30098 896fed07349e
Added lemmas for normalizing freshness results involving fresh_star.
src/HOL/Nominal/Nominal.thy
src/HOL/Nominal/nominal_induct.ML
     1.1 --- a/src/HOL/Nominal/Nominal.thy	Wed Feb 25 18:53:34 2009 +0100
     1.2 +++ b/src/HOL/Nominal/Nominal.thy	Wed Feb 25 19:34:00 2009 +0100
     1.3 @@ -397,6 +397,18 @@
     1.4  
     1.5  lemmas fresh_star_prod = fresh_star_prod_list fresh_star_prod_set
     1.6  
     1.7 +text {* Normalization of freshness results; cf.\ @{text nominal_induct} *}
     1.8 +
     1.9 +lemma fresh_star_unit_elim: 
    1.10 +  shows "((a::'a set)\<sharp>*() \<Longrightarrow> PROP C) \<equiv> PROP C"
    1.11 +  and "((b::'a list)\<sharp>*() \<Longrightarrow> PROP C) \<equiv> PROP C"
    1.12 +  by (simp_all add: fresh_star_def fresh_def supp_unit)
    1.13 +
    1.14 +lemma fresh_star_prod_elim: 
    1.15 +  shows "((a::'a set)\<sharp>*(x,y) \<Longrightarrow> PROP C) \<equiv> (a\<sharp>*x \<Longrightarrow> a\<sharp>*y \<Longrightarrow> PROP C)"
    1.16 +  and "((b::'a list)\<sharp>*(x,y) \<Longrightarrow> PROP C) \<equiv> (b\<sharp>*x \<Longrightarrow> b\<sharp>*y \<Longrightarrow> PROP C)"
    1.17 +  by (rule, simp_all add: fresh_star_prod)+
    1.18 +
    1.19  section {* Abstract Properties for Permutations and  Atoms *}
    1.20  (*=========================================================*)
    1.21  
     2.1 --- a/src/HOL/Nominal/nominal_induct.ML	Wed Feb 25 18:53:34 2009 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Wed Feb 25 19:34:00 2009 +0100
     2.3 @@ -1,5 +1,4 @@
     2.4 -(*  ID:         $Id$
     2.5 -    Author:     Christian Urban and Makarius
     2.6 +(*  Author:     Christian Urban and Makarius
     2.7  
     2.8  The nominal induct proof method.
     2.9  *)
    2.10 @@ -24,7 +23,8 @@
    2.11  
    2.12  val split_all_tuples =
    2.13    Simplifier.full_simplify (HOL_basic_ss addsimps
    2.14 -    [split_conv, split_paired_all, unit_all_eq1, thm "fresh_unit_elim", thm "fresh_prod_elim"]);
    2.15 +    [split_conv, split_paired_all, unit_all_eq1, @{thm fresh_unit_elim}, @{thm fresh_prod_elim}] @
    2.16 +    @{thms fresh_star_unit_elim} @ @{thms fresh_star_prod_elim});
    2.17  
    2.18  
    2.19  (* prepare rule *)