equal
deleted
inserted
replaced
66 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" |
66 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" |
67 where |
67 where |
68 "subst \<theta> (Var X) = lookup \<theta> X" |
68 "subst \<theta> (Var X) = lookup \<theta> X" |
69 | "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)" |
69 | "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)" |
70 | "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)" |
70 | "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)" |
|
71 thm subst_substs_graph_def subst_substs_graph_aux_def |
71 apply(simp add: subst_substs_graph_aux_def eqvt_def) |
72 apply(simp add: subst_substs_graph_aux_def eqvt_def) |
72 apply(rule TrueI) |
73 apply(rule TrueI) |
73 apply (case_tac x) |
74 apply (case_tac x) |
74 apply simp apply clarify |
75 apply simp apply clarify |
75 apply (rule_tac y="b" in ty_tys.exhaust(1)) |
76 apply (rule_tac y="b" in ty_tys.exhaust(1)) |