nominal2: Nominal/Ex/TypeSchemes1.thy@8779fb01d8b4 (annotated)

3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	1	theory TypeSchemes1
2454 9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2451 diff changeset	2	imports "../Nominal2"
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	begin
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	4
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	5	section {* Type Schemes defined as two separate nominal datatypes *}
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	6
2556 8ed62410236e added a test about subtyping; disabled two tests, because of problem with function package Christian Urban <urbanc@in.tum.de> parents: 2524 diff changeset	7	atom_decl name
8ed62410236e added a test about subtyping; disabled two tests, because of problem with function package Christian Urban <urbanc@in.tum.de> parents: 2524 diff changeset	8
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	9	nominal_datatype ty =
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	10	Var "name"
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	11	\| Fun "ty" "ty"
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 =
2950 0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2886 diff changeset	14	All xs::"name fset" ty::"ty" binds (set+) xs in ty
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
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	29
2707 747ebf2f066d made eqvt-proof explicit in the function definitions Christian Urban <urbanc@in.tum.de> parents: 2676 diff changeset	30	fun
747ebf2f066d made eqvt-proof explicit in the function definitions Christian Urban <urbanc@in.tum.de> parents: 2676 diff changeset	31	lookup :: "(name \<times> ty) list \<Rightarrow> name \<Rightarrow> ty"
747ebf2f066d made eqvt-proof explicit in the function definitions Christian Urban <urbanc@in.tum.de> parents: 2676 diff changeset	32	where
747ebf2f066d made eqvt-proof explicit in the function definitions Christian Urban <urbanc@in.tum.de> parents: 2676 diff changeset	33	"lookup [] Y = Var Y"
747ebf2f066d made eqvt-proof explicit in the function definitions Christian Urban <urbanc@in.tum.de> parents: 2676 diff changeset	34	\| "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	35
747ebf2f066d made eqvt-proof explicit in the function definitions Christian Urban <urbanc@in.tum.de> parents: 2676 diff changeset	36	lemma lookup_eqvt[eqvt]:
747ebf2f066d made eqvt-proof explicit in the function definitions Christian Urban <urbanc@in.tum.de> parents: 2676 diff changeset	37	shows "(p \<bullet> lookup Ts T) = lookup (p \<bullet> Ts) (p \<bullet> T)"
747ebf2f066d made eqvt-proof explicit in the function definitions Christian Urban <urbanc@in.tum.de> parents: 2676 diff changeset	38	apply(induct Ts T rule: lookup.induct)
747ebf2f066d made eqvt-proof explicit in the function definitions Christian Urban <urbanc@in.tum.de> parents: 2676 diff changeset	39	apply(simp_all)
747ebf2f066d made eqvt-proof explicit in the function definitions Christian Urban <urbanc@in.tum.de> parents: 2676 diff changeset	40	done
747ebf2f066d made eqvt-proof explicit in the function definitions Christian Urban <urbanc@in.tum.de> parents: 2676 diff changeset	41
2981 c8acaded1777 temporary fix Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	42
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	43	nominal_primrec
8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	44	subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"
2838 36544bac1659 More experiments with 'default' Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2836 diff changeset	45	where
36544bac1659 More experiments with 'default' Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2836 diff changeset	46	"subst \<theta> (Var X) = lookup \<theta> X"
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	47	\| "subst \<theta> (Fun T1 T) = Fun (subst \<theta> T1) (subst \<theta> T)"
8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	48	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	49	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	50	apply(rule TrueI)
2801 5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	51	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	52	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	53	apply(blast)
5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	54	apply(blast)
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	55	apply(simp_all)
2801 5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	56	done
2676 028d5511c15f some tryes about substitution over type-schemes Christian Urban <urbanc@in.tum.de> parents: 2634 diff changeset	57
2973 d1038e67923a added a flag (eqvt) to termination proofs arising fron nominal_primrecs Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	58	termination (eqvt)
2859 2eeb75cccb8d all tests work again Christian Urban <urbanc@in.tum.de> parents: 2850 diff changeset	59	by lexicographic_order
2676 028d5511c15f some tryes about substitution over type-schemes Christian Urban <urbanc@in.tum.de> parents: 2634 diff changeset	60
028d5511c15f some tryes about substitution over type-schemes Christian Urban <urbanc@in.tum.de> parents: 2634 diff changeset	61
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	62	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	63	assumes e: "eqvt f"
5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	64	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	65	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	66	by blast
5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	67
5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	68	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	69	"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	70	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	71	unfolding eqvt_def
8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	72	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	73
5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	74	lemma fresh_star_inter1:
5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	75	"xs \<sharp>* z \<Longrightarrow> (xs \<inter> ys) \<sharp>* z"
5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	76	unfolding fresh_star_def by blast
2830 297cff1d1048 FCB for res binding and simplified proof of subst for type schemes Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2822 diff changeset	77
2676 028d5511c15f some tryes about substitution over type-schemes Christian Urban <urbanc@in.tum.de> parents: 2634 diff changeset	78	nominal_primrec
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	79	substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"
2676 028d5511c15f some tryes about substitution over type-schemes Christian Urban <urbanc@in.tum.de> parents: 2634 diff changeset	80	where
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	81	"fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs t) = All xs (subst \<theta> t)"
8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	82	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	83	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	84	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	85	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	86	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	87	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	88	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	89	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	90	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	91	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	92	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	93	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	94	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	95	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	96	apply(auto simp add: fresh_star_def fresh_def)[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	97	apply(subgoal_tac "x \<in> supp t")
4a00077c008f completed the eqvt-proofs for functions; they are stored under the name function_name.eqvt and added to the eqvt-list Christian Urban <urbanc@in.tum.de> parents: 2981 diff changeset	98	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	99	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	100	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	101	apply(blast)
2832 76db0b854bf6 Simpler proof of TypeSchemes/substs Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2831 diff changeset	102	apply clarify
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	103	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	104	apply (subst Abs_eq_iff)
5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	105	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	106	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	107	apply (simp add: alphas fresh_star_zero)
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	108	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	109	apply blast
2839 bcf48a1cb24b abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2838 diff changeset	110	apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> t)")
bcf48a1cb24b abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2838 diff changeset	111	apply (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	112	apply auto[1]
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	113	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	114	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	115	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	116	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	117	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	118	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	119	apply (simp add: supp_Pair)
2832 76db0b854bf6 Simpler proof of TypeSchemes/substs Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2831 diff changeset	120	apply (rule perm_supp_eq)
76db0b854bf6 Simpler proof of TypeSchemes/substs Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2831 diff changeset	121	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	122	apply blast
5ecb857e9de7 proved subst for All constructor in type schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2787 diff changeset	123	done
2676 028d5511c15f some tryes about substitution over type-schemes Christian Urban <urbanc@in.tum.de> parents: 2634 diff changeset	124
028d5511c15f some tryes about substitution over type-schemes Christian Urban <urbanc@in.tum.de> parents: 2634 diff changeset	125	text {* Some Tests about Alpha-Equality *}
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	126
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	127	lemma
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	128	shows "All {\|a, b\|} (Fun (Var a) (Var b)) = All {\|b, a\|} (Fun (Var a) (Var b))"
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	129	apply(simp add: Abs_eq_iff)
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	130	apply(rule_tac x="0::perm" in exI)
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	131	apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	132	done
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	133
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	134	lemma
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	135	shows "All {\|a, b\|} (Fun (Var a) (Var b)) = All {\|a, b\|} (Fun (Var b) (Var a))"
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	136	apply(simp add: Abs_eq_iff)
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	137	apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	138	apply(simp add: alphas fresh_star_def supp_at_base ty.supp)
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	139	done
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	140
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	141	lemma
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	142	shows "All {\|a, b, c\|} (Fun (Var a) (Var b)) = All {\|a, b\|} (Fun (Var a) (Var b))"
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: Abs_eq_iff)
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	144	apply(rule_tac x="0::perm" in exI)
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	145	apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	146	done
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	147
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	148	lemma
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	149	assumes a: "a \<noteq> b"
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	150	shows "\<not>(All {\|a, b\|} (Fun (Var a) (Var b)) = All {\|c\|} (Fun (Var c) (Var c)))"
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	151	using a
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	152	apply(simp add: Abs_eq_iff)
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	153	apply(clarify)
3100 8779fb01d8b4 separated the two versions of type schemes into two files Christian Urban <urbanc@in.tum.de> parents: 2982 diff changeset	154	apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	155	apply auto
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	156	done
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	157
2566 a59d8e1e3a17 moved rest of the lemmas from Nominal2_FSet to the TypeScheme example Christian Urban <urbanc@in.tum.de> parents: 2556 diff changeset	158
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	159
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	160
e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: diff changeset	161	end

author	Christian Urban <urbanc@in.tum.de>
	Thu, 29 Dec 2011 15:56:54 +0000
changeset 3100	8779fb01d8b4
parent 2982	Nominal/Ex/TypeSchemes.thy@4a00077c008f
child 3102	5b5ade6bc889
permissions	-rw-r--r--