equal
deleted
inserted
replaced
535 fixes x::"'a::pt" |
535 fixes x::"'a::pt" |
536 shows "(p \<bullet> ([as]set. x)) = [p \<bullet> as]set. (p \<bullet> x)" |
536 shows "(p \<bullet> ([as]set. x)) = [p \<bullet> as]set. (p \<bullet> x)" |
537 by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"]) |
537 by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"]) |
538 |
538 |
539 instance |
539 instance |
540 apply(default) |
540 apply standard |
541 apply(case_tac [!] x) |
541 apply(case_tac [!] x) |
542 apply(simp_all) |
542 apply(simp_all) |
543 done |
543 done |
544 |
544 |
545 end |
545 end |
557 fixes x::"'a::pt" |
557 fixes x::"'a::pt" |
558 shows "(p \<bullet> ([as]res. x)) = [p \<bullet> as]res. (p \<bullet> x)" |
558 shows "(p \<bullet> ([as]res. x)) = [p \<bullet> as]res. (p \<bullet> x)" |
559 by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"]) |
559 by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"]) |
560 |
560 |
561 instance |
561 instance |
562 apply(default) |
562 apply standard |
563 apply(case_tac [!] x) |
563 apply(case_tac [!] x) |
564 apply(simp_all) |
564 apply(simp_all) |
565 done |
565 done |
566 |
566 |
567 end |
567 end |
579 fixes x::"'a::pt" |
579 fixes x::"'a::pt" |
580 shows "(p \<bullet> ([as]lst. x)) = [p \<bullet> as]lst. (p \<bullet> x)" |
580 shows "(p \<bullet> ([as]lst. x)) = [p \<bullet> as]lst. (p \<bullet> x)" |
581 by (lifting permute_prod.simps[where 'a="atom list" and 'b="'a"]) |
581 by (lifting permute_prod.simps[where 'a="atom list" and 'b="'a"]) |
582 |
582 |
583 instance |
583 instance |
584 apply(default) |
584 apply standard |
585 apply(case_tac [!] x) |
585 apply(case_tac [!] x) |
586 apply(simp_all) |
586 apply(simp_all) |
587 done |
587 done |
588 |
588 |
589 end |
589 end |
698 and "supp ([as]res. x) = (supp x) - as" |
698 and "supp ([as]res. x) = (supp x) - as" |
699 and "supp ([bs]lst. x) = (supp x) - (set bs)" |
699 and "supp ([bs]lst. x) = (supp x) - (set bs)" |
700 by (simp_all add: Abs_finite_supp finite_supp) |
700 by (simp_all add: Abs_finite_supp finite_supp) |
701 |
701 |
702 instance abs_set :: (fs) fs |
702 instance abs_set :: (fs) fs |
703 apply(default) |
703 apply standard |
704 apply(case_tac x) |
704 apply(case_tac x) |
705 apply(simp add: supp_Abs finite_supp) |
705 apply(simp add: supp_Abs finite_supp) |
706 done |
706 done |
707 |
707 |
708 instance abs_res :: (fs) fs |
708 instance abs_res :: (fs) fs |
709 apply(default) |
709 apply standard |
710 apply(case_tac x) |
710 apply(case_tac x) |
711 apply(simp add: supp_Abs finite_supp) |
711 apply(simp add: supp_Abs finite_supp) |
712 done |
712 done |
713 |
713 |
714 instance abs_lst :: (fs) fs |
714 instance abs_lst :: (fs) fs |
715 apply(default) |
715 apply standard |
716 apply(case_tac x) |
716 apply(case_tac x) |
717 apply(simp add: supp_Abs finite_supp) |
717 apply(simp add: supp_Abs finite_supp) |
718 done |
718 done |
719 |
719 |
720 lemma Abs_fresh_iff: |
720 lemma Abs_fresh_iff: |
931 |> map Free |
931 |> map Free |
932 |> HOLogic.mk_tuple |
932 |> HOLogic.mk_tuple |
933 |> Thm.cterm_of ctxt |
933 |> Thm.cterm_of ctxt |
934 val cvrs_ty = Thm.ctyp_of_cterm cvrs |
934 val cvrs_ty = Thm.ctyp_of_cterm cvrs |
935 val thm' = thm |
935 val thm' = thm |
936 |> Drule.instantiate' [NONE, NONE, SOME cvrs_ty] [NONE, NONE, NONE, NONE, SOME cvrs] |
936 |> Thm.instantiate' [NONE, NONE, SOME cvrs_ty] [NONE, NONE, NONE, NONE, SOME cvrs] |
937 in |
937 in |
938 SOME thm' |
938 SOME thm' |
939 end |
939 end |
940 *} |
940 *} |
941 |
941 |