--- 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\<bullet>nSome(x) = nSome(pi\<bullet>x)"
- perm_Nnone_def: "pi\<bullet>nNone = nNone"
+ perm_nSome_def: "pi\<bullet>nSome(x) = nSome(pi\<bullet>x)"
+ perm_nNone_def: "pi\<bullet>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\<bullet>(nPair x1 x2) = nPair (pi\<bullet>x1) (pi\<bullet>x2)"
(* permutation on characters (used in strings) *)
defs (overloaded)
@@ -143,6 +149,12 @@
shows "(supp (x,y)) = (supp x)\<union>(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)\<union>(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\<sharp>() \<Longrightarrow> 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)"
--- 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_<ak>) *)
(* list(pt_<ak>) *)
(* *(pt_<ak>,pt_<ak>) *)
+ (* nprod(pt_<ak>,pt_<ak>) *)
(* unit *)
(* set(pt_<ak>) *)
(* are instances of pt_<ak> *)
@@ -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_<ak>,fs_<ak>) *)
+ (* nprod(fs_<ak>,fs_<ak>) *)
(* list(fs_<ak>) *)
(* option(fs_<ak>) *)
(* are instances of fs_<ak> *)
@@ -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;