nominal2: Quot/Nominal/LFex.thy@cc5830c452c4 (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)"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	83	\| a2: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (rfv_kind K - {atom x} = rfv_kind K' - {atom x'} \<and> (rfv_kind K - {atom x})\<sharp>* pi \<and> (pi \<bullet> K) \<approx>ki K' \<and> (pi \<bullet> x) = x')\<rbrakk> \<Longrightarrow> (KPi A x K) \<approx>ki (KPi A' x' K')"
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')"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	86	\| a5: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (rfv_ty B - {atom x} = rfv_ty B' - {atom x'} \<and> (rfv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) \<approx>ty B' \<and> (pi \<bullet> x) = x')\<rbrakk> \<Longrightarrow> (TPi A x B) \<approx>ty (TPi A' x' B')"
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')"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	90	\| a9: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (rfv_trm M - {atom x} = rfv_trm M' - {atom x'} \<and> (rfv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) \<approx>tr M' \<and> (pi \<bullet> x) = x')\<rbrakk> \<Longrightarrow> (Lam A x M) \<approx>tr (Lam A' x' M')"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	91
991 928e80edf138 Added the experiments with fun and function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 985 diff changeset	92	(*
928e80edf138 Added the experiments with fun and function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 985 diff changeset	93	function(sequential)
928e80edf138 Added the experiments with fun and function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 985 diff changeset	94	akind :: "kind \<Rightarrow> kind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
928e80edf138 Added the experiments with fun and function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 985 diff changeset	95	and aty :: "ty \<Rightarrow> ty \<Rightarrow> bool" ("_ \<approx>ty _" [100, 100] 100)
928e80edf138 Added the experiments with fun and function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 985 diff changeset	96	and atrm :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<approx>tr _" [100, 100] 100)
928e80edf138 Added the experiments with fun and function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 985 diff changeset	97	where
928e80edf138 Added the experiments with fun and function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 985 diff changeset	98	a1: "(Type) \<approx>ki (Type) = True"
928e80edf138 Added the experiments with fun and function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 985 diff changeset	99	\| a2: "(KPi A x K) \<approx>ki (KPi A' x' K') = (A \<approx>ty A' \<and> (\<exists>pi. (rfv_kind K - {atom x} = rfv_kind K' - {atom x'} \<and> (rfv_kind K - {atom x})\<sharp>* pi \<and> (pi \<bullet> K) \<approx>ki K' \<and> (pi \<bullet> x) = x')))"
928e80edf138 Added the experiments with fun and function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 985 diff changeset	100	\| "_ \<approx>ki _ = False"
928e80edf138 Added the experiments with fun and function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 985 diff changeset	101	\| a3: "(TConst i) \<approx>ty (TConst j) = (i = j)"
928e80edf138 Added the experiments with fun and function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 985 diff changeset	102	\| a4: "(TApp A M) \<approx>ty (TApp A' M') = (A \<approx>ty A' \<and> M \<approx>tr M')"
928e80edf138 Added the experiments with fun and function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 985 diff changeset	103	\| a5: "(TPi A x B) \<approx>ty (TPi A' x' B') = ((A \<approx>ty A') \<and> (\<exists>pi. rfv_ty B - {atom x} = rfv_ty B' - {atom x'} \<and> (rfv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) \<approx>ty B' \<and> (pi \<bullet> x) = x'))"
928e80edf138 Added the experiments with fun and function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 985 diff changeset	104	\| "_ \<approx>ty _ = False"
928e80edf138 Added the experiments with fun and function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 985 diff changeset	105	\| a6: "(Const i) \<approx>tr (Const j) = (i = j)"
928e80edf138 Added the experiments with fun and function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 985 diff changeset	106	\| a7: "(Var x) \<approx>tr (Var y) = (x = y)"
928e80edf138 Added the experiments with fun and function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 985 diff changeset	107	\| a8: "(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')"
928e80edf138 Added the experiments with fun and function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 985 diff changeset	108	\| a9: "(Lam A x M) \<approx>tr (Lam A' x' M') = (A \<approx>ty A' \<and> (\<exists>pi. rfv_trm M - {atom x} = rfv_trm M' - {atom x'} \<and> (rfv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) \<approx>tr M' \<and> (pi \<bullet> x) = x'))"
928e80edf138 Added the experiments with fun and function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 985 diff changeset	109	\| "_ \<approx>tr _ = False"
928e80edf138 Added the experiments with fun and function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 985 diff changeset	110	apply (pat_completeness)
928e80edf138 Added the experiments with fun and function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 985 diff changeset	111	apply simp_all
928e80edf138 Added the experiments with fun and function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 985 diff changeset	112	done
928e80edf138 Added the experiments with fun and function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 985 diff changeset	113	termination
928e80edf138 Added the experiments with fun and function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 985 diff changeset	114	by (size_change)
928e80edf138 Added the experiments with fun and function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 985 diff changeset	115	*)
928e80edf138 Added the experiments with fun and function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 985 diff changeset	116
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	117	lemma akind_aty_atrm_inj:
992 74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	118	"(Type) \<approx>ki (Type) = True"
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	119	"(KPi A x K) \<approx>ki (KPi A' x' K') = (A \<approx>ty A' \<and> (\<exists>pi. (rfv_kind K - {atom x} = rfv_kind K' - {atom x'} \<and> (rfv_kind K - {atom x})\<sharp>* pi \<and> (pi \<bullet> K) \<approx>ki K' \<and> (pi \<bullet> x) = x')))"
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	120	"(TConst i) \<approx>ty (TConst j) = (i = j)"
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	121	"(TApp A M) \<approx>ty (TApp A' M') = (A \<approx>ty A' \<and> M \<approx>tr M')"
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	122	"(TPi A x B) \<approx>ty (TPi A' x' B') = ((A \<approx>ty A') \<and> (\<exists>pi. rfv_ty B - {atom x} = rfv_ty B' - {atom x'} \<and> (rfv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) \<approx>ty B' \<and> (pi \<bullet> x) = x'))"
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	123	"(Const i) \<approx>tr (Const j) = (i = j)"
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	124	"(Var x) \<approx>tr (Var y) = (x = y)"
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	125	"(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')"
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	126	"(Lam A x M) \<approx>tr (Lam A' x' M') = (A \<approx>ty A' \<and> (\<exists>pi. rfv_trm M - {atom x} = rfv_trm M' - {atom x'} \<and> (rfv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) \<approx>tr M' \<and> (pi \<bullet> x) = x'))"
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	127	apply -
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	128	apply (simp add: akind_aty_atrm.intros)
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	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	131	apply (simp only: akind_aty_atrm.intros)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	132
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	133	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	134	apply (simp only: akind_aty_atrm.intros)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	135
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	136	apply rule apply (erule aty.cases) apply simp apply simp apply simp
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	137	apply (simp only: akind_aty_atrm.intros)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	138
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	139	apply rule apply (erule aty.cases) apply simp apply simp apply blast
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	140	apply (simp only: akind_aty_atrm.intros)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	141
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	142	apply rule apply (erule 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	143	apply (simp only: akind_aty_atrm.intros)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	144
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	145	apply rule apply (erule 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	146	apply (simp only: akind_aty_atrm.intros)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	147
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	148	apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	149	apply (simp only: akind_aty_atrm.intros)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	150
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	151	apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	152	apply (simp only: akind_aty_atrm.intros)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	153	done
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	154
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	155	lemma rfv_eqvt[eqvt]:
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	156	"((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	157	"((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	158	"((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	159	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	160	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	161	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	162	done
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	163
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	164	lemma alpha_eqvt:
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	165	"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	166	"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	167	"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	168	apply(induct rule: akind_aty_atrm.inducts)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	169	apply (simp_all add: akind_aty_atrm.intros)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	170	apply(rule a2)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	171	apply simp
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	172	apply(erule conjE)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	173	apply(erule exE)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	174	apply(erule conjE)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	175	apply(rule_tac x="pi \<bullet> pia" in exI)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	176	apply(rule conjI)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	177	apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	178	apply(simp add: eqvts atom_eqvt)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	179	apply(rule conjI)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	180	apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	181	apply(simp add: eqvts atom_eqvt)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	182	apply(simp add: permute_eqvt[symmetric])
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	183	apply(rule a5)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	184	apply simp
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	185	apply(erule conjE)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	186	apply(erule exE)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	187	apply(erule conjE)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	188	apply(rule_tac x="pi \<bullet> pia" in exI)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	189	apply(rule conjI)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	190	apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	191	apply(simp add: eqvts atom_eqvt)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	192	apply(rule conjI)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	193	apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	194	apply(simp add: eqvts atom_eqvt)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	195	apply(simp add: permute_eqvt[symmetric])
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	196	apply(rule a9)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	197	apply simp
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	198	apply(erule conjE)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	199	apply(erule exE)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	200	apply(erule conjE)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	201	apply(rule_tac x="pi \<bullet> pia" in exI)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	202	apply(rule conjI)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	203	apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	204	apply(simp add: eqvts atom_eqvt)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	205	apply(rule conjI)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	206	apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	207	apply(simp add: eqvts atom_eqvt)
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	208	apply(simp add: permute_eqvt[symmetric])
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	209	done
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	210
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	211	lemma al_refl:
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	212	fixes K::"kind"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	213	and A::"ty"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	214	and M::"trm"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	215	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	216	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	217	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	218	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	219	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	220	apply (rule a2)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	221	apply auto
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	222	apply(rule_tac x="0" in exI)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	223	apply(simp_all add: fresh_star_def fresh_zero_perm)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	224	apply (rule a5)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	225	apply auto
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	226	apply(rule_tac x="0" in exI)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	227	apply(simp_all add: fresh_star_def fresh_zero_perm)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	228	apply (rule a9)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	229	apply auto
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	230	apply(rule_tac x="0" in exI)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	231	apply(simp_all add: fresh_star_def fresh_zero_perm)
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"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	238	sorry
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	239
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	240	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	241	by (rule alpha_equivps)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	242
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	243	quotient_type
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	244	TY = ty / aty and
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	245	TRM = trm / atrm
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	246	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	247
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	248	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	249	"TYP :: KIND"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	250	as
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	251	"Type"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	252
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	253	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	254	"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	255	as
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	256	"KPi"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	257
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	258	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	259	"TCONST :: ident \<Rightarrow> TY"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	260	as
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	261	"TConst"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	262
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	263	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	264	"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	265	as
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	266	"TApp"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	267
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	268	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	269	"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	270	as
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	271	"TPi"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	272
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	273	(* 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	274	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	275	"CONS :: ident \<Rightarrow> TRM"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	276	as
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	277	"Const"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	278
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	279	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	280	"VAR :: name \<Rightarrow> TRM"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	281	as
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	282	"Var"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	283
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	284	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	285	"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	286	as
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	287	"App"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	288
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	289	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	290	"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	291	as
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	292	"Lam"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	293
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	294	(* 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	295	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	296	"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	297	as
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	298	"rfv_kind"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	299
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	300	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	301	"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	302	as
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	303	"rfv_ty"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	304
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	305	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	306	"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	307	as
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	308	"rfv_trm"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	309
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	310	lemma alpha_rfv:
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	311	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	312	(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	313	(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	314	apply(rule akind_aty_atrm.induct)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	315	apply(simp_all)
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	316	done
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	317
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	318	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	319	"(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	320	"(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	321	"(op = ===> atrm ===> atrm) permute permute"
992 74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	322	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	323
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	324	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	325	"(op = ===> aty) TConst TConst"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	326	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	327	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	328	"(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	329	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	330	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	331	"(op = ===> atrm) Var Var"
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	332	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	333	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	334	"(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	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 const_rsp[quot_respect]:
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	337	"(op = ===> atrm) Const Const"
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
992 74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	339
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	340	lemma kpi_rsp[quot_respect]:
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	341	"(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	342	apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
5c0d9a507bcb Fixed the induction problem + some more proofs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 992 diff changeset	343	apply (rule a2) apply simp
5c0d9a507bcb Fixed the induction problem + some more proofs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 992 diff changeset	344	apply (rule_tac x="0" in exI)
5c0d9a507bcb Fixed the induction problem + some more proofs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 992 diff changeset	345	apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv)
5c0d9a507bcb Fixed the induction problem + some more proofs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 992 diff changeset	346	done
5c0d9a507bcb Fixed the induction problem + some more proofs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 992 diff changeset	347
992 74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	348	lemma tpi_rsp[quot_respect]:
74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	349	"(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	350	apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
5c0d9a507bcb Fixed the induction problem + some more proofs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 992 diff changeset	351	apply (rule a5) apply simp
5c0d9a507bcb Fixed the induction problem + some more proofs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 992 diff changeset	352	apply (rule_tac x="0" in exI)
5c0d9a507bcb Fixed the induction problem + some more proofs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 992 diff changeset	353	apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv)
5c0d9a507bcb Fixed the induction problem + some more proofs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 992 diff changeset	354	done
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	355	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	356	"(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	357	apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
5c0d9a507bcb Fixed the induction problem + some more proofs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 992 diff changeset	358	apply (rule a9) apply simp
5c0d9a507bcb Fixed the induction problem + some more proofs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 992 diff changeset	359	apply (rule_tac x="0" in exI)
5c0d9a507bcb Fixed the induction problem + some more proofs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 992 diff changeset	360	apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv)
5c0d9a507bcb Fixed the induction problem + some more proofs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 992 diff changeset	361	done
992 74e9a580448c equivariance of rfv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 991 diff changeset	362
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	363	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	364	"(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	365	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	366	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	367	"(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	368	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	369	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	370	"(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	371	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	372
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	373	lemma KIND_TY_TRM_induct: "\<lbrakk>P10 TYP; \<And>ty name kind. \<lbrakk>P20 ty; P10 kind\<rbrakk> \<Longrightarrow> P10 (KPI ty name kind); \<And>ident. P20 (TCONST ident);
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	374	\<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	375	\<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	376	\<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	377	\<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	378	\<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	379	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	380
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	381	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	382
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	383	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	384	"\<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	385	\<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	386	\<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	387	\<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	388	\<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	389	\<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	390	"\<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	391	\<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	392	\<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	393	\<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	394	\<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	395	\<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	396	"\<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	397	\<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	398	\<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	399	\<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	400	\<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	401	\<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	402	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	403
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	404	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	405	begin
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	406
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	407	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	408	"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	409	as
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	410	"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	411
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	412	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	413	"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	414	as
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	415	"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	416
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	417	quotient_definition
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	418	"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	419	as
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	420	"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	421
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	422	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	423	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	424	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	425	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	426	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	427	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	428	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	429	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	430	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	431	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	432	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	433	done
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	434
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	435	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	436	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	437	apply simp_all
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	438	done
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	439
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	440	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	441	"((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	442	"((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	443	"((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	444	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	445	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	446	done
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	447
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	448	instance
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	449	apply default
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	450	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	451	done
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	452
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	453	end
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	454
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	455	lemma "\<lbrakk>P10 TYP TYP;
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	456	\<And>A A' K x K' x'.
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	457	\<lbrakk>(A :: TY) = A'; P20 A A';
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	458	\<exists>pi. fv_kind K - {atom x} = fv_kind K' - {atom x'} \<and>
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	459	(fv_kind K - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> K) = K' \<and> P10 (pi \<bullet> K) K') \<and> pi \<bullet> x = x'\<rbrakk>
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	460	\<Longrightarrow> P10 (KPI A x K) (KPI A' x' K');
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	461	\<And>i j. i = j \<Longrightarrow> P20 (TCONST i) (TCONST j);
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	462	\<And>A A' M M'. \<lbrakk>A = A'; P20 A A'; M = M'; P30 M M'\<rbrakk> \<Longrightarrow> P20 (TAPP A M) (TAPP A' M');
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	463	\<And>A A' B x B' x'.
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	464	\<lbrakk>A = A'; P20 A A';
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	465	\<exists>pi. fv_ty B - {atom x} = fv_ty B' - {atom x'} \<and>
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	466	(fv_ty B - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> B) = B' \<and> P20 (pi \<bullet> B) B') \<and> pi \<bullet> x = x'\<rbrakk>
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	467	\<Longrightarrow> P20 (TPI A x B) (TPI A' x' B');
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	468	\<And>i j. i = j \<Longrightarrow> P30 (CONS i) (CONS j); \<And>x y. x = y \<Longrightarrow> P30 (VAR x) (VAR y);
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	469	\<And>M M' N N'. \<lbrakk>M = M'; P30 M M'; N = N'; P30 N N'\<rbrakk> \<Longrightarrow> P30 (APP M N) (APP M' N');
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	470	\<And>A A' M x M' x'.
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	471	\<lbrakk>A = A'; P20 A A';
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	472	\<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and>
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	473	(fv_trm M - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> M) = M' \<and> P30 (pi \<bullet> M) M') \<and> pi \<bullet> x = x'\<rbrakk>
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	474	\<Longrightarrow> P30 (LAM A x M) (LAM A' x' M')\<rbrakk>
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	475	\<Longrightarrow> (x10 = x20 \<longrightarrow> P10 x10 x20) \<and>
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	476	(x30 = x40 \<longrightarrow> P20 x30 x40) \<and> (x50 = x60 \<longrightarrow> P30 x50 x60)"
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	477	by (lifting akind_aty_atrm.induct)
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	478
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	479	lemma AKIND_ATY_ATRM_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	480	"\<lbrakk>x10 = x20; P10 TYP 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	481	\<And>A A' K x K' 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	482	\<lbrakk>A = A'; P20 A A';
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	483	\<exists>pi. fv_kind K - {atom x} = fv_kind K' - {atom x'} \<and>
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	484	(fv_kind K - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> K) = K' \<and> P10 (pi \<bullet> K) K') \<and> pi \<bullet> x = x'\<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	485	\<Longrightarrow> P10 (KPI A x K) (KPI A' x' K');
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	486	\<And>i j. i = j \<Longrightarrow> P20 (TCONST i) (TCONST 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	487	\<And>A A' M M'. \<lbrakk>A = A'; P20 A A'; M = M'; P30 M M'\<rbrakk> \<Longrightarrow> P20 (TAPP A M) (TAPP A' 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	488	\<And>A A' B x B' 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	489	\<lbrakk>A = A'; P20 A A';
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	490	\<exists>pi. fv_ty B - {atom x} = fv_ty B' - {atom x'} \<and>
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	491	(fv_ty B - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> B) = B' \<and> P20 (pi \<bullet> B) B') \<and> pi \<bullet> x = x'\<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	492	\<Longrightarrow> P20 (TPI A x B) (TPI A' x' B');
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	493	\<And>i j. i = j \<Longrightarrow> P30 (CONS i) (CONS j); \<And>x y. x = y \<Longrightarrow> P30 (VAR x) (VAR 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	494	\<And>M M' N N'. \<lbrakk>M = M'; P30 M M'; N = N'; P30 N N'\<rbrakk> \<Longrightarrow> P30 (APP M N) (APP M' 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	495	\<And>A A' M x M' 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	496	\<lbrakk>A = A'; P20 A A';
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	497	\<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and>
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	498	(fv_trm M - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> M) = M' \<and> P30 (pi \<bullet> M) M') \<and> pi \<bullet> x = x'\<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	499	\<Longrightarrow> P30 (LAM A x M) (LAM A' x' M')\<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	500	\<Longrightarrow> P10 x10 x20"
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	501	"\<lbrakk>x30 = x40; P10 TYP 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	502	\<And>A A' K x K' 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	503	\<lbrakk>A = A'; P20 A A';
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	504	\<exists>pi. fv_kind K - {atom x} = fv_kind K' - {atom x'} \<and>
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	505	(fv_kind K - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> K) = K' \<and> P10 (pi \<bullet> K) K') \<and> pi \<bullet> x = x'\<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	506	\<Longrightarrow> P10 (KPI A x K) (KPI A' x' K');
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	507	\<And>i j. i = j \<Longrightarrow> P20 (TCONST i) (TCONST 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	508	\<And>A A' M M'. \<lbrakk>A = A'; P20 A A'; M = M'; P30 M M'\<rbrakk> \<Longrightarrow> P20 (TAPP A M) (TAPP A' 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	509	\<And>A A' B x B' 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	510	\<lbrakk>A = A'; P20 A A';
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	511	\<exists>pi. fv_ty B - {atom x} = fv_ty B' - {atom x'} \<and>
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	512	(fv_ty B - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> B) = B' \<and> P20 (pi \<bullet> B) B') \<and> pi \<bullet> x = x'\<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	513	\<Longrightarrow> P20 (TPI A x B) (TPI A' x' B');
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	514	\<And>i j. i = j \<Longrightarrow> P30 (CONS i) (CONS j); \<And>x y. x = y \<Longrightarrow> P30 (VAR x) (VAR 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	515	\<And>M M' N N'. \<lbrakk>M = M'; P30 M M'; N = N'; P30 N N'\<rbrakk> \<Longrightarrow> P30 (APP M N) (APP M' 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	516	\<And>A A' M x M' 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	517	\<lbrakk>A = A'; P20 A A';
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	518	\<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and>
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	519	(fv_trm M - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> M) = M' \<and> P30 (pi \<bullet> M) M') \<and> pi \<bullet> x = x'\<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	520	\<Longrightarrow> P30 (LAM A x M) (LAM A' x' M')\<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	521	\<Longrightarrow> P20 x30 x40"
333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	522	"\<lbrakk>x50 = x60; P10 TYP 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	523	\<And>A A' K x K' 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	524	\<lbrakk>A = A'; P20 A A';
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	525	\<exists>pi. fv_kind K - {atom x} = fv_kind K' - {atom x'} \<and>
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	526	(fv_kind K - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> K) = K' \<and> P10 (pi \<bullet> K) K') \<and> pi \<bullet> x = x'\<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	527	\<Longrightarrow> P10 (KPI A x K) (KPI A' x' K');
333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	528	\<And>i j. i = j \<Longrightarrow> P20 (TCONST i) (TCONST 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	529	\<And>A A' M M'. \<lbrakk>A = A'; P20 A A'; M = M'; P30 M M'\<rbrakk> \<Longrightarrow> P20 (TAPP A M) (TAPP A' 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	530	\<And>A A' B x B' x'.
333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	531	\<lbrakk>A = A'; P20 A A';
333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	532	\<exists>pi. fv_ty B - {atom x} = fv_ty B' - {atom x'} \<and>
333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	533	(fv_ty B - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> B) = B' \<and> P20 (pi \<bullet> B) B') \<and> pi \<bullet> x = x'\<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	534	\<Longrightarrow> P20 (TPI A x B) (TPI A' x' B');
333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	535	\<And>i j. i = j \<Longrightarrow> P30 (CONS i) (CONS j); \<And>x y. x = y \<Longrightarrow> P30 (VAR x) (VAR 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	536	\<And>M M' N N'. \<lbrakk>M = M'; P30 M M'; N = N'; P30 N N'\<rbrakk> \<Longrightarrow> P30 (APP M N) (APP M' N');
333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	537	\<And>A A' M x M' 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	538	\<lbrakk>A = A'; P20 A A';
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	539	\<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and>
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	540	(fv_trm M - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> M) = M' \<and> P30 (pi \<bullet> M) M') \<and> pi \<bullet> x = x'\<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	541	\<Longrightarrow> P30 (LAM A x M) (LAM A' x' M')\<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	542	\<Longrightarrow> P30 x50 x60"
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	543	by (lifting akind_aty_atrm.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	544
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	545	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	546	"(TYP) = (TYP) = True"
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	547	"(KPI A x K) = (KPI A' x' K') = (A = A' \<and> (\<exists>pi. (fv_kind K - {atom x} = fv_kind K' - {atom x'} \<and> (fv_kind K - {atom x})\<sharp>* pi \<and> (pi \<bullet> K) = K' \<and> (pi \<bullet> x) = 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	548	"(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	549	"(TAPP A M) = (TAPP A' M') = (A = A' \<and> M = 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	550	"(TPI A x B) = (TPI A' x' B') = ((A = A') \<and> (\<exists>pi. fv_ty B - {atom x} = fv_ty B' - {atom x'} \<and> (fv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) = B' \<and> (pi \<bullet> x) = 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	551	"(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	552	"(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	553	"(APP M N) = (APP M' N') = (M = M' \<and> N = 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	554	"(LAM A x M) = (LAM A' x' M') = (A = A' \<and> (\<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and> (fv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) = M' \<and> (pi \<bullet> x) = 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	555	by (lifting akind_aty_atrm_inj)
333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	556
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	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	558	"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	559	"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	560	"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	561	"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	562	"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	563	"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	564	"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	565	"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	566	"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	567	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	568
333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	569	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	570	"(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	571	"(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	572	"(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	573	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	574
1002 3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	575	lemma supp_kind_ty_trm_easy:
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	576	"supp TYP = {}"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	577	"supp (TCONST i) = {atom i}"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	578	"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	579	"supp (CONS i) = {atom i}"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	580	"supp (VAR x) = {atom x}"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	581	"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	582	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	583	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	584	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	585	done
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	586
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	587	lemma supp_bind:
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	588	"(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	589	"(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	590	"(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	591	apply(simp_all add: supports_def)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	592	apply(fold fresh_def)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	593	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	594	apply(clarify)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	595	apply(subst swap_at_base_simps(3))
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	596	apply(simp_all add: fresh_atom)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	597	apply(clarify)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	598	apply(subst swap_at_base_simps(3))
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	599	apply(simp_all add: fresh_atom)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	600	apply(clarify)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	601	apply(subst swap_at_base_simps(3))
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	602	apply(simp_all add: fresh_atom)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	603	done
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	604
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	605	lemma KIND_TY_TRM_fs:
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	606	"finite (supp (x\<Colon>KIND))"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	607	"finite (supp (y\<Colon>TY))"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	608	"finite (supp (z\<Colon>TRM))"
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	609	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	610	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	611	apply(rule supports_finite)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	612	apply(rule supp_bind(1))
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	613	apply(simp add: supp_Pair supp_atom)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	614	apply(rule supports_finite)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	615	apply(rule supp_bind(2))
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	616	apply(simp add: supp_Pair supp_atom)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	617	apply(rule supports_finite)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	618	apply(rule supp_bind(3))
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	619	apply(simp add: supp_Pair supp_atom)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	620	done
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	621
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	622	instance KIND and TY and TRM :: fs
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	623	apply(default)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	624	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	625	done
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	626
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	627	lemma supp_fv:
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	628	"fv_kind t1 = supp 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	629	"fv_ty t2 = supp 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	630	"fv_trm t3 = supp 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	631	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	632	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	633	apply (simp_all add: fv_kind_ty_trm)
1002 3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	634	apply(subgoal_tac "supp (KPI ty name kind) = supp ty \<union> supp (Abst {atom name} kind)")
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	635	apply(simp add: supp_Abst Set.Un_commute)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	636	apply(simp (no_asm) add: supp_def)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	637	apply(simp add: KIND_TY_TRM_INJECT)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	638	apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric])
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	639	apply(simp add: abs_eq alpha_gen)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	640	apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	641	apply(simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric])
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	642	apply (fold supp_def)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	643	apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	644	apply (rule refl)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	645	apply(subst Set.Un_commute)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	646	apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	647	apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	648	apply (rule refl)
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	649	prefer 2
3f227ed7e3e5 More proofs in the LF example. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 997 diff changeset	650	apply(simp add: eqvts supp_eqvt atom_eqvt)
1004 44b013c59653 The current state of fv vs supp proofs in LF. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1002 diff changeset	651	sorry (* Stuck *)
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	652
997 b7d259ded92e Ported LF to the generic lambda and solved the simpler _supp cases. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 994 diff changeset	653	lemma supp_kpi_pre: "supp (KPI A x K) = (supp (Abst {atom x} K)) \<union> supp A"
1004 44b013c59653 The current state of fv vs supp proofs in LF. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1002 diff changeset	654	(apply (subst supp_Pair[symmetric]))
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	655	unfolding supp_def
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	656	apply (simp add: permute_set_eq)
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	657	apply(subst abs_eq)
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	658	apply(subst 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	659	apply(simp only: supp_fv)
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	660	apply simp
1004 44b013c59653 The current state of fv vs supp proofs in LF. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1002 diff changeset	661	apply (simp_all add: Collect_imp_eq Collect_neg_eq)
44b013c59653 The current state of fv vs supp proofs in LF. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1002 diff changeset	662	apply(subst Set.Un_commute)
44b013c59653 The current state of fv vs supp proofs in LF. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1002 diff changeset	663	apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
44b013c59653 The current state of fv vs supp proofs in LF. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1002 diff changeset	664	apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
44b013c59653 The current state of fv vs supp proofs in LF. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1002 diff changeset	665	apply (rule refl)
44b013c59653 The current state of fv vs supp proofs in LF. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1002 diff changeset	666	prefer 2
44b013c59653 The current state of fv vs supp proofs in LF. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1002 diff changeset	667	apply (rule refl)
44b013c59653 The current state of fv vs supp proofs in LF. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1002 diff changeset	668	sorry (* Stuck *)
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	669
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	670	lemma supp_kpi: "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	671	apply(subst supp_kpi_pre)
997 b7d259ded92e Ported LF to the generic lambda and solved the simpler _supp cases. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 994 diff changeset	672	apply(subst supp_Abst)
b7d259ded92e Ported LF to the generic lambda and solved the simpler _supp cases. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 994 diff changeset	673	apply (simp only: Set.Un_commute)
b7d259ded92e Ported LF to the generic lambda and solved the simpler _supp cases. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 994 diff changeset	674	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	675
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	676	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	677	"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	678	"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	679	"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	680	"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	681	"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	682	"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	683	"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	684	"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	685	"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	686	apply (simp_all only: 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	687	apply (simp add: supp_kpi)
1004 44b013c59653 The current state of fv vs supp proofs in LF. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1002 diff changeset	688	sorry (* Other ones will follow similarily *)
44b013c59653 The current state of fv vs supp proofs in LF. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1002 diff changeset	689
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	690
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	691	end
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	692
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	693
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	694
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	695

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Tue, 02 Feb 2010 10:43:48 +0100 (2010-02-02)
changeset 1022	cc5830c452c4
parent 1021	bacf3584640e
child 1027	163d6917af62
permissions	-rw-r--r--