3 |
3 |
4 Basic definitions and lemma infrastructure for |
4 Basic definitions and lemma infrastructure for |
5 Nominal Isabelle. |
5 Nominal Isabelle. |
6 *) |
6 *) |
7 theory Nominal2_Base |
7 theory Nominal2_Base |
8 imports Main |
8 imports "~~/src/HOL/Library/Old_Datatype" |
9 "~~/src/HOL/Library/Infinite_Set" |
9 "~~/src/HOL/Library/Infinite_Set" |
10 "~~/src/HOL/Quotient_Examples/FSet" |
10 "~~/src/HOL/Quotient_Examples/FSet" |
11 "~~/src/HOL/Library/FinFun" |
11 "~~/src/HOL/Library/FinFun" |
12 keywords |
12 keywords |
13 "atom_decl" "equivariance" :: thy_decl |
13 "atom_decl" "equivariance" :: thy_decl |
821 method_setup perm_strict_simp = |
820 method_setup perm_strict_simp = |
822 {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *} |
821 {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *} |
823 {* pushes permutations inside, raises an error if it cannot solve all permutations. *} |
822 {* pushes permutations inside, raises an error if it cannot solve all permutations. *} |
824 |
823 |
825 simproc_setup perm_simproc ("p \<bullet> t") = {* fn _ => fn ctxt => fn ctrm => |
824 simproc_setup perm_simproc ("p \<bullet> t") = {* fn _ => fn ctxt => fn ctrm => |
826 case term_of (Thm.dest_arg ctrm) of |
825 case Thm.term_of (Thm.dest_arg ctrm) of |
827 Free _ => NONE |
826 Free _ => NONE |
828 | Var _ => NONE |
827 | Var _ => NONE |
829 | Const (@{const_name permute}, _) $ _ $ _ => NONE |
828 | Const (@{const_name permute}, _) $ _ $ _ => NONE |
830 | _ => |
829 | _ => |
831 let |
830 let |
889 |
888 |
890 lemma imp_eqvt [eqvt]: |
889 lemma imp_eqvt [eqvt]: |
891 shows "p \<bullet> (A \<longrightarrow> B) \<longleftrightarrow> (p \<bullet> A) \<longrightarrow> (p \<bullet> B)" |
890 shows "p \<bullet> (A \<longrightarrow> B) \<longleftrightarrow> (p \<bullet> A) \<longrightarrow> (p \<bullet> B)" |
892 by (simp add: permute_bool_def) |
891 by (simp add: permute_bool_def) |
893 |
892 |
894 declare imp_eqvt[folded induct_implies_def, eqvt] |
893 declare imp_eqvt[folded HOL.induct_implies_def, eqvt] |
895 |
894 |
896 lemma all_eqvt [eqvt]: |
895 lemma all_eqvt [eqvt]: |
897 shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)" |
896 shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)" |
898 unfolding All_def |
897 unfolding All_def |
899 by (perm_simp) (rule refl) |
898 by (perm_simp) (rule refl) |
900 |
899 |
901 declare all_eqvt[folded induct_forall_def, eqvt] |
900 declare all_eqvt[folded HOL.induct_forall_def, eqvt] |
902 |
901 |
903 lemma ex_eqvt [eqvt]: |
902 lemma ex_eqvt [eqvt]: |
904 shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)" |
903 shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)" |
905 unfolding Ex_def |
904 unfolding Ex_def |
906 by (perm_simp) (rule refl) |
905 by (perm_simp) (rule refl) |
1883 |
1882 |
1884 text {* for handling of freshness of functions *} |
1883 text {* for handling of freshness of functions *} |
1885 |
1884 |
1886 simproc_setup fresh_fun_simproc ("a \<sharp> (f::'a::pt \<Rightarrow>'b::pt)") = {* fn _ => fn ctxt => fn ctrm => |
1885 simproc_setup fresh_fun_simproc ("a \<sharp> (f::'a::pt \<Rightarrow>'b::pt)") = {* fn _ => fn ctxt => fn ctrm => |
1887 let |
1886 let |
1888 val _ $ _ $ f = term_of ctrm |
1887 val _ $ _ $ f = Thm.term_of ctrm |
1889 in |
1888 in |
1890 case (Term.add_frees f [], Term.add_vars f []) of |
1889 case (Term.add_frees f [], Term.add_vars f []) of |
1891 ([], []) => SOME(@{thm fresh_fun_eqvt[simplified eqvt_def, THEN Eq_TrueI]}) |
1890 ([], []) => SOME(@{thm fresh_fun_eqvt[simplified eqvt_def, THEN Eq_TrueI]}) |
1892 | (x::_, []) => let |
1891 | (x::_, []) => |
1893 val thy = Proof_Context.theory_of ctxt |
1892 let |
1894 val argx = Free x |
1893 val argx = Free x |
1895 val absf = absfree x f |
1894 val absf = absfree x f |
1896 val cty_inst = [SOME (ctyp_of thy (fastype_of argx)), SOME (ctyp_of thy (fastype_of f))] |
1895 val cty_inst = |
1897 val ctrm_inst = [NONE, SOME (cterm_of thy absf), SOME (cterm_of thy argx)] |
1896 [SOME (Thm.ctyp_of ctxt (fastype_of argx)), SOME (Thm.ctyp_of ctxt (fastype_of f))] |
1898 val thm = Drule.instantiate' cty_inst ctrm_inst @{thm fresh_fun_app} |
1897 val ctrm_inst = [NONE, SOME (Thm.cterm_of ctxt absf), SOME (Thm.cterm_of ctxt argx)] |
|
1898 val thm = Drule.instantiate' cty_inst ctrm_inst @{thm fresh_fun_app} |
1899 in |
1899 in |
1900 SOME(thm RS @{thm Eq_TrueI}) |
1900 SOME(thm RS @{thm Eq_TrueI}) |
1901 end |
1901 end |
1902 | (_, _) => NONE |
1902 | (_, _) => NONE |
1903 end |
1903 end |
2950 and "atom a \<sharp> x \<Longrightarrow> P (if x = a then t else s) = P s" |
2950 and "atom a \<sharp> x \<Longrightarrow> P (if x = a then t else s) = P s" |
2951 by (simp_all add: fresh_at_base) |
2951 by (simp_all add: fresh_at_base) |
2952 |
2952 |
2953 |
2953 |
2954 simproc_setup fresh_ineq ("x \<noteq> (y::'a::at_base)") = {* fn _ => fn ctxt => fn ctrm => |
2954 simproc_setup fresh_ineq ("x \<noteq> (y::'a::at_base)") = {* fn _ => fn ctxt => fn ctrm => |
2955 case term_of ctrm of @{term "HOL.Not"} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) => |
2955 case Thm.term_of ctrm of @{term "HOL.Not"} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) => |
2956 let |
2956 let |
2957 fun first_is_neg lhs rhs [] = NONE |
2957 fun first_is_neg lhs rhs [] = NONE |
2958 | first_is_neg lhs rhs (thm::thms) = |
2958 | first_is_neg lhs rhs (thm::thms) = |
2959 (case Thm.prop_of thm of |
2959 (case Thm.prop_of thm of |
2960 _ $ (@{term "HOL.Not"} $ (Const (@{const_name HOL.eq}, _) $ l $ r)) => |
2960 _ $ (@{term "HOL.Not"} $ (Const (@{const_name HOL.eq}, _) $ l $ r)) => |
2971 val atms = a :: HOLogic.strip_tuple b |
2971 val atms = a :: HOLogic.strip_tuple b |
2972 in |
2972 in |
2973 member (op=) atms lhs andalso member (op=) atms rhs |
2973 member (op=) atms lhs andalso member (op=) atms rhs |
2974 end) |
2974 end) |
2975 | _ => false) |
2975 | _ => false) |
2976 |> map (simplify (put_simpset HOL_basic_ss ctxt addsimps simp_thms)) |
2976 |> map (simplify (put_simpset HOL_basic_ss ctxt addsimps simp_thms)) |
2977 |> map HOLogic.conj_elims |
2977 |> map (HOLogic.conj_elims ctxt) |
2978 |> flat |
2978 |> flat |
2979 in |
2979 in |
2980 case first_is_neg lhs rhs prems of |
2980 case first_is_neg lhs rhs prems of |
2981 SOME(thm) => SOME(thm RS @{thm Eq_TrueI}) |
2981 SOME(thm) => SOME(thm RS @{thm Eq_TrueI}) |
2982 | NONE => NONE |
2982 | NONE => NONE |
3351 apply (auto simp: fresh_Pair intro: a) |
3351 apply (auto simp: fresh_Pair intro: a) |
3352 done |
3352 done |
3353 |
3353 |
3354 simproc_setup Fresh_simproc ("Fresh (h::'a::at \<Rightarrow> 'b::pt)") = {* fn _ => fn ctxt => fn ctrm => |
3354 simproc_setup Fresh_simproc ("Fresh (h::'a::at \<Rightarrow> 'b::pt)") = {* fn _ => fn ctxt => fn ctrm => |
3355 let |
3355 let |
3356 val _ $ h = term_of ctrm |
3356 val _ $ h = Thm.term_of ctrm |
3357 |
3357 |
3358 val cfresh = @{const_name fresh} |
3358 val cfresh = @{const_name fresh} |
3359 val catom = @{const_name atom} |
3359 val catom = @{const_name atom} |
3360 |
3360 |
3361 val atoms = Simplifier.prems_of ctxt |
3361 val atoms = Simplifier.prems_of ctxt |