nominal2: Nominal/ExCoreHaskell.thy@a40dbea68d0b (annotated)

1601 5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	1	theory ExCoreHaskell
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	2	imports "Parser"
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	3	begin
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	4
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	5	(* core haskell *)
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	6
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	7	ML {* val _ = recursive := false *}
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	8
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	9	atom_decl var
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	10	atom_decl tvar
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	11
1606 75403378068b Initial list unfoldings in Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1601 diff changeset	12	(* there are types, coercion types and regular types list-data-structure *)
1609 c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	13
1601 5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	14	nominal_datatype tkind =
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	15	KStar
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	16	\| KFun "tkind" "tkind"
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	17	and ckind =
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	18	CKEq "ty" "ty"
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	19	and ty =
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	20	TVar "tvar"
1609 c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	21	\| TC "char"
1601 5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	22	\| TApp "ty" "ty"
1609 c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	23	\| TFun "char" "ty_lst"
1601 5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	24	\| TAll tv::"tvar" "tkind" T::"ty" bind tv in T
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	25	\| TEq "ty" "ty" "ty"
1606 75403378068b Initial list unfoldings in Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1601 diff changeset	26	and ty_lst =
75403378068b Initial list unfoldings in Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1601 diff changeset	27	TsNil
75403378068b Initial list unfoldings in Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1601 diff changeset	28	\| TsCons "ty" "ty_lst"
1601 5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	29	and co =
1609 c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	30	CC "char"
1601 5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	31	\| CApp "co" "co"
1609 c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	32	\| CFun "char" "co_lst"
1601 5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	33	\| CAll tv::"tvar" "ckind" C::"co" bind tv in C
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	34	\| CEq "co" "co" "co"
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	35	\| CSym "co"
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	36	\| CCir "co" "co"
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	37	\| CLeft "co"
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	38	\| CRight "co"
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	39	\| CSim "co"
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	40	\| CRightc "co"
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	41	\| CLeftc "co"
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	42	\| CCoe "co" "co"
1606 75403378068b Initial list unfoldings in Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1601 diff changeset	43	and co_lst =
75403378068b Initial list unfoldings in Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1601 diff changeset	44	CsNil
75403378068b Initial list unfoldings in Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1601 diff changeset	45	\| CsCons "co" "co_lst"
1609 c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	46	and trm =
1601 5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	47	Var "var"
1609 c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	48	\| C "char"
c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	49	\| LAMT tv::"tvar" "tkind" t::"trm" bind tv in t
c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	50	\| LAMC tv::"tvar" "ckind" t::"trm" bind tv in t
1601 5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	51	\| APP "trm" "ty"
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	52	\| Lam v::"var" "ty" t::"trm" bind v in t
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	53	\| App "trm" "trm"
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	54	\| Let x::"var" "ty" "trm" t::"trm" bind x in t
1609 c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	55	\| Case "trm" "assoc_lst"
c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	56	\| Cast "trm" "ty" --"ty is supposed to be a coercion type only"
c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	57	and assoc_lst =
c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	58	ANil
c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	59	\| ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t
1601 5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	60	and pat =
1609 c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	61	K "char" "tvtk_lst" "tvck_lst" "vt_lst"
1621 a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	62	and vt_lst =
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	63	VTNil
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	64	\| VTCons "var" "ty" "vt_lst"
1609 c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	65	and tvtk_lst =
c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	66	TVTKNil
c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	67	\| TVTKCons "tvar" "tkind" "tvtk_lst"
c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	68	and tvck_lst =
c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	69	TVCKNil
c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	70	\| TVCKCons "tvar" "ckind" "tvck_lst"
1601 5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	71	binder
1609 c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	72	bv :: "pat \<Rightarrow> atom set"
1621 a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	73	and bv_vt :: "vt_lst \<Rightarrow> atom set"
1609 c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	74	and bv_tvtk :: "tvtk_lst \<Rightarrow> atom set"
1621 a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	75	and bv_tvck :: "tvck_lst \<Rightarrow> atom set"
1601 5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	76	where
1621 a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	77	"bv (K s tvts tvcs vs) = (bv_tvtk tvts) \<union> (bv_tvck tvcs) \<union> (bv_vt vs)"
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	78	\| "bv_vt VTNil = {}"
1609 c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	79	\| "bv_vt (VTCons v k t) = {atom v} \<union> bv_vt t"
c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	80	\| "bv_tvtk TVTKNil = {}"
c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	81	\| "bv_tvtk (TVTKCons v k t) = {atom v} \<union> bv_tvtk t"
c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	82	\| "bv_tvck TVCKNil = {}"
1621 a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	83	\| "bv_tvck (TVCKCons v k t) = {atom v} \<union> bv_tvck t"
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	84
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	85	ML {* Sign.of_sort @{theory} (@{typ tkind}, @{sort fs}) *}
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	86
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	87	lemma helper: "((\<exists>p. P p) \<and> Q) = (\<exists>p. (P p \<and> Q))"
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	88	by auto
1601 5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	89
1621 a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	90	lemma supp:
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	91	"fv_tkind tkind = supp tkind \<and>
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	92	fv_ckind ckind = supp ckind \<and>
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	93	fv_ty ty = supp ty \<and>
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	94	fv_ty_lst ty_lst = supp ty_lst \<and>
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	95	fv_co co = supp co \<and>
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	96	fv_co_lst co_lst = supp co_lst \<and>
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	97	fv_trm trm = supp trm \<and>
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	98	fv_assoc_lst assoc_lst = supp assoc_lst \<and>
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	99	fv_pat pat = supp pat \<and>
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	100	fv_vt_lst vt_lst = supp vt_lst \<and>
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	101	fv_tvtk_lst tvtk_lst = supp tvtk_lst \<and>
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	102	fv_tvck_lst tvck_lst = supp tvck_lst"
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	103	apply(rule tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.induct)
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	104	ML_prf {*
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	105	fun supp_eq_tac fv perm eqiff ctxt =
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	106	asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	107	asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_Abs[symmetric]}) THEN_ALL_NEW
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	108	simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	109	simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	110	simp_tac (HOL_basic_ss addsimps (@{thm permute_ABS} :: perm)) THEN_ALL_NEW
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	111	simp_tac (HOL_basic_ss addsimps (@{thm Abs_eq_iff} :: eqiff)) THEN_ALL_NEW
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	112	simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	113	simp_tac (HOL_basic_ss addsimps @{thms alpha_gen}) THEN_ALL_NEW
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	114	asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	115	asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	116	simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	117	simp_tac (HOL_basic_ss addsimps @{thms infinite_Un[symmetric] Collect_disj_eq[symmetric]}) THEN_ALL_NEW
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	118	simp_tac (HOL_basic_ss addsimps @{thms de_Morgan_conj[symmetric]}) THEN_ALL_NEW
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	119	simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI})
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	120	*}
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	121	apply (tactic {* ALLGOALS (TRY o SOLVED' (supp_eq_tac
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	122	@{thms tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv}
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	123	@{thms tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.perm}
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	124	@{thms tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.eq_iff}
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	125	@{context})) *})
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	126	apply (simp only: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv)
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	127	apply (simp only: Un_assoc[symmetric])
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	128	apply (simp only: Un_Diff[symmetric])
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	129	apply (simp only: supp_Pair[symmetric])
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	130	apply (simp only: supp_Abs[symmetric])
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	131	apply (simp (no_asm) only: supp_def)
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	132	apply (simp only: permute_ABS)
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	133	apply (simp only: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.perm)
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	134	apply (simp only: Abs_eq_iff)
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	135	apply (simp only: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.eq_iff)
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	136	apply (simp only: alpha_gen2)
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	137	apply (simp only: alpha_gen)
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	138	apply (simp only: eqvts[symmetric])
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	139	apply (simp only: supp_Pair)
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	140	apply (simp only: eqvts)
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	141	apply (simp only: Pair_eq)
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	142	apply (simp only: infinite_Un[symmetric] Collect_disj_eq[symmetric])
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	143	apply (simp only: de_Morgan_conj[symmetric])
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	144	apply (simp only: helper)
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	145	by (simp)
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	146
a40dbea68d0b Core Haskell experiments. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1615 diff changeset	147	thm tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv[simplified supp]
1615 0ea578c6dae3 Parsing bn functions that call other bn functions and transmitting this information to fv/alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1609 diff changeset	148
0ea578c6dae3 Parsing bn functions that call other bn functions and transmitting this information to fv/alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1609 diff changeset	149
1601 5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	150	end
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	151
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	152
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	153

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Wed, 24 Mar 2010 08:45:54 +0100
changeset 1621	a40dbea68d0b
parent 1615	0ea578c6dae3
child 1624	91ab98dd9999
permissions	-rw-r--r--