I think the earlier version was completely broken
authorurbanc
Fri Dec 16 18:20:59 2005 +0100 (2005-12-16)
changeset 18425bcf13dbaa339
parent 18424 a37f06555c07
child 18426 d2303e8654a2
I think the earlier version was completely broken
(not sure about this one)
src/HOL/Nominal/Examples/Class.thy
     1.1 --- a/src/HOL/Nominal/Examples/Class.thy	Fri Dec 16 18:20:03 2005 +0100
     1.2 +++ b/src/HOL/Nominal/Examples/Class.thy	Fri Dec 16 18:20:59 2005 +0100
     1.3 @@ -1,478 +1,16 @@
     1.4 -theory class = nominal:
     1.5 +
     1.6 +theory class 
     1.7 +imports "../nominal" 
     1.8 +begin
     1.9  
    1.10  atom_decl name coname
    1.11  
    1.12  section {* Term-Calculus from my PHD *}
    1.13  
    1.14  nominal_datatype trm = Ax  "name" "coname"
    1.15 -                     | ImpR "\<guillemotleft>name\<guillemotright>(\<guillemotleft>coname\<guillemotright>trm)" "coname"
    1.16 -                     | ImpL "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name"
    1.17 -                     | Cut "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm"
    1.18 -
    1.19 -consts
    1.20 -  Ax   :: "name \<Rightarrow> coname \<Rightarrow> trm"
    1.21 -  ImpR :: "name \<Rightarrow> coname \<Rightarrow> trm \<Rightarrow> coname \<Rightarrow> trm"
    1.22 -          ("ImpR [_].[_]._ _" [100,100,100,100] 100)
    1.23 -  ImpL :: "coname \<Rightarrow> trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> name \<Rightarrow> trm"
    1.24 -          ("ImpL [_]._ [_]._ _" [100,100,100,100,100] 100)
    1.25 -  Cut  :: "coname \<Rightarrow> trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm"
    1.26 -          ("Cut [_]._ [_]._" [100,100,100,100] 100)
    1.27 -
    1.28 -defs
    1.29 -  Ax_trm_def:   "Ax x a 
    1.30 -                 \<equiv> Abs_trm (trm_Rep.Ax x a)"     
    1.31 -  ImpR_trm_def: "ImpR [x].[a].t b 
    1.32 -                 \<equiv> Abs_trm (trm_Rep.ImpR ([x].([a].(Rep_trm t))) b)"
    1.33 -  ImpL_trm_def: "ImpL [a].t1 [x].t2 y 
    1.34 -                 \<equiv> Abs_trm (trm_Rep.ImpL ([a].(Rep_trm t1)) ([x].(Rep_trm t2)) y)"
    1.35 -  Cut_trm_def:  "Cut [a].t1 [x].t2 
    1.36 -                 \<equiv> Abs_trm (trm_Rep.Cut ([a].(Rep_trm t1)) ([x].(Rep_trm t2)))"
    1.37 -
    1.38 -lemma Ax_inject:
    1.39 -  shows "(Ax x a = Ax y b) = (x=y\<and>a=b)"
    1.40 -apply(subgoal_tac "trm_Rep.Ax x a \<in> trm_Rep_set")(*A*)
    1.41 -apply(subgoal_tac "trm_Rep.Ax y b \<in> trm_Rep_set")(*B*)
    1.42 -apply(simp add: Ax_trm_def Abs_trm_inject)
    1.43 -  (*A B*)
    1.44 -apply(rule trm_Rep_set.intros)
    1.45 -apply(rule trm_Rep_set.intros)
    1.46 -done
    1.47 -
    1.48 -lemma permF_perm_name:  
    1.49 -  fixes t  :: "trm"
    1.50 -  and   pi :: "name prm" 
    1.51 -  shows "pi\<bullet>(Rep_trm t) = Rep_trm (pi\<bullet>t)"
    1.52 -apply(simp add: prm_trm_def) 
    1.53 -apply(subgoal_tac "pi\<bullet>(Rep_trm t)\<in>trm_Rep_set")(*A*)
    1.54 -apply(simp add: Abs_trm_inverse)
    1.55 -(*A*)
    1.56 -apply(rule perm_closed)
    1.57 -apply(rule Rep_trm)
    1.58 -done
    1.59 -
    1.60 -lemma permF_perm_coname:  
    1.61 -  fixes t  :: "trm"
    1.62 -  and   pi :: "coname prm" 
    1.63 -  shows "pi\<bullet>(Rep_trm t) = Rep_trm (pi\<bullet>t)"
    1.64 -apply(simp add: prm_trm_def) 
    1.65 -apply(subgoal_tac "pi\<bullet>(Rep_trm t)\<in>trm_Rep_set")(*A*)
    1.66 -apply(simp add: Abs_trm_inverse)
    1.67 -(*A*)
    1.68 -apply(rule perm_closed)
    1.69 -apply(rule Rep_trm)
    1.70 -done
    1.71 -
    1.72 -lemma freshF_fresh_name: 
    1.73 -  fixes t  :: "trm"
    1.74 -  and   b  :: "name"
    1.75 -  shows "b\<sharp>(Rep_trm t) = b\<sharp>t"
    1.76 -apply(simp add: fresh_def supp_def)
    1.77 -apply(simp add: permF_perm_name)
    1.78 -apply(simp add: Rep_trm_inject)
    1.79 -done
    1.80 -
    1.81 -lemma freshF_fresh_coname: 
    1.82 -  fixes t  :: "trm"
    1.83 -  and   b  :: "coname"
    1.84 -  shows "b\<sharp>(Rep_trm t) = b\<sharp>t"
    1.85 -apply(simp add: fresh_def supp_def)
    1.86 -apply(simp add: permF_perm_coname)
    1.87 -apply(simp add: Rep_trm_inject)
    1.88 -done
    1.89 -
    1.90 -lemma ImpR_inject:
    1.91 -  shows "((ImpR [x].[a].t1 b) = (ImpR [y].[c].t2 d)) = (([x].([a].t1) = [y].([c].t2)) \<and> b=d)"
    1.92 -apply(simp add: ImpR_trm_def)
    1.93 -apply(subgoal_tac "trm_Rep.ImpR ([x].([a].(Rep_trm t1))) b \<in> trm_Rep_set")(*A*)
    1.94 -apply(subgoal_tac "trm_Rep.ImpR ([y].([c].(Rep_trm t2))) d \<in> trm_Rep_set")(*B*)
    1.95 -apply(simp add: Abs_trm_inject)
    1.96 -apply(simp add: alpha abs_perm perm_dj abs_fresh
    1.97 -                permF_perm_name freshF_fresh_name 
    1.98 -                permF_perm_coname freshF_fresh_coname 
    1.99 -                Rep_trm_inject)
   1.100 -(* A B *)
   1.101 -apply(rule trm_Rep_set.intros, rule Rep_trm)
   1.102 -apply(rule trm_Rep_set.intros, rule Rep_trm)
   1.103 -done
   1.104 -
   1.105 -lemma ImpL_inject:
   1.106 -  shows "((ImpL [a1].t1 [x1].s1 y1) = (ImpL [a2].t2 [x2].s2 y2)) = 
   1.107 -         ([a1].t1 = [a2].t2 \<and>  [x1].s1 = [x2].s2 \<and> y1=y2)"
   1.108 -apply(simp add: ImpL_trm_def)
   1.109 -apply(subgoal_tac "(trm_Rep.ImpL ([a1].(Rep_trm t1)) ([x1].(Rep_trm s1)) y1) \<in> trm_Rep_set")(*A*)
   1.110 -apply(subgoal_tac "(trm_Rep.ImpL ([a2].(Rep_trm t2)) ([x2].(Rep_trm s2)) y2) \<in> trm_Rep_set")(*B*)
   1.111 -apply(simp add: Abs_trm_inject)
   1.112 -apply(simp add: alpha abs_perm perm_dj abs_fresh
   1.113 -                permF_perm_name freshF_fresh_name 
   1.114 -                permF_perm_coname freshF_fresh_coname 
   1.115 -                Rep_trm_inject)
   1.116 -(* A B *)
   1.117 -apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
   1.118 -apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
   1.119 -done                
   1.120 -
   1.121 -lemma Cut_inject:
   1.122 -  shows "((Cut [a1].t1 [x1].s1) = (Cut [a2].t2 [x2].s2)) = ([a1].t1 = [a2].t2 \<and>  [x1].s1 = [x2].s2)"
   1.123 -apply(simp add: Cut_trm_def)
   1.124 -apply(subgoal_tac "trm_Rep.Cut ([a1].(Rep_trm t1)) ([x1].(Rep_trm s1)) \<in> trm_Rep_set")(*A*)
   1.125 -apply(subgoal_tac "trm_Rep.Cut ([a2].(Rep_trm t2)) ([x2].(Rep_trm s2)) \<in> trm_Rep_set")(*B*)
   1.126 -apply(simp add: Abs_trm_inject)
   1.127 -apply(simp add: alpha abs_perm perm_dj abs_fresh
   1.128 -                permF_perm_name freshF_fresh_name 
   1.129 -                permF_perm_coname freshF_fresh_coname 
   1.130 -                Rep_trm_inject)
   1.131 -(* A B *)
   1.132 -apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
   1.133 -apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
   1.134 -done 
   1.135 -
   1.136 -
   1.137 -lemma Ax_ineqs:
   1.138 -  shows "Ax x a \<noteq> ImpR [y].[b].t1 c"
   1.139 -  and   "Ax x a \<noteq> ImpL [b].t1 [y].t2 z"
   1.140 -  and   "Ax x a \<noteq> Cut [b].t1 [y].t2"
   1.141 -  apply(auto)
   1.142 -(*1*)
   1.143 -  apply(subgoal_tac "trm_Rep.Ax x a\<in>trm_Rep_set")(*A*)
   1.144 -  apply(subgoal_tac "trm_Rep.ImpR ([y].([b].(Rep_trm t1))) c\<in>trm_Rep_set")(*B*)
   1.145 -  apply(simp add: Ax_trm_def ImpR_trm_def Abs_trm_inject)
   1.146 -  (*A B*)
   1.147 -  apply(rule trm_Rep_set.intros, rule Rep_trm)
   1.148 -  apply(rule trm_Rep_set.intros)
   1.149 -(*2*)
   1.150 -  apply(subgoal_tac "trm_Rep.Ax x a\<in>trm_Rep_set")(*C*)
   1.151 -  apply(subgoal_tac "trm_Rep.ImpL ([b].(Rep_trm t1)) ([y].(Rep_trm t2)) z\<in>trm_Rep_set")(*D*)
   1.152 -  apply(simp add: Ax_trm_def ImpL_trm_def Abs_trm_inject)
   1.153 -  (* C D *)
   1.154 -  apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
   1.155 -  apply(rule trm_Rep_set.intros)
   1.156 -(*3*)
   1.157 -  apply(subgoal_tac "trm_Rep.Ax x a\<in>trm_Rep_set")(*E*)
   1.158 -  apply(subgoal_tac "trm_Rep.Cut ([b].(Rep_trm t1)) ([y].(Rep_trm t2))\<in>trm_Rep_set")(*F*)
   1.159 -  apply(simp add: Ax_trm_def Cut_trm_def Abs_trm_inject)
   1.160 -  (* E F *)
   1.161 -  apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
   1.162 -  apply(rule trm_Rep_set.intros)
   1.163 -done
   1.164 -
   1.165 -lemma ImpR_ineqs:
   1.166 -  shows "ImpR [y].[b].t c \<noteq> Ax x a"
   1.167 -  and   "ImpR [y].[b].t c \<noteq> ImpL [a].t1 [x].t2 z"
   1.168 -  and   "ImpR [y].[b].t c \<noteq> Cut [a].t1 [x].t2"
   1.169 -  apply(auto)
   1.170 -(*1*)
   1.171 -  apply(subgoal_tac "trm_Rep.ImpR ([y].([b].(Rep_trm t))) c\<in>trm_Rep_set")(*B*)
   1.172 -  apply(subgoal_tac "trm_Rep.Ax x a\<in>trm_Rep_set")(*A*)
   1.173 -  apply(simp add: Ax_trm_def ImpR_trm_def Abs_trm_inject)
   1.174 -  (*A B*)
   1.175 -  apply(rule trm_Rep_set.intros)
   1.176 -  apply(rule trm_Rep_set.intros, rule Rep_trm)
   1.177 -(*2*)
   1.178 -  apply(subgoal_tac "trm_Rep.ImpR ([y].([b].(Rep_trm t))) c\<in>trm_Rep_set")(*C*)
   1.179 -  apply(subgoal_tac "trm_Rep.ImpL ([a].(Rep_trm t1)) ([x].(Rep_trm t2)) z\<in>trm_Rep_set")(*D*)
   1.180 -  apply(simp add: ImpR_trm_def ImpL_trm_def Abs_trm_inject)
   1.181 -  (* C D *)
   1.182 -  apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
   1.183 -  apply(rule trm_Rep_set.intros, rule Rep_trm)
   1.184 -(*3*)
   1.185 -  apply(subgoal_tac "trm_Rep.ImpR ([y].([b].(Rep_trm t))) c\<in>trm_Rep_set")(*E*)
   1.186 -  apply(subgoal_tac "trm_Rep.Cut ([a].(Rep_trm t1)) ([x].(Rep_trm t2))\<in>trm_Rep_set")(*F*)
   1.187 -  apply(simp add: ImpR_trm_def Cut_trm_def Abs_trm_inject)
   1.188 -  (* E F *)
   1.189 -  apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
   1.190 -  apply(rule trm_Rep_set.intros, rule Rep_trm)
   1.191 -done
   1.192 -
   1.193 -lemma ImpL_ineqs:
   1.194 -  shows "ImpL [b].t1 [x].t2 y \<noteq> Ax z a"
   1.195 -  and   "ImpL [b].t1 [x].t2 y \<noteq> ImpR [z].[a].s1 c"
   1.196 -  and   "ImpL [b].t1 [x].t2 y \<noteq> Cut [a].s1 [z].s2"
   1.197 -  apply(auto)
   1.198 -(*1*)
   1.199 -  apply(subgoal_tac "trm_Rep.ImpL ([b].(Rep_trm t1)) ([x].(Rep_trm t2)) y\<in>trm_Rep_set")(*B*)
   1.200 -  apply(subgoal_tac "trm_Rep.Ax z a\<in>trm_Rep_set")(*A*)
   1.201 -  apply(simp add: Ax_trm_def ImpL_trm_def Abs_trm_inject)
   1.202 -  (*A B*)
   1.203 -  apply(rule trm_Rep_set.intros)
   1.204 -  apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
   1.205 -(*2*)
   1.206 -  apply(subgoal_tac "trm_Rep.ImpL ([b].(Rep_trm t1)) ([x].(Rep_trm t2)) y\<in>trm_Rep_set")(*D*)
   1.207 -  apply(subgoal_tac "trm_Rep.ImpR ([z].([a].(Rep_trm s1))) c\<in>trm_Rep_set")(*C*)
   1.208 -  apply(simp add: ImpR_trm_def ImpL_trm_def Abs_trm_inject)
   1.209 -  (* C D *)
   1.210 -  apply(rule trm_Rep_set.intros, rule Rep_trm)
   1.211 -  apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
   1.212 -(*3*)
   1.213 -  apply(subgoal_tac "trm_Rep.ImpL ([b].(Rep_trm t1)) ([x].(Rep_trm t2)) y\<in>trm_Rep_set")(*E*)
   1.214 -  apply(subgoal_tac "trm_Rep.Cut ([a].(Rep_trm s1)) ([z].(Rep_trm s2))\<in>trm_Rep_set")(*F*)
   1.215 -  apply(simp add: ImpL_trm_def Cut_trm_def Abs_trm_inject)
   1.216 -  (* E F *)
   1.217 -  apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
   1.218 -  apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
   1.219 -done
   1.220 -
   1.221 -lemma Cut_ineqs:
   1.222 -  shows "Cut [b].t1 [x].t2 \<noteq> Ax z a"
   1.223 -  and   "Cut [b].t1 [x].t2 \<noteq> ImpR [z].[a].s1 c"
   1.224 -  and   "Cut [b].t1 [x].t2 \<noteq> ImpL [a].s1 [z].s2 y"
   1.225 -  apply(auto)
   1.226 -(*1*)
   1.227 -  apply(subgoal_tac "trm_Rep.Cut ([b].(Rep_trm t1)) ([x].(Rep_trm t2))\<in>trm_Rep_set")(*B*)
   1.228 -  apply(subgoal_tac "trm_Rep.Ax z a\<in>trm_Rep_set")(*A*)
   1.229 -  apply(simp add: Ax_trm_def Cut_trm_def Abs_trm_inject)
   1.230 -  (*A B*)
   1.231 -  apply(rule trm_Rep_set.intros)
   1.232 -  apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
   1.233 -(*2*)
   1.234 -  apply(subgoal_tac "trm_Rep.Cut ([b].(Rep_trm t1)) ([x].(Rep_trm t2))\<in>trm_Rep_set")(*D*)
   1.235 -  apply(subgoal_tac "trm_Rep.ImpR ([z].([a].(Rep_trm s1))) c\<in>trm_Rep_set")(*C*)
   1.236 -  apply(simp add: ImpR_trm_def Cut_trm_def Abs_trm_inject)
   1.237 -  (* C D *)
   1.238 -  apply(rule trm_Rep_set.intros, rule Rep_trm)
   1.239 -  apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
   1.240 -(*3*)
   1.241 -  apply(subgoal_tac "trm_Rep.Cut ([b].(Rep_trm t1)) ([x].(Rep_trm t2))\<in>trm_Rep_set")(*E*)
   1.242 -  apply(subgoal_tac "trm_Rep.ImpL ([a].(Rep_trm s1)) ([z].(Rep_trm s2)) y\<in>trm_Rep_set")(*F*)
   1.243 -  apply(simp add: ImpL_trm_def Cut_trm_def Abs_trm_inject)
   1.244 -  (* E F *)
   1.245 -  apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
   1.246 -  apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
   1.247 -done
   1.248 -
   1.249 -lemma pi_Ax[simp]: 
   1.250 -  fixes pi1 :: "name prm"
   1.251 -  and   pi2 :: "coname prm"
   1.252 -  shows "pi1\<bullet>(Ax x a) = Ax (pi1\<bullet>x) a"
   1.253 -  and   "pi2\<bullet>(Ax x a) = Ax x (pi2\<bullet>a)"
   1.254 -apply(subgoal_tac "trm_Rep.Ax x a\<in>trm_Rep_set")(*A*)
   1.255 -apply(simp add: prm_trm_def Ax_trm_def Abs_trm_inverse perm_dj)
   1.256 -(*A*)
   1.257 -apply(rule trm_Rep_set.intros)
   1.258 -apply(subgoal_tac "trm_Rep.Ax x a\<in>trm_Rep_set")(*B*)
   1.259 -apply(simp add: prm_trm_def Ax_trm_def Abs_trm_inverse perm_dj)
   1.260 -(*B*)
   1.261 -apply(rule trm_Rep_set.intros)
   1.262 -done
   1.263 -
   1.264 -lemma pi_ImpR[simp]: 
   1.265 -  fixes pi1 :: "name prm"
   1.266 -  and   pi2 :: "coname prm"
   1.267 -  shows "pi1\<bullet>(ImpR [x].[a].t b) = ImpR [(pi1\<bullet>x)].[a].(pi1\<bullet>t) b"
   1.268 -  and   "pi2\<bullet>(ImpR [x].[a].t b) = ImpR [x].[(pi2\<bullet>a)].(pi2\<bullet>t) (pi2\<bullet>b)"
   1.269 -apply(subgoal_tac "trm_Rep.ImpR ([x].([a].(Rep_trm t))) b\<in>trm_Rep_set")(*A*)
   1.270 -apply(subgoal_tac "pi1\<bullet>(Rep_trm t)\<in>trm_Rep_set")(*B*)
   1.271 -apply(simp add: prm_trm_def ImpR_trm_def Abs_trm_inverse perm_fun_def[symmetric] abs_perm)
   1.272 -apply(simp add: perm_dj)
   1.273 -(* A B *)
   1.274 -apply(rule perm_closed, rule Rep_trm)
   1.275 -apply(rule trm_Rep_set.intros, rule Rep_trm)
   1.276 -apply(subgoal_tac "trm_Rep.ImpR ([x].([a].(Rep_trm t))) b\<in>trm_Rep_set")(*C*)
   1.277 -apply(subgoal_tac "pi2\<bullet>(Rep_trm t)\<in>trm_Rep_set")(*D*)
   1.278 -apply(simp add: prm_trm_def ImpR_trm_def Abs_trm_inverse perm_fun_def[symmetric] abs_perm)
   1.279 -apply(simp add: perm_dj)
   1.280 -(* C D *)
   1.281 -apply(rule perm_closed, rule Rep_trm)
   1.282 -apply(rule trm_Rep_set.intros, rule Rep_trm)
   1.283 -done
   1.284 -
   1.285 -lemma pi_ImpL[simp]: 
   1.286 -  fixes pi1 :: "name prm"
   1.287 -  and   pi2 :: "coname prm"
   1.288 -  shows "pi1\<bullet>(ImpL [a].t1 [x].t2 y) = ImpL [a].(pi1\<bullet>t1) [(pi1\<bullet>x)].(pi1\<bullet>t2) (pi1\<bullet>y)"
   1.289 -  and   "pi2\<bullet>(ImpL [a].t1 [x].t2 y) = ImpL [(pi2\<bullet>a)].(pi2\<bullet>t1) [x].(pi2\<bullet>t2) y"
   1.290 -apply(subgoal_tac "trm_Rep.ImpL ([a].(Rep_trm t1)) ([x].(Rep_trm t2)) y\<in>trm_Rep_set")(*A*)
   1.291 -apply(subgoal_tac "pi1\<bullet>(Rep_trm t1)\<in>trm_Rep_set")(*B*)
   1.292 -apply(subgoal_tac "pi1\<bullet>(Rep_trm t2)\<in>trm_Rep_set")(*C*)
   1.293 -apply(simp add: prm_trm_def ImpL_trm_def Abs_trm_inverse perm_fun_def[symmetric] abs_perm)
   1.294 -apply(simp add: perm_dj)
   1.295 -(* A B C *)
   1.296 -apply(rule perm_closed, rule Rep_trm)
   1.297 -apply(rule perm_closed, rule Rep_trm)
   1.298 -apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
   1.299 -apply(subgoal_tac "trm_Rep.ImpL ([a].(Rep_trm t1)) ([x].(Rep_trm t2)) y\<in>trm_Rep_set")(*E*)
   1.300 -apply(subgoal_tac "pi2\<bullet>(Rep_trm t1)\<in>trm_Rep_set")(*D*)
   1.301 -apply(subgoal_tac "pi2\<bullet>(Rep_trm t2)\<in>trm_Rep_set")(*F*)
   1.302 -apply(simp add: prm_trm_def ImpL_trm_def Abs_trm_inverse perm_fun_def[symmetric] abs_perm)
   1.303 -apply(simp add: perm_dj)
   1.304 -(* C D *)
   1.305 -apply(rule perm_closed, rule Rep_trm)
   1.306 -apply(rule perm_closed, rule Rep_trm)
   1.307 -apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
   1.308 -done
   1.309 -
   1.310 -lemma pi_Cut[simp]: 
   1.311 -  fixes pi1 :: "name prm"
   1.312 -  and   pi2 :: "coname prm"
   1.313 -  shows "pi1\<bullet>(Cut [a].t1 [x].t2) = Cut [a].(pi1\<bullet>t1) [(pi1\<bullet>x)].(pi1\<bullet>t2)"
   1.314 -  and   "pi2\<bullet>(Cut [a].t1 [x].t2) = Cut [(pi2\<bullet>a)].(pi2\<bullet>t1) [x].(pi2\<bullet>t2)"
   1.315 -apply(subgoal_tac "trm_Rep.Cut ([a].(Rep_trm t1)) ([x].(Rep_trm t2))\<in>trm_Rep_set")(*A*)
   1.316 -apply(subgoal_tac "pi1\<bullet>(Rep_trm t1)\<in>trm_Rep_set")(*B*)
   1.317 -apply(subgoal_tac "pi1\<bullet>(Rep_trm t2)\<in>trm_Rep_set")(*C*)
   1.318 -apply(simp add: prm_trm_def Cut_trm_def Abs_trm_inverse perm_fun_def[symmetric] abs_perm)
   1.319 -apply(simp add: perm_dj)
   1.320 -(* A B C *)
   1.321 -apply(rule perm_closed, rule Rep_trm)
   1.322 -apply(rule perm_closed, rule Rep_trm)
   1.323 -apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
   1.324 -apply(subgoal_tac "trm_Rep.Cut ([a].(Rep_trm t1)) ([x].(Rep_trm t2))\<in>trm_Rep_set")(*E*)
   1.325 -apply(subgoal_tac "pi2\<bullet>(Rep_trm t1)\<in>trm_Rep_set")(*D*)
   1.326 -apply(subgoal_tac "pi2\<bullet>(Rep_trm t2)\<in>trm_Rep_set")(*F*)
   1.327 -apply(simp add: prm_trm_def Cut_trm_def Abs_trm_inverse perm_fun_def[symmetric] abs_perm)
   1.328 -apply(simp add: perm_dj)
   1.329 -(* C D *)
   1.330 -apply(rule perm_closed, rule Rep_trm)
   1.331 -apply(rule perm_closed, rule Rep_trm)
   1.332 -apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
   1.333 -done
   1.334 -
   1.335 -lemma supp_Ax:
   1.336 -  shows "((supp (Ax x a))::name set)   = (supp x)"
   1.337 -  and   "((supp (Ax x a))::coname set) = (supp a)"
   1.338 -  apply(simp add: supp_def Ax_inject)+
   1.339 -  done
   1.340 -
   1.341 -lemma supp_ImpR:
   1.342 -  shows "((supp (ImpR [x].[a].t b))::name set)   = (supp ([x].t))"
   1.343 -  and   "((supp (ImpR [x].[a].t b))::coname set) = (supp ([a].t,b))"
   1.344 -  apply(simp add: supp_def ImpR_inject)
   1.345 -  apply(simp add: abs_perm alpha perm_dj abs_fresh)
   1.346 -  apply(simp add: supp_def ImpR_inject)
   1.347 -  apply(simp add: abs_perm alpha perm_dj abs_fresh)
   1.348 -  done
   1.349 -
   1.350 -lemma supp_ImpL:
   1.351 -  shows "((supp (ImpL [a].t1 [x].t2 y))::name set)   = (supp (t1,[x].t2,y))"
   1.352 -  and   "((supp (ImpL [a].t1 [x].t2 y))::coname set) = (supp ([a].t1,t2))"
   1.353 -  apply(simp add: supp_def ImpL_inject)
   1.354 -  apply(simp add: abs_perm alpha perm_dj abs_fresh)
   1.355 -  apply(simp add: supp_def ImpL_inject)
   1.356 -  apply(simp add: abs_perm alpha perm_dj abs_fresh)
   1.357 -  done
   1.358 -
   1.359 -lemma supp_Cut:
   1.360 -  shows "((supp (Cut [a].t1 [x].t2))::name set)   = (supp (t1,[x].t2))"
   1.361 -  and   "((supp (Cut [a].t1 [x].t2))::coname set) = (supp ([a].t1,t2))"
   1.362 -  apply(simp add: supp_def Cut_inject)
   1.363 -  apply(simp add: abs_perm alpha perm_dj abs_fresh)
   1.364 -  apply(simp add: supp_def Cut_inject)
   1.365 -  apply(simp add: abs_perm alpha perm_dj abs_fresh)
   1.366 -  done
   1.367 -
   1.368 -lemma fresh_Ax[simp]:
   1.369 -  fixes x :: "name"
   1.370 -  and   a :: "coname"
   1.371 -  shows "x\<sharp>(Ax y b) = x\<sharp>y"
   1.372 -  and   "a\<sharp>(Ax y b) = a\<sharp>b"
   1.373 -  by (simp_all add: fresh_def supp_Ax)
   1.374 -
   1.375 -lemma fresh_ImpR[simp]:
   1.376 -  fixes x :: "name"
   1.377 -  and   a :: "coname"
   1.378 -  shows "x\<sharp>(ImpR [y].[b].t c) = x\<sharp>([y].t)"
   1.379 -  and   "a\<sharp>(ImpR [y].[b].t c) = a\<sharp>([b].t,c)"
   1.380 -  by (simp_all add: fresh_def supp_ImpR)
   1.381 -
   1.382 -lemma fresh_ImpL[simp]:
   1.383 -  fixes x :: "name"
   1.384 -  and   a :: "coname"
   1.385 -  shows "x\<sharp>(ImpL [b].t1 [y].t2 z) = x\<sharp>(t1,[y].t2,z)"
   1.386 -  and   "a\<sharp>(ImpL [b].t1 [y].t2 z) = a\<sharp>([b].t1,t2)"
   1.387 -  by (simp_all add: fresh_def supp_ImpL)
   1.388 -
   1.389 -lemma fresh_Cut[simp]:
   1.390 -  fixes x :: "name"
   1.391 -  and   a :: "coname"
   1.392 -  shows "x\<sharp>(Cut [b].t1 [y].t2) = x\<sharp>(t1,[y].t2)"
   1.393 -  and   "a\<sharp>(Cut [b].t1 [y].t2) = a\<sharp>([b].t1,t2)"
   1.394 -  by (simp_all add: fresh_def supp_Cut)
   1.395 -
   1.396 -lemma trm_inverses:
   1.397 -shows "Abs_trm (trm_Rep.Ax x a) = (Ax x a)"
   1.398 -and   "\<lbrakk>t1\<in>trm_Rep_set;t2\<in>trm_Rep_set\<rbrakk>
   1.399 -       \<Longrightarrow> Abs_trm (trm_Rep.ImpL ([a].t1) ([x].t2) y) = ImpL [a].(Abs_trm t1) [x].(Abs_trm t2) y"
   1.400 -and   "\<lbrakk>t1\<in>trm_Rep_set;t2\<in>trm_Rep_set\<rbrakk>
   1.401 -       \<Longrightarrow> Abs_trm (trm_Rep.Cut ([a].t1) ([x].t2)) = Cut [a].(Abs_trm t1) [x].(Abs_trm t2)"
   1.402 -and   "\<lbrakk>t1\<in>trm_Rep_set\<rbrakk>
   1.403 -       \<Longrightarrow> Abs_trm (trm_Rep.ImpR ([y].([a].t1)) b) = (ImpR [y].[a].(Abs_trm t1) b)"
   1.404 -(*1*)
   1.405 -apply(simp add: Ax_trm_def)
   1.406 -(*2*)
   1.407 -apply(simp add: ImpL_trm_def Abs_trm_inverse)
   1.408 -(*3*)
   1.409 -apply(simp add: Cut_trm_def Abs_trm_inverse)
   1.410 -(*4*)
   1.411 -apply(simp add: ImpR_trm_def Abs_trm_inverse)
   1.412 -done
   1.413 -
   1.414 -lemma trm_Rep_set_fsupp_name: 
   1.415 -  fixes t :: "trm_Rep" 
   1.416 -  shows "t\<in>trm_Rep_set \<Longrightarrow> finite ((supp (Abs_trm t))::name set)"
   1.417 -apply(erule trm_Rep_set.induct)
   1.418 -(* Ax_Rep *)
   1.419 -apply(simp add: trm_inverses supp_Ax at_supp[OF at_name_inst])
   1.420 -(* ImpR_Rep *)
   1.421 -apply(simp add: trm_inverses supp_ImpR abs_fun_supp[OF pt_name_inst, OF at_name_inst])
   1.422 -(* ImpL_Rep *)
   1.423 -apply(simp add: trm_inverses supp_prod supp_ImpL abs_fun_supp[OF pt_name_inst, OF at_name_inst] 
   1.424 -                at_supp[OF at_name_inst])
   1.425 -(* Cut_Rep *)
   1.426 -apply(simp add: trm_inverses supp_prod supp_Cut abs_fun_supp[OF pt_name_inst, OF at_name_inst])
   1.427 -done
   1.428 -
   1.429 -instance trm :: fs_name
   1.430 -apply(intro_classes)
   1.431 -apply(rule Abs_trm_induct)
   1.432 -apply(simp add: trm_Rep_set_fsupp_name)
   1.433 -done
   1.434 -
   1.435 -lemma trm_Rep_set_fsupp_coname: 
   1.436 -  fixes t :: "trm_Rep" 
   1.437 -  shows "t\<in>trm_Rep_set \<Longrightarrow> finite ((supp (Abs_trm t))::coname set)"
   1.438 -apply(erule trm_Rep_set.induct)
   1.439 -(* Ax_Rep *)
   1.440 -apply(simp add: trm_inverses supp_Ax at_supp[OF at_coname_inst])
   1.441 -(* ImpR_Rep *)
   1.442 -apply(simp add: trm_inverses supp_prod supp_ImpR abs_fun_supp[OF pt_coname_inst, OF at_coname_inst]
   1.443 -                at_supp[OF at_coname_inst])
   1.444 -(* ImpL_Rep *)
   1.445 -apply(simp add: trm_inverses supp_prod supp_ImpL abs_fun_supp[OF pt_coname_inst, OF at_coname_inst] 
   1.446 -                at_supp[OF at_coname_inst])
   1.447 -(* Cut_Rep *)
   1.448 -apply(simp add: trm_inverses supp_prod supp_Cut abs_fun_supp[OF pt_coname_inst, OF at_coname_inst])
   1.449 -done
   1.450 -
   1.451 -instance trm :: fs_coname
   1.452 -apply(intro_classes)
   1.453 -apply(rule Abs_trm_induct)
   1.454 -apply(simp add: trm_Rep_set_fsupp_coname)
   1.455 -done
   1.456 -
   1.457 -
   1.458 -section {* strong induction principle for lam *}
   1.459 -
   1.460 -lemma trm_induct_weak: 
   1.461 -  fixes P :: "trm \<Rightarrow> bool"
   1.462 -  assumes h1: "\<And>x a. P (Ax x a)"  
   1.463 -      and h2: "\<And>x a t b. P t \<Longrightarrow> P (ImpR [x].[a].t b)" 
   1.464 -      and h3: "\<And>a t1 x t2 y. P t1 \<Longrightarrow> P t2 \<Longrightarrow> P (ImpL [a].t1 [x].t2 y)"
   1.465 -      and h4: "\<And>a t1 x t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> P (Cut [a].t1 [x].t2)"
   1.466 -    shows "P t"
   1.467 -apply(rule Abs_trm_induct) 
   1.468 -apply(erule trm_Rep_set.induct)
   1.469 -apply(fold Ax_trm_def)
   1.470 -apply(rule h1)
   1.471 -apply(drule h2)
   1.472 -apply(unfold ImpR_trm_def)
   1.473 -apply(simp add: Abs_trm_inverse)
   1.474 -apply(drule h3)
   1.475 -apply(simp)
   1.476 -apply(unfold ImpL_trm_def)
   1.477 -apply(simp add: Abs_trm_inverse)
   1.478 -apply(drule h4)
   1.479 -apply(simp)
   1.480 -apply(unfold Cut_trm_def)
   1.481 -apply(simp add: Abs_trm_inverse)
   1.482 -done
   1.483 +                 | ImpR "\<guillemotleft>name\<guillemotright>(\<guillemotleft>coname\<guillemotright>trm)" "coname"  ("ImpR [_].[_]._ _" [100,100,100,100] 100)
   1.484 +                 | ImpL "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name"("ImpL [_]._ [_]._ _" [100,100,100,100,100] 100)
   1.485 +                 | Cut "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm"        ("Cut [_]._ [_]._" [100,100,100,100] 100)
   1.486  
   1.487  lemma trm_induct_aux:
   1.488    fixes P :: "trm \<Rightarrow> 'a \<Rightarrow> bool"
   1.489 @@ -487,7 +25,7 @@
   1.490        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) 
   1.491                 \<Longrightarrow> P (Cut [a].t1 [x].t2) k" 
   1.492    shows "\<forall>(pi1::name prm) (pi2::coname prm) k. P (pi1\<bullet>(pi2\<bullet>t)) k"
   1.493 -proof (induct rule: trm_induct_weak)
   1.494 +proof (induct rule: trm.induct_weak)
   1.495    case (goal1 a)
   1.496    show ?case using h1 by simp
   1.497  next