nominal2: Quot/Nominal/LFex.thy@c74c8ba46db7 (annotated)

985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	1	theory LFex
1219 c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	2	imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv"
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	3	begin
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	4
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	5	atom_decl name
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	6	atom_decl ident
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	7
992 74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	8	datatype kind =
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	9	Type
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	10	\| KPi "ty" "name" "kind"
992 74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	11	and ty =
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	12	TConst "ident"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	13	\| TApp "ty" "trm"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	14	\| TPi "ty" "name" "ty"
992 74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	15	and trm =
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	16	Const "ident"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	17	\| Var "name"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	18	\| App "trm" "trm"
992 74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	19	\| Lam "ty" "name" "trm"
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	20
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	21	instantiation kind and ty and trm :: pt
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	22	begin
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	23
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	24	primrec
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	25	permute_kind
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	26	and permute_ty
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	27	and permute_trm
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	28	where
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	29	"permute_kind pi Type = Type"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	30	\| "permute_kind pi (KPi t n k) = KPi (permute_ty pi t) (pi \<bullet> n) (permute_kind pi k)"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	31	\| "permute_ty pi (TConst i) = TConst (pi \<bullet> i)"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	32	\| "permute_ty pi (TApp A M) = TApp (permute_ty pi A) (permute_trm pi M)"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	33	\| "permute_ty pi (TPi A x B) = TPi (permute_ty pi A) (pi \<bullet> x) (permute_ty pi B)"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	34	\| "permute_trm pi (Const i) = Const (pi \<bullet> i)"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	35	\| "permute_trm pi (Var x) = Var (pi \<bullet> x)"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	36	\| "permute_trm pi (App M N) = App (permute_trm pi M) (permute_trm pi N)"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	37	\| "permute_trm pi (Lam A x M) = Lam (permute_ty pi A) (pi \<bullet> x) (permute_trm pi M)"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	38
1022 cc5830c452c4 With induct instead of induct_tac, just one induction is sufficient. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1021 diff changeset	39	lemma rperm_zero_ok:
cc5830c452c4 With induct instead of induct_tac, just one induction is sufficient. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1021 diff changeset	40	"0 \<bullet> (x :: kind) = x"
cc5830c452c4 With induct instead of induct_tac, just one induction is sufficient. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1021 diff changeset	41	"0 \<bullet> (y :: ty) = y"
cc5830c452c4 With induct instead of induct_tac, just one induction is sufficient. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1021 diff changeset	42	"0 \<bullet> (z :: trm) = z"
cc5830c452c4 With induct instead of induct_tac, just one induction is sufficient. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1021 diff changeset	43	apply(induct x and y and z rule: kind_ty_trm.inducts)
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	44	apply(simp_all)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	45	done
1022 cc5830c452c4 With induct instead of induct_tac, just one induction is sufficient. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1021 diff changeset	46
cc5830c452c4 With induct instead of induct_tac, just one induction is sufficient. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1021 diff changeset	47	lemma rperm_plus_ok:
cc5830c452c4 With induct instead of induct_tac, just one induction is sufficient. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1021 diff changeset	48	"(p + q) \<bullet> (x :: kind) = p \<bullet> q \<bullet> x"
cc5830c452c4 With induct instead of induct_tac, just one induction is sufficient. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1021 diff changeset	49	"(p + q) \<bullet> (y :: ty) = p \<bullet> q \<bullet> y"
cc5830c452c4 With induct instead of induct_tac, just one induction is sufficient. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1021 diff changeset	50	"(p + q) \<bullet> (z :: trm) = p \<bullet> q \<bullet> z"
cc5830c452c4 With induct instead of induct_tac, just one induction is sufficient. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1021 diff changeset	51	apply(induct x and y and z rule: kind_ty_trm.inducts)
cc5830c452c4 With induct instead of induct_tac, just one induction is sufficient. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1021 diff changeset	52	apply(simp_all)
cc5830c452c4 With induct instead of induct_tac, just one induction is sufficient. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1021 diff changeset	53	done
cc5830c452c4 With induct instead of induct_tac, just one induction is sufficient. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1021 diff changeset	54
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	55	instance
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	56	apply default
1022 cc5830c452c4 With induct instead of induct_tac, just one induction is sufficient. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1021 diff changeset	57	apply (simp_all only:rperm_zero_ok rperm_plus_ok)
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	58	done
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	59
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	60	end
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	61
1219 c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	62	(*
c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	63	setup {* snd o define_raw_perms ["kind", "ty", "trm"] ["LFex.kind", "LFex.ty", "LFex.trm"] *}
c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	64	local_setup {*
c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	65	snd o define_fv_alpha "LFex.kind"
c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	66	[[ [], [[], [(NONE, 1)], [(NONE, 1)]] ],
c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	67	[ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ],
c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	68	[ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	69	notation
c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	70	alpha_kind ("_ \<approx>ki _" [100, 100] 100)
c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	71	and alpha_ty ("_ \<approx>ty _" [100, 100] 100)
c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	72	and alpha_trm ("_ \<approx>tr _" [100, 100] 100)
c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	73	thm fv_kind_fv_ty_fv_trm.simps alpha_kind_alpha_ty_alpha_trm.intros
c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	74	local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alphas_inj}, []), (build_alpha_inj @{thms alpha_kind_alpha_ty_alpha_trm.intros} @{thms kind.distinct ty.distinct trm.distinct kind.inject ty.inject trm.inject} @{thms alpha_kind.cases alpha_ty.cases alpha_trm.cases} ctxt)) ctxt)) *}
c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	75	thm alphas_inj
c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	76
c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	77	lemma alphas_eqvt:
c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	78	"t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)"
c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	79	"t2 \<approx>ty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>ty (pi \<bullet> s2)"
c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	80	"t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)"
c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	81	sorry
c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	82
c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	83	local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alphas_equivp}, []),
c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	84	(build_equivps [@{term alpha_kind}, @{term alpha_ty}, @{term alpha_trm}]
c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	85	@{thm kind_ty_trm.induct} @{thm alpha_kind_alpha_ty_alpha_trm.induct}
c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	86	@{thms kind.inject ty.inject trm.inject} @{thms alphas_inj}
c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	87	@{thms kind.distinct ty.distinct trm.distinct}
c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	88	@{thms alpha_kind.cases alpha_ty.cases alpha_trm.cases}
c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	89	@{thms alphas_eqvt} ctxt)) ctxt)) *}
c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	90	thm alphas_equivp
c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	91	*)
c74c8ba46db7 All works in LF but will require renaming. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1218 diff changeset	92
1218 2bbfbc9a81fc Reordering in LF. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1210 diff changeset	93	primrec
2bbfbc9a81fc Reordering in LF. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1210 diff changeset	94	rfv_kind :: "kind \<Rightarrow> atom set"
2bbfbc9a81fc Reordering in LF. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1210 diff changeset	95	and rfv_ty :: "ty \<Rightarrow> atom set"
2bbfbc9a81fc Reordering in LF. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1210 diff changeset	96	and rfv_trm :: "trm \<Rightarrow> atom set"
2bbfbc9a81fc Reordering in LF. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1210 diff changeset	97	where
2bbfbc9a81fc Reordering in LF. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1210 diff changeset	98	"rfv_kind (Type) = {}"
2bbfbc9a81fc Reordering in LF. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1210 diff changeset	99	\| "rfv_kind (KPi A x K) = (rfv_ty A) \<union> ((rfv_kind K) - {atom x})"
2bbfbc9a81fc Reordering in LF. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1210 diff changeset	100	\| "rfv_ty (TConst i) = {atom i}"
2bbfbc9a81fc Reordering in LF. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1210 diff changeset	101	\| "rfv_ty (TApp A M) = (rfv_ty A) \<union> (rfv_trm M)"
2bbfbc9a81fc Reordering in LF. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1210 diff changeset	102	\| "rfv_ty (TPi A x B) = (rfv_ty A) \<union> ((rfv_ty B) - {atom x})"
2bbfbc9a81fc Reordering in LF. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1210 diff changeset	103	\| "rfv_trm (Const i) = {atom i}"
2bbfbc9a81fc Reordering in LF. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1210 diff changeset	104	\| "rfv_trm (Var x) = {atom x}"
2bbfbc9a81fc Reordering in LF. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1210 diff changeset	105	\| "rfv_trm (App M N) = (rfv_trm M) \<union> (rfv_trm N)"
2bbfbc9a81fc Reordering in LF. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1210 diff changeset	106	\| "rfv_trm (Lam A x M) = (rfv_ty A) \<union> ((rfv_trm M) - {atom x})"
2bbfbc9a81fc Reordering in LF. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1210 diff changeset	107
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	108	inductive
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	109	akind :: "kind \<Rightarrow> kind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	110	and aty :: "ty \<Rightarrow> ty \<Rightarrow> bool" ("_ \<approx>ty _" [100, 100] 100)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	111	and atrm :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<approx>tr _" [100, 100] 100)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	112	where
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	113	a1: "(Type) \<approx>ki (Type)"
1027 163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	114	\| a2: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (({atom a}, K) \<approx>gen akind rfv_kind pi ({atom b}, K'))\<rbrakk> \<Longrightarrow> (KPi A a K) \<approx>ki (KPi A' b K')"
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	115	\| a3: "i = j \<Longrightarrow> (TConst i) \<approx>ty (TConst j)"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	116	\| a4: "\<lbrakk>A \<approx>ty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (TApp A M) \<approx>ty (TApp A' M')"
1027 163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	117	\| a5: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (({atom a}, B) \<approx>gen aty rfv_ty pi ({atom b}, B'))\<rbrakk> \<Longrightarrow> (TPi A a B) \<approx>ty (TPi A' b B')"
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	118	\| a6: "i = j \<Longrightarrow> (Const i) \<approx>tr (Const j)"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	119	\| a7: "x = y \<Longrightarrow> (Var x) \<approx>tr (Var y)"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	120	\| a8: "\<lbrakk>M \<approx>tr M'; N \<approx>tr N'\<rbrakk> \<Longrightarrow> (App M N) \<approx>tr (App M' N')"
1027 163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	121	\| a9: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (({atom a}, M) \<approx>gen atrm rfv_trm pi ({atom b}, M'))\<rbrakk> \<Longrightarrow> (Lam A a M) \<approx>tr (Lam A' b M')"
991 928e80edf138 Added the experiments with fun and function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 985 diff changeset	122
994 333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	123	lemma akind_aty_atrm_inj:
992 74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	124	"(Type) \<approx>ki (Type) = True"
1027 163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	125	"((KPi A a K) \<approx>ki (KPi A' b K')) = ((A \<approx>ty A') \<and> (\<exists>pi. ({atom a}, K) \<approx>gen akind rfv_kind pi ({atom b}, K')))"
992 74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	126	"(TConst i) \<approx>ty (TConst j) = (i = j)"
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	127	"(TApp A M) \<approx>ty (TApp A' M') = (A \<approx>ty A' \<and> M \<approx>tr M')"
1027 163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	128	"((TPi A a B) \<approx>ty (TPi A' b B')) = ((A \<approx>ty A') \<and> (\<exists>pi. (({atom a}, B) \<approx>gen aty rfv_ty pi ({atom b}, B'))))"
992 74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	129	"(Const i) \<approx>tr (Const j) = (i = j)"
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	130	"(Var x) \<approx>tr (Var y) = (x = y)"
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	131	"(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')"
1027 163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	132	"((Lam A a M) \<approx>tr (Lam A' b M')) = ((A \<approx>ty A') \<and> (\<exists>pi. (({atom a}, M) \<approx>gen atrm rfv_trm pi ({atom b}, M'))))"
992 74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	133	apply -
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	134	apply (simp add: akind_aty_atrm.intros)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	135
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	136	apply rule apply (erule akind.cases) apply simp apply blast
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	137	apply (simp only: akind_aty_atrm.intros)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	138
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	139	apply rule apply (erule aty.cases) apply simp apply simp apply simp
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	140	apply (simp only: akind_aty_atrm.intros)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	141
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	142	apply rule apply (erule aty.cases) apply simp apply simp apply simp
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	143	apply (simp only: akind_aty_atrm.intros)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	144
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	145	apply rule apply (erule aty.cases) apply simp apply simp apply blast
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	146	apply (simp only: akind_aty_atrm.intros)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	147
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	148	apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	149	apply (simp only: akind_aty_atrm.intros)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	150
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	151	apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	152	apply (simp only: akind_aty_atrm.intros)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	153
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	154	apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	155	apply (simp only: akind_aty_atrm.intros)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	156
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	157	apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	158	apply (simp only: akind_aty_atrm.intros)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	159	done
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	160
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	161	lemma rfv_eqvt[eqvt]:
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	162	"((pi\<bullet>rfv_kind t1) = rfv_kind (pi\<bullet>t1))"
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	163	"((pi\<bullet>rfv_ty t2) = rfv_ty (pi\<bullet>t2))"
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	164	"((pi\<bullet>rfv_trm t3) = rfv_trm (pi\<bullet>t3))"
993 5c0d9a507bcb Fixed the induction problem + some more proofs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 992 diff changeset	165	apply(induct t1 and t2 and t3 rule: kind_ty_trm.inducts)
5c0d9a507bcb Fixed the induction problem + some more proofs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 992 diff changeset	166	apply(simp_all add: union_eqvt Diff_eqvt)
5c0d9a507bcb Fixed the induction problem + some more proofs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 992 diff changeset	167	apply(simp_all add: permute_set_eq atom_eqvt)
992 74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	168	done
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	169
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	170	lemma alpha_eqvt:
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	171	"t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)"
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	172	"t2 \<approx>ty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>ty (pi \<bullet> s2)"
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	173	"t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)"
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	174	apply(induct rule: akind_aty_atrm.inducts)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	175	apply (simp_all add: akind_aty_atrm.intros)
1027 163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	176	apply (simp_all add: akind_aty_atrm_inj)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	177	apply (rule alpha_gen_atom_eqvt)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	178	apply (simp add: rfv_eqvt)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	179	apply assumption
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	180	apply (rule alpha_gen_atom_eqvt)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	181	apply (simp add: rfv_eqvt)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	182	apply assumption
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	183	apply (rule alpha_gen_atom_eqvt)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	184	apply (simp add: rfv_eqvt)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	185	apply assumption
992 74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	186	done
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	187
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	188	lemma al_refl:
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	189	fixes K::"kind"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	190	and A::"ty"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	191	and M::"trm"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	192	shows "K \<approx>ki K"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	193	and "A \<approx>ty A"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	194	and "M \<approx>tr M"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	195	apply(induct K and A and M rule: kind_ty_trm.inducts)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	196	apply(auto intro: akind_aty_atrm.intros)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	197	apply (rule a2)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	198	apply auto
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	199	apply(rule_tac x="0" in exI)
1027 163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	200	apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	201	apply (rule a5)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	202	apply auto
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	203	apply(rule_tac x="0" in exI)
1027 163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	204	apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	205	apply (rule a9)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	206	apply auto
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	207	apply(rule_tac x="0" in exI)
1027 163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	208	apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	209	done
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	210
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	211	lemma al_sym:
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	212	fixes K K'::"kind" and A A'::"ty" and M M'::"trm"
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	213	shows "K \<approx>ki K' \<Longrightarrow> K' \<approx>ki K"
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	214	and "A \<approx>ty A' \<Longrightarrow> A' \<approx>ty A"
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	215	and "M \<approx>tr M' \<Longrightarrow> M' \<approx>tr M"
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	216	apply(induct K K' and A A' and M M' rule: akind_aty_atrm.inducts)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	217	apply(simp_all add: akind_aty_atrm.intros)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	218	apply (simp_all add: akind_aty_atrm_inj)
1210 10a0e3578507 Generalize atom_trans and atom_sym. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1139 diff changeset	219	apply(erule alpha_gen_compose_sym)
10a0e3578507 Generalize atom_trans and atom_sym. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1139 diff changeset	220	apply(erule alpha_eqvt)
10a0e3578507 Generalize atom_trans and atom_sym. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1139 diff changeset	221	apply(erule alpha_gen_compose_sym)
10a0e3578507 Generalize atom_trans and atom_sym. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1139 diff changeset	222	apply(erule alpha_eqvt)
10a0e3578507 Generalize atom_trans and atom_sym. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1139 diff changeset	223	apply(erule alpha_gen_compose_sym)
10a0e3578507 Generalize atom_trans and atom_sym. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1139 diff changeset	224	apply(erule alpha_eqvt)
1027 163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	225	done
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	226
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	227	lemma al_trans:
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	228	fixes K K' K''::"kind" and A A' A''::"ty" and M M' M''::"trm"
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	229	shows "K \<approx>ki K' \<Longrightarrow> K' \<approx>ki K'' \<Longrightarrow> K \<approx>ki K''"
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	230	and "A \<approx>ty A' \<Longrightarrow> A' \<approx>ty A'' \<Longrightarrow> A \<approx>ty A''"
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	231	and "M \<approx>tr M' \<Longrightarrow> M' \<approx>tr M'' \<Longrightarrow> M \<approx>tr M''"
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	232	apply(induct K K' and A A' and M M' arbitrary: K'' and A'' and M'' rule: akind_aty_atrm.inducts)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	233	apply(simp_all add: akind_aty_atrm.intros)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	234	apply(erule akind.cases)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	235	apply(simp_all add: akind_aty_atrm.intros)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	236	apply(simp add: akind_aty_atrm_inj)
1210 10a0e3578507 Generalize atom_trans and atom_sym. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1139 diff changeset	237	apply(erule alpha_gen_compose_trans)
10a0e3578507 Generalize atom_trans and atom_sym. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1139 diff changeset	238	apply(assumption)
10a0e3578507 Generalize atom_trans and atom_sym. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1139 diff changeset	239	apply(erule alpha_eqvt)
1027 163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	240	apply(rotate_tac 4)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	241	apply(erule aty.cases)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	242	apply(simp_all add: akind_aty_atrm.intros)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	243	apply(rotate_tac 3)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	244	apply(erule aty.cases)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	245	apply(simp_all add: akind_aty_atrm.intros)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	246	apply(simp add: akind_aty_atrm_inj)
1210 10a0e3578507 Generalize atom_trans and atom_sym. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1139 diff changeset	247	apply(erule alpha_gen_compose_trans)
10a0e3578507 Generalize atom_trans and atom_sym. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1139 diff changeset	248	apply(assumption)
10a0e3578507 Generalize atom_trans and atom_sym. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1139 diff changeset	249	apply(erule alpha_eqvt)
1027 163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	250	apply(rotate_tac 4)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	251	apply(erule atrm.cases)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	252	apply(simp_all add: akind_aty_atrm.intros)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	253	apply(rotate_tac 3)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	254	apply(erule atrm.cases)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	255	apply(simp_all add: akind_aty_atrm.intros)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	256	apply(simp add: akind_aty_atrm_inj)
1210 10a0e3578507 Generalize atom_trans and atom_sym. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1139 diff changeset	257	apply(erule alpha_gen_compose_trans)
10a0e3578507 Generalize atom_trans and atom_sym. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1139 diff changeset	258	apply(assumption)
10a0e3578507 Generalize atom_trans and atom_sym. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1139 diff changeset	259	apply(erule alpha_eqvt)
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	260	done
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	261
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	262	lemma alpha_equivps:
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	263	shows "equivp akind"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	264	and "equivp aty"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	265	and "equivp atrm"
1027 163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	266	apply(rule equivpI)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	267	unfolding reflp_def symp_def transp_def
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	268	apply(auto intro: al_refl al_sym al_trans)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	269	apply(rule equivpI)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	270	unfolding reflp_def symp_def transp_def
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	271	apply(auto intro: al_refl al_sym al_trans)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	272	apply(rule equivpI)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	273	unfolding reflp_def symp_def transp_def
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	274	apply(auto intro: al_refl al_sym al_trans)
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	275	done
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	276
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	277	quotient_type KIND = kind / akind
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	278	by (rule alpha_equivps)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	279
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	280	quotient_type
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	281	TY = ty / aty and
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	282	TRM = trm / atrm
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	283	by (auto intro: alpha_equivps)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	284
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	285	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	286	"TYP :: KIND"
1139 c4001cda9da3 renamed 'as' to 'is' everywhere. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1129 diff changeset	287	is
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	288	"Type"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	289
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	290	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	291	"KPI :: TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND"
1139 c4001cda9da3 renamed 'as' to 'is' everywhere. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1129 diff changeset	292	is
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	293	"KPi"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	294
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	295	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	296	"TCONST :: ident \<Rightarrow> TY"
1139 c4001cda9da3 renamed 'as' to 'is' everywhere. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1129 diff changeset	297	is
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	298	"TConst"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	299
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	300	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	301	"TAPP :: TY \<Rightarrow> TRM \<Rightarrow> TY"
1139 c4001cda9da3 renamed 'as' to 'is' everywhere. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1129 diff changeset	302	is
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	303	"TApp"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	304
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	305	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	306	"TPI :: TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY"
1139 c4001cda9da3 renamed 'as' to 'is' everywhere. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1129 diff changeset	307	is
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	308	"TPi"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	309
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	310	(* FIXME: does not work with CONST *)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	311	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	312	"CONS :: ident \<Rightarrow> TRM"
1139 c4001cda9da3 renamed 'as' to 'is' everywhere. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1129 diff changeset	313	is
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	314	"Const"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	315
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	316	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	317	"VAR :: name \<Rightarrow> TRM"
1139 c4001cda9da3 renamed 'as' to 'is' everywhere. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1129 diff changeset	318	is
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	319	"Var"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	320
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	321	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	322	"APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM"
1139 c4001cda9da3 renamed 'as' to 'is' everywhere. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1129 diff changeset	323	is
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	324	"App"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	325
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	326	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	327	"LAM :: TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM"
1139 c4001cda9da3 renamed 'as' to 'is' everywhere. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1129 diff changeset	328	is
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	329	"Lam"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	330
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	331	(* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	332	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	333	"fv_kind :: KIND \<Rightarrow> atom set"
1139 c4001cda9da3 renamed 'as' to 'is' everywhere. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1129 diff changeset	334	is
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	335	"rfv_kind"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	336
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	337	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	338	"fv_ty :: TY \<Rightarrow> atom set"
1139 c4001cda9da3 renamed 'as' to 'is' everywhere. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1129 diff changeset	339	is
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	340	"rfv_ty"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	341
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	342	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	343	"fv_trm :: TRM \<Rightarrow> atom set"
1139 c4001cda9da3 renamed 'as' to 'is' everywhere. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1129 diff changeset	344	is
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	345	"rfv_trm"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	346
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	347	lemma alpha_rfv:
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	348	shows "(t \<approx>ki s \<longrightarrow> rfv_kind t = rfv_kind s) \<and>
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	349	(t1 \<approx>ty s1 \<longrightarrow> rfv_ty t1 = rfv_ty s1) \<and>
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	350	(t2 \<approx>tr s2 \<longrightarrow> rfv_trm t2 = rfv_trm s2)"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	351	apply(rule akind_aty_atrm.induct)
1027 163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	352	apply(simp_all add: alpha_gen)
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	353	done
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	354
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	355	lemma perm_rsp[quot_respect]:
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	356	"(op = ===> akind ===> akind) permute permute"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	357	"(op = ===> aty ===> aty) permute permute"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	358	"(op = ===> atrm ===> atrm) permute permute"
992 74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	359	by (simp_all add:alpha_eqvt)
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	360
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	361	lemma tconst_rsp[quot_respect]:
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	362	"(op = ===> aty) TConst TConst"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	363	apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	364	lemma tapp_rsp[quot_respect]:
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	365	"(aty ===> atrm ===> aty) TApp TApp"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	366	apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	367	lemma var_rsp[quot_respect]:
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	368	"(op = ===> atrm) Var Var"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	369	apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	370	lemma app_rsp[quot_respect]:
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	371	"(atrm ===> atrm ===> atrm) App App"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	372	apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	373	lemma const_rsp[quot_respect]:
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	374	"(op = ===> atrm) Const Const"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	375	apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
992 74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	376
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	377	lemma kpi_rsp[quot_respect]:
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	378	"(aty ===> op = ===> akind ===> akind) KPi KPi"
993 5c0d9a507bcb Fixed the induction problem + some more proofs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 992 diff changeset	379	apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
1027 163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	380	apply (rule a2) apply assumption
993 5c0d9a507bcb Fixed the induction problem + some more proofs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 992 diff changeset	381	apply (rule_tac x="0" in exI)
1027 163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	382	apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
993 5c0d9a507bcb Fixed the induction problem + some more proofs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 992 diff changeset	383	done
5c0d9a507bcb Fixed the induction problem + some more proofs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 992 diff changeset	384
992 74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	385	lemma tpi_rsp[quot_respect]:
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	386	"(aty ===> op = ===> aty ===> aty) TPi TPi"
993 5c0d9a507bcb Fixed the induction problem + some more proofs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 992 diff changeset	387	apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
1027 163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	388	apply (rule a5) apply assumption
993 5c0d9a507bcb Fixed the induction problem + some more proofs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 992 diff changeset	389	apply (rule_tac x="0" in exI)
1027 163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	390	apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
993 5c0d9a507bcb Fixed the induction problem + some more proofs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 992 diff changeset	391	done
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	392	lemma lam_rsp[quot_respect]:
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	393	"(aty ===> op = ===> atrm ===> atrm) Lam Lam"
993 5c0d9a507bcb Fixed the induction problem + some more proofs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 992 diff changeset	394	apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
1027 163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	395	apply (rule a9) apply assumption
993 5c0d9a507bcb Fixed the induction problem + some more proofs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 992 diff changeset	396	apply (rule_tac x="0" in exI)
1027 163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	397	apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
993 5c0d9a507bcb Fixed the induction problem + some more proofs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 992 diff changeset	398	done
992 74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	399
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	400	lemma rfv_ty_rsp[quot_respect]:
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	401	"(aty ===> op =) rfv_ty rfv_ty"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	402	by (simp add: alpha_rfv)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	403	lemma rfv_kind_rsp[quot_respect]:
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	404	"(akind ===> op =) rfv_kind rfv_kind"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	405	by (simp add: alpha_rfv)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	406	lemma rfv_trm_rsp[quot_respect]:
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	407	"(atrm ===> op =) rfv_trm rfv_trm"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	408	by (simp add: alpha_rfv)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	409
1027 163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	410	thm kind_ty_trm.induct
1082 f8029d8c88a9 Fixed the context import/export and simplified LFex. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1045 diff changeset	411	lemmas KIND_TY_TRM_induct = kind_ty_trm.induct[quot_lifted]
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	412
994 333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	413	thm kind_ty_trm.inducts
1082 f8029d8c88a9 Fixed the context import/export and simplified LFex. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1045 diff changeset	414	lemmas KIND_TY_TRM_inducts = kind_ty_trm.inducts[quot_lifted]
994 333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	415
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	416	instantiation KIND and TY and TRM :: pt
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	417	begin
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	418
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	419	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	420	"permute_KIND :: perm \<Rightarrow> KIND \<Rightarrow> KIND"
1139 c4001cda9da3 renamed 'as' to 'is' everywhere. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1129 diff changeset	421	is
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	422	"permute :: perm \<Rightarrow> kind \<Rightarrow> kind"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	423
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	424	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	425	"permute_TY :: perm \<Rightarrow> TY \<Rightarrow> TY"
1139 c4001cda9da3 renamed 'as' to 'is' everywhere. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1129 diff changeset	426	is
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	427	"permute :: perm \<Rightarrow> ty \<Rightarrow> ty"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	428
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	429	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	430	"permute_TRM :: perm \<Rightarrow> TRM \<Rightarrow> TRM"
1139 c4001cda9da3 renamed 'as' to 'is' everywhere. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1129 diff changeset	431	is
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	432	"permute :: perm \<Rightarrow> trm \<Rightarrow> trm"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	433
1083 30550327651a Proper context fixes lifting inside instantiations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1082 diff changeset	434	lemmas permute_ktt[simp] = permute_kind_permute_ty_permute_trm.simps[quot_lifted]
30550327651a Proper context fixes lifting inside instantiations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1082 diff changeset	435
1082 f8029d8c88a9 Fixed the context import/export and simplified LFex. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1045 diff changeset	436	lemma perm_zero_ok: "0 \<bullet> (x :: KIND) = x \<and> 0 \<bullet> (y :: TY) = y \<and> 0 \<bullet> (z :: TRM) = z"
f8029d8c88a9 Fixed the context import/export and simplified LFex. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1045 diff changeset	437	apply (induct rule: KIND_TY_TRM_induct)
1083 30550327651a Proper context fixes lifting inside instantiations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1082 diff changeset	438	apply (simp_all)
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	439	done
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	440
1082 f8029d8c88a9 Fixed the context import/export and simplified LFex. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1045 diff changeset	441	lemma perm_add_ok:
994 333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	442	"((p + q) \<bullet> (x1 :: KIND) = (p \<bullet> q \<bullet> x1))"
333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	443	"((p + q) \<bullet> (x2 :: TY) = p \<bullet> q \<bullet> x2)"
333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	444	"((p + q) \<bullet> (x3 :: TRM) = p \<bullet> q \<bullet> x3)"
1082 f8029d8c88a9 Fixed the context import/export and simplified LFex. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1045 diff changeset	445	apply (induct x1 and x2 and x3 rule: KIND_TY_TRM_inducts)
1083 30550327651a Proper context fixes lifting inside instantiations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1082 diff changeset	446	apply (simp_all)
994 333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	447	done
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	448
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	449	instance
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	450	apply default
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	451	apply (simp_all add: perm_zero_ok perm_add_ok)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	452	done
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	453
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	454	end
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	455
1082 f8029d8c88a9 Fixed the context import/export and simplified LFex. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1045 diff changeset	456	lemmas AKIND_ATY_ATRM_inducts = akind_aty_atrm.inducts[unfolded alpha_gen, quot_lifted, folded alpha_gen]
994 333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	457
1082 f8029d8c88a9 Fixed the context import/export and simplified LFex. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1045 diff changeset	458	lemmas KIND_TY_TRM_INJECT = akind_aty_atrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
994 333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	459
1082 f8029d8c88a9 Fixed the context import/export and simplified LFex. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1045 diff changeset	460	lemmas fv_kind_ty_trm = rfv_kind_rfv_ty_rfv_trm.simps[quot_lifted]
994 333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	461
1082 f8029d8c88a9 Fixed the context import/export and simplified LFex. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1045 diff changeset	462	lemmas fv_eqvt = rfv_eqvt[quot_lifted]
994 333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	463
1002 3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	464	lemma supp_kind_ty_trm_easy:
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	465	"supp TYP = {}"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	466	"supp (TCONST i) = {atom i}"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	467	"supp (TAPP A M) = supp A \<union> supp M"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	468	"supp (CONS i) = {atom i}"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	469	"supp (VAR x) = {atom x}"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	470	"supp (APP M N) = supp M \<union> supp N"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	471	apply (simp_all add: supp_def permute_ktt KIND_TY_TRM_INJECT)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	472	apply (simp_all only: supp_at_base[simplified supp_def])
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	473	apply (simp_all add: Collect_imp_eq Collect_neg_eq)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	474	done
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	475
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	476	lemma supp_bind:
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	477	"(supp (atom na, (ty, ki))) supports (KPI ty na ki)"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	478	"(supp (atom na, (ty, ty2))) supports (TPI ty na ty2)"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	479	"(supp (atom na, (ty, trm))) supports (LAM ty na trm)"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	480	apply(simp_all add: supports_def)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	481	apply(fold fresh_def)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	482	apply(simp_all add: fresh_Pair swap_fresh_fresh)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	483	apply(clarify)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	484	apply(subst swap_at_base_simps(3))
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	485	apply(simp_all add: fresh_atom)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	486	apply(clarify)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	487	apply(subst swap_at_base_simps(3))
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	488	apply(simp_all add: fresh_atom)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	489	apply(clarify)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	490	apply(subst swap_at_base_simps(3))
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	491	apply(simp_all add: fresh_atom)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	492	done
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	493
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	494	lemma KIND_TY_TRM_fs:
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	495	"finite (supp (x\<Colon>KIND))"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	496	"finite (supp (y\<Colon>TY))"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	497	"finite (supp (z\<Colon>TRM))"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	498	apply(induct x and y and z rule: KIND_TY_TRM_inducts)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	499	apply(simp_all add: supp_kind_ty_trm_easy)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	500	apply(rule supports_finite)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	501	apply(rule supp_bind(1))
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	502	apply(simp add: supp_Pair supp_atom)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	503	apply(rule supports_finite)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	504	apply(rule supp_bind(2))
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	505	apply(simp add: supp_Pair supp_atom)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	506	apply(rule supports_finite)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	507	apply(rule supp_bind(3))
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	508	apply(simp add: supp_Pair supp_atom)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	509	done
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	510
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	511	instance KIND and TY and TRM :: fs
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	512	apply(default)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	513	apply(simp_all only: KIND_TY_TRM_fs)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	514	done
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	515
994 333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	516	lemma supp_fv:
1036 aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	517	"supp t1 = fv_kind t1"
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	518	"supp t2 = fv_ty t2"
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	519	"supp t3 = fv_trm t3"
994 333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	520	apply(induct t1 and t2 and t3 rule: KIND_TY_TRM_inducts)
1002 3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	521	apply (simp_all add: supp_kind_ty_trm_easy)
994 333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	522	apply (simp_all add: fv_kind_ty_trm)
1027 163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	523	apply(subgoal_tac "supp (KPI ty name kind) = supp ty \<union> supp (Abs {atom name} kind)")
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	524	apply(simp add: supp_Abs Set.Un_commute)
1002 3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	525	apply(simp (no_asm) add: supp_def)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	526	apply(simp add: KIND_TY_TRM_INJECT)
1036 aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	527	apply(simp add: Abs_eq_iff)
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	528	apply(simp add: alpha_gen)
1045 7a975641efbc another adaptation for the eqvt-change Christian Urban <urbanc@in.tum.de> parents: 1036 diff changeset	529	apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute insert_eqvt empty_eqvt atom_eqvt)
7a975641efbc another adaptation for the eqvt-change Christian Urban <urbanc@in.tum.de> parents: 1036 diff changeset	530	apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric])
1036 aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	531	apply(subgoal_tac "supp (TPI ty1 name ty2) = supp ty1 \<union> supp (Abs {atom name} ty2)")
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	532	apply(simp add: supp_Abs Set.Un_commute)
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	533	apply(simp (no_asm) add: supp_def)
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	534	apply(simp add: KIND_TY_TRM_INJECT)
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	535	apply(simp add: Abs_eq_iff)
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	536	apply(simp add: alpha_gen)
1045 7a975641efbc another adaptation for the eqvt-change Christian Urban <urbanc@in.tum.de> parents: 1036 diff changeset	537	apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] insert_eqvt empty_eqvt atom_eqvt)
1002 3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	538	apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)
1036 aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	539	apply(subgoal_tac "supp (LAM ty name trm) = supp ty \<union> supp (Abs {atom name} trm)")
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	540	apply(simp add: supp_Abs Set.Un_commute)
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	541	apply(simp (no_asm) add: supp_def)
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	542	apply(simp add: KIND_TY_TRM_INJECT)
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	543	apply(simp add: Abs_eq_iff)
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	544	apply(simp add: alpha_gen)
1045 7a975641efbc another adaptation for the eqvt-change Christian Urban <urbanc@in.tum.de> parents: 1036 diff changeset	545	apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] insert_eqvt empty_eqvt atom_eqvt)
1036 aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	546	apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	547	done
994 333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	548
1036 aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	549	(* Not needed anymore *)
1027 163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	550	lemma supp_kpi_pre: "supp (KPI A x K) = (supp (Abs {atom x} K)) \<union> supp A"
1036 aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	551	apply (simp add: permute_set_eq supp_def Abs_eq_iff KIND_TY_TRM_INJECT)
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	552	apply (simp add: alpha_gen supp_fv)
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	553	apply (simp add: Collect_imp_eq Collect_neg_eq add: atom_eqvt Set.Un_commute)
997 b7d259ded92e Ported LF to the generic lambda and solved the simpler _supp cases. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 994 diff changeset	554	done
994 333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	555
333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	556	lemma supp_kind_ty_trm:
333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	557	"supp TYP = {}"
333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	558	"supp (KPI A x K) = supp A \<union> (supp K - {atom x})"
333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	559	"supp (TCONST i) = {atom i}"
333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	560	"supp (TAPP A M) = supp A \<union> supp M"
333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	561	"supp (TPI A x B) = supp A \<union> (supp B - {atom x})"
333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	562	"supp (CONS i) = {atom i}"
333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	563	"supp (VAR x) = {atom x}"
333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	564	"supp (APP M N) = supp M \<union> supp N"
333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	565	"supp (LAM A x M) = supp A \<union> (supp M - {atom x})"
1002 3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	566	apply (simp_all only: supp_kind_ty_trm_easy)
1036 aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	567	apply (simp_all only: supp_fv fv_kind_ty_trm)
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	568	done
994 333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	569
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	570	end
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	571
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	572
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	573
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	574

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Tue, 23 Feb 2010 10:47:14 +0100
changeset 1219	c74c8ba46db7
parent 1218	2bbfbc9a81fc
child 1234	1240d5eb275d
permissions	-rw-r--r--