nominal2: Quot/Nominal/LFex.thy@aaac8274f08c (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
992 74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	2	imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "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"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	259	as
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"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	264	as
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"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	269	as
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"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	274	as
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"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	279	as
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"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	285	as
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"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	290	as
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"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	295	as
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"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	300	as
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"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	306	as
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"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	311	as
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"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	316	as
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
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	383
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	384	lemma KIND_TY_TRM_induct:
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	385	fixes P10 :: "KIND \<Rightarrow> bool" and P20 :: "TY \<Rightarrow> bool" and P30 :: "TRM \<Rightarrow> bool"
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	386	shows
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	387	"\<lbrakk>P10 TYP; \<And>ty name kind. \<lbrakk>P20 ty; P10 kind\<rbrakk> \<Longrightarrow> P10 (KPI ty name kind); \<And>ident. P20 (TCONST ident);
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	388	\<And>ty trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P20 (TAPP ty trm);
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	389	\<And>ty1 name ty2. \<lbrakk>P20 ty1; P20 ty2\<rbrakk> \<Longrightarrow> P20 (TPI ty1 name ty2); \<And>ident. P30 (CONS ident);
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	390	\<And>name. P30 (VAR name); \<And>trm1 trm2. \<lbrakk>P30 trm1; P30 trm2\<rbrakk> \<Longrightarrow> P30 (APP trm1 trm2);
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	391	\<And>ty name trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P30 (LAM ty name trm)\<rbrakk>
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	392	\<Longrightarrow> P10 kind \<and> P20 ty \<and> P30 trm"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	393	by (lifting kind_ty_trm.induct)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	394
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	395	thm kind_ty_trm.inducts
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	396
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	397	lemma KIND_TY_TRM_inducts:
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	398	"\<lbrakk>P10 TYP; \<And>ty name kind. \<lbrakk>P20 ty; P10 kind\<rbrakk> \<Longrightarrow> P10 (KPI ty name kind); \<And>ident. P20 (TCONST ident);
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	399	\<And>ty trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P20 (TAPP 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	400	\<And>ty1 name ty2. \<lbrakk>P20 ty1; P20 ty2\<rbrakk> \<Longrightarrow> P20 (TPI ty1 name ty2); \<And>ident. P30 (CONS ident);
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	401	\<And>name. P30 (VAR name); \<And>trm1 trm2. \<lbrakk>P30 trm1; P30 trm2\<rbrakk> \<Longrightarrow> P30 (APP trm1 trm2);
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	402	\<And>ty name trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P30 (LAM ty name trm)\<rbrakk>
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	403	\<Longrightarrow> P10 kind"
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	404	"\<lbrakk>P10 TYP; \<And>ty name kind. \<lbrakk>P20 ty; P10 kind\<rbrakk> \<Longrightarrow> P10 (KPI ty name kind); \<And>ident. P20 (TCONST ident);
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	405	\<And>ty trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P20 (TAPP 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	406	\<And>ty1 name ty2. \<lbrakk>P20 ty1; P20 ty2\<rbrakk> \<Longrightarrow> P20 (TPI ty1 name ty2); \<And>ident. P30 (CONS ident);
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	407	\<And>name. P30 (VAR name); \<And>trm1 trm2. \<lbrakk>P30 trm1; P30 trm2\<rbrakk> \<Longrightarrow> P30 (APP trm1 trm2);
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	408	\<And>ty name trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P30 (LAM ty name trm)\<rbrakk>
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	409	\<Longrightarrow> P20 ty"
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	410	"\<lbrakk>P10 TYP; \<And>ty name kind. \<lbrakk>P20 ty; P10 kind\<rbrakk> \<Longrightarrow> P10 (KPI ty name kind); \<And>ident. P20 (TCONST ident);
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	411	\<And>ty trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P20 (TAPP 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	412	\<And>ty1 name ty2. \<lbrakk>P20 ty1; P20 ty2\<rbrakk> \<Longrightarrow> P20 (TPI ty1 name ty2); \<And>ident. P30 (CONS ident);
333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	413	\<And>name. P30 (VAR name); \<And>trm1 trm2. \<lbrakk>P30 trm1; P30 trm2\<rbrakk> \<Longrightarrow> P30 (APP trm1 trm2);
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	\<And>ty name trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P30 (LAM ty name trm)\<rbrakk>
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	\<Longrightarrow> P30 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	416	by (lifting kind_ty_trm.inducts)
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	417
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	418	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	419	begin
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	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	422	"permute_KIND :: perm \<Rightarrow> KIND \<Rightarrow> KIND"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	423	as
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	424	"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	425
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	426	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	427	"permute_TY :: perm \<Rightarrow> TY \<Rightarrow> TY"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	428	as
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	429	"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	430
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	431	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	432	"permute_TRM :: perm \<Rightarrow> TRM \<Rightarrow> TRM"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	433	as
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	434	"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	435
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	436	lemma permute_ktt[simp]:
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	437	shows "pi \<bullet> TYP = TYP"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	438	and "pi \<bullet> (KPI t n k) = KPI (pi \<bullet> t) (pi \<bullet> n) (pi \<bullet> k)"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	439	and "pi \<bullet> (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	440	and "pi \<bullet> (TAPP A M) = TAPP (pi \<bullet> A) (pi \<bullet> M)"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	441	and "pi \<bullet> (TPI A x B) = TPI (pi \<bullet> A) (pi \<bullet> x) (pi \<bullet> B)"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	442	and "pi \<bullet> (CONS i) = CONS (pi \<bullet> i)"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	443	and "pi \<bullet> (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	444	and "pi \<bullet> (APP M N) = APP (pi \<bullet> M) (pi \<bullet> N)"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	445	and "pi \<bullet> (LAM A x M) = LAM (pi \<bullet> A) (pi \<bullet> x) (pi \<bullet> M)"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	446	apply (lifting permute_kind_permute_ty_permute_trm.simps)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	447	done
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	448
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	449	lemma perm_zero_ok: "0 \<bullet> (x :: KIND) = x \<and> 0 \<bullet> (y :: TY) = y \<and> 0 \<bullet> (z :: TRM) = z"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	450	apply (induct rule: KIND_TY_TRM_induct)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	451	apply simp_all
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	452	done
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	453
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	454	lemma perm_add_ok:
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	455	"((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	456	"((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	457	"((p + q) \<bullet> (x3 :: TRM) = p \<bullet> q \<bullet> x3)"
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	458	apply(induct x1 and x2 and x3 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	459	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	460	done
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	461
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	462	instance
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	463	apply default
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	464	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	465	done
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	466
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	467	end
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	468
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	469	lemma 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	470	"\<lbrakk>z1 = z2; P1 TYP TYP;
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	471	\<And>A A' a K b 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	472	\<lbrakk>A = A'; P2 A 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	473	\<exists>pi. ({atom 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	474	K) \<approx>gen (\<lambda>x1 x2.
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	475	x1 = x2 \<and> P1 x1 x2) fv_kind pi ({atom b}, K')\<rbrakk>
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	476	\<Longrightarrow> P1 (KPI A a K) (KPI A' b 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	477	\<And>i j. i = j \<Longrightarrow> P2 (TCONST i) (TCONST j);
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	478	\<And>A A' M 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	479	\<lbrakk>A = A'; P2 A A'; M = M'; P3 M M'\<rbrakk>
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	480	\<Longrightarrow> P2 (TAPP A M) (TAPP A' 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	481	\<And>A A' a B b B'.
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	482	\<lbrakk>A = A'; P2 A 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	483	\<exists>pi. ({atom 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	484	B) \<approx>gen (\<lambda>x1 x2. x1 = x2 \<and> P2 x1 x2) fv_ty pi ({atom b}, B')\<rbrakk>
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	485	\<Longrightarrow> P2 (TPI A a B) (TPI A' b B');
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	486	\<And>i j. i = j \<Longrightarrow> P3 (CONS i) (CONS j);
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	487	\<And>x y. x = y \<Longrightarrow> P3 (VAR x) (VAR y);
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	488	\<And>M M' N N'.
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	489	\<lbrakk>M = M'; P3 M M'; N = N'; P3 N N'\<rbrakk>
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	490	\<Longrightarrow> P3 (APP M N) (APP M' N');
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	491	\<And>A A' a M b 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	492	\<lbrakk>A = A'; P2 A 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	493	\<exists>pi. ({atom 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	494	M) \<approx>gen (\<lambda>x1 x2.
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	x1 = x2 \<and> P3 x1 x2) fv_trm pi ({atom b}, M')\<rbrakk>
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	\<Longrightarrow> P3 (LAM A a M) (LAM A' b M')\<rbrakk>
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	497	\<Longrightarrow> P1 z1 z2"
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	498	"\<lbrakk>z3 = z4; P1 TYP TYP;
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	499	\<And>A A' a K b 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	500	\<lbrakk>A = A'; P2 A 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	501	\<exists>pi. ({atom 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	502	K) \<approx>gen (\<lambda>x1 x2.
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	503	x1 = x2 \<and> P1 x1 x2) fv_kind pi ({atom b}, K')\<rbrakk>
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	504	\<Longrightarrow> P1 (KPI A a K) (KPI A' b 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	505	\<And>i j. i = j \<Longrightarrow> P2 (TCONST i) (TCONST j);
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	506	\<And>A A' M 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	507	\<lbrakk>A = A'; P2 A A'; M = M'; P3 M M'\<rbrakk>
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	508	\<Longrightarrow> P2 (TAPP A M) (TAPP A' 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	509	\<And>A A' a B b B'.
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	510	\<lbrakk>A = A'; P2 A 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	511	\<exists>pi. ({atom 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	512	B) \<approx>gen (\<lambda>x1 x2. x1 = x2 \<and> P2 x1 x2) fv_ty pi ({atom b}, B')\<rbrakk>
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	513	\<Longrightarrow> P2 (TPI A a B) (TPI A' b B');
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	514	\<And>i j. i = j \<Longrightarrow> P3 (CONS i) (CONS j);
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	515	\<And>x y. x = y \<Longrightarrow> P3 (VAR x) (VAR y);
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	516	\<And>M M' N N'.
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	517	\<lbrakk>M = M'; P3 M M'; N = N'; P3 N N'\<rbrakk>
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	518	\<Longrightarrow> P3 (APP M N) (APP M' N');
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	519	\<And>A A' a M b 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	520	\<lbrakk>A = A'; P2 A 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	521	\<exists>pi. ({atom 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	522	M) \<approx>gen (\<lambda>x1 x2.
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	523	x1 = x2 \<and> P3 x1 x2) fv_trm pi ({atom b}, M')\<rbrakk>
163d6917af62 LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1022 diff changeset	524	\<Longrightarrow> P3 (LAM A a M) (LAM A' b M')\<rbrakk>
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	525	\<Longrightarrow> P2 z3 z4"
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	526	"\<lbrakk>z5 = z6; P1 TYP TYP;
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	527	\<And>A A' a K b 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	528	\<lbrakk>A = A'; P2 A 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	529	\<exists>pi. ({atom 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	530	K) \<approx>gen (\<lambda>x1 x2.
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	531	x1 = x2 \<and> P1 x1 x2) fv_kind pi ({atom b}, K')\<rbrakk>
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	532	\<Longrightarrow> P1 (KPI A a K) (KPI A' b 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	533	\<And>i j. i = j \<Longrightarrow> P2 (TCONST i) (TCONST j);
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	534	\<And>A A' M 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	535	\<lbrakk>A = A'; P2 A A'; M = M'; P3 M M'\<rbrakk>
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	536	\<Longrightarrow> P2 (TAPP A M) (TAPP A' 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	537	\<And>A A' a B b B'.
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	538	\<lbrakk>A = A'; P2 A 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	539	\<exists>pi. ({atom 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	540	B) \<approx>gen (\<lambda>x1 x2. x1 = x2 \<and> P2 x1 x2) fv_ty pi ({atom b}, B')\<rbrakk>
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	541	\<Longrightarrow> P2 (TPI A a B) (TPI A' b B');
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	542	\<And>i j. i = j \<Longrightarrow> P3 (CONS i) (CONS j);
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	543	\<And>x y. x = y \<Longrightarrow> P3 (VAR x) (VAR y);
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	544	\<And>M M' N N'.
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	545	\<lbrakk>M = M'; P3 M M'; N = N'; P3 N N'\<rbrakk>
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	546	\<Longrightarrow> P3 (APP M N) (APP M' N');
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	547	\<And>A A' a M b 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	548	\<lbrakk>A = A'; P2 A 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	549	\<exists>pi. ({atom 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	550	M) \<approx>gen (\<lambda>x1 x2.
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	551	x1 = x2 \<and> P3 x1 x2) fv_trm pi ({atom b}, M')\<rbrakk>
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	552	\<Longrightarrow> P3 (LAM A a M) (LAM A' b M')\<rbrakk>
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	553	\<Longrightarrow> P3 z5 z6"
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	554	unfolding 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	555	apply (lifting akind_aty_atrm.inducts[unfolded 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	556	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	557
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	558	thm akind_aty_atrm_inj
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	559	lemma KIND_TY_TRM_INJECT:
333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	560	"(TYP) = (TYP) = 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	561	"(KPI A x K) = (KPI A' x' K') = (A = A' \<and> (\<exists>pi. ({atom x}, K) \<approx>gen (op =) fv_kind pi ({atom x'}, K')))"
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	562	"(TCONST i) = (TCONST j) = (i = j)"
333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	563	"(TAPP A M) = (TAPP A' M') = (A = A' \<and> M = 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	564	"(TPI A x B) = (TPI A' x' B') = (A = A' \<and> (\<exists>pi. ({atom x}, B) \<approx>gen (op =) fv_ty pi ({atom x'}, B')))"
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	565	"(CONS i) = (CONS j) = (i = j)"
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	566	"(VAR x) = (VAR y) = (x = y)"
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	567	"(APP M N) = (APP M' N') = (M = M' \<and> N = 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	568	"(LAM A x M) = (LAM A' x' M') = (A = A' \<and> (\<exists>pi. ({atom x}, M) \<approx>gen (op =) fv_trm pi ({atom x'}, 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	569	unfolding 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	570	by (lifting akind_aty_atrm_inj[unfolded 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	571
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	572	lemma fv_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	573	"fv_kind 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	574	"fv_kind (KPI A x K) = fv_ty A \<union> (fv_kind 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	575	"fv_ty (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	576	"fv_ty (TAPP A M) = fv_ty A \<union> fv_trm 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	577	"fv_ty (TPI A x B) = fv_ty A \<union> (fv_ty 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	578	"fv_trm (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	579	"fv_trm (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	580	"fv_trm (APP M N) = fv_trm M \<union> fv_trm 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	581	"fv_trm (LAM A x M) = fv_ty A \<union> (fv_trm M - {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	582	by(lifting rfv_kind_rfv_ty_rfv_trm.simps)
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	583
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	584	lemma fv_eqvt:
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	585	"(p \<bullet> fv_kind t1) = fv_kind (p \<bullet> t1)"
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	586	"(p \<bullet> fv_ty t2) = fv_ty (p \<bullet> t2)"
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	587	"(p \<bullet> fv_trm t3) = fv_trm (p \<bullet> t3)"
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	588	by(lifting rfv_eqvt)
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	589
1002 3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	590	lemma supp_kind_ty_trm_easy:
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	591	"supp TYP = {}"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	592	"supp (TCONST i) = {atom i}"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	593	"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	594	"supp (CONS i) = {atom i}"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	595	"supp (VAR x) = {atom x}"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	596	"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	597	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	598	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	599	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	600	done
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	601
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	602	lemma supp_bind:
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	603	"(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	604	"(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	605	"(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	606	apply(simp_all add: supports_def)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	607	apply(fold fresh_def)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	608	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	609	apply(clarify)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	610	apply(subst swap_at_base_simps(3))
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	611	apply(simp_all add: fresh_atom)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	612	apply(clarify)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	613	apply(subst swap_at_base_simps(3))
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	614	apply(simp_all add: fresh_atom)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	615	apply(clarify)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	616	apply(subst swap_at_base_simps(3))
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	617	apply(simp_all add: fresh_atom)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	618	done
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	619
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	620	lemma KIND_TY_TRM_fs:
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	621	"finite (supp (x\<Colon>KIND))"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	622	"finite (supp (y\<Colon>TY))"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	623	"finite (supp (z\<Colon>TRM))"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	624	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	625	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	626	apply(rule supports_finite)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	627	apply(rule supp_bind(1))
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	628	apply(simp add: supp_Pair supp_atom)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	629	apply(rule supports_finite)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	630	apply(rule supp_bind(2))
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	631	apply(simp add: supp_Pair supp_atom)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	632	apply(rule supports_finite)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	633	apply(rule supp_bind(3))
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	634	apply(simp add: supp_Pair supp_atom)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	635	done
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	636
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	637	instance KIND and TY and TRM :: fs
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	638	apply(default)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	639	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	640	done
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	641
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	642	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	643	"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	644	"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	645	"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	646	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	647	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	648	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	649	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	650	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	651	apply(simp (no_asm) add: supp_def)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	652	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	653	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	654	apply(simp add: alpha_gen)
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	655	apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] eqvts atom_eqvt)
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	656	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	657	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	658	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	659	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	660	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	661	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	662	apply(simp add: alpha_gen)
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	663	apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] eqvts atom_eqvt)
1002 3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	664	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	665	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	666	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	667	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	668	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	669	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	670	apply(simp add: alpha_gen)
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	671	apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] eqvts atom_eqvt)
aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	672	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	673	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	674
1036 aaac8274f08c The alpha-equivalence relation for let-rec. Not sure if correct... Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1027 diff changeset	675	(* 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	676	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	677	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	678	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	679	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	680	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	681
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	682	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	683	"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	684	"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	685	"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	686	"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	687	"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	688	"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	689	"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	690	"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	691	"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	692	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	693	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	694	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	695
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	696	end
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	697
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	698
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	699
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	700

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Wed, 03 Feb 2010 12:11:23 +0100 (2010-02-03)
changeset 1036	aaac8274f08c
parent 1027	163d6917af62
child 1045	7a975641efbc
permissions	-rw-r--r--