# HG changeset patch # User Christian Urban # Date 1308864103 -3600 # Node ID 304dfe6cc83ab3a4c2f21c4ce24a5102478ff0f9 # Parent 503630c553a8275f7f8852d408ada8ba6226f495 the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl diff -r 503630c553a8 -r 304dfe6cc83a Nominal/Atoms.thy --- a/Nominal/Atoms.thy Thu Jun 23 13:09:17 2011 +0100 +++ b/Nominal/Atoms.thy Thu Jun 23 22:21:43 2011 +0100 @@ -65,7 +65,7 @@ lemma sort_of_atom_name: shows "sort_of (atom (a::name)) = Sort ''name'' []" - unfolding atom_name_def using Rep_name by simp + by (simp add: atom_name_def Rep_name[simplified]) text {* Custom syntax for concrete atoms of type at *} @@ -104,11 +104,10 @@ atom_decl name2 -lemma sort_of_atom_name2: - "sort_of (atom (a::name2)) = Sort ''Atoms.name2'' []" -unfolding atom_name2_def -using Rep_name2 -by simp +lemma + "sort_of (atom (a::name2)) \ sort_of (atom (b::name))" +by (simp add: sort_of_atom_name) + text {* example swappings *} lemma diff -r 503630c553a8 -r 304dfe6cc83a Nominal/Ex/Classical.thy --- a/Nominal/Ex/Classical.thy Thu Jun 23 13:09:17 2011 +0100 +++ b/Nominal/Ex/Classical.thy Thu Jun 23 22:21:43 2011 +0100 @@ -9,7 +9,7 @@ nominal_datatype trm = Ax "name" "coname" -| Cut n::"coname" t1::"trm" c::"coname" t2::"trm" bind n in t1, bind c in t2 +| Cut c::"coname" t1::"trm" n::"name" t2::"trm" bind n in t1, bind c in t2 ("Cut <_>._ '(_')._" [100,100,100,100] 100) | NotR n::"name" t::"trm" "coname" bind n in t ("NotR '(_')._ _" [100,100,100] 100) @@ -46,7 +46,7 @@ thm trm.supp thm trm.supp[simplified] -nominal_primrec +nominal_primrec (* (invariant "\(_, e, d) y. atom e \ y \ atom d \ y") *) crename :: "trm \ coname \ coname \ trm" ("_[_\c>_]" [100,100,100] 100) where "(Ax x a)[d\c>e] = (if a=d then Ax x e else Ax x a)" @@ -68,6 +68,8 @@ apply(simp only: eqvt_def) apply(simp only: crename_graph_def) apply (rule, perm_simp, rule) + (*apply(erule crename_graph.induct) + apply(simp add: trm.fresh)*) apply(rule TrueI) -- "covered all cases" apply(case_tac x) @@ -96,8 +98,21 @@ apply(metis) apply(simp add: fresh_star_def) apply(metis) - -- "clashes" + -- "compatibility" apply(simp_all) + apply(rule conjI) + apply(erule conjE)+ + apply(erule Abs_lst1_fcb) + apply(simp add: Abs_fresh_iff) + apply(simp add: Abs_fresh_iff) + apply(erule fresh_eqvt_at) + apply(simp add: finite_supp) + apply(simp add: fresh_Pair fresh_at_base(1)) + apply(drule sym) + apply(drule sym) + apply(drule sym) + apply(drule sym) + apply(simp add: eqvt_at_def swap_fresh_fresh) oops end diff -r 503630c553a8 -r 304dfe6cc83a Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Thu Jun 23 13:09:17 2011 +0100 +++ b/Nominal/Ex/Lambda.thy Thu Jun 23 22:21:43 2011 +0100 @@ -18,7 +18,7 @@ val test:((Proof.context -> Method.method) context_parser) = Scan.succeed (fn ctxt => let - val _ = Inductive.the_inductive ctxt "Lambda.frees_lst_graph" + val _ = Inductive.the_inductive ctxt "local.frees_lst_graph" in Method.SIMPLE_METHOD' (K all_tac) end) diff -r 503630c553a8 -r 304dfe6cc83a Nominal/Nominal2_Base.thy --- a/Nominal/Nominal2_Base.thy Thu Jun 23 13:09:17 2011 +0100 +++ b/Nominal/Nominal2_Base.thy Thu Jun 23 22:21:43 2011 +0100 @@ -2577,9 +2577,13 @@ by (simp add: supp_atom [symmetric] supp_def atom_eqvt) lemma fresh_at_base: - shows "a \ b \ a \ atom b" - unfolding fresh_def by (simp add: supp_at_base) - + shows "sort_of a \ sort_of (atom b) \ a \ b" + and "a \ b \ a \ atom b" + unfolding fresh_def + apply(simp_all add: supp_at_base) + apply(metis) + done + lemma fresh_atom_at_base: fixes b::"'a::at_base" shows "a \ atom b \ a \ b" @@ -2684,7 +2688,6 @@ where "(a \ b) = (atom a \ atom b)" - lemma flip_self [simp]: "(a \ a) = 0" unfolding flip_def by (rule swap_self) @@ -2841,13 +2844,22 @@ unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep) qed +lemma at_class_sort: + fixes s :: atom_sort + fixes Rep :: "'a \ atom" and Abs :: "atom \ 'a" + fixes a::"'a" + assumes type: "type_definition Rep Abs {a. sort_of a = s}" + assumes atom_def: "\a. atom a = Rep a" + shows "sort_of (atom a) = s" + using atom_def type + unfolding type_definition_def by simp + + setup {* Sign.add_const_constraint (@{const_name "permute"}, SOME @{typ "perm \ 'a::pt \ 'a"}) *} setup {* Sign.add_const_constraint (@{const_name "atom"}, SOME @{typ "'a::at_base \ atom"}) *} - - section {* The freshness lemma according to Andy Pitts *} lemma freshness_lemma: diff -r 503630c553a8 -r 304dfe6cc83a Nominal/nominal_atoms.ML --- a/Nominal/nominal_atoms.ML Thu Jun 23 13:09:17 2011 +0100 +++ b/Nominal/nominal_atoms.ML Thu Jun 23 22:21:43 2011 +0100 @@ -15,6 +15,8 @@ structure Atom_Decl :> ATOM_DECL = struct +val simp_attr = Attrib.internal (K Simplifier.simp_add) + fun atom_decl_set (str : string) : term = let val a = Free ("a", @{typ atom}); @@ -48,6 +50,8 @@ (mk_perm p a, AbsC $ (mk_perm p (RepC $ a)))); val atom_def_name = Binding.prefix_name "atom_" (Binding.suffix_name "_def" name); + val sort_thm_name = + Binding.prefix_name "atom_" (Binding.suffix_name "_sort" name); val permute_def_name = Binding.prefix_name "permute_" (Binding.suffix_name "_def" name); @@ -62,8 +66,10 @@ 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 sort_thm = @{thm at_class_sort} OF [type_definition, atom_def] val thy = lthy - |> Class.prove_instantiation_instance (K (Tactic.rtac class_thm 1)) + |> snd o (Local_Theory.note ((sort_thm_name, [simp_attr]), [sort_thm])) + |> Class.prove_instantiation_instance (K (rtac class_thm 1)) |> Local_Theory.exit_global; in thy