nominal2: Nominal/Ex/CPS/CPS3_DanvyFilinski.thy@0435c4dfd6f6 (annotated)

2861 5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	1	header {* CPS transformation of Danvy and Filinski *}
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	2	theory DanvyFilinski imports Lt begin
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	3
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	4	nominal_primrec
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	5	CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_" [100,100] 100)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	6	and
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	7	CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	8	where
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	9	"eqvt k \<Longrightarrow> (x~)*k = k (x~)"
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	10	\| "eqvt k \<Longrightarrow> (M$N)k = M(%m. (N*(%n.((m $ n) $ (Abs c (k (c~)))))))"
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	11	\| "eqvt k \<Longrightarrow> atom c \<sharp> (x, M) \<Longrightarrow> (Abs x M)*k = k (Abs x (Abs c (M^(c~))))"
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	12	\| "\<not>eqvt k \<Longrightarrow> (CPS1 t k) = t"
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	13	\| "(x~)^l = l $ (x~)"
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	14	\| "(M$N)^l = M(%m. (N(%n.((m $ n) $ l))))"
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	15	\| "atom c \<sharp> (x, M) \<Longrightarrow> (Abs x M)^l = l $ (Abs x (Abs c (M^(c~))))"
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	16	apply (simp only: eqvt_def CPS1_CPS2_graph_def)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	17	apply (rule, perm_simp, rule)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	18	apply auto
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	19	apply (case_tac x)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	20	apply (case_tac a)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	21	apply (case_tac "eqvt b")
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	22	apply (rule_tac y="aa" in lt.strong_exhaust)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	23	apply auto[4]
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	24	apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	25	apply (simp add: fresh_at_base Abs1_eq_iff)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	26	apply (case_tac b)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	27	apply (rule_tac y="a" in lt.strong_exhaust)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	28	apply auto[3]
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	29	apply blast
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	30	apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	31	apply (simp add: fresh_at_base Abs1_eq_iff)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	32	apply blast
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	33	--"-"
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	34	apply (subgoal_tac "Abs c (ka (c~)) = Abs ca (ka (ca~))")
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	35	apply (simp only:)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	36	apply (simp add: Abs1_eq_iff)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	37	apply (case_tac "c=ca")
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	38	apply simp_all[2]
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	39	apply rule
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	40	apply (perm_simp)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	41	apply (simp add: eqvt_def)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	42	apply (simp add: fresh_def)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	43	apply (rule contra_subsetD[OF supp_fun_app])
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	44	back
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	45	apply (simp add: supp_fun_eqvt lt.supp supp_at_base)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	46	--"-"
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	47	apply (rule arg_cong)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	48	back
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	49	apply simp
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	50	apply (thin_tac "eqvt ka")
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	51	apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	52	apply (subgoal_tac "Abs c (CPS1_CPS2_sumC (Inr (M, c~))) = Abs a (CPS1_CPS2_sumC (Inr (M, a~)))")
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	53	prefer 2
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	54	apply (simp add: Abs1_eq_iff')
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	55	apply (case_tac "c = a")
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	56	apply simp_all[2]
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	57	apply rule
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	58	apply (simp add: eqvt_at_def)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	59	apply (simp add: swap_fresh_fresh fresh_Pair_elim)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	60	apply (erule fresh_eqvt_at)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	61	apply (simp add: supp_Inr finite_supp)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	62	apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	63	apply (subgoal_tac "Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Abs a (CPS1_CPS2_sumC (Inr (Ma, a~)))")
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	64	prefer 2
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	65	apply (simp add: Abs1_eq_iff')
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	66	apply (case_tac "ca = a")
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	67	apply simp_all[2]
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	68	apply rule
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	69	apply (simp add: eqvt_at_def)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	70	apply (simp add: swap_fresh_fresh fresh_Pair_elim)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	71	apply (erule fresh_eqvt_at)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	72	apply (simp add: supp_Inr finite_supp)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	73	apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	74	apply (simp only: )
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	75	apply (erule Abs_lst1_fcb)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	76	apply (simp add: Abs_fresh_iff)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	77	apply (drule sym)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	78	apply (simp only:)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	79	apply (simp add: Abs_fresh_iff lt.fresh)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	80	apply clarify
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	81	apply (erule fresh_eqvt_at)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	82	apply (simp add: supp_Inr finite_supp)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	83	apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	84	apply (drule sym)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	85	apply (drule sym)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	86	apply (drule sym)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	87	apply (simp only:)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	88	apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (M, a~))) = Abs c (CPS1_CPS2_sumC (Inr (M, c~)))")
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	89	apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))")
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	90	apply (thin_tac "atom a \<sharp> (c, ca, x, xa, M, Ma)")
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	91	apply (simp add: fresh_Pair_elim)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	92	apply (subst iffD1[OF meta_eq_to_obj_eq[OF eqvt_at_def]])
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	93	back
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	94	back
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	95	back
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	96	apply assumption
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	97	apply (simp add: Abs1_eq_iff' fresh_Pair_elim fresh_at_base swap_fresh_fresh lt.fresh)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	98	apply (case_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> c = ca")
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	99	apply simp_all[3]
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	100	apply rule
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	101	apply (case_tac "c = xa")
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	102	apply simp_all[2]
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	103	apply (simp add: eqvt_at_def)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	104	apply clarify
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	105	apply (smt flip_def permute_flip_at permute_swap_cancel swap_fresh_fresh)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	106	apply (simp add: eqvt_at_def)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	107	apply clarify
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	108	apply (smt atom_eq_iff atom_eqvt flip_def fresh_eqvt permute_flip_at permute_swap_cancel swap_at_base_simps(3) swap_fresh_fresh)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	109	apply (case_tac "c = xa")
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	110	apply simp
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	111	apply (subgoal_tac "((ca \<leftrightarrow> x) \<bullet> (atom x)) \<sharp> (ca \<leftrightarrow> x) \<bullet> CPS1_CPS2_sumC (Inr (Ma, ca~))")
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	112	apply (simp add: atom_eqvt eqvt_at_def)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	113	apply (simp add: flip_fresh_fresh)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	114	apply (subst fresh_permute_iff)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	115	apply (erule fresh_eqvt_at)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	116	apply (simp add: supp_Inr finite_supp)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	117	apply (simp add: fresh_Inr lt.fresh fresh_at_base fresh_Pair)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	118	apply simp
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	119	apply clarify
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	120	apply (subgoal_tac "atom ca \<sharp> (atom x \<rightleftharpoons> atom xa) \<bullet> CPS1_CPS2_sumC (Inr (M, c~))")
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	121	apply (simp add: eqvt_at_def)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	122	apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> atom ca \<sharp> CPS1_CPS2_sumC (Inr (M, c~))")
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	123	apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	124	apply (erule fresh_eqvt_at)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	125	apply (simp add: finite_supp supp_Inr)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	126	apply (simp add: fresh_Inr fresh_Pair lt.fresh)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	127	apply rule
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	128	apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	129	apply (simp add: fresh_def supp_at_base)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	130	apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3))
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	131	--"-"
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	132	apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	133	apply (subgoal_tac "Abs c (CPS1_CPS2_sumC (Inr (M, c~))) = Abs a (CPS1_CPS2_sumC (Inr (M, a~)))")
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	134	prefer 2
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	135	apply (simp add: Abs1_eq_iff')
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	136	apply (case_tac "c = a")
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	137	apply simp_all[2]
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	138	apply rule
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	139	apply (simp add: eqvt_at_def)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	140	apply (simp add: swap_fresh_fresh fresh_Pair_elim)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	141	apply (erule fresh_eqvt_at)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	142	apply (simp add: supp_Inr finite_supp)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	143	apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	144	apply (subgoal_tac "Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Abs a (CPS1_CPS2_sumC (Inr (Ma, a~)))")
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	145	prefer 2
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	146	apply (simp add: Abs1_eq_iff')
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	147	apply (case_tac "ca = a")
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	148	apply simp_all[2]
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	149	apply rule
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	150	apply (simp add: eqvt_at_def)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	151	apply (simp add: swap_fresh_fresh fresh_Pair_elim)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	152	apply (erule fresh_eqvt_at)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	153	apply (simp add: supp_Inr finite_supp)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	154	apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	155	apply (simp only: )
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	156	apply (erule Abs_lst1_fcb)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	157	apply (simp add: Abs_fresh_iff)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	158	apply (drule sym)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	159	apply (simp only:)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	160	apply (simp add: Abs_fresh_iff lt.fresh)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	161	apply clarify
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	162	apply (erule fresh_eqvt_at)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	163	apply (simp add: supp_Inr finite_supp)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	164	apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	165	apply (drule sym)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	166	apply (drule sym)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	167	apply (drule sym)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	168	apply (simp only:)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	169	apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (M, a~))) = Abs c (CPS1_CPS2_sumC (Inr (M, c~)))")
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	170	apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))")
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	171	apply (thin_tac "atom a \<sharp> (c, ca, x, xa, M, Ma)")
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	172	apply (simp add: fresh_Pair_elim)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	173	apply (subst iffD1[OF meta_eq_to_obj_eq[OF eqvt_at_def]])
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	174	back
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	175	back
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	176	back
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	177	apply assumption
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	178	apply (simp add: Abs1_eq_iff' fresh_Pair_elim fresh_at_base swap_fresh_fresh lt.fresh)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	179	apply (case_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> c = ca")
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	180	apply simp_all[3]
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	181	apply rule
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	182	apply (case_tac "c = xa")
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	183	apply simp_all[2]
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	184	apply (simp add: eqvt_at_def)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	185	apply clarify
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	186	apply (smt flip_def permute_flip_at permute_swap_cancel swap_fresh_fresh)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	187	apply (simp add: eqvt_at_def)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	188	apply clarify
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	189	apply (smt atom_eq_iff atom_eqvt flip_def fresh_eqvt permute_flip_at permute_swap_cancel swap_at_base_simps(3) swap_fresh_fresh)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	190	apply (case_tac "c = xa")
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	191	apply simp
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	192	apply (subgoal_tac "((ca \<leftrightarrow> x) \<bullet> (atom x)) \<sharp> (ca \<leftrightarrow> x) \<bullet> CPS1_CPS2_sumC (Inr (Ma, ca~))")
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	193	apply (simp add: atom_eqvt eqvt_at_def)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	194	apply (simp add: flip_fresh_fresh)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	195	apply (subst fresh_permute_iff)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	196	apply (erule fresh_eqvt_at)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	197	apply (simp add: supp_Inr finite_supp)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	198	apply (simp add: fresh_Inr lt.fresh fresh_at_base fresh_Pair)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	199	apply simp
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	200	apply clarify
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	201	apply (subgoal_tac "atom ca \<sharp> (atom x \<rightleftharpoons> atom xa) \<bullet> CPS1_CPS2_sumC (Inr (M, c~))")
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	202	apply (simp add: eqvt_at_def)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	203	apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> atom ca \<sharp> CPS1_CPS2_sumC (Inr (M, c~))")
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	204	apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	205	apply (erule fresh_eqvt_at)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	206	apply (simp add: finite_supp supp_Inr)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	207	apply (simp add: fresh_Inr fresh_Pair lt.fresh)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	208	apply rule
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	209	apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	210	apply (simp add: fresh_def supp_at_base)
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	211	apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3))
2865 a30d0bb76869 CPS3 can be defined with eqvt_rhs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2861 diff changeset	212	done
2861 5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	213
2865 a30d0bb76869 CPS3 can be defined with eqvt_rhs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2861 diff changeset	214	termination
a30d0bb76869 CPS3 can be defined with eqvt_rhs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2861 diff changeset	215	by lexicographic_order
2861 5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	216
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	217	definition psi:: "lt => lt"
2882 186ec672cc51 Minor Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2866 diff changeset	218	where [simp]: "psi V == V*(\<lambda>x. x)"
2861 5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	219
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	220	section {* Simple consequence of CPS *}
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	221
2882 186ec672cc51 Minor Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2866 diff changeset	222	lemma [simp]: "eqvt (\<lambda>x\<Colon>lt. x)"
186ec672cc51 Minor Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2866 diff changeset	223	by (simp add: eqvt_def eqvt_bound eqvt_lambda)
186ec672cc51 Minor Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2866 diff changeset	224
2861 5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	225	lemma value_eq1 : "isValue V \<Longrightarrow> eqvt k \<Longrightarrow> V*k = k (psi V)"
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	226	apply (cases V rule: lt.exhaust)
2882 186ec672cc51 Minor Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2866 diff changeset	227	apply simp_all
2861 5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	228	apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
2882 186ec672cc51 Minor Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2866 diff changeset	229	apply simp
2861 5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	230	done
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	231
2882 186ec672cc51 Minor Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2866 diff changeset	232	lemma value_eq2 : "isValue V \<Longrightarrow> V^K = K $ (psi V)"
186ec672cc51 Minor Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2866 diff changeset	233	apply (cases V rule: lt.exhaust)
186ec672cc51 Minor Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2866 diff changeset	234	apply simp_all
186ec672cc51 Minor Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2866 diff changeset	235	apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
186ec672cc51 Minor Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2866 diff changeset	236	apply simp
186ec672cc51 Minor Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2866 diff changeset	237	done
186ec672cc51 Minor Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2866 diff changeset	238
186ec672cc51 Minor Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2866 diff changeset	239	lemma value_eq3' : "~isValue M \<Longrightarrow> eqvt k \<Longrightarrow> M*k = (M^(Abs n (k (Var n))))"
186ec672cc51 Minor Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2866 diff changeset	240	by (cases M rule: lt.exhaust) auto
186ec672cc51 Minor Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2866 diff changeset	241
186ec672cc51 Minor Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2866 diff changeset	242
186ec672cc51 Minor Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2866 diff changeset	243
2861 5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	244	end
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	245
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	246
5635a968fd3f Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	247

author	Christian Urban <urbanc@in.tum.de>
	Thu, 23 Jun 2011 12:28:25 +0100 (2011-06-23)
changeset 2889	0435c4dfd6f6
parent 2882	186ec672cc51
child 2895	65efa1c7563c
permissions	-rw-r--r--