nominal2: Nominal/Ex/TypeSchemes1.thy@9a63d90d1752 (annotated)

3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	1	theory TypeSchemes1
2454 9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2451 diff changeset	2	imports "../Nominal2"
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	begin
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	4
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	5	section {* Type Schemes defined as two separate nominal datatypes *}
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	6
2556 8ed62410236e added a test about subtyping; disabled two tests, because of problem with function package Christian Urban <urbanc@in.tum.de> parents: 2524 diff changeset	7	atom_decl name
8ed62410236e added a test about subtyping; disabled two tests, because of problem with function package Christian Urban <urbanc@in.tum.de> parents: 2524 diff changeset	8
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	9	nominal_datatype ty =
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	10	Var "name"
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	11	\| Fun "ty" "ty" ("_ \<rightarrow> _")
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	12
8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	13	nominal_datatype tys =
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	14	All xs::"name fset" ty::"ty" binds (set+) xs in ty ("All [_]._")
2434 92dc6cfa3a95 automatic lifting Christian Urban <urbanc@in.tum.de> parents: 2424 diff changeset	15
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	16	thm tys.distinct
8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	17	thm tys.induct tys.strong_induct
8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	18	thm tys.exhaust tys.strong_exhaust
8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	19	thm tys.fv_defs
8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	20	thm tys.bn_defs
8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	21	thm tys.perm_simps
8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	22	thm tys.eq_iff
8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	23	thm tys.fv_bn_eqvt
8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	24	thm tys.size_eqvt
8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	25	thm tys.supports
8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	26	thm tys.supp
8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	27	thm tys.fresh
2885 1264f2a21ea9 some rudimentary infrastructure for storing data about nominal datatypes Christian Urban <urbanc@in.tum.de> parents: 2867 diff changeset	28
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	29	subsection {* Substitution function for types and type schemes *}
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	30
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	31	type_synonym
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	32	Subst = "(name \<times> ty) list"
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	33
2707 747ebf2f066d made eqvt-proof explicit in the function definitions Christian Urban <urbanc@in.tum.de> parents: 2676 diff changeset	34	fun
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	35	lookup :: "Subst \<Rightarrow> name \<Rightarrow> ty"
2707 747ebf2f066d made eqvt-proof explicit in the function definitions Christian Urban <urbanc@in.tum.de> parents: 2676 diff changeset	36	where
747ebf2f066d made eqvt-proof explicit in the function definitions Christian Urban <urbanc@in.tum.de> parents: 2676 diff changeset	37	"lookup [] Y = Var Y"
747ebf2f066d made eqvt-proof explicit in the function definitions Christian Urban <urbanc@in.tum.de> parents: 2676 diff changeset	38	\| "lookup ((X, T) # Ts) Y = (if X = Y then T else lookup Ts Y)"
747ebf2f066d made eqvt-proof explicit in the function definitions Christian Urban <urbanc@in.tum.de> parents: 2676 diff changeset	39
747ebf2f066d made eqvt-proof explicit in the function definitions Christian Urban <urbanc@in.tum.de> parents: 2676 diff changeset	40	lemma lookup_eqvt[eqvt]:
747ebf2f066d made eqvt-proof explicit in the function definitions Christian Urban <urbanc@in.tum.de> parents: 2676 diff changeset	41	shows "(p \<bullet> lookup Ts T) = lookup (p \<bullet> Ts) (p \<bullet> T)"
747ebf2f066d made eqvt-proof explicit in the function definitions Christian Urban <urbanc@in.tum.de> parents: 2676 diff changeset	42	apply(induct Ts T rule: lookup.induct)
747ebf2f066d made eqvt-proof explicit in the function definitions Christian Urban <urbanc@in.tum.de> parents: 2676 diff changeset	43	apply(simp_all)
747ebf2f066d made eqvt-proof explicit in the function definitions Christian Urban <urbanc@in.tum.de> parents: 2676 diff changeset	44	done
747ebf2f066d made eqvt-proof explicit in the function definitions Christian Urban <urbanc@in.tum.de> parents: 2676 diff changeset	45
2981 c8acaded1777 temporary fix Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	46
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	47	nominal_primrec
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	48	subst :: "Subst \<Rightarrow> ty \<Rightarrow> ty" ("_<_>" [100,60] 120)
2838 36544bac1659 More experiments with 'default' Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2836 diff changeset	49	where
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	50	"\<theta><Var X> = lookup \<theta> X"
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	51	\| "\<theta><T1 \<rightarrow> T2> = (\<theta><T1>) \<rightarrow> (\<theta><T2>)"
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	52	unfolding eqvt_def subst_graph_def
2801 5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	53	apply (rule, perm_simp, rule)
2822 23befefc6e73 cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file Christian Urban <urbanc@in.tum.de> parents: 2805 diff changeset	54	apply(rule TrueI)
2801 5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	55	apply(case_tac x)
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	56	apply(rule_tac y="b" in ty.exhaust)
2801 5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	57	apply(blast)
5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	58	apply(blast)
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	59	apply(simp_all)
2801 5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	60	done
2676 028d5511c15f some tryes about substitution over type-schemes Christian Urban <urbanc@in.tum.de> parents: 2634 diff changeset	61
2973 d1038e67923a added a flag (eqvt) to termination proofs arising fron nominal_primrecs Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	62	termination (eqvt)
2859 2eeb75cccb8d all tests work again Christian Urban <urbanc@in.tum.de> parents: 2850 diff changeset	63	by lexicographic_order
2676 028d5511c15f some tryes about substitution over type-schemes Christian Urban <urbanc@in.tum.de> parents: 2634 diff changeset	64
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	65	lemma supp_fun_app_eqvt:
2801 5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	66	assumes e: "eqvt f"
5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	67	shows "supp (f a b) \<subseteq> supp a \<union> supp b"
5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	68	using supp_fun_app_eqvt[OF e] supp_fun_app
5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	69	by blast
5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	70
5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	71	lemma supp_subst:
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	72	"supp (subst \<theta> t) \<subseteq> supp \<theta> \<union> supp t"
8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	73	apply (rule supp_fun_app_eqvt)
8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	74	unfolding eqvt_def
8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	75	by (simp add: permute_fun_def subst.eqvt)
2801 5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	76
2676 028d5511c15f some tryes about substitution over type-schemes Christian Urban <urbanc@in.tum.de> parents: 2634 diff changeset	77	nominal_primrec
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	78	substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" ("_<_>" [100,60] 120)
2676 028d5511c15f some tryes about substitution over type-schemes Christian Urban <urbanc@in.tum.de> parents: 2634 diff changeset	79	where
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	80	"fset (map_fset atom Xs) \<sharp>* \<theta> \<Longrightarrow> \<theta><All [Xs].T> = All [Xs].(\<theta><T>)"
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	81	unfolding eqvt_def substs_graph_def
2801 5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	82	apply (rule, perm_simp, rule)
2822 23befefc6e73 cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file Christian Urban <urbanc@in.tum.de> parents: 2805 diff changeset	83	apply auto[2]
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	84	apply (rule_tac y="b" and c="a" in tys.strong_exhaust)
2982 4a00077c008f completed the eqvt-proofs for functions; they are stored under the name function_name.eqvt and added to the eqvt-list Christian Urban <urbanc@in.tum.de> parents: 2981 diff changeset	85	apply auto[1]
4a00077c008f completed the eqvt-proofs for functions; they are stored under the name function_name.eqvt and added to the eqvt-list Christian Urban <urbanc@in.tum.de> parents: 2981 diff changeset	86	apply(simp)
4a00077c008f completed the eqvt-proofs for functions; they are stored under the name function_name.eqvt and added to the eqvt-list Christian Urban <urbanc@in.tum.de> parents: 2981 diff changeset	87	apply(erule conjE)
2830 297cff1d1048 FCB for res binding and simplified proof of subst for type schemes Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2822 diff changeset	88	apply (erule Abs_res_fcb)
297cff1d1048 FCB for res binding and simplified proof of subst for type schemes Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2822 diff changeset	89	apply (simp add: Abs_fresh_iff)
2982 4a00077c008f completed the eqvt-proofs for functions; they are stored under the name function_name.eqvt and added to the eqvt-list Christian Urban <urbanc@in.tum.de> parents: 2981 diff changeset	90	apply(simp add: fresh_def)
4a00077c008f completed the eqvt-proofs for functions; they are stored under the name function_name.eqvt and added to the eqvt-list Christian Urban <urbanc@in.tum.de> parents: 2981 diff changeset	91	apply(simp add: supp_Abs)
4a00077c008f completed the eqvt-proofs for functions; they are stored under the name function_name.eqvt and added to the eqvt-list Christian Urban <urbanc@in.tum.de> parents: 2981 diff changeset	92	apply(rule impI)
4a00077c008f completed the eqvt-proofs for functions; they are stored under the name function_name.eqvt and added to the eqvt-list Christian Urban <urbanc@in.tum.de> parents: 2981 diff changeset	93	apply(subgoal_tac "x \<notin> supp \<theta>")
4a00077c008f completed the eqvt-proofs for functions; they are stored under the name function_name.eqvt and added to the eqvt-list Christian Urban <urbanc@in.tum.de> parents: 2981 diff changeset	94	prefer 2
4a00077c008f completed the eqvt-proofs for functions; they are stored under the name function_name.eqvt and added to the eqvt-list Christian Urban <urbanc@in.tum.de> parents: 2981 diff changeset	95	apply(auto simp add: fresh_star_def fresh_def)[1]
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	96	apply(subgoal_tac "x \<in> supp T")
2982 4a00077c008f completed the eqvt-proofs for functions; they are stored under the name function_name.eqvt and added to the eqvt-list Christian Urban <urbanc@in.tum.de> parents: 2981 diff changeset	97	using supp_subst
4a00077c008f completed the eqvt-proofs for functions; they are stored under the name function_name.eqvt and added to the eqvt-list Christian Urban <urbanc@in.tum.de> parents: 2981 diff changeset	98	apply(blast)
4a00077c008f completed the eqvt-proofs for functions; they are stored under the name function_name.eqvt and added to the eqvt-list Christian Urban <urbanc@in.tum.de> parents: 2981 diff changeset	99	using supp_subst
4a00077c008f completed the eqvt-proofs for functions; they are stored under the name function_name.eqvt and added to the eqvt-list Christian Urban <urbanc@in.tum.de> parents: 2981 diff changeset	100	apply(blast)
2832 76db0b854bf6 Simpler proof of TypeSchemes/substs Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2831 diff changeset	101	apply clarify
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	102	apply (simp add: subst.eqvt)
2801 5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	103	apply (subst Abs_eq_iff)
5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	104	apply (rule_tac x="0::perm" in exI)
2832 76db0b854bf6 Simpler proof of TypeSchemes/substs Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2831 diff changeset	105	apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")
2801 5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	106	apply (simp add: alphas fresh_star_zero)
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	107	apply (subgoal_tac "\<And>x. x \<in> supp (subst \<theta>' (p \<bullet> T)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset Xs \<longleftrightarrow> x \<in> atom ` fset Xsa")
2804 db0ed02eba6e Remove SMT Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2801 diff changeset	108	apply blast
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	109	apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> T)")
2839 bcf48a1cb24b abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2838 diff changeset	110	apply (simp add: supp_Pair eqvts eqvts_raw)
bcf48a1cb24b abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2838 diff changeset	111	apply auto[1]
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	112	apply (subgoal_tac "(atom ` fset (p \<bullet> Xs)) \<sharp>* \<theta>'")
2801 5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	113	apply (simp add: fresh_star_def fresh_def)
2839 bcf48a1cb24b abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2838 diff changeset	114	apply(drule_tac p1="p" in iffD2[OF fresh_star_permute_iff])
bcf48a1cb24b abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2838 diff changeset	115	apply (simp add: eqvts eqvts_raw)
2801 5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	116	apply (simp add: fresh_star_def fresh_def)
2839 bcf48a1cb24b abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2838 diff changeset	117	apply (drule subsetD[OF supp_subst])
bcf48a1cb24b abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2838 diff changeset	118	apply (simp add: supp_Pair)
2832 76db0b854bf6 Simpler proof of TypeSchemes/substs Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2831 diff changeset	119	apply (rule perm_supp_eq)
76db0b854bf6 Simpler proof of TypeSchemes/substs Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2831 diff changeset	120	apply (simp add: fresh_def fresh_star_def)
2801 5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	121	apply blast
5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	122	done
2676 028d5511c15f some tryes about substitution over type-schemes Christian Urban <urbanc@in.tum.de> parents: 2634 diff changeset	123
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	124	termination (eqvt)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	125	by (lexicographic_order)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	126
2676 028d5511c15f some tryes about substitution over type-schemes Christian Urban <urbanc@in.tum.de> parents: 2634 diff changeset	127	text {* Some Tests about Alpha-Equality *}
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	128
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	129	lemma
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	130	shows "All [{\|a, b\|}].((Var a) \<rightarrow> (Var b)) = All [{\|b, a\|}]. ((Var a) \<rightarrow> (Var b))"
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	131	apply(simp add: Abs_eq_iff)
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	132	apply(rule_tac x="0::perm" in exI)
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	133	apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	134	done
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	135
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	136	lemma
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	137	shows "All [{\|a, b\|}].((Var a) \<rightarrow> (Var b)) = All [{\|a, b\|}].((Var b) \<rightarrow> (Var a))"
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	138	apply(simp add: Abs_eq_iff)
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	139	apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	140	apply(simp add: alphas fresh_star_def supp_at_base ty.supp)
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	141	done
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	142
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	143	lemma
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	144	shows "All [{\|a, b, c\|}].((Var a) \<rightarrow> (Var b)) = All [{\|a, b\|}].((Var a) \<rightarrow> (Var b))"
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	145	apply(simp add: Abs_eq_iff)
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	146	apply(rule_tac x="0::perm" in exI)
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	147	apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	148	done
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	149
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	150	lemma
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	151	assumes a: "a \<noteq> b"
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	152	shows "\<not>(All [{\|a, b\|}].((Var a) \<rightarrow> (Var b)) = All [{\|c\|}].((Var c) \<rightarrow> (Var c)))"
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	153	using a
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	154	apply(simp add: Abs_eq_iff)
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	155	apply(clarify)
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	156	apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	157	apply auto
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	158	done
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	159
2566 a59d8e1e3a17 moved rest of the lemmas from Nominal2_FSet to the TypeScheme example Christian Urban <urbanc@in.tum.de> parents: 2556 diff changeset	160
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	161	text {* HERE *}
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	162
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	163	fun
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	164	compose::"Subst \<Rightarrow> Subst \<Rightarrow> Subst" ("_ \<circ> _" [100,100] 100)
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	165	where
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	166	"\<theta>\<^isub>1 \<circ> [] = \<theta>\<^isub>1"
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	167	\| "\<theta>\<^isub>1 \<circ> ((X,T)#\<theta>\<^isub>2) = (X,\<theta>\<^isub>1<T>)#(\<theta>\<^isub>1 \<circ> \<theta>\<^isub>2)"
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	168
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	169	lemma compose_eqvt:
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	170	fixes \<theta>1 \<theta>2::"Subst"
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	171	shows "(p \<bullet> (\<theta>1 \<circ> \<theta>2)) = ((p \<bullet> \<theta>1) \<circ> (p \<bullet> \<theta>2))"
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	172	apply(induct \<theta>2)
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	173	apply(auto simp add: subst.eqvt)
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	174	done
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	175
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	176	lemma compose_ty:
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	177	fixes \<theta>1 :: "Subst"
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	178	and \<theta>2 :: "Subst"
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	179	and T :: "ty"
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	180	shows "\<theta>1<\<theta>2<T>> = (\<theta>1\<circ>\<theta>2)<T>"
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	181	proof (induct T rule: ty.induct)
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	182	case (Var X)
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	183	have "\<theta>1<lookup \<theta>2 X> = lookup (\<theta>1\<circ>\<theta>2) X"
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	184	by (induct \<theta>2) (auto)
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	185	then show ?case by simp
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	186	next
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	187	case (Fun T1 T2)
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	188	then show ?case by simp
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	189	qed
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	190
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	191	fun
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	192	subst_subst :: "Subst \<Rightarrow> Subst \<Rightarrow> Subst" ("_<_>" [100,60] 120)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	193	where
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	194	"\<theta><[]> = []"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	195	\| "\<theta> <((X,T)#\<theta>')> = (X,\<theta><T>)#(\<theta><\<theta>'>)"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	196
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	197	lemma redundant1:
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	198	fixes \<theta>1::"Subst"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	199	and \<theta>2::"Subst"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	200	shows "\<theta>1 \<circ> \<theta>2 = (\<theta>1<\<theta>2>)@\<theta>1"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	201	by (induct \<theta>2) (auto)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	202
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	203	fun
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	204	dom :: "Subst \<Rightarrow> name fset"
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	205	where
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	206	"dom [] = {\|\|}"
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	207	\| "dom ((X,T)#\<theta>) = {\|X\|} \|\<union>\| dom \<theta>"
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	208
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	209	lemma dom_eqvt[eqvt]:
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	210	shows "(p \<bullet> dom \<theta>) = dom (p \<bullet> \<theta>)"
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	211	apply(induct \<theta> rule: dom.induct)
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	212	apply(simp_all)
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	213	done
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	214
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	215	lemma dom_compose:
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	216	shows "dom (\<theta>1 \<circ> \<theta>2) = dom \<theta>1 \|\<union>\| dom \<theta>2"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	217	apply(induct rule: dom.induct)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	218	apply(simp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	219	apply(simp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	220	by (metis sup_commute union_insert_fset)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	221
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	222	lemma redundant3:
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	223	fixes \<theta>1::"Subst"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	224	and \<theta>2::"Subst"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	225	shows "dom (\<theta>2<\<theta>1>) = (dom \<theta>1)"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	226	by (induct \<theta>1) (auto)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	227
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	228	lemma dom_pi:
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	229	shows "(p \<bullet> (dom \<theta>)) = dom (map (\<lambda>(X, T). (p \<bullet> X, T)) \<theta>)"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	230	apply(induct \<theta>)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	231	apply(auto)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	232	done
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	233
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	234	lemma dom_fresh_lookup:
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	235	fixes \<theta>::"Subst"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	236	assumes "\<forall>X \<in> fset (dom \<theta>). atom X \<sharp> name"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	237	shows "lookup \<theta> name = Var name"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	238	using assms
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	239	apply(induct \<theta>)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	240	apply(auto simp add: fresh_at_base)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	241	done
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	242
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	243	lemma dom_fresh_ty:
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	244	fixes \<theta>::"Subst"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	245	and T::"ty"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	246	assumes "\<forall>X \<in> fset (dom \<theta>). atom X \<sharp> T"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	247	shows "\<theta><T> = T"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	248	using assms
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	249	apply(induct T rule: ty.induct)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	250	apply(auto simp add: ty.fresh dom_fresh_lookup)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	251	done
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	252
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	253	lemma dom_fresh_subst:
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	254	fixes \<theta> \<theta>'::"Subst"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	255	assumes "\<forall>X \<in> fset (dom \<theta>). atom X \<sharp> \<theta>'"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	256	shows "\<theta><\<theta>'> = \<theta>'"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	257	using assms
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	258	apply(induct \<theta>')
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	259	apply(auto simp add: fresh_Pair fresh_Cons dom_fresh_ty)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	260	done
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	261
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	262
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	263	abbreviation
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	264	"sub_list" :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<subseteq> _" [60,60] 60)
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	265	where
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	266	"xs\<^isub>1 \<subseteq> xs\<^isub>2 \<equiv> \<forall>x. x \<in> set xs\<^isub>1 \<longrightarrow> x \<in> set xs\<^isub>2"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	267
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	268
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	269	definition
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	270	generalises3 :: "ty \<Rightarrow> tys \<Rightarrow> bool" ("_ \<prec>\<prec>\<prec>\<prec> _")
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	271	where
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	272	" T \<prec>\<prec>\<prec>\<prec> S \<longleftrightarrow> (\<exists>\<theta> Xs T'. S = All [Xs].T'\<and> T = \<theta><T'> \<and> dom \<theta> = Xs)"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	273
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	274
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	275	lemma lookup_fresh:
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	276	fixes X::"name"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	277	assumes a: "atom X \<sharp> \<theta>"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	278	shows "lookup \<theta> X = Var X"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	279	using a
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	280	apply (induct \<theta>)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	281	apply (auto simp add: fresh_Cons fresh_Pair fresh_at_base)
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	282	done
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	283
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	284	lemma lookup_dom:
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	285	fixes X::"name"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	286	assumes a: "X \|\<notin>\| dom \<theta>"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	287	shows "lookup \<theta> X = Var X"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	288	using a
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	289	apply (induct \<theta>)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	290	apply(auto)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	291	done
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	292
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	293	lemma w1:
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	294	"\<theta><map (\<lambda>(X, y). (p \<bullet> X, y)) \<theta>'> = map (\<lambda>(X, y). (p \<bullet> X, y)) (\<theta><\<theta>'>)"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	295	apply(induct \<theta>')
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	296	apply(auto)
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	297	done
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	298
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	299	lemma w2:
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	300	assumes "name \|\<in>\| dom \<theta>'"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	301	shows "\<theta><lookup \<theta>' name> = lookup (\<theta><\<theta>'>) name"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	302	using assms
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	303	apply(induct \<theta>')
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	304	apply(auto)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	305	by (metis notin_empty_fset)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	306
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	307	lemma w3:
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	308	assumes "name \|\<in>\| dom \<theta>"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	309	shows "lookup \<theta> name = lookup (map (\<lambda>(X, y). (p \<bullet> X, y)) \<theta>) (p \<bullet> name)"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	310	using assms
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	311	apply(induct \<theta>)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	312	apply(auto)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	313	by (metis notin_empty_fset)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	314
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	315	lemma fresh_lookup:
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	316	fixes X Y::"name"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	317	and \<theta>::"Subst"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	318	assumes asms: "atom X \<sharp> Y" "atom X \<sharp> \<theta>"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	319	shows "atom X \<sharp> (lookup \<theta> Y)"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	320	using assms
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	321	apply (induct \<theta>)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	322	apply (auto simp add: fresh_Cons fresh_Pair fresh_at_base ty.fresh)
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	323	done
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	324
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	325	lemma test:
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	326	fixes \<theta> \<theta>'::"Subst"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	327	and T::"ty"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	328	assumes "(p \<bullet> atom ` fset (dom \<theta>')) \<sharp>* \<theta>" "supp All [dom \<theta>'].T \<sharp>* p"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	329	shows "\<theta><\<theta>'<T>> = \<theta><map (\<lambda>(X, y). (p \<bullet> X, y)) \<theta>'><\<theta><p \<bullet> T>>"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	330	using assms
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	331	apply(induct T rule: ty.induct)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	332	defer
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	333	apply(auto simp add: tys.supp ty.supp fresh_star_def)[1]
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	334	apply(auto simp add: tys.supp ty.supp fresh_star_def supp_at_base)[1]
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	335	apply(case_tac "name \|\<in>\| dom \<theta>'")
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	336	apply(subgoal_tac "atom (p \<bullet> name) \<sharp> \<theta>")
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	337	apply(subst (2) lookup_fresh)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	338	apply(perm_simp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	339	apply(auto simp add: fresh_star_def)[1]
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	340	apply(simp)
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	341	apply(simp add: w1)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	342	apply(simp add: w2)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	343	apply(subst w3[symmetric])
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	344	apply(simp add:redundant3)
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	345	apply(simp)
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	346	apply(perm_simp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	347	apply(rotate_tac 2)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	348	apply(drule_tac p="p" in permute_boolI)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	349	apply(perm_simp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	350	apply(auto simp add: fresh_star_def)[1]
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	351	apply(metis notin_fset)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	352	apply(simp add: lookup_dom)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	353	apply(perm_simp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	354	apply(subst dom_fresh_ty)
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	355	apply(auto)[1]
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	356	apply(rule fresh_lookup)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	357	apply(simp add: redundant3)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	358	apply(simp add: dom_pi[symmetric])
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	359	apply(perm_simp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	360	apply(rotate_tac 2)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	361	apply(drule_tac p="p" in permute_boolI)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	362	apply(perm_simp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	363	apply(simp add: fresh_at_base)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	364	apply (metis in_fset)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	365	apply(simp add: redundant3)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	366	apply(simp add: dom_pi[symmetric])
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	367	apply(perm_simp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	368	apply metis
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	369	apply(subst supp_perm_eq)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	370	apply(simp add: supp_at_base fresh_star_def)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	371	apply (smt Diff_iff atom_eq_iff image_iff insertI1 notin_fset)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	372	apply(simp)
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	373	done
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	374
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	375	lemma
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	376	shows "T \<prec>\<prec>\<prec>\<prec> S \<Longrightarrow> \<theta><T> \<prec>\<prec>\<prec>\<prec> \<theta><S>"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	377	unfolding generalises3_def
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	378	apply(erule exE)+
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	379	apply(erule conjE)+
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	380	apply(rule_tac t="S" and s="All [Xs].T'" in subst)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	381	apply(simp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	382	using at_set_avoiding3
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	383	apply -
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	384	apply(drule_tac x="fset (map_fset atom Xs)" in meta_spec)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	385	apply(drule_tac x="\<theta>" in meta_spec)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	386	apply(drule_tac x="All [Xs].T'" in meta_spec)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	387	apply(drule meta_mp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	388	apply(simp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	389	apply(drule meta_mp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	390	apply(simp add: finite_supp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	391	apply(drule meta_mp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	392	apply(simp add: finite_supp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	393	apply(drule meta_mp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	394	apply(simp add: tys.fresh fresh_star_def)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	395	apply(erule exE)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	396	apply(erule conjE)+
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	397	apply(rule_tac t="All[Xs].T'" and s="p \<bullet> (All [Xs].T')" in subst)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	398	apply(rule supp_perm_eq)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	399	apply(assumption)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	400	apply(perm_simp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	401	apply(subst substs.simps)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	402	apply(perm_simp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	403	apply(simp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	404	apply(rule_tac x="\<theta><map (\<lambda>(X, T). (p \<bullet> X, T)) \<theta>'>" in exI)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	405	apply(rule_tac x="p \<bullet> Xs" in exI)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	406	apply(rule_tac x="\<theta><p \<bullet> T'>" in exI)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	407	apply(rule conjI)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	408	apply(simp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	409	apply(rule conjI)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	410	defer
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	411	apply(simp add: redundant3)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	412	apply(simp add: dom_pi[symmetric])
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	413	apply(rule_tac t="T" and s="\<theta>'<T'>" in subst)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	414	apply(simp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	415	apply(rule test)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	416	apply(perm_simp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	417	apply(rotate_tac 2)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	418	apply(drule_tac p="p" in permute_boolI)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	419	apply(perm_simp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	420	apply(auto simp add: fresh_star_def)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	421	done
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	422
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	423
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	424	end

author	Christian Urban <urbanc@in.tum.de>
	Tue, 03 Jan 2012 01:42:10 +0000
changeset 3103	9a63d90d1752
parent 3102	5b5ade6bc889
child 3104	f7c4b8e6918b
permissions	-rw-r--r--