nominal2: Nominal/Ex/TypeSchemes1.thy@d79e936e30ea (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
3104 f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 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
3104 f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	29	subsection {* Some Tests about Alpha-Equality *}
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	30
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	31	lemma
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	32	shows "All [{\|a, b\|}].((Var a) \<rightarrow> (Var b)) = All [{\|b, a\|}]. ((Var a) \<rightarrow> (Var b))"
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	33	apply(simp add: Abs_eq_iff)
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	34	apply(rule_tac x="0::perm" in exI)
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	35	apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	36	done
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	37
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	38	lemma
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	39	shows "All [{\|a, b\|}].((Var a) \<rightarrow> (Var b)) = All [{\|a, b\|}].((Var b) \<rightarrow> (Var a))"
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	40	apply(simp add: Abs_eq_iff)
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	41	apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	42	apply(simp add: alphas fresh_star_def supp_at_base ty.supp)
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	43	done
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	44
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	45	lemma
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	46	shows "All [{\|a, b, c\|}].((Var a) \<rightarrow> (Var b)) = All [{\|a, b\|}].((Var a) \<rightarrow> (Var b))"
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	47	apply(simp add: Abs_eq_iff)
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	48	apply(rule_tac x="0::perm" in exI)
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	49	apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	50	done
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	51
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	52	lemma
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	53	assumes a: "a \<noteq> b"
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	54	shows "\<not>(All [{\|a, b\|}].((Var a) \<rightarrow> (Var b)) = All [{\|c\|}].((Var c) \<rightarrow> (Var c)))"
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	55	using a
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	56	apply(simp add: Abs_eq_iff)
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	57	apply(clarify)
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	58	apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	59	apply auto
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	60	done
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	61
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	62
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	63	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	64
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	65	type_synonym
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	66	Subst = "(name \<times> ty) list"
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	67
2707 747ebf2f066d made eqvt-proof explicit in the function definitions Christian Urban <urbanc@in.tum.de> parents: 2676 diff changeset	68	fun
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	69	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	70	where
747ebf2f066d made eqvt-proof explicit in the function definitions Christian Urban <urbanc@in.tum.de> parents: 2676 diff changeset	71	"lookup [] Y = Var Y"
747ebf2f066d made eqvt-proof explicit in the function definitions Christian Urban <urbanc@in.tum.de> parents: 2676 diff changeset	72	\| "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	73
747ebf2f066d made eqvt-proof explicit in the function definitions Christian Urban <urbanc@in.tum.de> parents: 2676 diff changeset	74	lemma lookup_eqvt[eqvt]:
747ebf2f066d made eqvt-proof explicit in the function definitions Christian Urban <urbanc@in.tum.de> parents: 2676 diff changeset	75	shows "(p \<bullet> lookup Ts T) = lookup (p \<bullet> Ts) (p \<bullet> T)"
3104 f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	76	by (induct Ts T rule: lookup.induct) (simp_all)
2981 c8acaded1777 temporary fix Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	77
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	78	nominal_primrec
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	79	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	80	where
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	81	"\<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	82	\| "\<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	83	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	84	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	85	apply(rule TrueI)
2801 5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	86	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	87	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	88	apply(blast)
5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	89	apply(blast)
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	90	apply(simp_all)
2801 5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	91	done
2676 028d5511c15f some tryes about substitution over type-schemes Christian Urban <urbanc@in.tum.de> parents: 2634 diff changeset	92
2973 d1038e67923a added a flag (eqvt) to termination proofs arising fron nominal_primrecs Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	93	termination (eqvt)
2859 2eeb75cccb8d all tests work again Christian Urban <urbanc@in.tum.de> parents: 2850 diff changeset	94	by lexicographic_order
2676 028d5511c15f some tryes about substitution over type-schemes Christian Urban <urbanc@in.tum.de> parents: 2634 diff changeset	95
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	96	lemma subst_id1:
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	97	fixes T::"ty"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	98	shows "[]<T> = T"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	99	by (induct T rule: ty.induct) (simp_all)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	100
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	101	lemma subst_id2:
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	102	fixes T::"ty"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	103	shows "[(X, Var X)]<T> = T"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	104	by (induct T rule: ty.induct) (simp_all)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	105
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	106	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	107	assumes e: "eqvt f"
5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	108	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	109	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	110	by blast
5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	111
5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	112	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	113	"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	114	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	115	unfolding eqvt_def
8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	116	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	117
2676 028d5511c15f some tryes about substitution over type-schemes Christian Urban <urbanc@in.tum.de> parents: 2634 diff changeset	118	nominal_primrec
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	119	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	120	where
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	121	"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	122	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	123	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	124	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	125	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	126	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	127	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	128	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	129	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	130	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	131	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	132	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	133	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	134	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	135	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	136	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	137	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	138	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	139	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	140	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	141	apply(blast)
2832 76db0b854bf6 Simpler proof of TypeSchemes/substs Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2831 diff changeset	142	apply clarify
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	143	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	144	apply (subst Abs_eq_iff)
5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	145	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	146	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	147	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	148	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	149	apply blast
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	150	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	151	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	152	apply auto[1]
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	153	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	154	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	155	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	156	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	157	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	158	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	159	apply (simp add: supp_Pair)
2832 76db0b854bf6 Simpler proof of TypeSchemes/substs Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2831 diff changeset	160	apply (rule perm_supp_eq)
76db0b854bf6 Simpler proof of TypeSchemes/substs Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2831 diff changeset	161	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	162	apply blast
5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	163	done
2676 028d5511c15f some tryes about substitution over type-schemes Christian Urban <urbanc@in.tum.de> parents: 2634 diff changeset	164
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	165	termination (eqvt)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	166	by (lexicographic_order)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	167
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	168
3104 f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	169	subsection {* Generalisation of types and type-schemes*}
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	170
3104 f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	171	fun
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	172	subst_Dom_pi :: "Subst \<Rightarrow> perm \<Rightarrow> Subst" ("_\|_")
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	173	where
3104 f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	174	"[]\|p = []"
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	175	\| "((X,T)#\<theta>)\|p = (p \<bullet> X, T)#(\<theta>\|p)"
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	176
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	177	fun
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	178	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	179	where
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	180	"\<theta><[]> = []"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	181	\| "\<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	182
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	183	fun
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	184	Dom :: "Subst \<Rightarrow> name set"
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	185	where
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	186	"Dom [] = {}"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	187	\| "Dom ((X,T)#\<theta>) = {X} \<union> Dom \<theta>"
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	188
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	189	lemma Dom_eqvt[eqvt]:
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	190	shows "p \<bullet> (Dom \<theta>) = Dom (p \<bullet> \<theta>)"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	191	apply (induct \<theta> rule: Dom.induct)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	192	apply (simp_all add: permute_set_def)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	193	apply (auto)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	194	done
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	195
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	196	lemma Dom_subst:
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	197	fixes \<theta>1 \<theta>2::"Subst"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	198	shows "Dom (\<theta>2<\<theta>1>) = (Dom \<theta>1)"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	199	by (induct \<theta>1) (auto)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	200
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	201	lemma Dom_pi:
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	202	shows "Dom (\<theta>\|p) = Dom (p \<bullet> \<theta>)"
3104 f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	203	by (induct \<theta>) (auto)
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	204
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	205	lemma Dom_fresh_lookup:
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	206	fixes \<theta>::"Subst"
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	207	assumes "\<forall>Y \<in> Dom \<theta>. atom Y \<sharp> X"
3104 f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	208	shows "lookup \<theta> X = Var X"
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	209	using assms
3104 f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	210	by (induct \<theta>) (auto simp add: fresh_at_base)
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	211
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	212	lemma Dom_fresh_ty:
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	213	fixes \<theta>::"Subst"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	214	and T::"ty"
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	215	assumes "\<forall>X \<in> Dom \<theta>. atom X \<sharp> T"
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	216	shows "\<theta><T> = T"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	217	using assms
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	218	by (induct T rule: ty.induct) (auto simp add: ty.fresh Dom_fresh_lookup)
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	219
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	220	lemma Dom_fresh_subst:
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	221	fixes \<theta> \<theta>'::"Subst"
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	222	assumes "\<forall>X \<in> Dom \<theta>. atom X \<sharp> \<theta>'"
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	223	shows "\<theta><\<theta>'> = \<theta>'"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	224	using assms
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	225	by (induct \<theta>') (auto simp add: fresh_Pair fresh_Cons Dom_fresh_ty)
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	226
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	227	lemma s1:
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	228	assumes "name \<in> Dom \<theta>"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	229	shows "lookup \<theta> name = lookup \<theta>\|p (p \<bullet> name)"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	230	using assms
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	231	apply(induct \<theta>)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	232	apply(auto)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	233	done
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	234
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	235	lemma lookup_fresh:
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	236	fixes X::"name"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	237	assumes a: "atom X \<sharp> \<theta>"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	238	shows "lookup \<theta> X = Var X"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	239	using a
3104 f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	240	by (induct \<theta>) (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	241
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	242	lemma lookup_Dom:
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	243	fixes X::"name"
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	244	assumes "X \<notin> Dom \<theta>"
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	245	shows "lookup \<theta> X = Var X"
3104 f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	246	using assms
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	247	by (induct \<theta>) (auto)
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	248
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	249	lemma t:
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	250	fixes T::"ty"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	251	assumes a: "(supp T - atom ` Dom \<theta>) \<sharp>* p"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	252	shows "\<theta><T> = \<theta>\|p<p \<bullet> T>"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	253	using a
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	254	apply(induct T rule: ty.induct)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	255	defer
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	256	apply(simp add: ty.supp fresh_star_def)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	257	apply(simp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	258	apply(case_tac "name \<in> Dom \<theta>")
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	259	apply(rule s1)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	260	apply(assumption)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	261	apply(subst lookup_Dom)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	262	apply(assumption)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	263	apply(subst lookup_Dom)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	264	apply(simp add: Dom_pi)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	265	apply(rule_tac p="- p" in permute_boolE)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	266	apply(perm_simp add: permute_minus_cancel)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	267	apply(simp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	268	apply(simp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	269	apply(simp add: ty.supp supp_at_base)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	270	apply(simp add: fresh_star_def)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	271	apply(drule_tac x="atom name" in bspec)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	272	apply(auto)[1]
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	273	apply(simp add: fresh_def supp_perm)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	274	apply(perm_simp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	275	apply(auto)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	276	done
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	277
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	278	nominal_primrec
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	279	generalises :: "ty \<Rightarrow> tys \<Rightarrow> bool" ("_ \<prec>\<prec> _")
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	280	where
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	281	"atom ` (fset Xs) \<sharp>* T \<Longrightarrow>
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	282	T \<prec>\<prec> All [Xs].T' \<longleftrightarrow> (\<exists>\<theta>. T = \<theta><T'> \<and> atom ` Dom \<theta> = atom ` fset Xs \<inter> supp T')"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	283	unfolding generalises_graph_def
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	284	unfolding eqvt_def
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	285	apply(perm_simp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	286	apply(simp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	287	apply(rule TrueI)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	288	apply(case_tac x)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	289	apply(simp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	290	apply(rule_tac y="b" and c="a" in tys.strong_exhaust)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	291	apply(simp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	292	apply(clarify)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	293	apply(simp only: tys.eq_iff map_fset_image)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	294	apply(erule_tac c="Ta" in Abs_res_fcb2)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	295	apply(simp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	296	apply(simp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	297	apply(simp add: fresh_star_def pure_fresh)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	298	apply(simp add: fresh_star_def pure_fresh)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	299	apply(simp add: fresh_star_def pure_fresh)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	300	apply(perm_simp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	301	apply(subst perm_supp_eq)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	302	apply(simp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	303	apply(simp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	304	apply(perm_simp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	305	apply(subst perm_supp_eq)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	306	apply(simp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	307	apply(simp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	308	done
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	309
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	310	termination (eqvt)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	311	by lexicographic_order
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	312
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	313	lemma better:
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	314	"T \<prec>\<prec> All [Xs].T' \<longleftrightarrow> (\<exists>\<theta>. T = \<theta><T'> \<and> atom ` Dom \<theta> = atom ` fset Xs \<inter> supp T')"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	315	using at_set_avoiding3
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	316	apply -
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	317	apply(drule_tac x="atom ` fset Xs" in meta_spec)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	318	apply(drule_tac x="T" in meta_spec)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	319	apply(drule_tac x="All [Xs].T'" in meta_spec)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	320	apply(drule meta_mp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	321	apply(simp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	322	apply(drule meta_mp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	323	apply(simp add: finite_supp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	324	apply(drule meta_mp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	325	apply(simp add: finite_supp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	326	apply(drule_tac meta_mp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	327	apply(simp add: fresh_star_def tys.fresh)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	328	apply(clarify)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	329	apply(rule_tac t="All [Xs].T'" and s="p \<bullet> All [Xs].T'" in subst)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	330	apply(rule supp_perm_eq)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	331	apply(assumption)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	332	apply(perm_simp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	333	apply(subst generalises.simps)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	334	apply(assumption)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	335	apply(rule iffI)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	336	defer
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	337	apply(clarify)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	338	apply(rule_tac x="\<theta>\|p" in exI)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	339	apply(rule conjI)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	340	apply(rule t)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	341	apply(simp add: tys.supp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	342	apply (metis Diff_Int_distrib Int_Diff Int_commute inf_sup_absorb)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	343	apply(simp add: Dom_pi)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	344	apply(rotate_tac 3)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	345	apply(drule_tac p="p" in permute_boolI)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	346	apply(perm_simp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	347	apply(assumption)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	348	apply(clarify)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	349	apply(rule_tac x="\<theta>\|- p" in exI)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	350	apply(rule conjI)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	351	apply(subst t[where p="- p"])
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	352	apply(simp add: tys.supp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	353	apply(rotate_tac 1)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	354	apply(drule_tac p="p" in permute_boolI)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	355	apply(perm_simp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	356	apply(simp add: permute_self)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	357	apply(simp add: fresh_star_def)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	358	apply(simp add: fresh_minus_perm)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	359	apply (metis Diff_Int_distrib Int_Diff Int_commute inf_sup_absorb)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	360	apply(simp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	361	apply(simp add: Dom_pi)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	362	apply(rule_tac p="p" in permute_boolE)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	363	apply(perm_simp add: permute_minus_cancel)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	364	apply(assumption)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	365	done
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	366
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	367
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	368	(* Tests *)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	369
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	370	fun
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	371	compose::"Subst \<Rightarrow> Subst \<Rightarrow> Subst" ("_ \<circ> _" [100,100] 100)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	372	where
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	373	"\<theta>\<^isub>1 \<circ> [] = \<theta>\<^isub>1"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	374	\| "\<theta>\<^isub>1 \<circ> ((X,T)#\<theta>\<^isub>2) = (X,\<theta>\<^isub>1<T>)#(\<theta>\<^isub>1 \<circ> \<theta>\<^isub>2)"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	375
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	376	lemma compose_ty:
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	377	fixes \<theta>1 \<theta>2 :: "Subst"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	378	and T :: "ty"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	379	shows "\<theta>1<\<theta>2<T>> = (\<theta>1\<circ>\<theta>2)<T>"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	380	proof (induct T rule: ty.induct)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	381	case (Var X)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	382	have "\<theta>1<lookup \<theta>2 X> = lookup (\<theta>1\<circ>\<theta>2) X"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	383	by (induct \<theta>2) (auto)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	384	then show ?case by simp
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	385	next
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	386	case (Fun T1 T2)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	387	then show ?case by simp
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	388	qed
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	389
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	390	lemma compose_Dom:
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	391	shows "Dom (\<theta>1 \<circ> \<theta>2) = Dom \<theta>1 \<union> Dom \<theta>2"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	392	apply(induct \<theta>2)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	393	apply(auto)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	394	done
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	395
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	396	lemma t1:
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	397	fixes T::"ty"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	398	and Xs::"name fset"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	399	shows "\<exists>\<theta>. atom ` Dom \<theta> = atom ` fset Xs \<and> \<theta><T> = T"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	400	apply(induct Xs)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	401	apply(rule_tac x="[]" in exI)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	402	apply(simp add: subst_id1)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	403	apply(clarify)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	404	apply(rule_tac x="[(x, Var x)] \<circ> \<theta>" in exI)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	405	apply(simp add: compose_ty[symmetric] subst_id2 compose_Dom)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	406	done
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	407
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	408	nominal_primrec
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	409	ftv :: "ty \<Rightarrow> name fset"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	410	where
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	411	"ftv (Var X) = {\|X\|}"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	412	\| "ftv (T1 \<rightarrow> T2) = (ftv T1) \|\<union>\| (ftv T2)"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	413	unfolding eqvt_def ftv_graph_def
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	414	apply (rule, perm_simp, rule)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	415	apply(rule TrueI)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	416	apply(rule_tac y="x" in ty.exhaust)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	417	apply(blast)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	418	apply(blast)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	419	apply(simp_all)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	420	done
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	421
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	422	termination (eqvt)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	423	by lexicographic_order
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	424
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	425	lemma tt:
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	426	shows "supp T = atom ` fset (ftv T)"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	427	apply(induct T rule: ty.induct)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	428	apply(simp_all add: ty.supp supp_at_base)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	429	apply(auto)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	430	done
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	431
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	432
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	433	lemma t2:
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	434	shows "T \<prec>\<prec> All [Xs].T"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	435	unfolding better
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	436	using t1
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	437	apply -
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	438	apply(drule_tac x="Xs \|\<inter>\| ftv T" in meta_spec)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	439	apply(drule_tac x="T" in meta_spec)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	440	apply(clarify)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	441	apply(rule_tac x="\<theta>" in exI)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	442	apply(simp add: tt)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	443	apply(auto)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	444	done
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	445
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	446	(* HERE *)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	447
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	448	lemma w1:
3104 f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	449	shows "\<theta><\<theta>'\|p> = (\<theta><\<theta>'>)\|p"
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	450	by (induct \<theta>')(auto)
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	451
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	452	(*
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	453	lemma w2:
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	454	assumes "name \|\<in>\| Dom \<theta>'"
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	455	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	456	using assms
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	457	apply(induct \<theta>')
3104 f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	458	apply(auto simp add: notin_empty_fset)
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	459	done
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	460
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	461	lemma w3:
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	462	assumes "name \|\<in>\| Dom \<theta>"
3104 f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	463	shows "lookup \<theta> name = lookup (\<theta>\|p) (p \<bullet> name)"
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	464	using assms
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	465	apply(induct \<theta>)
3104 f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	466	apply(auto simp add: notin_empty_fset)
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	467	done
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	468
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	469	lemma fresh_lookup:
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	470	fixes X Y::"name"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	471	and \<theta>::"Subst"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	472	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	473	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	474	using assms
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	475	apply (induct \<theta>)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	476	apply (auto simp add: fresh_Cons fresh_Pair fresh_at_base ty.fresh)
3104 f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	477	done
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	478
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	479	lemma test:
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	480	fixes \<theta> \<theta>'::"Subst"
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	481	and T::"ty"
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	482	assumes "(p \<bullet> atom ` fset (Dom \<theta>')) \<sharp>* \<theta>" "supp All [Dom \<theta>'].T \<sharp>* p"
3104 f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	483	shows "\<theta><\<theta>'<T>> = \<theta><\<theta>'\|p><\<theta><p \<bullet> T>>"
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	484	using assms
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	485	apply(induct T rule: ty.induct)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	486	defer
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	487	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	488	apply(auto simp add: tys.supp ty.supp fresh_star_def supp_at_base)[1]
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	489	apply(case_tac "name \|\<in>\| Dom \<theta>'")
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	490	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	491	apply(subst (2) lookup_fresh)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	492	apply(perm_simp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	493	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	494	apply(simp)
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	495	apply(simp add: w1)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	496	apply(simp add: w2)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	497	apply(subst w3[symmetric])
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	498	apply(simp add: Dom_subst)
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	499	apply(simp)
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	500	apply(perm_simp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	501	apply(rotate_tac 2)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	502	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	503	apply(perm_simp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	504	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	505	apply(metis notin_fset)
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	506	apply(simp add: lookup_Dom)
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	507	apply(perm_simp)
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	508	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	509	apply(auto)[1]
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	510	apply(rule fresh_lookup)
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	511	apply(simp add: Dom_subst)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	512	apply(simp add: Dom_pi)
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	513	apply(perm_simp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	514	apply(rotate_tac 2)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	515	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	516	apply(perm_simp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	517	apply(simp add: fresh_at_base)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	518	apply (metis in_fset)
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	519	apply(simp add: Dom_subst)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	520	apply(simp add: Dom_pi[symmetric])
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	521	apply(perm_simp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	522	apply(subst supp_perm_eq)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	523	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	524	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	525	apply(simp)
3102 5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	526	done
5b5ade6bc889 added definition for generalisation of type schemes (for paper) Christian Urban <urbanc@in.tum.de> parents: 3100 diff changeset	527
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	528	lemma generalises_subst:
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	529	shows "T \<prec>\<prec> All [Xs].T' \<Longrightarrow> \<theta><T> \<prec>\<prec> \<theta><All [Xs].T'>"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	530	using at_set_avoiding3
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	531	apply -
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	532	apply(drule_tac x="fset (map_fset atom Xs)" in meta_spec)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	533	apply(drule_tac x="\<theta>" in meta_spec)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	534	apply(drule_tac x="All [Xs].T'" in meta_spec)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	535	apply(drule meta_mp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	536	apply(simp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	537	apply(drule meta_mp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	538	apply(simp add: finite_supp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	539	apply(drule meta_mp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	540	apply(simp add: finite_supp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	541	apply(drule meta_mp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	542	apply(simp add: tys.fresh fresh_star_def)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	543	apply(erule exE)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	544	apply(erule conjE)+
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	545	apply(rule_tac t="All[Xs].T'" and s="p \<bullet> (All [Xs].T')" in subst)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	546	apply(rule supp_perm_eq)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	547	apply(assumption)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	548	apply(perm_simp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	549	apply(subst substs.simps)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	550	apply(simp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	551	apply(simp add: better)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	552	apply(erule exE)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	553	apply(simp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	554	apply(rule_tac x="\<theta><\<theta>'\|p>" in exI)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	555	apply(rule conjI)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	556	apply(rule test)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	557	apply(simp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	558	apply(perm_simp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	559	apply(simp add: fresh_star_def)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	560	apply(auto)[1]
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	561	apply(simp add: tys.supp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	562	apply(simp add: fresh_star_def)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	563	apply(auto)[1]
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	564	oops
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	565
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	566	lemma generalises_subst:
3104 f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	567	shows "T \<prec>\<prec> S \<Longrightarrow> \<theta><T> \<prec>\<prec> \<theta><S>"
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	568	unfolding generalises_def
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	569	apply(erule exE)+
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	570	apply(erule conjE)+
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	571	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	572	apply(simp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	573	using at_set_avoiding3
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	574	apply -
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	575	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	576	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	577	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	578	apply(drule meta_mp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	579	apply(simp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	580	apply(drule meta_mp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	581	apply(simp add: finite_supp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	582	apply(drule meta_mp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	583	apply(simp add: finite_supp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	584	apply(drule meta_mp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	585	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	586	apply(erule exE)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	587	apply(erule conjE)+
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	588	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	589	apply(rule supp_perm_eq)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	590	apply(assumption)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	591	apply(perm_simp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	592	apply(subst substs.simps)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	593	apply(perm_simp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	594	apply(simp)
3104 f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	595	apply(rule_tac x="\<theta><\<theta>'\|p>" in exI)
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	596	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	597	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	598	apply(rule conjI)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	599	apply(simp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	600	apply(rule conjI)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	601	defer
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	602	apply(simp add: Dom_subst)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	603	apply(simp add: Dom_pi Dom_eqvt[symmetric])
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	604	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	605	apply(simp)
3104 f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	606	apply(simp)
3103 9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	607	apply(rule test)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	608	apply(perm_simp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	609	apply(rotate_tac 2)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	610	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	611	apply(perm_simp)
9a63d90d1752 proved that generalisation is closed under substitution Christian Urban <urbanc@in.tum.de> parents: 3102 diff changeset	612	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	613	done
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	614
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	615
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	616	lemma r:
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	617	"A - (B \<inter> A) = A - B"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	618	by (metis Diff_Int Diff_cancel sup_bot_right)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	619
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	620
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	621	lemma t3:
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	622	"T \<prec>\<prec> All [Xs].T' \<longleftrightarrow> (\<exists>\<theta>. T = \<theta><T'> \<and> Dom \<theta> = Xs)"
3104 f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	623	apply(auto)
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	624	defer
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	625	apply(simp add: generalises_def)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	626	apply(auto)[1]
3104 f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	627	unfolding generalises_def
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	628	apply(auto)[1]
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	629	apply(simp add: Abs_eq_res_set)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	630	apply(simp add: Abs_eq_iff2)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	631	apply(simp add: alphas)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	632	apply(perm_simp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	633	apply(clarify)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	634	apply(simp add: r)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	635	apply(drule sym)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	636	apply(simp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	637	apply(rule_tac x="\<theta>\|p" in exI)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	638	sorry
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	639
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	640	definition
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	641	generalises_tys :: "tys \<Rightarrow> tys \<Rightarrow> bool" ("_ \<prec>\<prec> _")
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	642	where
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	643	"S1 \<prec>\<prec> S2 = (\<forall>T::ty. T \<prec>\<prec> S1 \<longrightarrow> T \<prec>\<prec> S2)"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	644
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	645	lemma
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	646	"All [Xs1].T1 \<prec>\<prec> All [Xs2].T2
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	647	\<longleftrightarrow> (\<exists>\<theta>. Dom \<theta> = Xs2 \<and> T1 = \<theta><T2> \<and> (\<forall>X \<in> fset Xs1. atom X \<sharp> All [Xs2].T2))"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	648	apply(rule iffI)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	649	apply(simp add: generalises_tys_def)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	650	apply(drule_tac x="T1" in spec)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	651	apply(drule mp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	652	apply(rule t2)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	653	apply(simp add: t3)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	654	apply(clarify)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	655	apply(rule_tac x="\<theta>" in exI)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	656	apply(simp)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	657	apply(rule ballI)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	658	defer
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	659	apply(simp add: generalises_tys_def)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	660	apply(clarify)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	661	apply(simp add: t3)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	662	apply(clarify)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	663
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	664
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	665
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	666	lemma
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	667	"T \<prec>\<prec> All [Xs].T' \<longleftrightarrow> (\<exists>\<theta>. T = \<theta><T'> \<and> Dom \<theta> = Xs)"
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	668	apply(auto)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	669	defer
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	670	apply(simp add: generalises_def)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	671	apply(auto)[1]
3104 f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	672	apply(auto)[1]
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	673	apply(drule sym)
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	674	apply(simp add: Abs_eq_iff2)
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	675	apply(simp add: alphas)
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	676	apply(auto)
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	677	apply(rule_tac x="map (\<lambda>(X, T). (p \<bullet> X, T)) \<theta>" in exI)
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	678	apply(auto)
f7c4b8e6918b updated to explicit set type constructor (post Isabelle 3rd January) Christian Urban <urbanc@in.tum.de> parents: 3103 diff changeset	679	oops
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	680
3109 d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	681	*)
d79e936e30ea commented out parts of TypeScheme1 in order to run all tests Christian Urban <urbanc@in.tum.de> parents: 3104 diff changeset	682
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	683	end

author	Christian Urban <urbanc@in.tum.de>
	Mon, 16 Jan 2012 13:53:35 +0000
changeset 3109	d79e936e30ea
parent 3104	f7c4b8e6918b
child 3183	313e6f2cdd89
permissions	-rw-r--r--