nominal2: Quot/Nominal/LFex.thy@c4001cda9da3 (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
1129 9a86f0ef6503 Notation available locally Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1128 diff changeset	2	imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs"
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
992 74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	21	primrec
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	22	rfv_kind :: "kind \<Rightarrow> atom set"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	23	and rfv_ty :: "ty \<Rightarrow> atom set"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	24	and rfv_trm :: "trm \<Rightarrow> atom set"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	25	where
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	26	"rfv_kind (Type) = {}"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	27	\| "rfv_kind (KPi A x K) = (rfv_ty A) \<union> ((rfv_kind K) - {atom x})"
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	28	\| "rfv_ty (TConst i) = {atom i}"
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	29	\| "rfv_ty (TApp A M) = (rfv_ty A) \<union> (rfv_trm M)"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	30	\| "rfv_ty (TPi A x B) = (rfv_ty A) \<union> ((rfv_ty B) - {atom x})"
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	31	\| "rfv_trm (Const i) = {atom i}"
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	32	\| "rfv_trm (Var x) = {atom x}"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	33	\| "rfv_trm (App M N) = (rfv_trm M) \<union> (rfv_trm N)"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	34	\| "rfv_trm (Lam A x M) = (rfv_ty A) \<union> ((rfv_trm M) - {atom x})"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	35
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	36	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	37	begin
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	38
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	39	primrec
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	40	permute_kind
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	41	and permute_ty
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	42	and permute_trm
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	43	where
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	44	"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	45	\| "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	46	\| "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	47	\| "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	48	\| "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	49	\| "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	50	\| "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	51	\| "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	52	\| "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	53
1022 cc5830c452c4 With induct instead of induct_tac, just one induction is sufficient. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1021 diff changeset	54	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	55	"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	56	"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	57	"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	58	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	59	apply(simp_all)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	60	done
1022 cc5830c452c4 With induct instead of induct_tac, just one induction is sufficient. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1021 diff changeset	61
cc5830c452c4 With induct instead of induct_tac, just one induction is sufficient. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1021 diff changeset	62	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	63	"(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	64	"(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	65	"(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	66	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	67	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	68	done
cc5830c452c4 With induct instead of induct_tac, just one induction is sufficient. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1021 diff changeset	69
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	70	instance
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	71	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	72	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	73	done
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	74
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	75	end
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	76
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	77	inductive
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	78	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	79	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	80	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	81	where
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	82	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	83	\| 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	84	\| 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	85	\| 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	86	\| 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	87	\| 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	88	\| 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	89	\| 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	90	\| 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	91
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	92	lemma akind_aty_atrm_inj:
992 74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	93	"(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	94	"((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	95	"(TConst i) \<approx>ty (TConst j) = (i = j)"
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	96	"(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	97	"((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	98	"(Const i) \<approx>tr (Const j) = (i = j)"
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	99	"(Var x) \<approx>tr (Var y) = (x = y)"
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	100	"(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	101	"((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	102	apply -
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	103	apply (simp add: akind_aty_atrm.intros)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	104
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	105	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	106	apply (simp only: akind_aty_atrm.intros)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	107
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	108	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	109	apply (simp only: akind_aty_atrm.intros)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	110
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	111	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	112	apply (simp only: akind_aty_atrm.intros)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	113
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	114	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	115	apply (simp only: akind_aty_atrm.intros)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	116
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	117	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	118	apply (simp only: akind_aty_atrm.intros)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	119
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	120	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	121	apply (simp only: akind_aty_atrm.intros)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	122
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	123	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	124	apply (simp only: akind_aty_atrm.intros)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	125
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	126	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	127	apply (simp only: akind_aty_atrm.intros)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	128	done
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	129
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	130	lemma rfv_eqvt[eqvt]:
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	131	"((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	132	"((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	133	"((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	134	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	135	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	136	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	137	done
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	lemma alpha_eqvt:
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	140	"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	141	"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	142	"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	143	apply(induct rule: akind_aty_atrm.inducts)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	144	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	145	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	146	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	147	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	148	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	149	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	150	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	151	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	152	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	153	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	154	apply assumption
992 74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	155	done
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	156
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	157	lemma al_refl:
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	158	fixes K::"kind"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	159	and A::"ty"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	160	and M::"trm"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	161	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	162	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	163	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	164	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	165	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	166	apply (rule a2)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	167	apply auto
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	168	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	169	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	170	apply (rule a5)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	171	apply auto
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	172	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	173	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	174	apply (rule a9)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	175	apply auto
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	176	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	177	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	178	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	179
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	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	181	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	182	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	183	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	184	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	185	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	186	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	187	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	188	apply(rule alpha_gen_atom_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	189	apply(rule alpha_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	190	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	191	apply(rule alpha_gen_atom_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	192	apply(rule alpha_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	193	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	194	apply(rule alpha_gen_atom_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	195	apply(rule alpha_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	196	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	197	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	198
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	199	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	200	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	201	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	202	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	203	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	204	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	205	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	206	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	207	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	208	apply(simp 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	209	apply(rule alpha_gen_atom_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	210	apply(rule alpha_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	211	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	212	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	213	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	214	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	215	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	216	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	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 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	219	apply(rule alpha_gen_atom_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	220	apply(rule alpha_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	221	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	222	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	223	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	224	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	225	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	226	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	227	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	228	apply(simp 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	229	apply(rule alpha_gen_atom_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	230	apply(rule alpha_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	231	apply(assumption)+
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	232	done
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	233
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	234	lemma alpha_equivps:
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	235	shows "equivp akind"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	236	and "equivp aty"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	237	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	238	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	239	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	240	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	241	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	242	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	243	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	244	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	245	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	246	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	247	done
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	248
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	249	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	250	by (rule alpha_equivps)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	251
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	252	quotient_type
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	253	TY = ty / aty and
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	254	TRM = trm / atrm
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	255	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	256
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	257	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	258	"TYP :: KIND"
1139 c4001cda9da3 renamed 'as' to 'is' everywhere. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1129 diff changeset	259	is
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	260	"Type"
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	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	263	"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	264	is
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	265	"KPi"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	266
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	267	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	268	"TCONST :: ident \<Rightarrow> TY"
1139 c4001cda9da3 renamed 'as' to 'is' everywhere. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1129 diff changeset	269	is
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	270	"TConst"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	271
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	272	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	273	"TAPP :: TY \<Rightarrow> TRM \<Rightarrow> TY"
1139 c4001cda9da3 renamed 'as' to 'is' everywhere. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1129 diff changeset	274	is
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	275	"TApp"
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_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	278	"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	279	is
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	280	"TPi"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	281
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	282	(* 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	283	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	284	"CONS :: ident \<Rightarrow> TRM"
1139 c4001cda9da3 renamed 'as' to 'is' everywhere. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1129 diff changeset	285	is
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	286	"Const"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	287
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	288	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	289	"VAR :: name \<Rightarrow> TRM"
1139 c4001cda9da3 renamed 'as' to 'is' everywhere. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1129 diff changeset	290	is
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	291	"Var"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	292
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	293	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	294	"APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM"
1139 c4001cda9da3 renamed 'as' to 'is' everywhere. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1129 diff changeset	295	is
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	296	"App"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	297
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	298	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	299	"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	300	is
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	301	"Lam"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	302
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	303	(* 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	304	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	305	"fv_kind :: KIND \<Rightarrow> atom set"
1139 c4001cda9da3 renamed 'as' to 'is' everywhere. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1129 diff changeset	306	is
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	307	"rfv_kind"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	308
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	309	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	310	"fv_ty :: TY \<Rightarrow> atom set"
1139 c4001cda9da3 renamed 'as' to 'is' everywhere. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1129 diff changeset	311	is
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	312	"rfv_ty"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	313
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	314	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	315	"fv_trm :: TRM \<Rightarrow> atom set"
1139 c4001cda9da3 renamed 'as' to 'is' everywhere. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1129 diff changeset	316	is
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	317	"rfv_trm"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	318
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	319	lemma alpha_rfv:
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	320	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	321	(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	322	(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	323	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	324	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	325	done
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	326
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	327	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	328	"(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	329	"(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	330	"(op = ===> atrm ===> atrm) permute permute"
992 74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	331	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	332
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	333	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	334	"(op = ===> aty) TConst TConst"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	335	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	336	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	337	"(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	338	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	339	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	340	"(op = ===> atrm) Var Var"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	341	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	342	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	343	"(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	344	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	345	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	346	"(op = ===> atrm) Const Const"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	347	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	348
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	349	lemma kpi_rsp[quot_respect]:
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	350	"(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	351	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	352	apply (rule a2) apply assumption
993 5c0d9a507bcb Fixed the induction problem + some more proofs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 992 diff changeset	353	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	354	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	355	done
5c0d9a507bcb Fixed the induction problem + some more proofs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 992 diff changeset	356
992 74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	357	lemma tpi_rsp[quot_respect]:
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	358	"(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	359	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	360	apply (rule a5) apply assumption
993 5c0d9a507bcb Fixed the induction problem + some more proofs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 992 diff changeset	361	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	362	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	363	done
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	364	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	365	"(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	366	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	367	apply (rule a9) apply assumption
993 5c0d9a507bcb Fixed the induction problem + some more proofs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 992 diff changeset	368	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	369	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	370	done
992 74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	371
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	372	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	373	"(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	374	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	375	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	376	"(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	377	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	378	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	379	"(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	380	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	381
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	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	383	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	384
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	385	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	386	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	387
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	388	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	389	begin
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	390
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	391	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	392	"permute_KIND :: perm \<Rightarrow> KIND \<Rightarrow> KIND"
1139 c4001cda9da3 renamed 'as' to 'is' everywhere. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1129 diff changeset	393	is
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	394	"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	395
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	396	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	397	"permute_TY :: perm \<Rightarrow> TY \<Rightarrow> TY"
1139 c4001cda9da3 renamed 'as' to 'is' everywhere. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1129 diff changeset	398	is
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	399	"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	400
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	401	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	402	"permute_TRM :: perm \<Rightarrow> TRM \<Rightarrow> TRM"
1139 c4001cda9da3 renamed 'as' to 'is' everywhere. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1129 diff changeset	403	is
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	404	"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	405
1083 30550327651a Proper context fixes lifting inside instantiations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1082 diff changeset	406	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	407
1082 f8029d8c88a9 Fixed the context import/export and simplified LFex. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1045 diff changeset	408	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	409	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	410	apply (simp_all)
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	411	done
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	412
1082 f8029d8c88a9 Fixed the context import/export and simplified LFex. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1045 diff changeset	413	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	414	"((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	415	"((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	416	"((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	417	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	418	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	419	done
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	420
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	421	instance
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	422	apply default
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	423	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	424	done
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	425
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	426	end
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	427
1082 f8029d8c88a9 Fixed the context import/export and simplified LFex. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1045 diff changeset	428	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	429
1082 f8029d8c88a9 Fixed the context import/export and simplified LFex. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1045 diff changeset	430	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	431
1082 f8029d8c88a9 Fixed the context import/export and simplified LFex. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1045 diff changeset	432	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	433
1082 f8029d8c88a9 Fixed the context import/export and simplified LFex. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1045 diff changeset	434	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	435
1002 3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	436	lemma supp_kind_ty_trm_easy:
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	437	"supp TYP = {}"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	438	"supp (TCONST i) = {atom i}"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	439	"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	440	"supp (CONS i) = {atom i}"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	441	"supp (VAR x) = {atom x}"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	442	"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	443	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	444	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	445	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	446	done
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	447
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	448	lemma supp_bind:
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	449	"(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	450	"(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	451	"(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	452	apply(simp_all add: supports_def)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	453	apply(fold fresh_def)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	454	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	455	apply(clarify)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	456	apply(subst swap_at_base_simps(3))
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	457	apply(simp_all add: fresh_atom)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	458	apply(clarify)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	459	apply(subst swap_at_base_simps(3))
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	460	apply(simp_all add: fresh_atom)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	461	apply(clarify)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	462	apply(subst swap_at_base_simps(3))
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	463	apply(simp_all add: fresh_atom)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	464	done
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	465
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	466	lemma KIND_TY_TRM_fs:
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	467	"finite (supp (x\<Colon>KIND))"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	468	"finite (supp (y\<Colon>TY))"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	469	"finite (supp (z\<Colon>TRM))"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	470	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	471	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	472	apply(rule supports_finite)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	473	apply(rule supp_bind(1))
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	474	apply(simp add: supp_Pair supp_atom)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	475	apply(rule supports_finite)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	476	apply(rule supp_bind(2))
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	477	apply(simp add: supp_Pair supp_atom)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	478	apply(rule supports_finite)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	479	apply(rule supp_bind(3))
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	480	apply(simp add: supp_Pair supp_atom)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	481	done
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	482
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	483	instance KIND and TY and TRM :: fs
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	484	apply(default)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	485	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	486	done
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	487
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	488	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	489	"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	490	"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	491	"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	492	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	493	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	494	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	495	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	496	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	497	apply(simp (no_asm) add: supp_def)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	498	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	499	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	500	apply(simp add: alpha_gen)
1045 7a975641efbc another adaptation for the eqvt-change Christian Urban <urbanc@in.tum.de> parents: 1036 diff changeset	501	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	502	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	503	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	504	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	505	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	506	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	507	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	508	apply(simp add: alpha_gen)
1045 7a975641efbc another adaptation for the eqvt-change Christian Urban <urbanc@in.tum.de> parents: 1036 diff changeset	509	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	510	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	511	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	512	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	513	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	514	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	515	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	516	apply(simp add: alpha_gen)
1045 7a975641efbc another adaptation for the eqvt-change Christian Urban <urbanc@in.tum.de> parents: 1036 diff changeset	517	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	518	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	519	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	520
1036 aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	521	(* 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	522	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	523	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	524	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	525	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	526	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	527
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	528	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	529	"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	530	"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	531	"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	532	"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	533	"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	534	"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	535	"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	536	"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	537	"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	538	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	539	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	540	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	541
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	542	end
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	543
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	544
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	545
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	546

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Fri, 12 Feb 2010 16:04:10 +0100 (2010-02-12)
changeset 1139	c4001cda9da3
parent 1129	9a86f0ef6503
child 1210	10a0e3578507
permissions	-rw-r--r--