--- a/src/HOL/Nominal/Examples/Iteration.thy Tue May 16 13:05:37 2006 +0200
+++ b/src/HOL/Nominal/Examples/Iteration.thy Tue May 16 14:11:39 2006 +0200
@@ -4,6 +4,7 @@
imports "../Nominal"
begin
+
atom_decl name
nominal_datatype lam = Var "name"
@@ -15,402 +16,189 @@
'a f3_ty = "name\<Rightarrow>'a\<Rightarrow>('a::pt_name)"
consts
- it :: "'a f1_ty \<Rightarrow> 'a f2_ty \<Rightarrow> 'a f3_ty \<Rightarrow> (lam \<times> (name prm \<Rightarrow> 'a::pt_name)) set"
+ it :: "'a f1_ty \<Rightarrow> 'a f2_ty \<Rightarrow> 'a f3_ty \<Rightarrow> (lam \<times> 'a::pt_name) set"
inductive "it f1 f2 f3"
intros
-it1: "(Var a,\<lambda>pi. f1(pi\<bullet>a)) \<in> it f1 f2 f3"
-it2: "\<lbrakk>(t1,r1) \<in> it f1 f2 f3; (t2,r2) \<in> it f1 f2 f3\<rbrakk> \<Longrightarrow>
- (App t1 t2,\<lambda>pi. f2 (r1 pi) (r2 pi)) \<in> it f1 f2 f3"
-it3: "(t,r) \<in> it f1 f2 f3 \<Longrightarrow> (Lam [a].t,\<lambda>pi. fresh_fun (\<lambda>a'. f3 a' (r (pi@[(a,a')])))) \<in> it f1 f2 f3"
+it1: "(Var a, f1 a) \<in> it f1 f2 f3"
+it2: "\<lbrakk>(t1,r1) \<in> it f1 f2 f3; (t2,r2) \<in> it f1 f2 f3\<rbrakk> \<Longrightarrow> (App t1 t2, f2 r1 r2) \<in> it f1 f2 f3"
+it3: "\<lbrakk>a\<sharp>(f1,f2,f3); (t,r) \<in> it f1 f2 f3\<rbrakk> \<Longrightarrow> (Lam [a].t,f3 a r) \<in> it f1 f2 f3"
-constdefs
- itfun' :: "'a f1_ty \<Rightarrow> 'a f2_ty \<Rightarrow> 'a f3_ty \<Rightarrow> lam \<Rightarrow> name prm \<Rightarrow> ('a::pt_name)"
- "itfun' f1 f2 f3 t \<equiv> (THE y. (t,y) \<in> it f1 f2 f3)"
+lemma it_equiv:
+ fixes pi::"name prm"
+ assumes a: "(t,r) \<in> it f1 f2 f3"
+ shows "(pi\<bullet>t,pi\<bullet>r) \<in> it (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3)"
+ using a
+ apply(induct)
+ apply(perm_simp | auto intro!: it.intros simp add: fresh_right)+
+ done
- itfun :: "'a f1_ty \<Rightarrow> 'a f2_ty \<Rightarrow> 'a f3_ty \<Rightarrow> lam \<Rightarrow> ('a::pt_name)"
- "itfun f1 f2 f3 t \<equiv> itfun' f1 f2 f3 t ([]::name prm)"
+lemma it_fin_supp:
+ assumes f: "finite ((supp (f1,f2,f3))::name set)"
+ and a: "(t,r) \<in> it f1 f2 f3"
+ shows "finite ((supp r)::name set)"
+ using a f
+ apply(induct)
+ apply(finite_guess, simp add: supp_prod fs_name1)+
+ done
lemma it_total:
- shows "\<exists>r. (t,r) \<in> it f1 f2 f3"
- by (induct t rule: lam.induct_weak, auto intro: it.intros)
-
-lemma it_prm_eq:
- assumes a: "(t,y) \<in> it f1 f2 f3" and b: "pi1 \<triangleq> pi2"
- shows "y pi1 = y pi2"
-using a b
-apply(induct fixing: pi1 pi2)
-apply(auto simp add: pt3[OF pt_name_inst])
-apply(rule_tac f="fresh_fun" in arg_cong)
-apply(auto simp add: expand_fun_eq)
-apply(drule_tac x="pi1@[(a,x)]" in meta_spec)
-apply(drule_tac x="pi2@[(a,x)]" in meta_spec)
-apply(force simp add: prm_eq_def pt2[OF pt_name_inst])
+ assumes a: "finite ((supp (f1,f2,f3))::name set)"
+ and b: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
+ shows "\<exists>r. (t,r)\<in>it f1 f2 f3"
+apply(rule_tac lam.induct'[of "\<lambda>_. (supp (f1,f2,f3))::name set"
+ "\<lambda>z. \<lambda>t. \<exists>r. (t,r)\<in>it f1 f2 f3", simplified])
+apply(fold fresh_def)
+apply(auto intro: it.intros a)
done
-lemma f3_freshness_conditions:
- fixes f3::"('a::pt_name) f3_ty"
- and y ::"name prm \<Rightarrow> 'a::pt_name"
- assumes a: "finite ((supp f3)::name set)"
- and b: "finite ((supp y)::name set)"
- and c: "\<exists>a. a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
- shows "\<exists>a''. a''\<sharp>(\<lambda>a'. f3 a' (y (pi1@[(a,a')]@pi2))) \<and> a''\<sharp>(\<lambda>a'. f3 a' (y (pi1@[(a,a')]@pi2))) a''"
-proof -
- from c obtain a' where d0: "a'\<sharp>f3" and d1: "\<forall>(y::'a::pt_name). a'\<sharp>f3 a' y" by force
- have "\<exists>(a''::name). a''\<sharp>(f3,a,a',pi1,pi2,y)"
- by (rule at_exists_fresh[OF at_name_inst], simp add: supp_prod fs_name1 a b)
- then obtain a'' where d2: "a''\<sharp>f3" and d3: "a''\<noteq>a'" and d3b: "a''\<sharp>(f3,a,pi1,pi2,y)"
- by (auto simp add: fresh_prod at_fresh[OF at_name_inst])
- have d3c: "a''\<notin>((supp (f3,a,pi1,pi2,y))::name set)" using d3b by (simp add: fresh_def)
- have d4: "a''\<sharp>f3 a'' (y (pi1@[(a,a'')]@pi2))"
- proof -
- have d5: "[(a'',a')]\<bullet>f3 = f3" using d2 d0 by perm_simp
- from d1 have "\<forall>(y::'a::pt_name). ([(a'',a')]\<bullet>a')\<sharp>([(a'',a')]\<bullet>(f3 a' y))" by (simp add: fresh_eqvt)
- hence "\<forall>(y::'a::pt_name). a''\<sharp>(f3 a'' ([(a'',a')]\<bullet>y))" using d3 d5 by (perm_simp add: calc_atm)
- hence "a''\<sharp>(f3 a'' ([(a'',a')]\<bullet>((rev [(a'',a')])\<bullet>(y (pi1@[(a,a'')]@pi2)))))" by force
- thus ?thesis by perm_simp
- qed
- have d6: "a''\<sharp>(\<lambda>a'. f3 a' (y (pi1@[(a,a')]@pi2)))"
- proof -
- from a b have d7: "finite ((supp (f3,a,pi1,pi2,y))::name set)" by (simp add: supp_prod fs_name1)
- have e: "((supp (f3,a,pi1,pi2,y))::name set) supports (\<lambda>a'. f3 a' (y (pi1@[(a,a')]@pi2)))"
- by (supports_simp add: perm_append)
- from e d7 d3c show ?thesis by (rule supports_fresh)
- qed
- from d6 d4 show ?thesis by force
-qed
-
-lemma f3_freshness_conditions_simple:
- fixes f3::"('a::pt_name) f3_ty"
- and y ::"name prm \<Rightarrow> 'a::pt_name"
- assumes a: "finite ((supp f3)::name set)"
- and b: "finite ((supp y)::name set)"
- and c: "\<exists>a. a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
- shows "\<exists>a''. a''\<sharp>(\<lambda>a'. f3 a' (y (pi@[(a,a')]))) \<and> a''\<sharp>(\<lambda>a'. f3 a' (y (pi@[(a,a')]))) a''"
-using a b c by (simp add: f3_freshness_conditions[of _ _ _ _ "[]",simplified])
-
-lemma it_fin_supp:
- assumes f: "finite ((supp (f1,f2,f3))::name set)"
- and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(r::'a::pt_name). a\<sharp>f3 a r)"
- and a: "(t,r) \<in> it f1 f2 f3"
- shows "finite ((supp r)::name set)"
-using a
-proof (induct)
- case it1 thus ?case using f by (finite_guess add: supp_prod fs_name1)
-next
- case it2 thus ?case using f by (finite_guess add: supp_prod fs_name1)
-next
- case (it3 c r t)
- have ih: "finite ((supp r)::name set)" by fact
- let ?g' = "\<lambda>pi a'. f3 a' (r (pi@[(c,a')]))" --"helper function"
- have fact1: "\<forall>pi. finite ((supp (?g' pi))::name set)" using f ih
- by (rule_tac allI, finite_guess add: perm_append supp_prod fs_name1)
- have fact2: "\<forall>pi. \<exists>(a''::name). a''\<sharp>(?g' pi) \<and> a''\<sharp>((?g' pi) a'')"
- proof
- fix pi::"name prm"
- show "\<exists>(a''::name). a''\<sharp>(?g' pi) \<and> a''\<sharp>((?g' pi) a'')" using f c ih
- by (rule_tac f3_freshness_conditions_simple, simp_all add: supp_prod)
- qed
- show ?case using fact1 fact2 ih f by (finite_guess add: fresh_fun_eqvt perm_append supp_prod fs_name1)
-qed
-
-lemma it_trans: "\<lbrakk>(t,r)\<in>rec f1 f2 f3; r=r'\<rbrakk> \<Longrightarrow> (t,r')\<in>rec f1 f2 f3" by simp
-
-lemma it_perm_aux:
- assumes f: "finite ((supp (f1,f2,f3))::name set)"
- and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
- and a: "(t,y) \<in> it f1 f2 f3"
- shows "(pi1\<bullet>t, \<lambda>pi2. y (pi2@pi1)) \<in> it f1 f2 f3"
-using a
-proof (induct)
- case (it1 c) show ?case by (auto simp add: pt_name2, rule it.intros)
-next
- case (it2 t1 t2 r1 r2) thus ?case by (auto intro: it.intros)
-next
- case (it3 c r t)
- let ?g = "\<lambda>pi' a'. f3 a' (r (pi'@[(pi1\<bullet>c,a')]@pi1))"
- and ?h = "\<lambda>pi' a'. f3 a' (r ((pi'@pi1)@[(c,a')]))"
- have ih': "(t,r) \<in> it f1 f2 f3" by fact
- hence fin_r: "finite ((supp r)::name set)" using f c by (auto intro: it_fin_supp)
- have ih: "(pi1\<bullet>t,\<lambda>pi2. r (pi2@pi1)) \<in> it f1 f2 f3" by fact
- hence "(Lam [(pi1\<bullet>c)].(pi1\<bullet>t),\<lambda>pi'. fresh_fun (?g pi')) \<in> it f1 f2 f3"
- by (auto intro: it_trans it.intros)
- moreover
- have "\<forall>pi'. (fresh_fun (?g pi')) = (fresh_fun (?h pi'))"
- proof
- fix pi'::"name prm"
- have fin_g: "finite ((supp (?g pi'))::name set)"
- using f fin_r by (finite_guess add: perm_append supp_prod fs_name1)
- have fr_g: "\<exists>(a::name). (a\<sharp>(?g pi')\<and> a\<sharp>(?g pi' a))"
- using f c fin_r by (rule_tac f3_freshness_conditions, simp_all add: supp_prod)
- have fin_h: "finite ((supp (?h pi'))::name set)"
- using f fin_r by (finite_guess add: perm_append supp_prod fs_name1)
- have fr_h: "\<exists>(a::name). (a\<sharp>(?h pi')\<and> a\<sharp>(?h pi' a))"
- using f c fin_r by (rule_tac f3_freshness_conditions_simple, simp_all add: supp_prod)
- show "fresh_fun (?g pi') = fresh_fun (?h pi')"
- proof -
- have "\<exists>(d::name). d\<sharp>(?g pi', ?h pi', pi1)" using fin_g fin_h
- by (rule_tac at_exists_fresh[OF at_name_inst], simp only: supp_prod finite_Un fs_name1, simp)
- then obtain d::"name" where f1: "d\<sharp>?g pi'" and f2: "d\<sharp>?h pi'" and f3: "d\<sharp>(rev pi1)"
- by (auto simp only: fresh_prod fresh_list_rev)
- have "?g pi' d = ?h pi' d"
- proof -
- have "r (pi'@[(pi1\<bullet>c,d)]@pi1) = r ((pi'@pi1)@[(c,d)])" using f3 ih'
- by (auto intro!: it_prm_eq at_prm_eq_append[OF at_name_inst]
- simp only: append_assoc at_ds10[OF at_name_inst])
- then show ?thesis by simp
- qed
- then show "fresh_fun (?g pi') = fresh_fun (?h pi')"
- using f1 fin_g fr_g f2 fin_h fr_h by (simp add: fresh_fun_app[OF pt_name_inst, OF at_name_inst])
- qed
- qed
- hence "(\<lambda>pi'. (fresh_fun (?g pi'))) = (\<lambda>pi'. (fresh_fun (?h pi')))" by (simp add: expand_fun_eq)
- ultimately show ?case by simp
-qed
-
-lemma it_perm:
- assumes f: "finite ((supp (f1,f2,f3))::name set)"
- and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
- and a: "(pi\<bullet>t,y) \<in> it f1 f2 f3"
- shows "(t, \<lambda>pi2. y (pi2@(rev pi))) \<in> it f1 f2 f3"
-proof -
- from a f c have "((rev pi)\<bullet>(pi\<bullet>t),\<lambda>pi2. y (pi2@(rev pi))) \<in> it f1 f2 f3" by (simp add: it_perm_aux)
- thus ?thesis by perm_simp
-qed
-
-lemma it_unique:
- assumes f: "finite ((supp (f1,f2,f3))::name set)"
- and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
- and a: "(t,y) \<in> it f1 f2 f3"
- and b: "(t,y') \<in> it f1 f2 f3"
- shows "y pi = y' pi"
-using a b
-proof (induct fixing: y' pi)
- case (it1 c) thus ?case by (cases, simp_all add: lam.inject)
+lemma it_unique:
+ assumes a: "finite ((supp (f1,f2,f3))::name set)"
+ and b: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
+ and c1: "(t,r)\<in>it f1 f2 f3"
+ and c2: "(t,r')\<in>it f1 f2 f3"
+ shows "r=r'"
+using c1 c2
+proof (induct fixing: r')
+ case it1
+ then show ?case by cases (simp_all add: lam.inject)
next
case (it2 r1 r2 t1 t2)
- with `(App t1 t2, y') \<in> it f1 f2 f3` show ?case
- by (cases, simp_all (no_asm_use) add: lam.inject, force)
+ have ih1: "\<And>r'. (t1,r') \<in> it f1 f2 f3 \<Longrightarrow> r1 = r'" by fact
+ have ih2: "\<And>r'. (t2,r') \<in> it f1 f2 f3 \<Longrightarrow> r2 = r'" by fact
+ have "(App t1 t2, r') \<in>it f1 f2 f3" by fact
+ then show ?case
+ proof cases
+ case it2
+ then show ?thesis using ih1 ih2 by (simp add: lam.inject)
+ qed (simp_all (no_asm_use))
next
- case (it3 c r t r')
- have "(t,r) \<in> it f1 f2 f3" by fact
- hence fin_r: "finite ((supp r)::name set)" using f c by (simp only: it_fin_supp)
- have ih: "\<And>r' pi. (t,r') \<in> it f1 f2 f3 \<Longrightarrow> r pi = r' pi" by fact
- have "(Lam [c].t, r') \<in> it f1 f2 f3" by fact
- then show "fresh_fun (\<lambda>a'. f3 a' (r (pi@[(c,a')]))) = r' pi"
- proof (cases, auto simp add: lam.inject)
- fix a::"name" and t'::"lam" and r''::"name prm\<Rightarrow>'a::pt_name"
- assume i5: "[c].t = [a].t'"
- and i6: "(t',r'') \<in> it f1 f2 f3"
- hence fin_r'': "finite ((supp r'')::name set)" using f c by (auto intro: it_fin_supp)
- let ?g = "\<lambda>a'. f3 a' (r (pi@[(c,a')]))" and ?h = "\<lambda>a'. f3 a' (r'' (pi@[(a,a')]))"
- show "fresh_fun ?g = fresh_fun ?h" using i5
- proof (cases "a=c")
- case True
- have i7: "a=c" by fact
- with i5 have i8: "t=t'" by (simp add: alpha)
- show "fresh_fun ?g = fresh_fun ?h" using i6 i7 i8 ih by simp
- next
- case False
- assume i9: "a\<noteq>c"
- with i5[symmetric] have i10: "t'=[(a,c)]\<bullet>t" and i11: "a\<sharp>t" by (simp_all add: alpha)
- have fin_g: "finite ((supp ?g)::name set)"
- using f fin_r by (finite_guess add: perm_append supp_prod fs_name1)
- have fin_h: "finite ((supp ?h)::name set)"
- using f fin_r'' by (finite_guess add: perm_append supp_prod fs_name1)
- have fr_g: "\<exists>(a''::name). a''\<sharp>?g \<and> a''\<sharp>(?g a'')"
- using f c fin_r by (simp add: f3_freshness_conditions_simple supp_prod)
- have fr_h: "\<exists>(a''::name). a''\<sharp>?h \<and> a''\<sharp>(?h a'')"
- using f c fin_r'' by (simp add: f3_freshness_conditions_simple supp_prod)
- have "\<exists>(d::name). d\<sharp>(?g,?h,t,a,c)" using fin_g fin_h
- by (rule_tac at_exists_fresh[OF at_name_inst], simp only: finite_Un supp_prod fs_name1, simp)
- then obtain d::"name"
- where f1: "d\<sharp>?g" and f2: "d\<sharp>?h" and f3: "d\<sharp>t" and f4: "d\<noteq>a" and f5: "d\<noteq>c"
- by (force simp add: fresh_prod fresh_atm)
- have g1: "[(a,d)]\<bullet>t = t" using i11 f3 by perm_simp
- from i6 have "(([(a,c)]@[(a,d)])\<bullet>t,r'') \<in> it f1 f2 f3" using g1 i10 by (simp only: pt_name2)
- hence "(t, \<lambda>pi2. r'' (pi2@(rev ([(a,c)]@[(a,d)])))) \<in> it f1 f2 f3"
- by (simp only: it_perm[OF f, OF c])
- hence g2: "(t, \<lambda>pi2. r'' (pi2@([(a,d)]@[(a,c)]))) \<in> it f1 f2 f3" by simp
- have "distinct [a,c,d]" using i9 f4 f5 by force
- hence g3: "(pi@[(c,d)]@[(a,d)]@[(a,c)]) \<triangleq> (pi@[(a,d)])"
- by (rule_tac at_prm_eq_append[OF at_name_inst], force simp add: prm_eq_def calc_atm)
- have "fresh_fun ?g = ?g d" using fin_g fr_g f1
- by (simp add: fresh_fun_app[OF pt_name_inst, OF at_name_inst])
- also have "\<dots> = f3 d ((\<lambda>pi2. r'' (pi2@([(a,d)]@[(a,c)]))) (pi@[(c,d)]))" using ih g2 by simp
- also have "\<dots> = f3 d (r'' (pi@[(c,d)]@[(a,d)]@[(a,c)]))" by simp
- also have "\<dots> = f3 d (r'' (pi@[(a,d)]))" using i6 g3 by (simp add: it_prm_eq)
- also have "\<dots> = fresh_fun ?h" using fin_h fr_h f2
- by (simp add: fresh_fun_app[OF pt_name_inst, OF at_name_inst])
- finally show "fresh_fun ?g = fresh_fun ?h" by simp
- qed
- qed
+ case (it3 a1 r1 t1)
+ have f1: "a1\<sharp>(f1,f2,f3)" by fact
+ have ih: "\<And>r'. (t1,r') \<in> it f1 f2 f3 \<Longrightarrow> r1 = r'" by fact
+ have it1: "(t1,r1) \<in> it f1 f2 f3" by fact
+ have "(Lam [a1].t1, r') \<in> it f1 f2 f3" by fact
+ then show ?case
+ proof cases
+ case (it3 a2 r2 t2)
+ then have f2: "a2\<sharp>(f1,f2,f3)"
+ and it2: "(t2,r2) \<in> it f1 f2 f3"
+ and eq1: "[a1].t1 = [a2].t2" and eq2: "r' = f3 a2 r2" by (simp_all add: lam.inject)
+ have "\<exists>(c::name). c\<sharp>(f1,f2,f3,a1,a2,t1,t2,r1,r2)" using a it1 it2
+ by (auto intro!: at_exists_fresh[OF at_name_inst] simp add: supp_prod fs_name1 it_fin_supp[OF a])
+ then obtain c where fresh: "c\<sharp>f1" "c\<sharp>f2" "c\<sharp>f3" "c\<noteq>a1" "c\<noteq>a2" "c\<sharp>t1" "c\<sharp>t2" "c\<sharp>r1" "c\<sharp>r2"
+ by (force simp add: fresh_prod fresh_atm)
+ have eq3: "[(a1,c)]\<bullet>t1 = [(a2,c)]\<bullet>t2" using eq1 fresh
+ apply(auto simp add: alpha)
+ apply(rule trans)
+ apply(rule perm_compose)
+ apply(simp add: calc_atm perm_fresh_fresh)
+ apply(rule pt_name3, rule at_ds5[OF at_name_inst])
+ done
+ have eq4: "[(a1,c)]\<bullet>r1 = [(a2,c)]\<bullet>r2" using eq3 it2 f1 f2 fresh
+ apply(drule_tac sym)
+ apply(rule_tac pt_bij2[OF pt_name_inst, OF at_name_inst])
+ apply(rule ih)
+ apply(drule_tac pi="[(a2,c)]" in it_equiv)
+ apply(perm_simp only: fresh_prod)
+ apply(drule_tac pi="[(a1,c)]" in it_equiv)
+ apply(perm_simp)
+ done
+ have fs1: "a1\<sharp>f3 a1 r1" using b f1
+ apply(auto)
+ apply(case_tac "a=a1")
+ apply(simp)
+ apply(rule_tac pi="[(a1,a)]" in pt_fresh_bij2[OF pt_name_inst, OF at_name_inst])
+ apply(perm_simp add: calc_atm fresh_prod)
+ done
+ have fs2: "a2\<sharp>f3 a2 r2" using b f2
+ apply(auto)
+ apply(case_tac "a=a2")
+ apply(simp)
+ apply(rule_tac pi="[(a2,a)]" in pt_fresh_bij2[OF pt_name_inst, OF at_name_inst])
+ apply(perm_simp add: calc_atm fresh_prod)
+ done
+ have fs3: "c\<sharp>f3 a1 r1" using fresh it1 a
+ apply(rule_tac S="supp (f3,a1,r1)" in supports_fresh)
+ apply(supports_simp)
+ apply(simp add: supp_prod fs_name1 it_fin_supp[OF a])
+ apply(simp add: fresh_def[symmetric] fresh_prod fresh_atm)
+ done
+ have fs4: "c\<sharp>f3 a2 r2" using fresh it2 a
+ apply(rule_tac S="supp (f3,a2,r2)" in supports_fresh)
+ apply(supports_simp)
+ apply(simp add: supp_prod fs_name1 it_fin_supp[OF a])
+ apply(simp add: fresh_def[symmetric] fresh_prod fresh_atm)
+ done
+ have "f3 a1 r1 = [(a1,c)]\<bullet>(f3 a1 r1)" using fs1 fs3 by perm_simp
+ also have "\<dots> = f3 c ([(a1,c)]\<bullet>r1)" using f1 fresh by (perm_simp add: calc_atm fresh_prod)
+ also have "\<dots> = f3 c ([(a2,c)]\<bullet>r2)" using eq4 by simp
+ also have "\<dots> = [(a2,c)]\<bullet>(f3 a2 r2)" using f2 fresh by (perm_simp add: calc_atm fresh_prod)
+ also have "\<dots> = f3 a2 r2" using fs2 fs4 by perm_simp
+ finally have eq4: "f3 a1 r1 = f3 a2 r2" by simp
+ then show ?thesis using eq2 by simp
+ qed (simp_all (no_asm_use))
qed
lemma it_function:
assumes f: "finite ((supp (f1,f2,f3))::name set)"
and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(r::'a::pt_name). a\<sharp>f3 a r)"
shows "\<exists>!r. (t,r) \<in> it f1 f2 f3"
-proof (rule ex_ex1I, rule it_total)
+proof (rule ex_ex1I, rule it_total[OF f, OF c])
case (goal1 r1 r2)
have a1: "(t,r1) \<in> it f1 f2 f3" and a2: "(t,r2) \<in> it f1 f2 f3" by fact
- hence "\<forall>pi. r1 pi = r2 pi" using it_unique[OF f, OF c] by simp
- thus "r1=r2" by (simp add: expand_fun_eq)
+ thus "r1 = r2" using it_unique[OF f, OF c] by simp
qed
-
-lemma it_eqvt:
+
+constdefs
+ itfun :: "'a f1_ty \<Rightarrow> 'a f2_ty \<Rightarrow> 'a f3_ty \<Rightarrow> lam \<Rightarrow> ('a::pt_name)"
+ "itfun f1 f2 f3 t \<equiv> (THE r. (t,r) \<in> it f1 f2 f3)"
+
+lemma itfun_eqvt:
fixes pi::"name prm"
assumes f: "finite ((supp (f1,f2,f3))::name set)"
and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(r::'a::pt_name). a\<sharp>f3 a r)"
- and a: "(t,r) \<in> it f1 f2 f3"
- shows "(pi\<bullet>t,pi\<bullet>r) \<in> it (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3)"
-using a proof(induct)
- case it1 show ?case by (perm_simp add: it.intros perm_compose')
-next
- case it2 thus ?case by (perm_simp add: it.intros)
-next
- case (it3 c r t) (* lam case *)
- let ?g = "pi\<bullet>(\<lambda>pi'. fresh_fun (\<lambda>a'. f3 a' (r (pi'@[(c,a')]))))"
- and ?h = "\<lambda>pi'. fresh_fun (\<lambda>a'. (pi\<bullet>f3) a' ((pi\<bullet>r) (pi'@[((pi\<bullet>c),a')])))"
- have "(t,r) \<in> it f1 f2 f3" by fact
- hence fin_r: "finite ((supp r)::name set)" using f c by (auto intro: it_fin_supp)
- have ih: "(pi\<bullet>t,pi\<bullet>r) \<in> it (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3)" by fact
- hence "(Lam [(pi\<bullet>c)].(pi\<bullet>t),?h) \<in> it (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3)" by (simp add: it.intros)
- moreover
- have "?g = ?h"
+ shows "pi\<bullet>(itfun f1 f2 f3 t) = itfun (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3) (pi\<bullet>t)"
+proof -
+ have f_pi: "finite ((supp (pi\<bullet>f1,pi\<bullet>f2,pi\<bullet>f3))::name set)" using f
+ by (simp add: supp_prod pt_supp_finite_pi[OF pt_name_inst, OF at_name_inst])
+ have fs_pi: "\<exists>(a::name). a\<sharp>(pi\<bullet>f3) \<and> (\<forall>(r::'a::pt_name). a\<sharp>(pi\<bullet>f3) a r)"
proof -
- let ?g' = "\<lambda>pi a'. f3 a' (r (pi@[(c,a')]))"
- have fact1: "\<forall>pi. finite ((supp (?g' pi))::name set)" using fin_r f
- by (rule_tac allI, finite_guess add: perm_append supp_prod fs_name1)
- have fact2: "\<forall>pi. \<exists>(a''::name). a''\<sharp>(?g' pi) \<and> a''\<sharp>((?g' pi) a'')"
- proof
- fix pi::"name prm"
- show "\<exists>(a''::name). a''\<sharp>(?g' pi) \<and> a''\<sharp>((?g' pi) a'')" using f c fin_r
- by (simp add: f3_freshness_conditions_simple supp_prod)
- qed
- from fact1 fact2 show "?g = ?h" by (perm_simp add: fresh_fun_eqvt perm_append)
- qed
- ultimately show "(pi\<bullet>Lam [c].t,?g) \<in> it (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3)" by simp
-qed
-
-lemma the1_equality':
- assumes a: "\<exists>!r. P r" and b: "P b" and c: "b y = a"
- shows "(THE r. P r) y = a"
- by (simp add: c[symmetric], rule fun_cong[OF the1_equality, OF a, OF b])
-
-lemma itfun'_prm:
- assumes f: "finite ((supp (f1,f2,f3))::name set)"
- and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
- shows "itfun' f1 f2 f3 (pi1\<bullet>t) pi2 = itfun' f1 f2 f3 t (pi2@pi1)"
-apply(auto simp add: itfun_def itfun'_def)
-apply(rule the1_equality'[OF it_function, OF f, OF c])
-apply(rule it_perm_aux[OF f, OF c])
-apply(rule theI'[OF it_function,OF f, OF c], simp)
-done
-
-lemma itfun'_eqvt:
- fixes pi1::"name prm"
- assumes f: "finite ((supp (f1,f2,f3))::name set)"
- and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
- shows "pi1\<bullet>(itfun' f1 f2 f3 t pi2) = itfun' (pi1\<bullet>f1) (pi1\<bullet>f2) (pi1\<bullet>f3) (pi1\<bullet>t) (pi1\<bullet>pi2)"
-proof -
- have f_pi: "finite ((supp (pi1\<bullet>f1,pi1\<bullet>f2,pi1\<bullet>f3))::name set)" using f
- by (simp add: supp_prod pt_supp_finite_pi[OF pt_name_inst, OF at_name_inst])
- have fs_pi: "\<exists>(a::name). a\<sharp>(pi1\<bullet>f3) \<and> (\<forall>(y::'a::pt_name). a\<sharp>(pi1\<bullet>f3) a y)"
- proof -
- from c obtain a where fs1: "a\<sharp>f3" and fs2: "(\<forall>(y::'a::pt_name). a\<sharp>f3 a y)" by force
- have "(pi1\<bullet>a)\<sharp>(pi1\<bullet>f3)" using fs1 by (simp add: fresh_eqvt)
+ from c obtain a where fs1: "a\<sharp>f3" and fs2: "\<forall>(r::'a::pt_name). a\<sharp>f3 a r" by force
+ have "(pi\<bullet>a)\<sharp>(pi\<bullet>f3)" using fs1 by (simp add: fresh_eqvt)
moreover
- have "\<forall>(y::'a::pt_name). (pi1\<bullet>a)\<sharp>((pi1\<bullet>f3) (pi1\<bullet>a) y)"
- proof
- fix y::"'a::pt_name"
- from fs2 have "a\<sharp>f3 a ((rev pi1)\<bullet>y)" by simp
- then show "(pi1\<bullet>a)\<sharp>((pi1\<bullet>f3) (pi1\<bullet>a) y)"
- by (perm_simp add: pt_fresh_right[OF pt_name_inst, OF at_name_inst])
- qed
- ultimately show "\<exists>(a::name). a\<sharp>(pi1\<bullet>f3) \<and> (\<forall>(y::'a::pt_name). a\<sharp>(pi1\<bullet>f3) a y)" by blast
+ have "\<forall>(r::'a::pt_name). (pi\<bullet>a)\<sharp>((pi\<bullet>f3) (pi\<bullet>a) r)" using fs2 by (perm_simp add: fresh_right)
+ ultimately show "\<exists>(a::name). a\<sharp>(pi\<bullet>f3) \<and> (\<forall>(r::'a::pt_name). a\<sharp>(pi\<bullet>f3) a r)" by blast
qed
show ?thesis
apply(rule sym)
- apply(auto simp add: itfun_def itfun'_def)
- apply(rule the1_equality'[OF it_function, OF f_pi, OF fs_pi])
- apply(rule it_eqvt[OF f, OF c])
+ apply(auto simp add: itfun_def)
+ apply(rule the1_equality[OF it_function, OF f_pi, OF fs_pi])
+ apply(rule it_equiv)
apply(rule theI'[OF it_function,OF f, OF c])
- apply(rule sym)
- apply(rule pt_bij2[OF pt_name_inst, OF at_name_inst], perm_simp)
done
qed
lemma itfun_Var:
assumes f: "finite ((supp (f1,f2,f3))::name set)"
- and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
+ and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(r::'a::pt_name). a\<sharp>f3 a r)"
shows "itfun f1 f2 f3 (Var c) = (f1 c)"
-using f c by (auto intro!: the1_equality' it_function it.intros simp add: itfun_def itfun'_def)
+using f c by (auto intro!: the1_equality it_function it.intros simp add: itfun_def)
lemma itfun_App:
assumes f: "finite ((supp (f1,f2,f3))::name set)"
- and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
+ and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(r::'a::pt_name). a\<sharp>f3 a r)"
shows "itfun f1 f2 f3 (App t1 t2) = (f2 (itfun f1 f2 f3 t1) (itfun f1 f2 f3 t2))"
-by (auto intro!: the1_equality' it_function[OF f, OF c] it.intros
- intro: theI'[OF it_function, OF f, OF c] simp add: itfun_def itfun'_def)
-
-lemma itfun_Lam_aux1:
- assumes f: "finite ((supp (f1,f2,f3))::name set)"
- and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
- shows "itfun f1 f2 f3 (Lam [a].t) = fresh_fun (\<lambda>a'. f3 a' (itfun' f1 f2 f3 t ([]@[(a,a')])))"
-by (auto intro!: the1_equality' it_function[OF f, OF c] it.intros
- intro: theI'[OF it_function, OF f, OF c] simp add: itfun_def itfun'_def)
-
-lemma itfun_Lam_aux2:
- assumes f: "finite ((supp (f1,f2,f3))::name set)"
- and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
- and a: "b\<sharp>(a,t,f1,f2,f3)"
- shows "itfun f1 f2 f3 (Lam [b].([(b,a)]\<bullet>t)) = f3 b (itfun f1 f2 f3 ([(a,b)]\<bullet>t))"
-proof -
- have eq1: "itfun f1 f2 f3 (Lam [b].([(b,a)]\<bullet>t)) = itfun f1 f2 f3 (Lam [a].t)"
- proof -
- have "Lam [b].([(b,a)]\<bullet>t) = Lam [a].t" using a by (simp add: lam.inject alpha fresh_prod fresh_atm)
- thus ?thesis by simp
- qed
- let ?g = "(\<lambda>a'. f3 a' (itfun' f1 f2 f3 t ([]@[(a,a')])))"
- have fin_g: "finite ((supp ?g)::name set)"
- using f by (finite_guess add: itfun'_eqvt[OF f, OF c] supp_prod fs_name1)
- have fr_g: "\<exists>(a''::name). a''\<sharp>?g \<and> a''\<sharp>(?g a'')" using f c
- apply (rule_tac f3_freshness_conditions_simple, auto simp add: supp_prod,
- finite_guess add: itfun'_eqvt[OF f, OF c] supp_prod fs_name1)
- done
- have fresh_b: "b\<sharp>?g"
- proof -
- have "finite ((supp (a,t,f1,f2,f3))::name set)" using f by (simp add: supp_prod fs_name1)
- moreover
- have "((supp (a,t,f1,f2,f3))::name set) supports ?g"
- by (supports_simp add: itfun'_eqvt[OF f, OF c] perm_append)
- ultimately show ?thesis using a by (auto intro!: supports_fresh, simp add: fresh_def)
- qed
- have "itfun f1 f2 f3 (Lam [b].([(b,a)]\<bullet>t)) = itfun f1 f2 f3 (Lam [a].t)" by (simp add: eq1)
- also have "\<dots> = fresh_fun ?g" by (rule itfun_Lam_aux1[OF f, OF c])
- also have "\<dots> = ?g b" using fresh_b fin_g fr_g
- by (simp add: fresh_fun_app[OF pt_name_inst, OF at_name_inst])
- also have "\<dots> = f3 b (itfun f1 f2 f3 ([(a,b)]\<bullet>t))" by (simp add: itfun_def itfun'_prm[OF f, OF c])
- finally show "itfun f1 f2 f3 (Lam [b].([(b,a)]\<bullet>t)) = f3 b (itfun f1 f2 f3 ([(a,b)]\<bullet>t))" by simp
-qed
+by (auto intro!: the1_equality it_function[OF f, OF c] it.intros
+ intro: theI'[OF it_function, OF f, OF c] simp add: itfun_def)
lemma itfun_Lam:
assumes f: "finite ((supp (f1,f2,f3))::name set)"
- and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
- and a: "b\<sharp>(f1,f2,f3)"
- shows "itfun f1 f2 f3 (Lam [b].t) = f3 b (itfun f1 f2 f3 t)"
-proof -
- have "\<exists>(a::name). a\<sharp>(b,t)"
- by (rule at_exists_fresh[OF at_name_inst], simp add: supp_prod fs_name1)
- then obtain a::"name" where a1: "a\<sharp>b" and a2: "a\<sharp>t" by (force simp add: fresh_prod)
- have fresh_b: "b\<sharp>(a,[(b,a)]\<bullet>t,f1,f2,f3)" using a a1 a2
- by (simp add: fresh_prod fresh_atm fresh_left calc_atm)
- have "itfun f1 f2 f3 (Lam [b].t) = itfun f1 f2 f3 (Lam [b].(([(b,a)])\<bullet>([(b,a)]\<bullet>t)))" by (perm_simp)
- also have "\<dots> = f3 b (itfun f1 f2 f3 (([(a,b)])\<bullet>([(b,a)]\<bullet>t)))"
- using fresh_b f c by (simp add: itfun_Lam_aux2)
- also have "\<dots> = f3 b (itfun f1 f2 f3 t)" by (simp add: pt_swap_bij'[OF pt_name_inst, OF at_name_inst])
- finally show ?thesis by simp
-qed
+ and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(r::'a::pt_name). a\<sharp>f3 a r)"
+ and a: "a\<sharp>(f1,f2,f3)"
+ shows "itfun f1 f2 f3 (Lam [a].t) = f3 a (itfun f1 f2 f3 t)"
+using a
+by (auto intro!: the1_equality it_function[OF f, OF c] it.intros
+ intro: theI'[OF it_function, OF f, OF c] simp add: itfun_def)
end