# HG changeset patch # User urbanc # Date 1136630622 -3600 # Node ID 20ad06db427b1102b6f0bc8e1be302be4ac7aac3 # Parent e01112713fdc538a0ffea33156df74974cf17318 added private datatype nprod (copy of prod) to be used in the induction rule diff -r e01112713fdc -r 20ad06db427b src/HOL/Nominal/Nominal.thy --- a/src/HOL/Nominal/Nominal.thy Sat Jan 07 11:36:58 2006 +0100 +++ b/src/HOL/Nominal/Nominal.thy Sat Jan 07 11:43:42 2006 +0100 @@ -85,8 +85,14 @@ datatype 'a noption = nSome 'a | nNone primrec (perm_noption) - perm_Nsome_def: "pi\nSome(x) = nSome(pi\x)" - perm_Nnone_def: "pi\nNone = nNone" + perm_nSome_def: "pi\nSome(x) = nSome(pi\x)" + perm_nNone_def: "pi\nNone = nNone" + +(* a "private" copy of the product type used in the nominal induct method *) +datatype ('a,'b) nprod = nPair 'a 'b + +primrec (perm_nprod) + perm_nProd_def: "pi\(nPair x1 x2) = nPair (pi\x1) (pi\x2)" (* permutation on characters (used in strings) *) defs (overloaded) @@ -143,6 +149,12 @@ shows "(supp (x,y)) = (supp x)\(supp y)" by (force simp add: supp_def Collect_imp_eq Collect_neg_eq) +lemma supp_nprod: + fixes x :: "'a" + and y :: "'b" + shows "(supp (nPair x y)) = (supp x)\(supp y)" + by (force simp add: supp_def Collect_imp_eq Collect_neg_eq) + lemma supp_list_nil: shows "supp [] = {}" apply(simp add: supp_def) @@ -244,7 +256,6 @@ apply(simp add: fresh_def supp_some) done - text {* Normalization of freshness results; cf.\ @{text nominal_induct} *} lemma fresh_unit_elim: "(a\() \ PROP C) == PROP C" @@ -625,6 +636,17 @@ apply(rule fs1[OF fsb]) done +lemma fs_nprod_inst: + assumes fsa: "fs TYPE('a) TYPE('x)" + and fsb: "fs TYPE('b) TYPE('x)" + shows "fs TYPE(('a,'b) nprod) TYPE('x)" +apply(unfold fs_def, rule allI) +apply(case_tac x) +apply(auto simp add: supp_nprod) +apply(rule fs1[OF fsa]) +apply(rule fs1[OF fsb]) +done + lemma fs_list_inst: assumes fs: "fs TYPE('a) TYPE('x)" shows "fs TYPE('a list) TYPE('x)" @@ -764,6 +786,19 @@ apply(rule pt3[OF ptb],assumption) done +lemma pt_nprod_inst: + assumes pta: "pt TYPE('a) TYPE('x)" + and ptb: "pt TYPE('b) TYPE('x)" + shows "pt TYPE(('a,'b) nprod) TYPE('x)" + apply(auto simp add: pt_def) + apply(case_tac x) + apply(simp add: pt1[OF pta] pt1[OF ptb]) + apply(case_tac x) + apply(simp add: pt2[OF pta] pt2[OF ptb]) + apply(case_tac x) + apply(simp add: pt3[OF pta] pt3[OF ptb]) + done + lemma pt_fun_inst: assumes pta: "pt TYPE('a) TYPE('x)" and ptb: "pt TYPE('b) TYPE('x)" diff -r e01112713fdc -r 20ad06db427b src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Sat Jan 07 11:36:58 2006 +0100 +++ b/src/HOL/Nominal/nominal_atoms.ML Sat Jan 07 11:43:42 2006 +0100 @@ -374,6 +374,7 @@ val pt_set_inst = thm "pt_set_inst"; val pt_unit_inst = thm "pt_unit_inst"; val pt_prod_inst = thm "pt_prod_inst"; + val pt_nprod_inst = thm "pt_nprod_inst"; val pt_list_inst = thm "pt_list_inst"; val pt_optn_inst = thm "pt_option_inst"; val pt_noptn_inst = thm "pt_noption_inst"; @@ -410,6 +411,7 @@ (* option(pt_) *) (* list(pt_) *) (* *(pt_,pt_) *) + (* nprod(pt_,pt_) *) (* unit *) (* set(pt_) *) (* are instances of pt_ *) @@ -428,6 +430,7 @@ val pt_thm_optn = pt_inst RS pt_optn_inst; val pt_thm_list = pt_inst RS pt_list_inst; val pt_thm_prod = pt_inst RS (pt_inst RS pt_prod_inst); + val pt_thm_nprod = pt_inst RS (pt_inst RS pt_nprod_inst); val pt_thm_unit = pt_unit_inst; val pt_thm_set = pt_inst RS pt_set_inst in @@ -437,6 +440,8 @@ |> AxClass.add_inst_arity_i ("Datatype.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn) |> AxClass.add_inst_arity_i ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list) |> AxClass.add_inst_arity_i ("*",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod) + |> AxClass.add_inst_arity_i ("nominal.nprod",[[cls_name],[cls_name]],[cls_name]) + (pt_proof pt_thm_nprod) |> AxClass.add_inst_arity_i ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit) |> AxClass.add_inst_arity_i ("set",[[cls_name]],[cls_name]) (pt_proof pt_thm_set) end) ak_names thy13; @@ -448,6 +453,7 @@ val fs_at_inst = thm "fs_at_inst"; val fs_unit_inst = thm "fs_unit_inst"; val fs_prod_inst = thm "fs_prod_inst"; + val fs_nprod_inst = thm "fs_nprod_inst"; val fs_list_inst = thm "fs_list_inst"; val fs_option_inst = thm "fs_option_inst"; val dj_supp = thm "dj_supp" @@ -476,6 +482,7 @@ (* shows that *) (* unit *) (* *(fs_,fs_) *) + (* nprod(fs_,fs_) *) (* list(fs_) *) (* option(fs_) *) (* are instances of fs_ *) @@ -486,14 +493,17 @@ val fs_inst = PureThy.get_thm thy (Name ("fs_"^ak_name^"_inst")); fun fs_proof thm = EVERY [AxClass.intro_classes_tac [], rtac (thm RS fs1) 1]; - val fs_thm_unit = fs_unit_inst; - val fs_thm_prod = fs_inst RS (fs_inst RS fs_prod_inst); - val fs_thm_list = fs_inst RS fs_list_inst; - val fs_thm_optn = fs_inst RS fs_option_inst; + val fs_thm_unit = fs_unit_inst; + val fs_thm_prod = fs_inst RS (fs_inst RS fs_prod_inst); + val fs_thm_nprod = fs_inst RS (fs_inst RS fs_nprod_inst); + val fs_thm_list = fs_inst RS fs_list_inst; + val fs_thm_optn = fs_inst RS fs_option_inst; in thy |> AxClass.add_inst_arity_i ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit) - |> AxClass.add_inst_arity_i ("*",[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) + |> AxClass.add_inst_arity_i ("*",[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) + |> AxClass.add_inst_arity_i ("nominal.nprod",[[cls_name],[cls_name]],[cls_name]) + (fs_proof fs_thm_nprod) |> AxClass.add_inst_arity_i ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list) |> AxClass.add_inst_arity_i ("Datatype.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn) end) ak_names thy20;