444 done |
444 done |
445 |
445 |
446 end |
446 end |
447 |
447 |
448 lemma permute_set_eq: |
448 lemma permute_set_eq: |
449 shows "p \<bullet> X = {x. - p \<bullet> x \<in> X}" |
449 shows "p \<bullet> X = {x. - p \<bullet> x \<in> X}" |
450 unfolding permute_set_def |
450 unfolding permute_set_def |
451 by (auto) (metis permute_minus_cancel(1)) |
451 by (auto) (metis permute_minus_cancel(1)) |
452 |
452 |
453 lemma permute_set_eq_image: |
453 lemma permute_set_eq_image: |
454 shows "p \<bullet> X = permute p ` X" |
454 shows "p \<bullet> X = permute p ` X" |
821 |
821 |
822 method_setup perm_strict_simp = |
822 method_setup perm_strict_simp = |
823 {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *} |
823 {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *} |
824 {* pushes permutations inside, raises an error if it cannot solve all permutations. *} |
824 {* pushes permutations inside, raises an error if it cannot solve all permutations. *} |
825 |
825 |
826 simproc_setup perm_simproc ("p \<bullet> t") = {* fn _ => fn ss => fn ctrm => |
826 simproc_setup perm_simproc ("p \<bullet> t") = {* fn _ => fn ctxt => fn ctrm => |
827 case term_of (Thm.dest_arg ctrm) of |
827 case term_of (Thm.dest_arg ctrm) of |
828 Free _ => NONE |
828 Free _ => NONE |
829 | Var _ => NONE |
829 | Var _ => NONE |
830 | Const (@{const_name permute}, _) $ _ $ _ => NONE |
830 | Const (@{const_name permute}, _) $ _ $ _ => NONE |
831 | _ => |
831 | _ => |
832 let |
832 let |
833 val ctxt = Simplifier.the_context ss |
|
834 val thm = Nominal_Permeq.eqvt_conv ctxt Nominal_Permeq.eqvt_strict_config ctrm |
833 val thm = Nominal_Permeq.eqvt_conv ctxt Nominal_Permeq.eqvt_strict_config ctrm |
835 handle ERROR _ => Thm.reflexive ctrm |
834 handle ERROR _ => Thm.reflexive ctrm |
836 in |
835 in |
837 if Thm.is_reflexive thm then NONE else SOME(thm) |
836 if Thm.is_reflexive thm then NONE else SOME(thm) |
838 end |
837 end |
1862 using supp_eqvt_at[OF asm fin] |
1861 using supp_eqvt_at[OF asm fin] |
1863 by auto |
1862 by auto |
1864 |
1863 |
1865 text {* for handling of freshness of functions *} |
1864 text {* for handling of freshness of functions *} |
1866 |
1865 |
1867 simproc_setup fresh_fun_simproc ("a \<sharp> (f::'a::pt \<Rightarrow>'b::pt)") = {* fn _ => fn ss => fn ctrm => |
1866 simproc_setup fresh_fun_simproc ("a \<sharp> (f::'a::pt \<Rightarrow>'b::pt)") = {* fn _ => fn ctxt => fn ctrm => |
1868 let |
1867 let |
1869 val _ $ _ $ f = term_of ctrm |
1868 val _ $ _ $ f = term_of ctrm |
1870 in |
1869 in |
1871 case (Term.add_frees f [], Term.add_vars f []) of |
1870 case (Term.add_frees f [], Term.add_vars f []) of |
1872 ([], []) => SOME(@{thm fresh_fun_eqvt[simplified eqvt_def, THEN Eq_TrueI]}) |
1871 ([], []) => SOME(@{thm fresh_fun_eqvt[simplified eqvt_def, THEN Eq_TrueI]}) |
1873 | (x::_, []) => let |
1872 | (x::_, []) => let |
1874 val thy = Proof_Context.theory_of (Simplifier.the_context ss) |
1873 val thy = Proof_Context.theory_of ctxt |
1875 val argx = Free x |
1874 val argx = Free x |
1876 val absf = absfree x f |
1875 val absf = absfree x f |
1877 val cty_inst = [SOME (ctyp_of thy (fastype_of argx)), SOME (ctyp_of thy (fastype_of f))] |
1876 val cty_inst = [SOME (ctyp_of thy (fastype_of argx)), SOME (ctyp_of thy (fastype_of f))] |
1878 val ctrm_inst = [NONE, SOME (cterm_of thy absf), SOME (cterm_of thy argx)] |
1877 val ctrm_inst = [NONE, SOME (cterm_of thy absf), SOME (cterm_of thy argx)] |
1879 val thm = Drule.instantiate' cty_inst ctrm_inst @{thm fresh_fun_app} |
1878 val thm = Drule.instantiate' cty_inst ctrm_inst @{thm fresh_fun_app} |
2926 shows "atom a \<sharp> x \<Longrightarrow> P (if a = x then t else s) = P s" |
2925 shows "atom a \<sharp> x \<Longrightarrow> P (if a = x then t else s) = P s" |
2927 and "atom a \<sharp> x \<Longrightarrow> P (if x = a then t else s) = P s" |
2926 and "atom a \<sharp> x \<Longrightarrow> P (if x = a then t else s) = P s" |
2928 by (simp_all add: fresh_at_base) |
2927 by (simp_all add: fresh_at_base) |
2929 |
2928 |
2930 |
2929 |
2931 simproc_setup fresh_ineq ("x \<noteq> (y::'a::at_base)") = {* fn _ => fn ss => fn ctrm => |
2930 simproc_setup fresh_ineq ("x \<noteq> (y::'a::at_base)") = {* fn _ => fn ctxt => fn ctrm => |
2932 let |
2931 let |
2933 fun first_is_neg lhs rhs [] = NONE |
2932 fun first_is_neg lhs rhs [] = NONE |
2934 | first_is_neg lhs rhs (thm::thms) = |
2933 | first_is_neg lhs rhs (thm::thms) = |
2935 (case Thm.prop_of thm of |
2934 (case Thm.prop_of thm of |
2936 _ $ (@{term "HOL.Not"} $ (Const ("HOL.eq", _) $ l $ r)) => |
2935 _ $ (@{term "HOL.Not"} $ (Const ("HOL.eq", _) $ l $ r)) => |
2938 else if r = lhs andalso l = rhs then SOME(thm RS @{thm not_sym}) |
2937 else if r = lhs andalso l = rhs then SOME(thm RS @{thm not_sym}) |
2939 else first_is_neg lhs rhs thms) |
2938 else first_is_neg lhs rhs thms) |
2940 | _ => first_is_neg lhs rhs thms) |
2939 | _ => first_is_neg lhs rhs thms) |
2941 |
2940 |
2942 val simp_thms = @{thms fresh_Pair fresh_at_base atom_eq_iff} |
2941 val simp_thms = @{thms fresh_Pair fresh_at_base atom_eq_iff} |
2943 val prems = Simplifier.prems_of ss |
2942 val prems = Simplifier.prems_of ctxt |
2944 |> filter (fn thm => case Thm.prop_of thm of |
2943 |> filter (fn thm => case Thm.prop_of thm of |
2945 _ $ (Const (@{const_name fresh}, _) $ _ $ _) => true | _ => false) |
2944 _ $ (Const (@{const_name fresh}, _) $ _ $ _) => true | _ => false) |
2946 |> map (simplify (HOL_basic_ss addsimps simp_thms)) |
2945 |> map (simplify (put_simpset HOL_basic_ss ctxt addsimps simp_thms)) |
2947 |> map HOLogic.conj_elims |
2946 |> map HOLogic.conj_elims |
2948 |> flat |
2947 |> flat |
2949 in |
2948 in |
2950 case term_of ctrm of |
2949 case term_of ctrm of |
2951 @{term "HOL.Not"} $ (Const ("HOL.eq", _) $ lhs $ rhs) => |
2950 @{term "HOL.Not"} $ (Const ("HOL.eq", _) $ lhs $ rhs) => |
3317 shows "Fresh h = h a" |
3316 shows "Fresh h = h a" |
3318 apply (rule Fresh_apply) |
3317 apply (rule Fresh_apply) |
3319 apply (auto simp add: fresh_Pair intro: a) |
3318 apply (auto simp add: fresh_Pair intro: a) |
3320 done |
3319 done |
3321 |
3320 |
3322 simproc_setup Fresh_simproc ("Fresh (h::'a::at \<Rightarrow> 'b::pt)") = {* fn _ => fn ss => fn ctrm => |
3321 simproc_setup Fresh_simproc ("Fresh (h::'a::at \<Rightarrow> 'b::pt)") = {* fn _ => fn ctxt => fn ctrm => |
3323 let |
3322 let |
3324 val ctxt = Simplifier.the_context ss |
|
3325 val _ $ h = term_of ctrm |
3323 val _ $ h = term_of ctrm |
3326 |
3324 |
3327 val cfresh = @{const_name fresh} |
3325 val cfresh = @{const_name fresh} |
3328 val catom = @{const_name atom} |
3326 val catom = @{const_name atom} |
3329 |
3327 |
3330 val atoms = Simplifier.prems_of ss |
3328 val atoms = Simplifier.prems_of ctxt |
3331 |> map_filter (fn thm => case Thm.prop_of thm of |
3329 |> map_filter (fn thm => case Thm.prop_of thm of |
3332 _ $ (Const (cfresh, _) $ (Const (catom, _) $ atm) $ _) => SOME (atm) | _ => NONE) |
3330 _ $ (Const (cfresh, _) $ (Const (catom, _) $ atm) $ _) => SOME (atm) | _ => NONE) |
3333 |> distinct (op=) |
3331 |> distinct (op=) |
3334 |
3332 |
3335 fun get_thm atm = |
3333 fun get_thm atm = |
3336 let |
3334 let |
3337 val goal1 = HOLogic.mk_Trueprop (mk_fresh (mk_atom atm) h) |
3335 val goal1 = HOLogic.mk_Trueprop (mk_fresh (mk_atom atm) h) |
3338 val goal2 = HOLogic.mk_Trueprop (mk_fresh (mk_atom atm) (h $ atm)) |
3336 val goal2 = HOLogic.mk_Trueprop (mk_fresh (mk_atom atm) (h $ atm)) |
3339 |
3337 |
3340 val thm1 = Goal.prove ctxt [] [] goal1 (K (asm_simp_tac ss 1)) |
3338 val thm1 = Goal.prove ctxt [] [] goal1 (K (asm_simp_tac ctxt 1)) |
3341 val thm2 = Goal.prove ctxt [] [] goal2 (K (asm_simp_tac ss 1)) |
3339 val thm2 = Goal.prove ctxt [] [] goal2 (K (asm_simp_tac ctxt 1)) |
3342 in |
3340 in |
3343 SOME (@{thm Fresh_apply'} OF [thm1, thm2] RS eq_reflection) |
3341 SOME (@{thm Fresh_apply'} OF [thm1, thm2] RS eq_reflection) |
3344 end handle ERROR _ => NONE |
3342 end handle ERROR _ => NONE |
3345 in |
3343 in |
3346 get_first get_thm atoms |
3344 get_first get_thm atoms |