69 and "E \<subseteq> A \<union> B" |
69 and "E \<subseteq> A \<union> B" |
70 shows "E - C = E - D" |
70 shows "E - C = E - D" |
71 using assms |
71 using assms |
72 by blast |
72 by blast |
73 |
73 |
74 nominal_primrec |
74 definition "MYUNDEFINED \<equiv> undefined" |
|
75 |
|
76 nominal_primrec (default "\<lambda>x. MYUNDEFINED") |
75 subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty" |
77 subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty" |
76 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" |
78 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" |
77 where |
79 where |
78 "subst \<theta> (Var X) = lookup \<theta> X" |
80 "subst \<theta> (Var X) = lookup \<theta> X" |
79 | "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)" |
81 | "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)" |
80 | "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)" |
82 | "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)" |
|
83 thm subst_substs_graph_def |
|
84 thm subst_substs_sumC_def |
|
85 oops |
|
86 |
|
87 nominal_primrec |
|
88 subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty" |
|
89 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" |
|
90 where |
|
91 "subst \<theta> (Var X) = lookup \<theta> X" |
|
92 | "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)" |
|
93 | "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)" |
|
94 thm subst_substs_graph_def |
|
95 thm subst_substs_sumC_def |
81 apply(subgoal_tac "\<And>p x r. subst_substs_graph x r \<Longrightarrow> subst_substs_graph (p \<bullet> x) (p \<bullet> r)") |
96 apply(subgoal_tac "\<And>p x r. subst_substs_graph x r \<Longrightarrow> subst_substs_graph (p \<bullet> x) (p \<bullet> r)") |
82 apply(simp add: eqvt_def) |
97 apply(simp add: eqvt_def) |
83 apply(rule allI) |
98 apply(rule allI) |
84 apply(simp add: permute_fun_def permute_bool_def) |
99 apply(simp add: permute_fun_def permute_bool_def) |
85 apply(rule ext) |
100 apply(rule ext) |