added private datatype nprod (copy of prod) to be
authorurbanc
Sat Jan 07 11:43:42 2006 +0100 (2006-01-07)
changeset 1860020ad06db427b
parent 18599 e01112713fdc
child 18601 b248754b60bc
added private datatype nprod (copy of prod) to be
used in the induction rule
src/HOL/Nominal/Nominal.thy
src/HOL/Nominal/nominal_atoms.ML
     1.1 --- a/src/HOL/Nominal/Nominal.thy	Sat Jan 07 11:36:58 2006 +0100
     1.2 +++ b/src/HOL/Nominal/Nominal.thy	Sat Jan 07 11:43:42 2006 +0100
     1.3 @@ -85,8 +85,14 @@
     1.4  datatype 'a noption = nSome 'a | nNone
     1.5  
     1.6  primrec (perm_noption)
     1.7 -  perm_Nsome_def:  "pi\<bullet>nSome(x) = nSome(pi\<bullet>x)"
     1.8 -  perm_Nnone_def:  "pi\<bullet>nNone    = nNone"
     1.9 +  perm_nSome_def: "pi\<bullet>nSome(x) = nSome(pi\<bullet>x)"
    1.10 +  perm_nNone_def: "pi\<bullet>nNone    = nNone"
    1.11 +
    1.12 +(* a "private" copy of the product type used in the nominal induct method *)
    1.13 +datatype ('a,'b) nprod = nPair 'a 'b
    1.14 +
    1.15 +primrec (perm_nprod)
    1.16 +  perm_nProd_def: "pi\<bullet>(nPair x1 x2)  = nPair (pi\<bullet>x1) (pi\<bullet>x2)"
    1.17  
    1.18  (* permutation on characters (used in strings) *)
    1.19  defs (overloaded)
    1.20 @@ -143,6 +149,12 @@
    1.21    shows "(supp (x,y)) = (supp x)\<union>(supp y)"
    1.22    by  (force simp add: supp_def Collect_imp_eq Collect_neg_eq)
    1.23  
    1.24 +lemma supp_nprod: 
    1.25 +  fixes x :: "'a"
    1.26 +  and   y :: "'b"
    1.27 +  shows "(supp (nPair x y)) = (supp x)\<union>(supp y)"
    1.28 +  by  (force simp add: supp_def Collect_imp_eq Collect_neg_eq)
    1.29 +
    1.30  lemma supp_list_nil:
    1.31    shows "supp [] = {}"
    1.32  apply(simp add: supp_def)
    1.33 @@ -244,7 +256,6 @@
    1.34    apply(simp add: fresh_def supp_some)
    1.35    done
    1.36  
    1.37 -
    1.38  text {* Normalization of freshness results; cf.\ @{text nominal_induct} *}
    1.39  
    1.40  lemma fresh_unit_elim: "(a\<sharp>() \<Longrightarrow> PROP C) == PROP C"
    1.41 @@ -625,6 +636,17 @@
    1.42  apply(rule fs1[OF fsb])
    1.43  done
    1.44  
    1.45 +lemma fs_nprod_inst:
    1.46 +  assumes fsa: "fs TYPE('a) TYPE('x)"
    1.47 +  and     fsb: "fs TYPE('b) TYPE('x)"
    1.48 +  shows "fs TYPE(('a,'b) nprod) TYPE('x)"
    1.49 +apply(unfold fs_def, rule allI)
    1.50 +apply(case_tac x)
    1.51 +apply(auto simp add: supp_nprod)
    1.52 +apply(rule fs1[OF fsa])
    1.53 +apply(rule fs1[OF fsb])
    1.54 +done
    1.55 +
    1.56  lemma fs_list_inst:
    1.57    assumes fs: "fs TYPE('a) TYPE('x)"
    1.58    shows "fs TYPE('a list) TYPE('x)"
    1.59 @@ -764,6 +786,19 @@
    1.60    apply(rule pt3[OF ptb],assumption)
    1.61    done
    1.62  
    1.63 +lemma pt_nprod_inst:
    1.64 +  assumes pta: "pt TYPE('a) TYPE('x)"
    1.65 +  and     ptb: "pt TYPE('b) TYPE('x)"
    1.66 +  shows  "pt TYPE(('a,'b) nprod) TYPE('x)"
    1.67 +  apply(auto simp add: pt_def)
    1.68 +  apply(case_tac x)
    1.69 +  apply(simp add: pt1[OF pta] pt1[OF ptb])
    1.70 +  apply(case_tac x)
    1.71 +  apply(simp add: pt2[OF pta] pt2[OF ptb])
    1.72 +  apply(case_tac x)
    1.73 +  apply(simp add: pt3[OF pta] pt3[OF ptb])
    1.74 +  done
    1.75 +
    1.76  lemma pt_fun_inst:
    1.77    assumes pta: "pt TYPE('a) TYPE('x)"
    1.78    and     ptb: "pt TYPE('b) TYPE('x)"
     2.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sat Jan 07 11:36:58 2006 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Jan 07 11:43:42 2006 +0100
     2.3 @@ -374,6 +374,7 @@
     2.4        val pt_set_inst   = thm "pt_set_inst"; 
     2.5        val pt_unit_inst  = thm "pt_unit_inst";
     2.6        val pt_prod_inst  = thm "pt_prod_inst"; 
     2.7 +      val pt_nprod_inst = thm "pt_nprod_inst"; 
     2.8        val pt_list_inst  = thm "pt_list_inst";   
     2.9        val pt_optn_inst  = thm "pt_option_inst";   
    2.10        val pt_noptn_inst = thm "pt_noption_inst";   
    2.11 @@ -410,6 +411,7 @@
    2.12       (*      option(pt_<ak>)            *)
    2.13       (*      list(pt_<ak>)              *)
    2.14       (*      *(pt_<ak>,pt_<ak>)         *)
    2.15 +     (*      nprod(pt_<ak>,pt_<ak>)     *)
    2.16       (*      unit                       *)
    2.17       (*      set(pt_<ak>)               *)
    2.18       (* are instances of pt_<ak>        *)
    2.19 @@ -428,6 +430,7 @@
    2.20            val pt_thm_optn  = pt_inst RS pt_optn_inst; 
    2.21            val pt_thm_list  = pt_inst RS pt_list_inst;
    2.22            val pt_thm_prod  = pt_inst RS (pt_inst RS pt_prod_inst);
    2.23 +          val pt_thm_nprod = pt_inst RS (pt_inst RS pt_nprod_inst);
    2.24            val pt_thm_unit  = pt_unit_inst;
    2.25            val pt_thm_set   = pt_inst RS pt_set_inst
    2.26         in 
    2.27 @@ -437,6 +440,8 @@
    2.28          |> AxClass.add_inst_arity_i ("Datatype.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
    2.29          |> AxClass.add_inst_arity_i ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
    2.30          |> AxClass.add_inst_arity_i ("*",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
    2.31 +        |> AxClass.add_inst_arity_i ("nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
    2.32 +                                    (pt_proof pt_thm_nprod)
    2.33          |> AxClass.add_inst_arity_i ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit)
    2.34          |> AxClass.add_inst_arity_i ("set",[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
    2.35       end) ak_names thy13; 
    2.36 @@ -448,6 +453,7 @@
    2.37         val fs_at_inst     = thm "fs_at_inst";
    2.38         val fs_unit_inst   = thm "fs_unit_inst";
    2.39         val fs_prod_inst   = thm "fs_prod_inst";
    2.40 +       val fs_nprod_inst  = thm "fs_nprod_inst";
    2.41         val fs_list_inst   = thm "fs_list_inst";
    2.42         val fs_option_inst = thm "fs_option_inst";
    2.43         val dj_supp        = thm "dj_supp"
    2.44 @@ -476,6 +482,7 @@
    2.45         (* shows that                  *)
    2.46         (*    unit                     *)
    2.47         (*    *(fs_<ak>,fs_<ak>)       *)
    2.48 +       (*    nprod(fs_<ak>,fs_<ak>)   *)
    2.49         (*    list(fs_<ak>)            *)
    2.50         (*    option(fs_<ak>)          *) 
    2.51         (* are instances of fs_<ak>    *)
    2.52 @@ -486,14 +493,17 @@
    2.53            val fs_inst  = PureThy.get_thm thy (Name ("fs_"^ak_name^"_inst"));
    2.54            fun fs_proof thm = EVERY [AxClass.intro_classes_tac [], rtac (thm RS fs1) 1];      
    2.55  
    2.56 -          val fs_thm_unit = fs_unit_inst;
    2.57 -          val fs_thm_prod = fs_inst RS (fs_inst RS fs_prod_inst);
    2.58 -          val fs_thm_list = fs_inst RS fs_list_inst;
    2.59 -          val fs_thm_optn = fs_inst RS fs_option_inst;
    2.60 +          val fs_thm_unit  = fs_unit_inst;
    2.61 +          val fs_thm_prod  = fs_inst RS (fs_inst RS fs_prod_inst);
    2.62 +          val fs_thm_nprod = fs_inst RS (fs_inst RS fs_nprod_inst);
    2.63 +          val fs_thm_list  = fs_inst RS fs_list_inst;
    2.64 +          val fs_thm_optn  = fs_inst RS fs_option_inst;
    2.65          in 
    2.66           thy 
    2.67           |> AxClass.add_inst_arity_i ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit) 
    2.68 -         |> AxClass.add_inst_arity_i ("*",[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod)    
    2.69 +         |> AxClass.add_inst_arity_i ("*",[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) 
    2.70 +         |> AxClass.add_inst_arity_i ("nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
    2.71 +                                     (fs_proof fs_thm_nprod) 
    2.72           |> AxClass.add_inst_arity_i ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
    2.73           |> AxClass.add_inst_arity_i ("Datatype.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
    2.74          end) ak_names thy20;