--- a/Quot/Nominal/Nominal2_Atoms.thy Sat Feb 06 12:58:56 2010 +0100
+++ b/Quot/Nominal/Nominal2_Atoms.thy Sun Feb 07 10:16:21 2010 +0100
@@ -5,7 +5,7 @@
*)
theory Nominal2_Atoms
imports Nominal2_Base
-uses ("atom_decl.ML")
+uses ("nominal_atoms.ML")
begin
section {* Concrete atom types *}
@@ -30,14 +30,13 @@
shows "supp a = {atom a}"
by (simp add: supp_atom [symmetric] supp_def atom_eqvt)
-lemma fresh_at:
+lemma fresh_at_base:
shows "a \<sharp> b \<longleftrightarrow> a \<noteq> atom b"
unfolding fresh_def by (simp add: supp_at_base)
instance at_base < fs
proof qed (simp add: supp_at_base)
-
lemma at_base_infinite [simp]:
shows "infinite (UNIV :: 'a::at_base set)" (is "infinite ?U")
proof
@@ -157,20 +156,24 @@
New atom types are defined as subtypes of @{typ atom}.
*}
-lemma exists_eq_sort:
+lemma exists_eq_simple_sort:
shows "\<exists>a. a \<in> {a. sort_of a = s}"
by (rule_tac x="Atom s 0" in exI, simp)
+lemma exists_eq_sort:
+ shows "\<exists>a. a \<in> {a. sort_of a \<in> range sort_fun}"
+ by (rule_tac x="Atom (sort_fun x) y" in exI, simp)
+
lemma at_base_class:
- fixes s :: atom_sort
+ fixes sort_fun :: "'b \<Rightarrow>atom_sort"
fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"
- assumes type: "type_definition Rep Abs {a. P (sort_of a)}"
+ assumes type: "type_definition Rep Abs {a. sort_of a \<in> range sort_fun}"
assumes atom_def: "\<And>a. atom a = Rep a"
assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"
shows "OFCLASS('a, at_base_class)"
proof
- interpret type_definition Rep Abs "{a. P (sort_of a)}" by (rule type)
- have sort_of_Rep: "\<And>a. P (sort_of (Rep a))" using Rep by simp
+ interpret type_definition Rep Abs "{a. sort_of a \<in> range sort_fun}" by (rule type)
+ have sort_of_Rep: "\<And>a. sort_of (Rep a) \<in> range sort_fun" using Rep by simp
fix a b :: 'a and p p1 p2 :: perm
show "0 \<bullet> a = a"
unfolding permute_def by (simp add: Rep_inverse)
@@ -182,6 +185,31 @@
unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)
qed
+(*
+lemma at_class:
+ fixes s :: atom_sort
+ fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"
+ assumes type: "type_definition Rep Abs {a. sort_of a \<in> range (\<lambda>x::unit. s)}"
+ assumes atom_def: "\<And>a. atom a = Rep a"
+ assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"
+ shows "OFCLASS('a, at_class)"
+proof
+ interpret type_definition Rep Abs "{a. sort_of a \<in> range (\<lambda>x::unit. s)}" by (rule type)
+ have sort_of_Rep: "\<And>a. sort_of (Rep a) = s" using Rep by (simp add: image_def)
+ fix a b :: 'a and p p1 p2 :: perm
+ show "0 \<bullet> a = a"
+ unfolding permute_def by (simp add: Rep_inverse)
+ show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a"
+ unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)
+ show "sort_of (atom a) = sort_of (atom b)"
+ unfolding atom_def by (simp add: sort_of_Rep)
+ show "atom a = atom b \<longleftrightarrow> a = b"
+ unfolding atom_def by (simp add: Rep_inject)
+ show "p \<bullet> atom a = atom (p \<bullet> a)"
+ unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)
+qed
+*)
+
lemma at_class:
fixes s :: atom_sort
fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"
@@ -191,7 +219,7 @@
shows "OFCLASS('a, at_class)"
proof
interpret type_definition Rep Abs "{a. sort_of a = s}" by (rule type)
- have sort_of_Rep: "\<And>a. sort_of (Rep a) = s" using Rep by simp
+ have sort_of_Rep: "\<And>a. sort_of (Rep a) = s" using Rep by (simp add: image_def)
fix a b :: 'a and p p1 p2 :: perm
show "0 \<bullet> a = a"
unfolding permute_def by (simp add: Rep_inverse)
@@ -215,7 +243,9 @@
text {* at the moment only single-sort concrete atoms are supported *}
-use "atom_decl.ML"
+use "nominal_atoms.ML"
+
+
end
--- a/Quot/Nominal/Nominal2_Eqvt.thy Sat Feb 06 12:58:56 2010 +0100
+++ b/Quot/Nominal/Nominal2_Eqvt.thy Sun Feb 07 10:16:21 2010 +0100
@@ -226,8 +226,6 @@
use "nominal_thmdecls.ML"
setup "Nominal_ThmDecls.setup"
-
-
lemmas [eqvt] =
(* connectives *)
eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt
@@ -235,7 +233,8 @@
imp_eqvt [folded induct_implies_def]
(* nominal *)
- supp_eqvt fresh_eqvt permute_pure
+ permute_eqvt supp_eqvt fresh_eqvt
+ permute_pure
(* datatypes *)
permute_prod.simps
@@ -245,8 +244,6 @@
empty_eqvt UNIV_eqvt union_eqvt inter_eqvt
Diff_eqvt Compl_eqvt insert_eqvt
-lemmas [eqvt_raw] = permute_eqvt
-
thm eqvts
thm eqvts_raw
--- a/Quot/Nominal/atom_decl.ML Sat Feb 06 12:58:56 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,94 +0,0 @@
-(* Title: atom_decl/ML
- Authors: Brian Huffman, Christian Urban
-
- Command for defining concrete atom types.
-
- At the moment, only single-sorted atom types
- are supported.
-*)
-
-signature ATOM_DECL =
-sig
- val add_atom_decl: binding -> theory -> theory
-end;
-
-structure Atom_Decl :> ATOM_DECL =
-struct
-
-val atomT = @{typ atom};
-val permT = @{typ perm};
-
-val sort_of_const = @{term sort_of};
-fun atom_const T = Const (@{const_name atom}, T --> atomT);
-fun permute_const T = Const (@{const_name permute}, permT --> T --> T);
-
-fun mk_sort_of t = sort_of_const $ t;
-fun mk_atom t = atom_const (fastype_of t) $ t;
-fun mk_permute (p, t) = permute_const (fastype_of t) $ p $ t;
-
-fun atom_decl_set (str : string) : term =
- let
- val a = Free ("a", atomT);
- val s = Const (@{const_name "Sort"}, @{typ "string => atom_sort list => atom_sort"})
- $ HOLogic.mk_string str $ HOLogic.nil_const @{typ "atom_sort"};
- in
- HOLogic.mk_Collect ("a", atomT, HOLogic.mk_eq (mk_sort_of a, s))
- end
-
-fun add_atom_decl (name : binding) (thy : theory) =
- let
- val _ = Theory.requires thy "Nominal2_Atoms" "nominal logic";
- val str = Sign.full_name thy name;
-
- (* typedef *)
- val set = atom_decl_set str;
- val tac = rtac @{thm exists_eq_sort} 1;
- val ((full_tname, info as {type_definition, Rep_name, Abs_name, ...}), thy) =
- Typedef.add_typedef false NONE (name, [], NoSyn) set NONE tac thy;
-
- (* definition of atom and permute *)
- val newT = #abs_type info;
- val RepC = Const (Rep_name, newT --> atomT);
- val AbsC = Const (Abs_name, atomT --> newT);
- val a = Free ("a", newT);
- val p = Free ("p", permT);
- val atom_eqn =
- HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_atom a, RepC $ a));
- val permute_eqn =
- HOLogic.mk_Trueprop (HOLogic.mk_eq
- (mk_permute (p, a), AbsC $ (mk_permute (p, RepC $ a))));
- val atom_def_name =
- Binding.prefix_name "atom_" (Binding.suffix_name "_def" name);
- val permute_def_name =
- Binding.prefix_name "permute_" (Binding.suffix_name "_def" name);
-
- (* at class instance *)
- val lthy =
- Theory_Target.instantiation ([full_tname], [], @{sort at}) thy;
- val ((_, (_, permute_ldef)), lthy) =
- Specification.definition (NONE, ((permute_def_name, []), permute_eqn)) lthy;
- val ((_, (_, atom_ldef)), lthy) =
- Specification.definition (NONE, ((atom_def_name, []), atom_eqn)) lthy;
- val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
- val permute_def = singleton (ProofContext.export lthy ctxt_thy) permute_ldef;
- val atom_def = singleton (ProofContext.export lthy ctxt_thy) atom_ldef;
- val class_thm = @{thm at_class} OF [type_definition, atom_def, permute_def];
- val thy = lthy
- |> Class.prove_instantiation_instance (K (Tactic.rtac class_thm 1))
- |> Local_Theory.exit_global;
- in
- thy
- end;
-
-(** outer syntax **)
-
-local structure P = OuterParse and K = OuterKeyword in
-
-val _ =
- OuterSyntax.command "atom_decl" "declaration of a concrete atom type" K.thy_decl
- (P.binding >>
- (Toplevel.print oo (Toplevel.theory o add_atom_decl)));
-
-end;
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/Nominal/nominal_atoms.ML Sun Feb 07 10:16:21 2010 +0100
@@ -0,0 +1,94 @@
+(* Title: nominal_atoms/ML
+ Authors: Brian Huffman, Christian Urban
+
+ Command for defining concrete atom types.
+
+ At the moment, only single-sorted atom types
+ are supported.
+*)
+
+signature ATOM_DECL =
+sig
+ val add_atom_decl: (binding * (binding option)) -> theory -> theory
+end;
+
+structure Atom_Decl :> ATOM_DECL =
+struct
+
+val atomT = @{typ atom};
+val permT = @{typ perm};
+
+val sort_of_const = @{term sort_of};
+fun atom_const T = Const (@{const_name atom}, T --> atomT);
+fun permute_const T = Const (@{const_name permute}, permT --> T --> T);
+
+fun mk_sort_of t = sort_of_const $ t;
+fun mk_atom t = atom_const (fastype_of t) $ t;
+fun mk_permute (p, t) = permute_const (fastype_of t) $ p $ t;
+
+fun atom_decl_set (str : string) : term =
+ let
+ val a = Free ("a", atomT);
+ val s = Const (@{const_name "Sort"}, @{typ "string => atom_sort list => atom_sort"})
+ $ HOLogic.mk_string str $ HOLogic.nil_const @{typ "atom_sort"};
+ in
+ HOLogic.mk_Collect ("a", atomT, HOLogic.mk_eq (mk_sort_of a, s))
+ end
+
+fun add_atom_decl (name : binding, arg : binding option) (thy : theory) =
+ let
+ val _ = Theory.requires thy "Nominal2_Atoms" "nominal logic";
+ val str = Sign.full_name thy name;
+
+ (* typedef *)
+ val set = atom_decl_set str;
+ val tac = rtac @{thm exists_eq_simple_sort} 1;
+ val ((full_tname, info as {type_definition, Rep_name, Abs_name, ...}), thy) =
+ Typedef.add_typedef false NONE (name, [], NoSyn) set NONE tac thy;
+
+ (* definition of atom and permute *)
+ val newT = #abs_type info;
+ val RepC = Const (Rep_name, newT --> atomT);
+ val AbsC = Const (Abs_name, atomT --> newT);
+ val a = Free ("a", newT);
+ val p = Free ("p", permT);
+ val atom_eqn =
+ HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_atom a, RepC $ a));
+ val permute_eqn =
+ HOLogic.mk_Trueprop (HOLogic.mk_eq
+ (mk_permute (p, a), AbsC $ (mk_permute (p, RepC $ a))));
+ val atom_def_name =
+ Binding.prefix_name "atom_" (Binding.suffix_name "_def" name);
+ val permute_def_name =
+ Binding.prefix_name "permute_" (Binding.suffix_name "_def" name);
+
+ (* at class instance *)
+ val lthy =
+ Theory_Target.instantiation ([full_tname], [], @{sort at}) thy;
+ val ((_, (_, permute_ldef)), lthy) =
+ Specification.definition (NONE, ((permute_def_name, []), permute_eqn)) lthy;
+ val ((_, (_, atom_ldef)), lthy) =
+ Specification.definition (NONE, ((atom_def_name, []), atom_eqn)) lthy;
+ val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
+ val permute_def = singleton (ProofContext.export lthy ctxt_thy) permute_ldef;
+ val atom_def = singleton (ProofContext.export lthy ctxt_thy) atom_ldef;
+ val class_thm = @{thm at_class} OF [type_definition, atom_def, permute_def];
+ val thy = lthy
+ |> Class.prove_instantiation_instance (K (Tactic.rtac class_thm 1))
+ |> Local_Theory.exit_global;
+ in
+ thy
+ end;
+
+(** outer syntax **)
+
+local structure P = OuterParse and K = OuterKeyword in
+
+val _ =
+ OuterSyntax.command "atom_decl" "declaration of a concrete atom type" K.thy_decl
+ ((P.binding -- Scan.option (Args.parens (P.binding))) >>
+ (Toplevel.print oo (Toplevel.theory o add_atom_decl)));
+
+end;
+
+end;