Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Nominal/Examples/Class.thy
changeset 18425 bcf13dbaa339
parent 18395 87217764cec2
child 18661 dde117622dac
equal deleted inserted replaced
18424:a37f06555c07 18425:bcf13dbaa339 
     1 theory class = nominal:
 
     1 
       
     2 theory class 
       
     3 imports "../nominal" 
       
     4 begin
 
     2 
     5 
     3 atom_decl name coname
 
     6 atom_decl name coname
 
     4 
     7 
     5 section {* Term-Calculus from my PHD *}
 
     8 section {* Term-Calculus from my PHD *}
 
     6 
     9 
     7 nominal_datatype trm = Ax  "name" "coname"
 
    10 nominal_datatype trm = Ax  "name" "coname"
 
     8                      | ImpR "\<guillemotleft>name\<guillemotright>(\<guillemotleft>coname\<guillemotright>trm)" "coname"
 
    11                  | ImpR "\<guillemotleft>name\<guillemotright>(\<guillemotleft>coname\<guillemotright>trm)" "coname"  ("ImpR [_].[_]._ _" [100,100,100,100] 100)
 
     9                      | ImpL "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name"
 
    12                  | ImpL "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name"("ImpL [_]._ [_]._ _" [100,100,100,100,100] 100)
 
    10                      | Cut "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm"
 
    13                  | Cut "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm"        ("Cut [_]._ [_]._" [100,100,100,100] 100)
 
    11 
       
    12 consts
 
       
    13   Ax   :: "name \<Rightarrow> coname \<Rightarrow> trm"
 
       
    14   ImpR :: "name \<Rightarrow> coname \<Rightarrow> trm \<Rightarrow> coname \<Rightarrow> trm"
 
       
    15           ("ImpR [_].[_]._ _" [100,100,100,100] 100)
 
       
    16   ImpL :: "coname \<Rightarrow> trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> name \<Rightarrow> trm"
 
       
    17           ("ImpL [_]._ [_]._ _" [100,100,100,100,100] 100)
 
       
    18   Cut  :: "coname \<Rightarrow> trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm"
 
       
    19           ("Cut [_]._ [_]._" [100,100,100,100] 100)
 
       
    20 
       
    21 defs
 
       
    22   Ax_trm_def:   "Ax x a 
       
    23                  \<equiv> Abs_trm (trm_Rep.Ax x a)"     
       
    24   ImpR_trm_def: "ImpR [x].[a].t b 
       
    25                  \<equiv> Abs_trm (trm_Rep.ImpR ([x].([a].(Rep_trm t))) b)"
 
       
    26   ImpL_trm_def: "ImpL [a].t1 [x].t2 y 
       
    27                  \<equiv> Abs_trm (trm_Rep.ImpL ([a].(Rep_trm t1)) ([x].(Rep_trm t2)) y)"
 
       
    28   Cut_trm_def:  "Cut [a].t1 [x].t2 
       
    29                  \<equiv> Abs_trm (trm_Rep.Cut ([a].(Rep_trm t1)) ([x].(Rep_trm t2)))"
 
       
    30 
       
    31 lemma Ax_inject:
 
       
    32   shows "(Ax x a = Ax y b) = (x=y\<and>a=b)"
 
       
    33 apply(subgoal_tac "trm_Rep.Ax x a \<in> trm_Rep_set")(*A*)
 
       
    34 apply(subgoal_tac "trm_Rep.Ax y b \<in> trm_Rep_set")(*B*)
 
       
    35 apply(simp add: Ax_trm_def Abs_trm_inject)
 
       
    36   (*A B*)
 
       
    37 apply(rule trm_Rep_set.intros)
 
       
    38 apply(rule trm_Rep_set.intros)
 
       
    39 done
 
       
    40 
       
    41 lemma permF_perm_name:  
       
    42   fixes t  :: "trm"
 
       
    43   and   pi :: "name prm" 
       
    44   shows "pi\<bullet>(Rep_trm t) = Rep_trm (pi\<bullet>t)"
 
       
    45 apply(simp add: prm_trm_def) 
       
    46 apply(subgoal_tac "pi\<bullet>(Rep_trm t)\<in>trm_Rep_set")(*A*)
 
       
    47 apply(simp add: Abs_trm_inverse)
 
       
    48 (*A*)
 
       
    49 apply(rule perm_closed)
 
       
    50 apply(rule Rep_trm)
 
       
    51 done
 
       
    52 
       
    53 lemma permF_perm_coname:  
       
    54   fixes t  :: "trm"
 
       
    55   and   pi :: "coname prm" 
       
    56   shows "pi\<bullet>(Rep_trm t) = Rep_trm (pi\<bullet>t)"
 
       
    57 apply(simp add: prm_trm_def) 
       
    58 apply(subgoal_tac "pi\<bullet>(Rep_trm t)\<in>trm_Rep_set")(*A*)
 
       
    59 apply(simp add: Abs_trm_inverse)
 
       
    60 (*A*)
 
       
    61 apply(rule perm_closed)
 
       
    62 apply(rule Rep_trm)
 
       
    63 done
 
       
    64 
       
    65 lemma freshF_fresh_name: 
       
    66   fixes t  :: "trm"
 
       
    67   and   b  :: "name"
 
       
    68   shows "b\<sharp>(Rep_trm t) = b\<sharp>t"
 
       
    69 apply(simp add: fresh_def supp_def)
 
       
    70 apply(simp add: permF_perm_name)
 
       
    71 apply(simp add: Rep_trm_inject)
 
       
    72 done
 
       
    73 
       
    74 lemma freshF_fresh_coname: 
       
    75   fixes t  :: "trm"
 
       
    76   and   b  :: "coname"
 
       
    77   shows "b\<sharp>(Rep_trm t) = b\<sharp>t"
 
       
    78 apply(simp add: fresh_def supp_def)
 
       
    79 apply(simp add: permF_perm_coname)
 
       
    80 apply(simp add: Rep_trm_inject)
 
       
    81 done
 
       
    82 
       
    83 lemma ImpR_inject:
 
       
    84   shows "((ImpR [x].[a].t1 b) = (ImpR [y].[c].t2 d)) = (([x].([a].t1) = [y].([c].t2)) \<and> b=d)"
 
       
    85 apply(simp add: ImpR_trm_def)
 
       
    86 apply(subgoal_tac "trm_Rep.ImpR ([x].([a].(Rep_trm t1))) b \<in> trm_Rep_set")(*A*)
 
       
    87 apply(subgoal_tac "trm_Rep.ImpR ([y].([c].(Rep_trm t2))) d \<in> trm_Rep_set")(*B*)
 
       
    88 apply(simp add: Abs_trm_inject)
 
       
    89 apply(simp add: alpha abs_perm perm_dj abs_fresh
 
       
    90                 permF_perm_name freshF_fresh_name 
       
    91                 permF_perm_coname freshF_fresh_coname 
       
    92                 Rep_trm_inject)
 
       
    93 (* A B *)
 
       
    94 apply(rule trm_Rep_set.intros, rule Rep_trm)
 
       
    95 apply(rule trm_Rep_set.intros, rule Rep_trm)
 
       
    96 done
 
       
    97 
       
    98 lemma ImpL_inject:
 
       
    99   shows "((ImpL [a1].t1 [x1].s1 y1) = (ImpL [a2].t2 [x2].s2 y2)) = 
       
   100          ([a1].t1 = [a2].t2 \<and>  [x1].s1 = [x2].s2 \<and> y1=y2)"
 
       
   101 apply(simp add: ImpL_trm_def)
 
       
   102 apply(subgoal_tac "(trm_Rep.ImpL ([a1].(Rep_trm t1)) ([x1].(Rep_trm s1)) y1) \<in> trm_Rep_set")(*A*)
 
       
   103 apply(subgoal_tac "(trm_Rep.ImpL ([a2].(Rep_trm t2)) ([x2].(Rep_trm s2)) y2) \<in> trm_Rep_set")(*B*)
 
       
   104 apply(simp add: Abs_trm_inject)
 
       
   105 apply(simp add: alpha abs_perm perm_dj abs_fresh
 
       
   106                 permF_perm_name freshF_fresh_name 
       
   107                 permF_perm_coname freshF_fresh_coname 
       
   108                 Rep_trm_inject)
 
       
   109 (* A B *)
 
       
   110 apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
 
       
   111 apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
 
       
   112 done                
       
   113 
       
   114 lemma Cut_inject:
 
       
   115   shows "((Cut [a1].t1 [x1].s1) = (Cut [a2].t2 [x2].s2)) = ([a1].t1 = [a2].t2 \<and>  [x1].s1 = [x2].s2)"
 
       
   116 apply(simp add: Cut_trm_def)
 
       
   117 apply(subgoal_tac "trm_Rep.Cut ([a1].(Rep_trm t1)) ([x1].(Rep_trm s1)) \<in> trm_Rep_set")(*A*)
 
       
   118 apply(subgoal_tac "trm_Rep.Cut ([a2].(Rep_trm t2)) ([x2].(Rep_trm s2)) \<in> trm_Rep_set")(*B*)
 
       
   119 apply(simp add: Abs_trm_inject)
 
       
   120 apply(simp add: alpha abs_perm perm_dj abs_fresh
 
       
   121                 permF_perm_name freshF_fresh_name 
       
   122                 permF_perm_coname freshF_fresh_coname 
       
   123                 Rep_trm_inject)
 
       
   124 (* A B *)
 
       
   125 apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
 
       
   126 apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
 
       
   127 done 
       
   128 
       
   129 
       
   130 lemma Ax_ineqs:
 
       
   131   shows "Ax x a \<noteq> ImpR [y].[b].t1 c"
 
       
   132   and   "Ax x a \<noteq> ImpL [b].t1 [y].t2 z"
 
       
   133   and   "Ax x a \<noteq> Cut [b].t1 [y].t2"
 
       
   134   apply(auto)
 
       
   135 (*1*)
 
       
   136   apply(subgoal_tac "trm_Rep.Ax x a\<in>trm_Rep_set")(*A*)
 
       
   137   apply(subgoal_tac "trm_Rep.ImpR ([y].([b].(Rep_trm t1))) c\<in>trm_Rep_set")(*B*)
 
       
   138   apply(simp add: Ax_trm_def ImpR_trm_def Abs_trm_inject)
 
       
   139   (*A B*)
 
       
   140   apply(rule trm_Rep_set.intros, rule Rep_trm)
 
       
   141   apply(rule trm_Rep_set.intros)
 
       
   142 (*2*)
 
       
   143   apply(subgoal_tac "trm_Rep.Ax x a\<in>trm_Rep_set")(*C*)
 
       
   144   apply(subgoal_tac "trm_Rep.ImpL ([b].(Rep_trm t1)) ([y].(Rep_trm t2)) z\<in>trm_Rep_set")(*D*)
 
       
   145   apply(simp add: Ax_trm_def ImpL_trm_def Abs_trm_inject)
 
       
   146   (* C D *)
 
       
   147   apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
 
       
   148   apply(rule trm_Rep_set.intros)
 
       
   149 (*3*)
 
       
   150   apply(subgoal_tac "trm_Rep.Ax x a\<in>trm_Rep_set")(*E*)
 
       
   151   apply(subgoal_tac "trm_Rep.Cut ([b].(Rep_trm t1)) ([y].(Rep_trm t2))\<in>trm_Rep_set")(*F*)
 
       
   152   apply(simp add: Ax_trm_def Cut_trm_def Abs_trm_inject)
 
       
   153   (* E F *)
 
       
   154   apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
 
       
   155   apply(rule trm_Rep_set.intros)
 
       
   156 done
 
       
   157 
       
   158 lemma ImpR_ineqs:
 
       
   159   shows "ImpR [y].[b].t c \<noteq> Ax x a"
 
       
   160   and   "ImpR [y].[b].t c \<noteq> ImpL [a].t1 [x].t2 z"
 
       
   161   and   "ImpR [y].[b].t c \<noteq> Cut [a].t1 [x].t2"
 
       
   162   apply(auto)
 
       
   163 (*1*)
 
       
   164   apply(subgoal_tac "trm_Rep.ImpR ([y].([b].(Rep_trm t))) c\<in>trm_Rep_set")(*B*)
 
       
   165   apply(subgoal_tac "trm_Rep.Ax x a\<in>trm_Rep_set")(*A*)
 
       
   166   apply(simp add: Ax_trm_def ImpR_trm_def Abs_trm_inject)
 
       
   167   (*A B*)
 
       
   168   apply(rule trm_Rep_set.intros)
 
       
   169   apply(rule trm_Rep_set.intros, rule Rep_trm)
 
       
   170 (*2*)
 
       
   171   apply(subgoal_tac "trm_Rep.ImpR ([y].([b].(Rep_trm t))) c\<in>trm_Rep_set")(*C*)
 
       
   172   apply(subgoal_tac "trm_Rep.ImpL ([a].(Rep_trm t1)) ([x].(Rep_trm t2)) z\<in>trm_Rep_set")(*D*)
 
       
   173   apply(simp add: ImpR_trm_def ImpL_trm_def Abs_trm_inject)
 
       
   174   (* C D *)
 
       
   175   apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
 
       
   176   apply(rule trm_Rep_set.intros, rule Rep_trm)
 
       
   177 (*3*)
 
       
   178   apply(subgoal_tac "trm_Rep.ImpR ([y].([b].(Rep_trm t))) c\<in>trm_Rep_set")(*E*)
 
       
   179   apply(subgoal_tac "trm_Rep.Cut ([a].(Rep_trm t1)) ([x].(Rep_trm t2))\<in>trm_Rep_set")(*F*)
 
       
   180   apply(simp add: ImpR_trm_def Cut_trm_def Abs_trm_inject)
 
       
   181   (* E F *)
 
       
   182   apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
 
       
   183   apply(rule trm_Rep_set.intros, rule Rep_trm)
 
       
   184 done
 
       
   185 
       
   186 lemma ImpL_ineqs:
 
       
   187   shows "ImpL [b].t1 [x].t2 y \<noteq> Ax z a"
 
       
   188   and   "ImpL [b].t1 [x].t2 y \<noteq> ImpR [z].[a].s1 c"
 
       
   189   and   "ImpL [b].t1 [x].t2 y \<noteq> Cut [a].s1 [z].s2"
 
       
   190   apply(auto)
 
       
   191 (*1*)
 
       
   192   apply(subgoal_tac "trm_Rep.ImpL ([b].(Rep_trm t1)) ([x].(Rep_trm t2)) y\<in>trm_Rep_set")(*B*)
 
       
   193   apply(subgoal_tac "trm_Rep.Ax z a\<in>trm_Rep_set")(*A*)
 
       
   194   apply(simp add: Ax_trm_def ImpL_trm_def Abs_trm_inject)
 
       
   195   (*A B*)
 
       
   196   apply(rule trm_Rep_set.intros)
 
       
   197   apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
 
       
   198 (*2*)
 
       
   199   apply(subgoal_tac "trm_Rep.ImpL ([b].(Rep_trm t1)) ([x].(Rep_trm t2)) y\<in>trm_Rep_set")(*D*)
 
       
   200   apply(subgoal_tac "trm_Rep.ImpR ([z].([a].(Rep_trm s1))) c\<in>trm_Rep_set")(*C*)
 
       
   201   apply(simp add: ImpR_trm_def ImpL_trm_def Abs_trm_inject)
 
       
   202   (* C D *)
 
       
   203   apply(rule trm_Rep_set.intros, rule Rep_trm)
 
       
   204   apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
 
       
   205 (*3*)
 
       
   206   apply(subgoal_tac "trm_Rep.ImpL ([b].(Rep_trm t1)) ([x].(Rep_trm t2)) y\<in>trm_Rep_set")(*E*)
 
       
   207   apply(subgoal_tac "trm_Rep.Cut ([a].(Rep_trm s1)) ([z].(Rep_trm s2))\<in>trm_Rep_set")(*F*)
 
       
   208   apply(simp add: ImpL_trm_def Cut_trm_def Abs_trm_inject)
 
       
   209   (* E F *)
 
       
   210   apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
 
       
   211   apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
 
       
   212 done
 
       
   213 
       
   214 lemma Cut_ineqs:
 
       
   215   shows "Cut [b].t1 [x].t2 \<noteq> Ax z a"
 
       
   216   and   "Cut [b].t1 [x].t2 \<noteq> ImpR [z].[a].s1 c"
 
       
   217   and   "Cut [b].t1 [x].t2 \<noteq> ImpL [a].s1 [z].s2 y"
 
       
   218   apply(auto)
 
       
   219 (*1*)
 
       
   220   apply(subgoal_tac "trm_Rep.Cut ([b].(Rep_trm t1)) ([x].(Rep_trm t2))\<in>trm_Rep_set")(*B*)
 
       
   221   apply(subgoal_tac "trm_Rep.Ax z a\<in>trm_Rep_set")(*A*)
 
       
   222   apply(simp add: Ax_trm_def Cut_trm_def Abs_trm_inject)
 
       
   223   (*A B*)
 
       
   224   apply(rule trm_Rep_set.intros)
 
       
   225   apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
 
       
   226 (*2*)
 
       
   227   apply(subgoal_tac "trm_Rep.Cut ([b].(Rep_trm t1)) ([x].(Rep_trm t2))\<in>trm_Rep_set")(*D*)
 
       
   228   apply(subgoal_tac "trm_Rep.ImpR ([z].([a].(Rep_trm s1))) c\<in>trm_Rep_set")(*C*)
 
       
   229   apply(simp add: ImpR_trm_def Cut_trm_def Abs_trm_inject)
 
       
   230   (* C D *)
 
       
   231   apply(rule trm_Rep_set.intros, rule Rep_trm)
 
       
   232   apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
 
       
   233 (*3*)
 
       
   234   apply(subgoal_tac "trm_Rep.Cut ([b].(Rep_trm t1)) ([x].(Rep_trm t2))\<in>trm_Rep_set")(*E*)
 
       
   235   apply(subgoal_tac "trm_Rep.ImpL ([a].(Rep_trm s1)) ([z].(Rep_trm s2)) y\<in>trm_Rep_set")(*F*)
 
       
   236   apply(simp add: ImpL_trm_def Cut_trm_def Abs_trm_inject)
 
       
   237   (* E F *)
 
       
   238   apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
 
       
   239   apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
 
       
   240 done
 
       
   241 
       
   242 lemma pi_Ax[simp]: 
       
   243   fixes pi1 :: "name prm"
 
       
   244   and   pi2 :: "coname prm"
 
       
   245   shows "pi1\<bullet>(Ax x a) = Ax (pi1\<bullet>x) a"
 
       
   246   and   "pi2\<bullet>(Ax x a) = Ax x (pi2\<bullet>a)"
 
       
   247 apply(subgoal_tac "trm_Rep.Ax x a\<in>trm_Rep_set")(*A*)
 
       
   248 apply(simp add: prm_trm_def Ax_trm_def Abs_trm_inverse perm_dj)
 
       
   249 (*A*)
 
       
   250 apply(rule trm_Rep_set.intros)
 
       
   251 apply(subgoal_tac "trm_Rep.Ax x a\<in>trm_Rep_set")(*B*)
 
       
   252 apply(simp add: prm_trm_def Ax_trm_def Abs_trm_inverse perm_dj)
 
       
   253 (*B*)
 
       
   254 apply(rule trm_Rep_set.intros)
 
       
   255 done
 
       
   256 
       
   257 lemma pi_ImpR[simp]: 
       
   258   fixes pi1 :: "name prm"
 
       
   259   and   pi2 :: "coname prm"
 
       
   260   shows "pi1\<bullet>(ImpR [x].[a].t b) = ImpR [(pi1\<bullet>x)].[a].(pi1\<bullet>t) b"
 
       
   261   and   "pi2\<bullet>(ImpR [x].[a].t b) = ImpR [x].[(pi2\<bullet>a)].(pi2\<bullet>t) (pi2\<bullet>b)"
 
       
   262 apply(subgoal_tac "trm_Rep.ImpR ([x].([a].(Rep_trm t))) b\<in>trm_Rep_set")(*A*)
 
       
   263 apply(subgoal_tac "pi1\<bullet>(Rep_trm t)\<in>trm_Rep_set")(*B*)
 
       
   264 apply(simp add: prm_trm_def ImpR_trm_def Abs_trm_inverse perm_fun_def[symmetric] abs_perm)
 
       
   265 apply(simp add: perm_dj)
 
       
   266 (* A B *)
 
       
   267 apply(rule perm_closed, rule Rep_trm)
 
       
   268 apply(rule trm_Rep_set.intros, rule Rep_trm)
 
       
   269 apply(subgoal_tac "trm_Rep.ImpR ([x].([a].(Rep_trm t))) b\<in>trm_Rep_set")(*C*)
 
       
   270 apply(subgoal_tac "pi2\<bullet>(Rep_trm t)\<in>trm_Rep_set")(*D*)
 
       
   271 apply(simp add: prm_trm_def ImpR_trm_def Abs_trm_inverse perm_fun_def[symmetric] abs_perm)
 
       
   272 apply(simp add: perm_dj)
 
       
   273 (* C D *)
 
       
   274 apply(rule perm_closed, rule Rep_trm)
 
       
   275 apply(rule trm_Rep_set.intros, rule Rep_trm)
 
       
   276 done
 
       
   277 
       
   278 lemma pi_ImpL[simp]: 
       
   279   fixes pi1 :: "name prm"
 
       
   280   and   pi2 :: "coname prm"
 
       
   281   shows "pi1\<bullet>(ImpL [a].t1 [x].t2 y) = ImpL [a].(pi1\<bullet>t1) [(pi1\<bullet>x)].(pi1\<bullet>t2) (pi1\<bullet>y)"
 
       
   282   and   "pi2\<bullet>(ImpL [a].t1 [x].t2 y) = ImpL [(pi2\<bullet>a)].(pi2\<bullet>t1) [x].(pi2\<bullet>t2) y"
 
       
   283 apply(subgoal_tac "trm_Rep.ImpL ([a].(Rep_trm t1)) ([x].(Rep_trm t2)) y\<in>trm_Rep_set")(*A*)
 
       
   284 apply(subgoal_tac "pi1\<bullet>(Rep_trm t1)\<in>trm_Rep_set")(*B*)
 
       
   285 apply(subgoal_tac "pi1\<bullet>(Rep_trm t2)\<in>trm_Rep_set")(*C*)
 
       
   286 apply(simp add: prm_trm_def ImpL_trm_def Abs_trm_inverse perm_fun_def[symmetric] abs_perm)
 
       
   287 apply(simp add: perm_dj)
 
       
   288 (* A B C *)
 
       
   289 apply(rule perm_closed, rule Rep_trm)
 
       
   290 apply(rule perm_closed, rule Rep_trm)
 
       
   291 apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
 
       
   292 apply(subgoal_tac "trm_Rep.ImpL ([a].(Rep_trm t1)) ([x].(Rep_trm t2)) y\<in>trm_Rep_set")(*E*)
 
       
   293 apply(subgoal_tac "pi2\<bullet>(Rep_trm t1)\<in>trm_Rep_set")(*D*)
 
       
   294 apply(subgoal_tac "pi2\<bullet>(Rep_trm t2)\<in>trm_Rep_set")(*F*)
 
       
   295 apply(simp add: prm_trm_def ImpL_trm_def Abs_trm_inverse perm_fun_def[symmetric] abs_perm)
 
       
   296 apply(simp add: perm_dj)
 
       
   297 (* C D *)
 
       
   298 apply(rule perm_closed, rule Rep_trm)
 
       
   299 apply(rule perm_closed, rule Rep_trm)
 
       
   300 apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
 
       
   301 done
 
       
   302 
       
   303 lemma pi_Cut[simp]: 
       
   304   fixes pi1 :: "name prm"
 
       
   305   and   pi2 :: "coname prm"
 
       
   306   shows "pi1\<bullet>(Cut [a].t1 [x].t2) = Cut [a].(pi1\<bullet>t1) [(pi1\<bullet>x)].(pi1\<bullet>t2)"
 
       
   307   and   "pi2\<bullet>(Cut [a].t1 [x].t2) = Cut [(pi2\<bullet>a)].(pi2\<bullet>t1) [x].(pi2\<bullet>t2)"
 
       
   308 apply(subgoal_tac "trm_Rep.Cut ([a].(Rep_trm t1)) ([x].(Rep_trm t2))\<in>trm_Rep_set")(*A*)
 
       
   309 apply(subgoal_tac "pi1\<bullet>(Rep_trm t1)\<in>trm_Rep_set")(*B*)
 
       
   310 apply(subgoal_tac "pi1\<bullet>(Rep_trm t2)\<in>trm_Rep_set")(*C*)
 
       
   311 apply(simp add: prm_trm_def Cut_trm_def Abs_trm_inverse perm_fun_def[symmetric] abs_perm)
 
       
   312 apply(simp add: perm_dj)
 
       
   313 (* A B C *)
 
       
   314 apply(rule perm_closed, rule Rep_trm)
 
       
   315 apply(rule perm_closed, rule Rep_trm)
 
       
   316 apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
 
       
   317 apply(subgoal_tac "trm_Rep.Cut ([a].(Rep_trm t1)) ([x].(Rep_trm t2))\<in>trm_Rep_set")(*E*)
 
       
   318 apply(subgoal_tac "pi2\<bullet>(Rep_trm t1)\<in>trm_Rep_set")(*D*)
 
       
   319 apply(subgoal_tac "pi2\<bullet>(Rep_trm t2)\<in>trm_Rep_set")(*F*)
 
       
   320 apply(simp add: prm_trm_def Cut_trm_def Abs_trm_inverse perm_fun_def[symmetric] abs_perm)
 
       
   321 apply(simp add: perm_dj)
 
       
   322 (* C D *)
 
       
   323 apply(rule perm_closed, rule Rep_trm)
 
       
   324 apply(rule perm_closed, rule Rep_trm)
 
       
   325 apply(rule trm_Rep_set.intros, rule Rep_trm, rule Rep_trm)
 
       
   326 done
 
       
   327 
       
   328 lemma supp_Ax:
 
       
   329   shows "((supp (Ax x a))::name set)   = (supp x)"
 
       
   330   and   "((supp (Ax x a))::coname set) = (supp a)"
 
       
   331   apply(simp add: supp_def Ax_inject)+
 
       
   332   done
 
       
   333 
       
   334 lemma supp_ImpR:
 
       
   335   shows "((supp (ImpR [x].[a].t b))::name set)   = (supp ([x].t))"
 
       
   336   and   "((supp (ImpR [x].[a].t b))::coname set) = (supp ([a].t,b))"
 
       
   337   apply(simp add: supp_def ImpR_inject)
 
       
   338   apply(simp add: abs_perm alpha perm_dj abs_fresh)
 
       
   339   apply(simp add: supp_def ImpR_inject)
 
       
   340   apply(simp add: abs_perm alpha perm_dj abs_fresh)
 
       
   341   done
 
       
   342 
       
   343 lemma supp_ImpL:
 
       
   344   shows "((supp (ImpL [a].t1 [x].t2 y))::name set)   = (supp (t1,[x].t2,y))"
 
       
   345   and   "((supp (ImpL [a].t1 [x].t2 y))::coname set) = (supp ([a].t1,t2))"
 
       
   346   apply(simp add: supp_def ImpL_inject)
 
       
   347   apply(simp add: abs_perm alpha perm_dj abs_fresh)
 
       
   348   apply(simp add: supp_def ImpL_inject)
 
       
   349   apply(simp add: abs_perm alpha perm_dj abs_fresh)
 
       
   350   done
 
       
   351 
       
   352 lemma supp_Cut:
 
       
   353   shows "((supp (Cut [a].t1 [x].t2))::name set)   = (supp (t1,[x].t2))"
 
       
   354   and   "((supp (Cut [a].t1 [x].t2))::coname set) = (supp ([a].t1,t2))"
 
       
   355   apply(simp add: supp_def Cut_inject)
 
       
   356   apply(simp add: abs_perm alpha perm_dj abs_fresh)
 
       
   357   apply(simp add: supp_def Cut_inject)
 
       
   358   apply(simp add: abs_perm alpha perm_dj abs_fresh)
 
       
   359   done
 
       
   360 
       
   361 lemma fresh_Ax[simp]:
 
       
   362   fixes x :: "name"
 
       
   363   and   a :: "coname"
 
       
   364   shows "x\<sharp>(Ax y b) = x\<sharp>y"
 
       
   365   and   "a\<sharp>(Ax y b) = a\<sharp>b"
 
       
   366   by (simp_all add: fresh_def supp_Ax)
 
       
   367 
       
   368 lemma fresh_ImpR[simp]:
 
       
   369   fixes x :: "name"
 
       
   370   and   a :: "coname"
 
       
   371   shows "x\<sharp>(ImpR [y].[b].t c) = x\<sharp>([y].t)"
 
       
   372   and   "a\<sharp>(ImpR [y].[b].t c) = a\<sharp>([b].t,c)"
 
       
   373   by (simp_all add: fresh_def supp_ImpR)
 
       
   374 
       
   375 lemma fresh_ImpL[simp]:
 
       
   376   fixes x :: "name"
 
       
   377   and   a :: "coname"
 
       
   378   shows "x\<sharp>(ImpL [b].t1 [y].t2 z) = x\<sharp>(t1,[y].t2,z)"
 
       
   379   and   "a\<sharp>(ImpL [b].t1 [y].t2 z) = a\<sharp>([b].t1,t2)"
 
       
   380   by (simp_all add: fresh_def supp_ImpL)
 
       
   381 
       
   382 lemma fresh_Cut[simp]:
 
       
   383   fixes x :: "name"
 
       
   384   and   a :: "coname"
 
       
   385   shows "x\<sharp>(Cut [b].t1 [y].t2) = x\<sharp>(t1,[y].t2)"
 
       
   386   and   "a\<sharp>(Cut [b].t1 [y].t2) = a\<sharp>([b].t1,t2)"
 
       
   387   by (simp_all add: fresh_def supp_Cut)
 
       
   388 
       
   389 lemma trm_inverses:
 
       
   390 shows "Abs_trm (trm_Rep.Ax x a) = (Ax x a)"
 
       
   391 and   "\<lbrakk>t1\<in>trm_Rep_set;t2\<in>trm_Rep_set\<rbrakk>
 
       
   392        \<Longrightarrow> Abs_trm (trm_Rep.ImpL ([a].t1) ([x].t2) y) = ImpL [a].(Abs_trm t1) [x].(Abs_trm t2) y"
 
       
   393 and   "\<lbrakk>t1\<in>trm_Rep_set;t2\<in>trm_Rep_set\<rbrakk>
 
       
   394        \<Longrightarrow> Abs_trm (trm_Rep.Cut ([a].t1) ([x].t2)) = Cut [a].(Abs_trm t1) [x].(Abs_trm t2)"
 
       
   395 and   "\<lbrakk>t1\<in>trm_Rep_set\<rbrakk>
 
       
   396        \<Longrightarrow> Abs_trm (trm_Rep.ImpR ([y].([a].t1)) b) = (ImpR [y].[a].(Abs_trm t1) b)"
 
       
   397 (*1*)
 
       
   398 apply(simp add: Ax_trm_def)
 
       
   399 (*2*)
 
       
   400 apply(simp add: ImpL_trm_def Abs_trm_inverse)
 
       
   401 (*3*)
 
       
   402 apply(simp add: Cut_trm_def Abs_trm_inverse)
 
       
   403 (*4*)
 
       
   404 apply(simp add: ImpR_trm_def Abs_trm_inverse)
 
       
   405 done
 
       
   406 
       
   407 lemma trm_Rep_set_fsupp_name: 
       
   408   fixes t :: "trm_Rep" 
       
   409   shows "t\<in>trm_Rep_set \<Longrightarrow> finite ((supp (Abs_trm t))::name set)"
 
       
   410 apply(erule trm_Rep_set.induct)
 
       
   411 (* Ax_Rep *)
 
       
   412 apply(simp add: trm_inverses supp_Ax at_supp[OF at_name_inst])
 
       
   413 (* ImpR_Rep *)
 
       
   414 apply(simp add: trm_inverses supp_ImpR abs_fun_supp[OF pt_name_inst, OF at_name_inst])
 
       
   415 (* ImpL_Rep *)
 
       
   416 apply(simp add: trm_inverses supp_prod supp_ImpL abs_fun_supp[OF pt_name_inst, OF at_name_inst] 
       
   417                 at_supp[OF at_name_inst])
 
       
   418 (* Cut_Rep *)
 
       
   419 apply(simp add: trm_inverses supp_prod supp_Cut abs_fun_supp[OF pt_name_inst, OF at_name_inst])
 
       
   420 done
 
       
   421 
       
   422 instance trm :: fs_name
 
       
   423 apply(intro_classes)
 
       
   424 apply(rule Abs_trm_induct)
 
       
   425 apply(simp add: trm_Rep_set_fsupp_name)
 
       
   426 done
 
       
   427 
       
   428 lemma trm_Rep_set_fsupp_coname: 
       
   429   fixes t :: "trm_Rep" 
       
   430   shows "t\<in>trm_Rep_set \<Longrightarrow> finite ((supp (Abs_trm t))::coname set)"
 
       
   431 apply(erule trm_Rep_set.induct)
 
       
   432 (* Ax_Rep *)
 
       
   433 apply(simp add: trm_inverses supp_Ax at_supp[OF at_coname_inst])
 
       
   434 (* ImpR_Rep *)
 
       
   435 apply(simp add: trm_inverses supp_prod supp_ImpR abs_fun_supp[OF pt_coname_inst, OF at_coname_inst]
 
       
   436                 at_supp[OF at_coname_inst])
 
       
   437 (* ImpL_Rep *)
 
       
   438 apply(simp add: trm_inverses supp_prod supp_ImpL abs_fun_supp[OF pt_coname_inst, OF at_coname_inst] 
       
   439                 at_supp[OF at_coname_inst])
 
       
   440 (* Cut_Rep *)
 
       
   441 apply(simp add: trm_inverses supp_prod supp_Cut abs_fun_supp[OF pt_coname_inst, OF at_coname_inst])
 
       
   442 done
 
       
   443 
       
   444 instance trm :: fs_coname
 
       
   445 apply(intro_classes)
 
       
   446 apply(rule Abs_trm_induct)
 
       
   447 apply(simp add: trm_Rep_set_fsupp_coname)
 
       
   448 done
 
       
   449 
       
   450 
       
   451 section {* strong induction principle for lam *}
 
       
   452 
       
   453 lemma trm_induct_weak: 
       
   454   fixes P :: "trm \<Rightarrow> bool"
 
       
   455   assumes h1: "\<And>x a. P (Ax x a)"  
       
   456       and h2: "\<And>x a t b. P t \<Longrightarrow> P (ImpR [x].[a].t b)" 
       
   457       and h3: "\<And>a t1 x t2 y. P t1 \<Longrightarrow> P t2 \<Longrightarrow> P (ImpL [a].t1 [x].t2 y)"
 
       
   458       and h4: "\<And>a t1 x t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> P (Cut [a].t1 [x].t2)"
 
       
   459     shows "P t"
 
       
   460 apply(rule Abs_trm_induct) 
       
   461 apply(erule trm_Rep_set.induct)
 
       
   462 apply(fold Ax_trm_def)
 
       
   463 apply(rule h1)
 
       
   464 apply(drule h2)
 
       
   465 apply(unfold ImpR_trm_def)
 
       
   466 apply(simp add: Abs_trm_inverse)
 
       
   467 apply(drule h3)
 
       
   468 apply(simp)
 
       
   469 apply(unfold ImpL_trm_def)
 
       
   470 apply(simp add: Abs_trm_inverse)
 
       
   471 apply(drule h4)
 
       
   472 apply(simp)
 
       
   473 apply(unfold Cut_trm_def)
 
       
   474 apply(simp add: Abs_trm_inverse)
 
       
   475 done
 
       
   476 
    14 
   477 lemma trm_induct_aux:
 
    15 lemma trm_induct_aux:
 
   478   fixes P :: "trm \<Rightarrow> 'a \<Rightarrow> bool"
 
    16   fixes P :: "trm \<Rightarrow> 'a \<Rightarrow> bool"
 
   479   and   f1 :: "'a \<Rightarrow> name set"
 
    17   and   f1 :: "'a \<Rightarrow> name set"
 
   480   and   f2 :: "'a \<Rightarrow> coname set"
 
    18   and   f2 :: "'a \<Rightarrow> coname set"
 
   485       and h3: "\<And>k a t1 x t2 y. a\<notin>f2 k \<Longrightarrow> x\<notin>f1 k \<Longrightarrow> (\<forall>l. P t1 l) \<Longrightarrow> (\<forall>l. P t2 l) 
    23       and h3: "\<And>k a t1 x t2 y. a\<notin>f2 k \<Longrightarrow> x\<notin>f1 k \<Longrightarrow> (\<forall>l. P t1 l) \<Longrightarrow> (\<forall>l. P t2 l) 
   486                \<Longrightarrow> P (ImpL [a].t1 [x].t2 y) k" 
    24                \<Longrightarrow> P (ImpL [a].t1 [x].t2 y) k" 
   487       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) 
    25       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) 
   488                \<Longrightarrow> P (Cut [a].t1 [x].t2) k" 
    26                \<Longrightarrow> P (Cut [a].t1 [x].t2) k" 
   489   shows "\<forall>(pi1::name prm) (pi2::coname prm) k. P (pi1\<bullet>(pi2\<bullet>t)) k"
 
    27   shows "\<forall>(pi1::name prm) (pi2::coname prm) k. P (pi1\<bullet>(pi2\<bullet>t)) k"
 
   490 proof (induct rule: trm_induct_weak)
 
    28 proof (induct rule: trm.induct_weak)
 
   491   case (goal1 a)
 
    29   case (goal1 a)
 
   492   show ?case using h1 by simp
 
    30   show ?case using h1 by simp
 
   493 next
 
    31 next
 
   494   case (goal2 x a t b)
 
    32   case (goal2 x a t b)
 
   495   assume i1: "\<forall>(pi1::name prm)(pi2::coname prm) k. P (pi1\<bullet>(pi2\<bullet>t)) k" 
    33   assume i1: "\<forall>(pi1::name prm)(pi2::coname prm) k. P (pi1\<bullet>(pi2\<bullet>t)) k"
isabelle