nominal2: Nominal/Ex/Lambda_F_T.thy@2f5ce0ecbf31 (annotated)

2812 1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	1	theory Lambda
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	2	imports "../Nominal2"
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	3	begin
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	4
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	5	atom_decl name
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	6
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	7	nominal_datatype lam =
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	8	Var "name"
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	9	\| App "lam" "lam"
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	10	\| Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100)
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	11
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	12	lemma Abs1_eq_fdest:
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	13	fixes x y :: "'a :: at_base"
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	14	and S T :: "'b :: fs"
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	15	assumes "(Abs_lst [atom x] T) = (Abs_lst [atom y] S)"
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	16	and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> atom x \<sharp> f x T"
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	17	and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> atom y \<sharp> f x T"
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	18	and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> T = S \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> (f x T) = f y S"
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	19	and "sort_of (atom x) = sort_of (atom y)"
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	20	shows "f x T = f y S"
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	21	using assms apply -
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	22	apply (subst (asm) Abs1_eq_iff')
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	23	apply simp_all
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	24	apply (elim conjE disjE)
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	25	apply simp
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	26	apply(rule trans)
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	27	apply (rule_tac p="(atom x \<rightleftharpoons> atom y)" in supp_perm_eq[symmetric])
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	28	apply(rule fresh_star_supp_conv)
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	29	apply(simp add: supp_swap fresh_star_def)
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	30	apply(simp add: swap_commute)
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	31	done
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	32
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	33	lemma fresh_fun_eqvt_app3:
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	34	assumes a: "eqvt f"
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	35	and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z"
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	36	shows "a \<sharp> f x y z"
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	37	using fresh_fun_eqvt_app[OF a b(1)] a b
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	38	by (metis fresh_fun_app)
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	39
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	40	lemma fresh_fun_eqvt_app4:
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	41	assumes a: "eqvt f"
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	42	and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z" "a \<sharp> w"
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	43	shows "a \<sharp> f x y z w"
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	44	using fresh_fun_eqvt_app[OF a b(1)] a b
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	45	by (metis fresh_fun_app)
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	46
2817 2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	47	lemma the_default_pty:
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	48	assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	49	and unique: "\<exists>!y. G x y"
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	50	and pty: "\<And>x y. G x y \<Longrightarrow> P x y"
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	51	shows "P x (f x)"
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	52	apply(subst f_def)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	53	apply (rule ex1E[OF unique])
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	54	apply (subst THE_default1_equality[OF unique])
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	55	apply assumption
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	56	apply (rule pty)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	57	apply assumption
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	58	done
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	59
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	60	locale test =
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	61	fixes f1::"name \<Rightarrow> name list \<Rightarrow> ('a::pt)"
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	62	and f2::"lam \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> name list \<Rightarrow> ('a::pt)"
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	63	and f3::"name \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> name list \<Rightarrow> ('a::pt)"
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	64	assumes fs: "finite (supp (f1, f2, f3))"
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	65	and eq: "eqvt f1" "eqvt f2" "eqvt f3"
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	66	and fcb1: "\<And>l n. atom ` set l \<sharp>* f1 n l"
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	67	and fcb2: "\<And>l t1 t2 r1 r2. atom ` set l \<sharp>* (r1, r2) \<Longrightarrow> atom ` set l \<sharp>* f2 t1 t2 r1 r2 l"
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	68	and fcb3: "\<And>t l r. atom ` set (x # l) \<sharp>* r \<Longrightarrow> atom ` set (x # l) \<sharp>* f3 x t r l"
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	69	begin
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	70
2812 1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	71	nominal_primrec
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	72	f
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	73	where
2817 2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	74	"f (Var x) l = f1 x l"
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	75	\| "f (App t1 t2) l = f2 t1 t2 (f t1 l) (f t2 l) l"
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	76	\| "atom x \<sharp> l \<Longrightarrow> (f (Lam [x].t) l) = f3 x t (f t (x # l)) l"
2812 1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	77	apply (simp add: eqvt_def f_graph_def)
2817 2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	78	apply (rule, perm_simp)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	79	apply (simp only: eq[unfolded eqvt_def])
2812 1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	80	apply(case_tac x)
2817 2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	81	apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
2812 1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	82	apply(auto simp add: fresh_star_def)
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	83	apply(erule Abs1_eq_fdest)
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	84	defer
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	85	apply simp_all
2817 2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	86	apply (rule fresh_fun_eqvt_app4[OF eq(3)])
2812 1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	87	apply (simp add: fresh_at_base)
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	88	apply assumption
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	89	apply (erule fresh_eqvt_at)
2817 2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	90	apply (simp add: finite_supp)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	91	apply (simp add: fresh_Pair fresh_Cons fresh_at_base)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	92	apply assumption
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	93	apply (subgoal_tac "\<And>p y r l. p \<bullet> (f3 x y r l) = f3 (p \<bullet> x) (p \<bullet> y) (p \<bullet> r) (p \<bullet> l)")
2812 1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	94	apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> la = la")
2817 2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	95	apply (simp add: eqvt_at_def)
2812 1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	96	apply (simp add: swap_fresh_fresh)
2817 2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	97	apply (simp add: permute_fun_app_eq eq[unfolded eqvt_def])
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	98	apply (subgoal_tac "atom ` set (x # la) \<sharp>* f3 x t (f_sumC (t, x # la)) la")
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	99	apply (simp add: fresh_star_def)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	100	apply (rule fcb3)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	101	apply (rule_tac x="x # la" in meta_spec)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	102	apply (thin_tac "eqvt_at f_sumC (t, x # la)")
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	103	apply (thin_tac "atom x \<sharp> la")
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	104	apply (thin_tac "atom xa \<sharp> la")
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	105	apply (thin_tac "x \<noteq> xa")
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	106	apply (thin_tac "atom xa \<sharp> t")
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	107	apply (subgoal_tac "atom ` set (snd (t, xb)) \<sharp>* f_sumC (t, xb)")
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	108	apply simp
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	109	apply (rule_tac x="(t, xb)" in meta_spec)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	110	apply (simp only: triv_forall_equality)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	111	--"We start induction on the graph. We need the 2nd subgoal in the first one"
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	112	apply (subgoal_tac "\<And>x y. f_graph x y \<Longrightarrow> atom ` set (snd x) \<sharp>* y")
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	113	apply (rule the_default_pty[OF f_sumC_def])
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	114	prefer 2
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	115	apply blast
2812 1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	116	prefer 2
2817 2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	117	apply (erule f_graph.induct)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	118	apply (simp add: fcb1)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	119	apply (simp add: fcb2 fresh_star_Pair)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	120	apply (simp only: snd_conv)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	121	apply (subgoal_tac "atom ` set (xa # l) \<sharp>* f3 xa t (f_sum (t, xa # l)) l")
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	122	apply (simp add: fresh_star_def)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	123	apply (rule fcb3)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	124	apply assumption
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	125	--"We'd like to do the proof with this property"
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	126	apply (case_tac xc)
2812 1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	127	apply simp
2817 2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	128	apply (rule_tac lam="a" and c="b" in lam.strong_induct)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	129	apply (rule_tac a="f1 name c" in ex1I)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	130	apply (rule f_graph.intros)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	131	apply (erule f_graph.cases)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	132	apply simp_all[3]
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	133	apply (drule_tac x="c" in meta_spec)+
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	134	apply (erule ex1E)+
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	135	apply (subgoal_tac "f_graph (lam1, c) (f_sumC (lam1, c))")
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	136	apply (subgoal_tac "f_graph (lam2, c) (f_sumC (lam2, c))")
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	137	apply (rule_tac a="f2 lam1 lam2 (f_sumC (lam1, c)) (f_sumC (lam2, c)) c" in ex1I)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	138	apply (rule_tac f_graph.intros(2))
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	139	apply assumption+
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	140	apply (rotate_tac 8)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	141	apply (erule f_graph.cases)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	142	apply simp
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	143	apply auto[1]
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	144	apply metis
2812 1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	145	apply simp
2817 2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	146	apply (simp add: f_sumC_def)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	147	apply (rule THE_defaultI')
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	148	apply metis
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	149	apply (simp add: f_sumC_def)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	150	apply (rule THE_defaultI')
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	151	apply metis
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	152	--"Only the Lambda case left"
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	153	apply (subgoal_tac "f_graph (lam, (name # c)) (f_sumC (lam, (name # c)))")
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	154	prefer 2
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	155	apply (simp add: f_sumC_def)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	156	apply (rule THE_defaultI')
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	157	apply assumption
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	158	apply (rule_tac a="f3 name lam (f_sumC (lam, name # c)) c" in ex1I)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	159	apply (rule f_graph.intros(3))
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	160	apply (simp add: fresh_star_def)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	161	apply assumption
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	162	apply (rotate_tac -1)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	163	apply (erule f_graph.cases)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	164	apply simp_all[2]
2812 1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	165	apply simp
2817 2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	166	apply auto[1]
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	167	apply (subgoal_tac "f_sumC (lam, name # l) = f_sum (lam, name # l)")
2812 1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	168	apply simp
2817 2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	169	apply (rule sym)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	170	apply (erule Abs1_eq_fdest)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	171	apply (subgoal_tac "atom ` set (name # l) \<sharp>* f3 name lam (f_sum (lam, name # l)) l")
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	172	apply (simp add: fresh_star_def)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	173	apply (rule fcb3)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	174	apply metis
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	175	apply (rule fresh_fun_eqvt_app4[OF eq(3)])
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	176	apply (simp add: fresh_at_base)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	177	apply assumption
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	178	defer --"eqvt_at f_sumC"
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	179	apply assumption
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	180	apply (subgoal_tac "\<And>p y r l. p \<bullet> (f3 name y r l) = f3 (p \<bullet> name) (p \<bullet> y) (p \<bullet> r) (p \<bullet> l)")
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	181	apply (subgoal_tac "(atom name \<rightleftharpoons> atom xa) \<bullet> l = l")
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	182	apply (simp add: eq[unfolded eqvt_def])
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	183	defer --"eqvt_at f_sumC"
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	184	apply (metis fresh_star_insert swap_fresh_fresh)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	185	apply (simp add: permute_fun_app_eq eq[unfolded eqvt_def])
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	186	apply simp
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	187	sorry
2812 1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	188
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	189	termination
2817 2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	190	by (relation "measure (\<lambda>(x,_). size x)") (auto simp add: lam.size)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	191
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	192	end
2812 1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	193
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	194	section {* Locally Nameless Terms *}
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	195
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	196	nominal_datatype ln =
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	197	LNBnd nat
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	198	\| LNVar name
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	199	\| LNApp ln ln
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	200	\| LNLam ln
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	201
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	202	fun
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	203	lookup :: "name list \<Rightarrow> nat \<Rightarrow> name \<Rightarrow> ln"
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	204	where
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	205	"lookup [] n x = LNVar x"
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	206	\| "lookup (y # ys) n x = (if x = y then LNBnd n else (lookup ys (n + 1) x))"
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	207
2817 2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	208	lemma lookup_eqvt[eqvt]:
2812 1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	209	shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	210	by (induct xs arbitrary: n) (simp_all add: permute_pure)
1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	211
2817 2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	212	lemma fresh_at_list: "atom x \<sharp> xs \<longleftrightarrow> x \<notin> set xs"
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	213	unfolding fresh_def supp_set[symmetric]
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	214	apply (induct xs)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	215	apply (simp add: supp_set_empty)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	216	apply simp
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	217	apply auto
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	218	apply (simp_all add: insert_absorb UnI2 finite_set supp_of_finite_insert supp_at_base)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	219	done
2812 1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	220
2817 2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	221	interpretation trans: test
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	222	"%x l. lookup l 0 x"
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	223	"%t1 t2 r1 r2 l. LNApp r1 r2"
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	224	"%n t r l. LNLam r"
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	225	apply default
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	226	apply (auto simp add: pure_fresh supp_Pair)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	227	apply (simp_all add: fresh_def supp_def permute_fun_def permute_pure lookup_eqvt)[3]
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	228	apply (simp_all add: eqvt_def permute_fun_def permute_pure lookup_eqvt)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	229	apply (simp add: fresh_star_def)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	230	apply (rule_tac x="0 :: nat" in spec)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	231	apply (induct_tac l)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	232	apply (simp add: ln.fresh pure_fresh)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	233	apply (auto simp add: ln.fresh pure_fresh)[1]
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	234	apply (case_tac "a \<in> set list")
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	235	apply simp
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	236	apply (rule_tac f="lookup" in fresh_fun_eqvt_app3)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	237	unfolding eqvt_def
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	238	apply rule
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	239	using eqvts_raw(35)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	240	apply auto[1]
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	241	apply (simp add: fresh_at_list)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	242	apply (simp add: pure_fresh)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	243	apply (simp add: fresh_at_base)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	244	apply (simp add: fresh_star_Pair fresh_star_def ln.fresh)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	245	apply (simp add: fresh_star_def ln.fresh)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	246	done
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	247
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	248	thm trans.f.simps
2812 1135a14927bb F for lambda used to define translation to locally nameless Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	249
2815 812cfadeb8b7 FiniteSupp precondition in the function is enough to get rid of completeness obligationss Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2812 diff changeset	250	lemma lam_strong_exhaust2:
812cfadeb8b7 FiniteSupp precondition in the function is enough to get rid of completeness obligationss Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2812 diff changeset	251	"\<lbrakk>\<And>name. y = Var name \<Longrightarrow> P;
812cfadeb8b7 FiniteSupp precondition in the function is enough to get rid of completeness obligationss Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2812 diff changeset	252	\<And>lam1 lam2. y = App lam1 lam2 \<Longrightarrow> P;
812cfadeb8b7 FiniteSupp precondition in the function is enough to get rid of completeness obligationss Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2812 diff changeset	253	\<And>name lam. \<lbrakk>{atom name} \<sharp>* c; y = Lam [name]. lam\<rbrakk> \<Longrightarrow> P;
812cfadeb8b7 FiniteSupp precondition in the function is enough to get rid of completeness obligationss Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2812 diff changeset	254	finite (supp c)\<rbrakk>
812cfadeb8b7 FiniteSupp precondition in the function is enough to get rid of completeness obligationss Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2812 diff changeset	255	\<Longrightarrow> P"
812cfadeb8b7 FiniteSupp precondition in the function is enough to get rid of completeness obligationss Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2812 diff changeset	256	sorry
812cfadeb8b7 FiniteSupp precondition in the function is enough to get rid of completeness obligationss Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2812 diff changeset	257
812cfadeb8b7 FiniteSupp precondition in the function is enough to get rid of completeness obligationss Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2812 diff changeset	258	nominal_primrec
812cfadeb8b7 FiniteSupp precondition in the function is enough to get rid of completeness obligationss Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2812 diff changeset	259	g
812cfadeb8b7 FiniteSupp precondition in the function is enough to get rid of completeness obligationss Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2812 diff changeset	260	where
812cfadeb8b7 FiniteSupp precondition in the function is enough to get rid of completeness obligationss Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2812 diff changeset	261	"(~finite (supp (g1, g2, g3))) \<Longrightarrow> g g1 g2 g3 t = t"
812cfadeb8b7 FiniteSupp precondition in the function is enough to get rid of completeness obligationss Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2812 diff changeset	262	\| "finite (supp (g1, g2, g3)) \<Longrightarrow> g g1 g2 g3 (Var x) = g1 x"
812cfadeb8b7 FiniteSupp precondition in the function is enough to get rid of completeness obligationss Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2812 diff changeset	263	\| "finite (supp (g1, g2, g3)) \<Longrightarrow> g g1 g2 g3 (App t1 t2) = g2 t1 t2 (g g1 g2 g3 t1) (g g1 g2 g3 t2)"
812cfadeb8b7 FiniteSupp precondition in the function is enough to get rid of completeness obligationss Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2812 diff changeset	264	\| "finite (supp (g1, g2, g3)) \<Longrightarrow> atom x \<sharp> (g1,g2,g3) \<Longrightarrow> (g g1 g2 g3 (Lam [x].t)) = g3 x t (g g1 g2 g3 t)"
812cfadeb8b7 FiniteSupp precondition in the function is enough to get rid of completeness obligationss Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2812 diff changeset	265	apply (simp add: eqvt_def g_graph_def)
812cfadeb8b7 FiniteSupp precondition in the function is enough to get rid of completeness obligationss Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2812 diff changeset	266	apply (rule, perm_simp, rule)
2817 2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	267	apply simp_all
2815 812cfadeb8b7 FiniteSupp precondition in the function is enough to get rid of completeness obligationss Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2812 diff changeset	268	apply (case_tac x)
812cfadeb8b7 FiniteSupp precondition in the function is enough to get rid of completeness obligationss Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2812 diff changeset	269	apply (case_tac "finite (supp (a, b, c))")
812cfadeb8b7 FiniteSupp precondition in the function is enough to get rid of completeness obligationss Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2812 diff changeset	270	prefer 2
812cfadeb8b7 FiniteSupp precondition in the function is enough to get rid of completeness obligationss Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2812 diff changeset	271	apply simp
812cfadeb8b7 FiniteSupp precondition in the function is enough to get rid of completeness obligationss Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2812 diff changeset	272	apply(rule_tac y="d" and c="(a,b,c)" in lam_strong_exhaust2)
2817 2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	273	apply auto
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	274	apply blast
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	275	apply (simp add: Abs1_eq_iff fresh_star_def)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	276	sorry
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	277
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	278	termination
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	279	by (relation "measure (\<lambda>(_,_,_,t). size t)") (simp_all add: lam.size)
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	280
2f5ce0ecbf31 Trying the induction on the graph Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2815 diff changeset	281	end

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Sat, 04 Jun 2011 14:50:57 +0900
changeset 2817	2f5ce0ecbf31
parent 2815	812cfadeb8b7
child 2823	e92ce4d110f4
permissions	-rw-r--r--