--- a/src/HOL/Nominal/Examples/Class.thy Fri Dec 16 18:20:03 2005 +0100
+++ b/src/HOL/Nominal/Examples/Class.thy Fri Dec 16 18:20:59 2005 +0100
@@ -1,478 +1,16 @@
-theory class = nominal:
+
+theory class
+imports "../nominal"
+begin
atom_decl name coname
section {* Term-Calculus from my PHD *}
nominal_datatype trm = Ax "name" "coname"
- | ImpR "\<guillemotleft>name\<guillemotright>(\<guillemotleft>coname\<guillemotright>trm)" "coname"
- | ImpL "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name"
- | Cut "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm"
-
-consts
- Ax :: "name \<Rightarrow> coname \<Rightarrow> trm"
- ImpR :: "name \<Rightarrow> coname \<Rightarrow> trm \<Rightarrow> coname \<Rightarrow> trm"
- ("ImpR [_].[_]._ _" [100,100,100,100] 100)
- ImpL :: "coname \<Rightarrow> trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> name \<Rightarrow> trm"
- ("ImpL [_]._ [_]._ _" [100,100,100,100,100] 100)
- Cut :: "coname \<Rightarrow> trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm"
- ("Cut [_]._ [_]._" [100,100,100,100] 100)
-
-defs
- Ax_trm_def: "Ax x a
- \<equiv> Abs_trm (trm_Rep.Ax x a)"
- ImpR_trm_def: "ImpR [x].[a].t b
- \<equiv> Abs_trm (trm_Rep.ImpR ([x].([a].(Rep_trm t))) b)"
- ImpL_trm_def: "ImpL [a].t1 [x].t2 y
- \<equiv> Abs_trm (trm_Rep.ImpL ([a].(Rep_trm t1)) ([x].(Rep_trm t2)) y)"
- Cut_trm_def: "Cut [a].t1 [x].t2
- \<equiv> Abs_trm (trm_Rep.Cut ([a].(Rep_trm t1)) ([x].(Rep_trm t2)))"
-
-lemma Ax_inject:
- shows "(Ax x a = Ax y b) = (x=y\<and>a=b)"
-apply(subgoal_tac "trm_Rep.Ax x a \<in> trm_Rep_set")(*A*)
-apply(subgoal_tac "trm_Rep.Ax y b \<in> trm_Rep_set")(*B*)
-apply(simp add: Ax_trm_def Abs_trm_inject)
- (*A B*)
-apply(rule trm_Rep_set.intros)
-apply(rule trm_Rep_set.intros)
-done
-
-lemma permF_perm_name:
- fixes t :: "trm"
- and pi :: "name prm"
- shows "pi\<bullet>(Rep_trm t) = Rep_trm (pi\<bullet>t)"
-apply(simp add: prm_trm_def)
-apply(subgoal_tac "pi\<bullet>(Rep_trm t)\<in>trm_Rep_set")(*A*)
-apply(simp add: Abs_trm_inverse)
-(*A*)
-apply(rule perm_closed)
-apply(rule Rep_trm)
-done
-
-lemma permF_perm_coname:
- fixes t :: "trm"
- and pi :: "coname prm"
- shows "pi\<bullet>(Rep_trm t) = Rep_trm (pi\<bullet>t)"
-apply(simp add: prm_trm_def)
-apply(subgoal_tac "pi\<bullet>(Rep_trm t)\<in>trm_Rep_set")(*A*)
-apply(simp add: Abs_trm_inverse)
-(*A*)
-apply(rule perm_closed)
-apply(rule Rep_trm)
-done
-
-lemma freshF_fresh_name:
- fixes t :: "trm"
- and b :: "name"
- shows "b\<sharp>(Rep_trm t) = b\<sharp>t"
-apply(simp add: fresh_def supp_def)
-apply(simp add: permF_perm_name)
-apply(simp add: Rep_trm_inject)
-done
-
-lemma freshF_fresh_coname:
- fixes t :: "trm"
- and b :: "coname"
- shows "b\<sharp>(Rep_trm t) = b\<sharp>t"
-apply(simp add: fresh_def supp_def)
-apply(simp add: permF_perm_coname)
-apply(simp add: Rep_trm_inject)
-done
-
-lemma ImpR_inject:
- shows "((ImpR [x].[a].t1 b) = (ImpR [y].[c].t2 d)) = (([x].([a].t1) = [y].([c].t2)) \<and> b=d)"
-apply(simp add: ImpR_trm_def)
-apply(subgoal_tac "trm_Rep.ImpR ([x].([a].(Rep_trm t1))) b \<in> trm_Rep_set")(*A*)
-apply(subgoal_tac "trm_Rep.ImpR ([y].([c].(Rep_trm t2))) d \<in> trm_Rep_set")(*B*)
-apply(simp add: Abs_trm_inject)
-apply(simp add: alpha abs_perm perm_dj abs_fresh
- permF_perm_name freshF_fresh_name
- permF_perm_coname freshF_fresh_coname
- Rep_trm_inject)
-(* A B *)
-apply(rule trm_Rep_set.intros, rule Rep_trm)
-apply(rule trm_Rep_set.intros, rule Rep_trm)
-done
-
-lemma ImpL_inject:
- shows "((ImpL [a1].t1 [x1].s1 y1) = (ImpL [a2].t2 [x2].s2 y2)) =
- ([a1].t1 = [a2].t2 \<and> [x1].s1 = [x2].s2 \<and> y1=y2)"
-apply(simp add: ImpL_trm_def)
-apply(subgoal_tac "(trm_Rep.ImpL ([a1].(Rep_trm t1)) ([x1].(Rep_trm s1)) y1) \<in> trm_Rep_set")(*A*)
-apply(subgoal_tac "(trm_Rep.ImpL ([a2].(Rep_trm t2)) ([x2].(Rep_trm s2)) y2) \<in> trm_Rep_set")(*B*)
-apply(simp add: Abs_trm_inject)
-apply(simp add: alpha abs_perm perm_dj abs_fresh
- permF_perm_name freshF_fresh_name
- permF_perm_coname freshF_fresh_coname
- Rep_trm_inject)
-(* A B *)
-apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
-apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
-done
-
-lemma Cut_inject:
- shows "((Cut [a1].t1 [x1].s1) = (Cut [a2].t2 [x2].s2)) = ([a1].t1 = [a2].t2 \<and> [x1].s1 = [x2].s2)"
-apply(simp add: Cut_trm_def)
-apply(subgoal_tac "trm_Rep.Cut ([a1].(Rep_trm t1)) ([x1].(Rep_trm s1)) \<in> trm_Rep_set")(*A*)
-apply(subgoal_tac "trm_Rep.Cut ([a2].(Rep_trm t2)) ([x2].(Rep_trm s2)) \<in> trm_Rep_set")(*B*)
-apply(simp add: Abs_trm_inject)
-apply(simp add: alpha abs_perm perm_dj abs_fresh
- permF_perm_name freshF_fresh_name
- permF_perm_coname freshF_fresh_coname
- Rep_trm_inject)
-(* A B *)
-apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
-apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
-done
-
-
-lemma Ax_ineqs:
- shows "Ax x a \<noteq> ImpR [y].[b].t1 c"
- and "Ax x a \<noteq> ImpL [b].t1 [y].t2 z"
- and "Ax x a \<noteq> Cut [b].t1 [y].t2"
- apply(auto)
-(*1*)
- apply(subgoal_tac "trm_Rep.Ax x a\<in>trm_Rep_set")(*A*)
- apply(subgoal_tac "trm_Rep.ImpR ([y].([b].(Rep_trm t1))) c\<in>trm_Rep_set")(*B*)
- apply(simp add: Ax_trm_def ImpR_trm_def Abs_trm_inject)
- (*A B*)
- apply(rule trm_Rep_set.intros, rule Rep_trm)
- apply(rule trm_Rep_set.intros)
-(*2*)
- apply(subgoal_tac "trm_Rep.Ax x a\<in>trm_Rep_set")(*C*)
- apply(subgoal_tac "trm_Rep.ImpL ([b].(Rep_trm t1)) ([y].(Rep_trm t2)) z\<in>trm_Rep_set")(*D*)
- apply(simp add: Ax_trm_def ImpL_trm_def Abs_trm_inject)
- (* C D *)
- apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
- apply(rule trm_Rep_set.intros)
-(*3*)
- apply(subgoal_tac "trm_Rep.Ax x a\<in>trm_Rep_set")(*E*)
- apply(subgoal_tac "trm_Rep.Cut ([b].(Rep_trm t1)) ([y].(Rep_trm t2))\<in>trm_Rep_set")(*F*)
- apply(simp add: Ax_trm_def Cut_trm_def Abs_trm_inject)
- (* E F *)
- apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
- apply(rule trm_Rep_set.intros)
-done
-
-lemma ImpR_ineqs:
- shows "ImpR [y].[b].t c \<noteq> Ax x a"
- and "ImpR [y].[b].t c \<noteq> ImpL [a].t1 [x].t2 z"
- and "ImpR [y].[b].t c \<noteq> Cut [a].t1 [x].t2"
- apply(auto)
-(*1*)
- apply(subgoal_tac "trm_Rep.ImpR ([y].([b].(Rep_trm t))) c\<in>trm_Rep_set")(*B*)
- apply(subgoal_tac "trm_Rep.Ax x a\<in>trm_Rep_set")(*A*)
- apply(simp add: Ax_trm_def ImpR_trm_def Abs_trm_inject)
- (*A B*)
- apply(rule trm_Rep_set.intros)
- apply(rule trm_Rep_set.intros, rule Rep_trm)
-(*2*)
- apply(subgoal_tac "trm_Rep.ImpR ([y].([b].(Rep_trm t))) c\<in>trm_Rep_set")(*C*)
- apply(subgoal_tac "trm_Rep.ImpL ([a].(Rep_trm t1)) ([x].(Rep_trm t2)) z\<in>trm_Rep_set")(*D*)
- apply(simp add: ImpR_trm_def ImpL_trm_def Abs_trm_inject)
- (* C D *)
- apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
- apply(rule trm_Rep_set.intros, rule Rep_trm)
-(*3*)
- apply(subgoal_tac "trm_Rep.ImpR ([y].([b].(Rep_trm t))) c\<in>trm_Rep_set")(*E*)
- apply(subgoal_tac "trm_Rep.Cut ([a].(Rep_trm t1)) ([x].(Rep_trm t2))\<in>trm_Rep_set")(*F*)
- apply(simp add: ImpR_trm_def Cut_trm_def Abs_trm_inject)
- (* E F *)
- apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
- apply(rule trm_Rep_set.intros, rule Rep_trm)
-done
-
-lemma ImpL_ineqs:
- shows "ImpL [b].t1 [x].t2 y \<noteq> Ax z a"
- and "ImpL [b].t1 [x].t2 y \<noteq> ImpR [z].[a].s1 c"
- and "ImpL [b].t1 [x].t2 y \<noteq> Cut [a].s1 [z].s2"
- apply(auto)
-(*1*)
- apply(subgoal_tac "trm_Rep.ImpL ([b].(Rep_trm t1)) ([x].(Rep_trm t2)) y\<in>trm_Rep_set")(*B*)
- apply(subgoal_tac "trm_Rep.Ax z a\<in>trm_Rep_set")(*A*)
- apply(simp add: Ax_trm_def ImpL_trm_def Abs_trm_inject)
- (*A B*)
- apply(rule trm_Rep_set.intros)
- apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
-(*2*)
- apply(subgoal_tac "trm_Rep.ImpL ([b].(Rep_trm t1)) ([x].(Rep_trm t2)) y\<in>trm_Rep_set")(*D*)
- apply(subgoal_tac "trm_Rep.ImpR ([z].([a].(Rep_trm s1))) c\<in>trm_Rep_set")(*C*)
- apply(simp add: ImpR_trm_def ImpL_trm_def Abs_trm_inject)
- (* C D *)
- apply(rule trm_Rep_set.intros, rule Rep_trm)
- apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
-(*3*)
- apply(subgoal_tac "trm_Rep.ImpL ([b].(Rep_trm t1)) ([x].(Rep_trm t2)) y\<in>trm_Rep_set")(*E*)
- apply(subgoal_tac "trm_Rep.Cut ([a].(Rep_trm s1)) ([z].(Rep_trm s2))\<in>trm_Rep_set")(*F*)
- apply(simp add: ImpL_trm_def Cut_trm_def Abs_trm_inject)
- (* E F *)
- apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
- apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
-done
-
-lemma Cut_ineqs:
- shows "Cut [b].t1 [x].t2 \<noteq> Ax z a"
- and "Cut [b].t1 [x].t2 \<noteq> ImpR [z].[a].s1 c"
- and "Cut [b].t1 [x].t2 \<noteq> ImpL [a].s1 [z].s2 y"
- apply(auto)
-(*1*)
- apply(subgoal_tac "trm_Rep.Cut ([b].(Rep_trm t1)) ([x].(Rep_trm t2))\<in>trm_Rep_set")(*B*)
- apply(subgoal_tac "trm_Rep.Ax z a\<in>trm_Rep_set")(*A*)
- apply(simp add: Ax_trm_def Cut_trm_def Abs_trm_inject)
- (*A B*)
- apply(rule trm_Rep_set.intros)
- apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
-(*2*)
- apply(subgoal_tac "trm_Rep.Cut ([b].(Rep_trm t1)) ([x].(Rep_trm t2))\<in>trm_Rep_set")(*D*)
- apply(subgoal_tac "trm_Rep.ImpR ([z].([a].(Rep_trm s1))) c\<in>trm_Rep_set")(*C*)
- apply(simp add: ImpR_trm_def Cut_trm_def Abs_trm_inject)
- (* C D *)
- apply(rule trm_Rep_set.intros, rule Rep_trm)
- apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
-(*3*)
- apply(subgoal_tac "trm_Rep.Cut ([b].(Rep_trm t1)) ([x].(Rep_trm t2))\<in>trm_Rep_set")(*E*)
- apply(subgoal_tac "trm_Rep.ImpL ([a].(Rep_trm s1)) ([z].(Rep_trm s2)) y\<in>trm_Rep_set")(*F*)
- apply(simp add: ImpL_trm_def Cut_trm_def Abs_trm_inject)
- (* E F *)
- apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
- apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
-done
-
-lemma pi_Ax[simp]:
- fixes pi1 :: "name prm"
- and pi2 :: "coname prm"
- shows "pi1\<bullet>(Ax x a) = Ax (pi1\<bullet>x) a"
- and "pi2\<bullet>(Ax x a) = Ax x (pi2\<bullet>a)"
-apply(subgoal_tac "trm_Rep.Ax x a\<in>trm_Rep_set")(*A*)
-apply(simp add: prm_trm_def Ax_trm_def Abs_trm_inverse perm_dj)
-(*A*)
-apply(rule trm_Rep_set.intros)
-apply(subgoal_tac "trm_Rep.Ax x a\<in>trm_Rep_set")(*B*)
-apply(simp add: prm_trm_def Ax_trm_def Abs_trm_inverse perm_dj)
-(*B*)
-apply(rule trm_Rep_set.intros)
-done
-
-lemma pi_ImpR[simp]:
- fixes pi1 :: "name prm"
- and pi2 :: "coname prm"
- shows "pi1\<bullet>(ImpR [x].[a].t b) = ImpR [(pi1\<bullet>x)].[a].(pi1\<bullet>t) b"
- and "pi2\<bullet>(ImpR [x].[a].t b) = ImpR [x].[(pi2\<bullet>a)].(pi2\<bullet>t) (pi2\<bullet>b)"
-apply(subgoal_tac "trm_Rep.ImpR ([x].([a].(Rep_trm t))) b\<in>trm_Rep_set")(*A*)
-apply(subgoal_tac "pi1\<bullet>(Rep_trm t)\<in>trm_Rep_set")(*B*)
-apply(simp add: prm_trm_def ImpR_trm_def Abs_trm_inverse perm_fun_def[symmetric] abs_perm)
-apply(simp add: perm_dj)
-(* A B *)
-apply(rule perm_closed, rule Rep_trm)
-apply(rule trm_Rep_set.intros, rule Rep_trm)
-apply(subgoal_tac "trm_Rep.ImpR ([x].([a].(Rep_trm t))) b\<in>trm_Rep_set")(*C*)
-apply(subgoal_tac "pi2\<bullet>(Rep_trm t)\<in>trm_Rep_set")(*D*)
-apply(simp add: prm_trm_def ImpR_trm_def Abs_trm_inverse perm_fun_def[symmetric] abs_perm)
-apply(simp add: perm_dj)
-(* C D *)
-apply(rule perm_closed, rule Rep_trm)
-apply(rule trm_Rep_set.intros, rule Rep_trm)
-done
-
-lemma pi_ImpL[simp]:
- fixes pi1 :: "name prm"
- and pi2 :: "coname prm"
- shows "pi1\<bullet>(ImpL [a].t1 [x].t2 y) = ImpL [a].(pi1\<bullet>t1) [(pi1\<bullet>x)].(pi1\<bullet>t2) (pi1\<bullet>y)"
- and "pi2\<bullet>(ImpL [a].t1 [x].t2 y) = ImpL [(pi2\<bullet>a)].(pi2\<bullet>t1) [x].(pi2\<bullet>t2) y"
-apply(subgoal_tac "trm_Rep.ImpL ([a].(Rep_trm t1)) ([x].(Rep_trm t2)) y\<in>trm_Rep_set")(*A*)
-apply(subgoal_tac "pi1\<bullet>(Rep_trm t1)\<in>trm_Rep_set")(*B*)
-apply(subgoal_tac "pi1\<bullet>(Rep_trm t2)\<in>trm_Rep_set")(*C*)
-apply(simp add: prm_trm_def ImpL_trm_def Abs_trm_inverse perm_fun_def[symmetric] abs_perm)
-apply(simp add: perm_dj)
-(* A B C *)
-apply(rule perm_closed, rule Rep_trm)
-apply(rule perm_closed, rule Rep_trm)
-apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
-apply(subgoal_tac "trm_Rep.ImpL ([a].(Rep_trm t1)) ([x].(Rep_trm t2)) y\<in>trm_Rep_set")(*E*)
-apply(subgoal_tac "pi2\<bullet>(Rep_trm t1)\<in>trm_Rep_set")(*D*)
-apply(subgoal_tac "pi2\<bullet>(Rep_trm t2)\<in>trm_Rep_set")(*F*)
-apply(simp add: prm_trm_def ImpL_trm_def Abs_trm_inverse perm_fun_def[symmetric] abs_perm)
-apply(simp add: perm_dj)
-(* C D *)
-apply(rule perm_closed, rule Rep_trm)
-apply(rule perm_closed, rule Rep_trm)
-apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
-done
-
-lemma pi_Cut[simp]:
- fixes pi1 :: "name prm"
- and pi2 :: "coname prm"
- shows "pi1\<bullet>(Cut [a].t1 [x].t2) = Cut [a].(pi1\<bullet>t1) [(pi1\<bullet>x)].(pi1\<bullet>t2)"
- and "pi2\<bullet>(Cut [a].t1 [x].t2) = Cut [(pi2\<bullet>a)].(pi2\<bullet>t1) [x].(pi2\<bullet>t2)"
-apply(subgoal_tac "trm_Rep.Cut ([a].(Rep_trm t1)) ([x].(Rep_trm t2))\<in>trm_Rep_set")(*A*)
-apply(subgoal_tac "pi1\<bullet>(Rep_trm t1)\<in>trm_Rep_set")(*B*)
-apply(subgoal_tac "pi1\<bullet>(Rep_trm t2)\<in>trm_Rep_set")(*C*)
-apply(simp add: prm_trm_def Cut_trm_def Abs_trm_inverse perm_fun_def[symmetric] abs_perm)
-apply(simp add: perm_dj)
-(* A B C *)
-apply(rule perm_closed, rule Rep_trm)
-apply(rule perm_closed, rule Rep_trm)
-apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
-apply(subgoal_tac "trm_Rep.Cut ([a].(Rep_trm t1)) ([x].(Rep_trm t2))\<in>trm_Rep_set")(*E*)
-apply(subgoal_tac "pi2\<bullet>(Rep_trm t1)\<in>trm_Rep_set")(*D*)
-apply(subgoal_tac "pi2\<bullet>(Rep_trm t2)\<in>trm_Rep_set")(*F*)
-apply(simp add: prm_trm_def Cut_trm_def Abs_trm_inverse perm_fun_def[symmetric] abs_perm)
-apply(simp add: perm_dj)
-(* C D *)
-apply(rule perm_closed, rule Rep_trm)
-apply(rule perm_closed, rule Rep_trm)
-apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
-done
-
-lemma supp_Ax:
- shows "((supp (Ax x a))::name set) = (supp x)"
- and "((supp (Ax x a))::coname set) = (supp a)"
- apply(simp add: supp_def Ax_inject)+
- done
-
-lemma supp_ImpR:
- shows "((supp (ImpR [x].[a].t b))::name set) = (supp ([x].t))"
- and "((supp (ImpR [x].[a].t b))::coname set) = (supp ([a].t,b))"
- apply(simp add: supp_def ImpR_inject)
- apply(simp add: abs_perm alpha perm_dj abs_fresh)
- apply(simp add: supp_def ImpR_inject)
- apply(simp add: abs_perm alpha perm_dj abs_fresh)
- done
-
-lemma supp_ImpL:
- shows "((supp (ImpL [a].t1 [x].t2 y))::name set) = (supp (t1,[x].t2,y))"
- and "((supp (ImpL [a].t1 [x].t2 y))::coname set) = (supp ([a].t1,t2))"
- apply(simp add: supp_def ImpL_inject)
- apply(simp add: abs_perm alpha perm_dj abs_fresh)
- apply(simp add: supp_def ImpL_inject)
- apply(simp add: abs_perm alpha perm_dj abs_fresh)
- done
-
-lemma supp_Cut:
- shows "((supp (Cut [a].t1 [x].t2))::name set) = (supp (t1,[x].t2))"
- and "((supp (Cut [a].t1 [x].t2))::coname set) = (supp ([a].t1,t2))"
- apply(simp add: supp_def Cut_inject)
- apply(simp add: abs_perm alpha perm_dj abs_fresh)
- apply(simp add: supp_def Cut_inject)
- apply(simp add: abs_perm alpha perm_dj abs_fresh)
- done
-
-lemma fresh_Ax[simp]:
- fixes x :: "name"
- and a :: "coname"
- shows "x\<sharp>(Ax y b) = x\<sharp>y"
- and "a\<sharp>(Ax y b) = a\<sharp>b"
- by (simp_all add: fresh_def supp_Ax)
-
-lemma fresh_ImpR[simp]:
- fixes x :: "name"
- and a :: "coname"
- shows "x\<sharp>(ImpR [y].[b].t c) = x\<sharp>([y].t)"
- and "a\<sharp>(ImpR [y].[b].t c) = a\<sharp>([b].t,c)"
- by (simp_all add: fresh_def supp_ImpR)
-
-lemma fresh_ImpL[simp]:
- fixes x :: "name"
- and a :: "coname"
- shows "x\<sharp>(ImpL [b].t1 [y].t2 z) = x\<sharp>(t1,[y].t2,z)"
- and "a\<sharp>(ImpL [b].t1 [y].t2 z) = a\<sharp>([b].t1,t2)"
- by (simp_all add: fresh_def supp_ImpL)
-
-lemma fresh_Cut[simp]:
- fixes x :: "name"
- and a :: "coname"
- shows "x\<sharp>(Cut [b].t1 [y].t2) = x\<sharp>(t1,[y].t2)"
- and "a\<sharp>(Cut [b].t1 [y].t2) = a\<sharp>([b].t1,t2)"
- by (simp_all add: fresh_def supp_Cut)
-
-lemma trm_inverses:
-shows "Abs_trm (trm_Rep.Ax x a) = (Ax x a)"
-and "\<lbrakk>t1\<in>trm_Rep_set;t2\<in>trm_Rep_set\<rbrakk>
- \<Longrightarrow> Abs_trm (trm_Rep.ImpL ([a].t1) ([x].t2) y) = ImpL [a].(Abs_trm t1) [x].(Abs_trm t2) y"
-and "\<lbrakk>t1\<in>trm_Rep_set;t2\<in>trm_Rep_set\<rbrakk>
- \<Longrightarrow> Abs_trm (trm_Rep.Cut ([a].t1) ([x].t2)) = Cut [a].(Abs_trm t1) [x].(Abs_trm t2)"
-and "\<lbrakk>t1\<in>trm_Rep_set\<rbrakk>
- \<Longrightarrow> Abs_trm (trm_Rep.ImpR ([y].([a].t1)) b) = (ImpR [y].[a].(Abs_trm t1) b)"
-(*1*)
-apply(simp add: Ax_trm_def)
-(*2*)
-apply(simp add: ImpL_trm_def Abs_trm_inverse)
-(*3*)
-apply(simp add: Cut_trm_def Abs_trm_inverse)
-(*4*)
-apply(simp add: ImpR_trm_def Abs_trm_inverse)
-done
-
-lemma trm_Rep_set_fsupp_name:
- fixes t :: "trm_Rep"
- shows "t\<in>trm_Rep_set \<Longrightarrow> finite ((supp (Abs_trm t))::name set)"
-apply(erule trm_Rep_set.induct)
-(* Ax_Rep *)
-apply(simp add: trm_inverses supp_Ax at_supp[OF at_name_inst])
-(* ImpR_Rep *)
-apply(simp add: trm_inverses supp_ImpR abs_fun_supp[OF pt_name_inst, OF at_name_inst])
-(* ImpL_Rep *)
-apply(simp add: trm_inverses supp_prod supp_ImpL abs_fun_supp[OF pt_name_inst, OF at_name_inst]
- at_supp[OF at_name_inst])
-(* Cut_Rep *)
-apply(simp add: trm_inverses supp_prod supp_Cut abs_fun_supp[OF pt_name_inst, OF at_name_inst])
-done
-
-instance trm :: fs_name
-apply(intro_classes)
-apply(rule Abs_trm_induct)
-apply(simp add: trm_Rep_set_fsupp_name)
-done
-
-lemma trm_Rep_set_fsupp_coname:
- fixes t :: "trm_Rep"
- shows "t\<in>trm_Rep_set \<Longrightarrow> finite ((supp (Abs_trm t))::coname set)"
-apply(erule trm_Rep_set.induct)
-(* Ax_Rep *)
-apply(simp add: trm_inverses supp_Ax at_supp[OF at_coname_inst])
-(* ImpR_Rep *)
-apply(simp add: trm_inverses supp_prod supp_ImpR abs_fun_supp[OF pt_coname_inst, OF at_coname_inst]
- at_supp[OF at_coname_inst])
-(* ImpL_Rep *)
-apply(simp add: trm_inverses supp_prod supp_ImpL abs_fun_supp[OF pt_coname_inst, OF at_coname_inst]
- at_supp[OF at_coname_inst])
-(* Cut_Rep *)
-apply(simp add: trm_inverses supp_prod supp_Cut abs_fun_supp[OF pt_coname_inst, OF at_coname_inst])
-done
-
-instance trm :: fs_coname
-apply(intro_classes)
-apply(rule Abs_trm_induct)
-apply(simp add: trm_Rep_set_fsupp_coname)
-done
-
-
-section {* strong induction principle for lam *}
-
-lemma trm_induct_weak:
- fixes P :: "trm \<Rightarrow> bool"
- assumes h1: "\<And>x a. P (Ax x a)"
- and h2: "\<And>x a t b. P t \<Longrightarrow> P (ImpR [x].[a].t b)"
- and h3: "\<And>a t1 x t2 y. P t1 \<Longrightarrow> P t2 \<Longrightarrow> P (ImpL [a].t1 [x].t2 y)"
- and h4: "\<And>a t1 x t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> P (Cut [a].t1 [x].t2)"
- shows "P t"
-apply(rule Abs_trm_induct)
-apply(erule trm_Rep_set.induct)
-apply(fold Ax_trm_def)
-apply(rule h1)
-apply(drule h2)
-apply(unfold ImpR_trm_def)
-apply(simp add: Abs_trm_inverse)
-apply(drule h3)
-apply(simp)
-apply(unfold ImpL_trm_def)
-apply(simp add: Abs_trm_inverse)
-apply(drule h4)
-apply(simp)
-apply(unfold Cut_trm_def)
-apply(simp add: Abs_trm_inverse)
-done
+ | ImpR "\<guillemotleft>name\<guillemotright>(\<guillemotleft>coname\<guillemotright>trm)" "coname" ("ImpR [_].[_]._ _" [100,100,100,100] 100)
+ | ImpL "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name"("ImpL [_]._ [_]._ _" [100,100,100,100,100] 100)
+ | Cut "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" ("Cut [_]._ [_]._" [100,100,100,100] 100)
lemma trm_induct_aux:
fixes P :: "trm \<Rightarrow> 'a \<Rightarrow> bool"
@@ -487,7 +25,7 @@
and h4: "\<And>k a t1 x t2. a\<notin>f2 k \<Longrightarrow> x\<notin>f1 k \<Longrightarrow> (\<forall>l. P t1 l) \<Longrightarrow> (\<forall>l. P t2 l)
\<Longrightarrow> P (Cut [a].t1 [x].t2) k"
shows "\<forall>(pi1::name prm) (pi2::coname prm) k. P (pi1\<bullet>(pi2\<bullet>t)) k"
-proof (induct rule: trm_induct_weak)
+proof (induct rule: trm.induct_weak)
case (goal1 a)
show ?case using h1 by simp
next