# HG changeset patch # User Christian Urban # Date 1265534181 -3600 # Node ID c70e7545b73851fb727c0c54b49d1163227bbff7 # Parent f4da251473897a0acafbfbb7cd52af8b359d130e updated to latest Nominal2 diff -r f4da25147389 -r c70e7545b738 Quot/Nominal/Nominal2_Atoms.thy --- 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 \ b \ a \ 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 "\a. a \ {a. sort_of a = s}" by (rule_tac x="Atom s 0" in exI, simp) +lemma exists_eq_sort: + shows "\a. a \ {a. sort_of a \ 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 \atom_sort" fixes Rep :: "'a \ atom" and Abs :: "atom \ 'a" - assumes type: "type_definition Rep Abs {a. P (sort_of a)}" + assumes type: "type_definition Rep Abs {a. sort_of a \ range sort_fun}" assumes atom_def: "\a. atom a = Rep a" assumes permute_def: "\p a. p \ a = Abs (p \ 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: "\a. P (sort_of (Rep a))" using Rep by simp + interpret type_definition Rep Abs "{a. sort_of a \ range sort_fun}" by (rule type) + have sort_of_Rep: "\a. sort_of (Rep a) \ range sort_fun" using Rep by simp fix a b :: 'a and p p1 p2 :: perm show "0 \ 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 \ atom" and Abs :: "atom \ 'a" + assumes type: "type_definition Rep Abs {a. sort_of a \ range (\x::unit. s)}" + assumes atom_def: "\a. atom a = Rep a" + assumes permute_def: "\p a. p \ a = Abs (p \ Rep a)" + shows "OFCLASS('a, at_class)" +proof + interpret type_definition Rep Abs "{a. sort_of a \ range (\x::unit. s)}" by (rule type) + have sort_of_Rep: "\a. sort_of (Rep a) = s" using Rep by (simp add: image_def) + fix a b :: 'a and p p1 p2 :: perm + show "0 \ a = a" + unfolding permute_def by (simp add: Rep_inverse) + show "(p1 + p2) \ a = p1 \ p2 \ 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 \ a = b" + unfolding atom_def by (simp add: Rep_inject) + show "p \ atom a = atom (p \ 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 \ atom" and Abs :: "atom \ '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: "\a. sort_of (Rep a) = s" using Rep by simp + have sort_of_Rep: "\a. sort_of (Rep a) = s" using Rep by (simp add: image_def) fix a b :: 'a and p p1 p2 :: perm show "0 \ 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 diff -r f4da25147389 -r c70e7545b738 Quot/Nominal/Nominal2_Eqvt.thy --- 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 diff -r f4da25147389 -r c70e7545b738 Quot/Nominal/atom_decl.ML --- 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; diff -r f4da25147389 -r c70e7545b738 Quot/Nominal/nominal_atoms.ML --- /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;