equal
deleted
inserted
replaced
60 |
60 |
61 lemma supp_PTuple [simp]: "((supp \<langle>\<langle>p, q\<rangle>\<rangle>)::name set) = supp p \<union> supp q" |
61 lemma supp_PTuple [simp]: "((supp \<langle>\<langle>p, q\<rangle>\<rangle>)::name set) = supp p \<union> supp q" |
62 by (simp add: supp_def Collect_disj_eq del: disj_not1) |
62 by (simp add: supp_def Collect_disj_eq del: disj_not1) |
63 |
63 |
64 instance pat :: pt_name |
64 instance pat :: pt_name |
65 proof (default, goal_cases) |
65 proof (standard, goal_cases) |
66 case (1 x) |
66 case (1 x) |
67 show ?case by (induct x) simp_all |
67 show ?case by (induct x) simp_all |
68 next |
68 next |
69 case (2 _ _ x) |
69 case (2 _ _ x) |
70 show ?case by (induct x) (simp_all add: pt_name2) |
70 show ?case by (induct x) (simp_all add: pt_name2) |
72 case (3 _ _ x) |
72 case (3 _ _ x) |
73 then show ?case by (induct x) (simp_all add: pt_name3) |
73 then show ?case by (induct x) (simp_all add: pt_name3) |
74 qed |
74 qed |
75 |
75 |
76 instance pat :: fs_name |
76 instance pat :: fs_name |
77 proof (default, goal_cases) |
77 proof (standard, goal_cases) |
78 case (1 x) |
78 case (1 x) |
79 show ?case by (induct x) (simp_all add: fin_supp) |
79 show ?case by (induct x) (simp_all add: fin_supp) |
80 qed |
80 qed |
81 |
81 |
82 (* the following function cannot be defined using nominal_primrec, *) |
82 (* the following function cannot be defined using nominal_primrec, *) |