# HG changeset patch # User Cezary Kaliszyk # Date 1274800169 -7200 # Node ID 7687f97eca53edf11966db5e105a62569411a5df # Parent e559513143e997d1a609e32762d41aca46ad02b0 A lemma about substitution in TypeSchemes. diff -r e559513143e9 -r 7687f97eca53 Nominal/Ex/TypeSchemes.thy --- a/Nominal/Ex/TypeSchemes.thy Tue May 25 17:01:37 2010 +0200 +++ b/Nominal/Ex/TypeSchemes.thy Tue May 25 17:09:29 2010 +0200 @@ -152,6 +152,53 @@ apply auto done +fun + lookup :: "(name \ ty) list \ name \ ty" +where + "lookup [] n = Var n" +| "lookup ((p, s) # t) n = (if p = n then s else lookup t n)" + +locale subst_loc = +fixes + subst :: "(name \ ty) list \ ty \ ty" +and substs :: "(name \ ty) list \ tys \ tys" +assumes + s1: "subst \ (Var n) = lookup \ n" +and s2: "subst \ (Fun l r) = Fun (subst \ l) (subst \ r)" +and s3: "fset_to_set (fmap atom xs) \* \ \ substs \ (All xs t) = All xs (subst \ t)" +begin + +lemma subst_ty: + assumes x: "atom x \ t" + shows "subst [(x, S)] t = t" + using x + apply (induct t rule: ty_tys.induct[of _ "\t. True" _ , simplified]) + by (simp_all add: s1 s2 fresh_def ty_tys.fv[simplified ty_tys.supp] supp_at_base) + +lemma subst_tyS: + shows "atom x \ T \ substs [(x, S)] T = T" + apply (rule strong_induct[of + "\a t. True" "\d T. (atom (fst d) \ T \ substs [d] T = T)" _ "t" "(x, S)", simplified]) + apply (rule impI) + apply (subst s3) + apply (simp add: fresh_star_def fresh_Cons fresh_Nil) + apply (case_tac b) + apply clarify + apply (subst subst_ty) + apply simp_all + apply (simp add: fresh_star_prod) + apply clarify + apply (thin_tac "fset_to_set (fmap atom fset) \* ba") + apply (drule fresh_star_atom) + apply (unfold fresh_def) + apply (simp only: ty_tys.fv[simplified ty_tys.supp]) + apply (subgoal_tac "atom aa \ fset_to_set (fmap atom fset)") + apply blast + apply (metis supp_finite_atom_set finite_fset) + done + +end + (* PROBLEM: Type schemes with separate datatypes