src/HOL/Nominal/Examples/Class3.thy
author wenzelm
Sun Dec 27 22:07:17 2015 +0100 (2015-12-27)
changeset 61943 7fba644ed827
parent 55417 01fbfb60c33e
child 63167 0909deb8059b
permissions -rw-r--r--
discontinued ASCII replacement syntax <*>;
wenzelm@36277
     1
theory Class3
wenzelm@36277
     2
imports Class2
wenzelm@36277
     3
begin
wenzelm@36277
     4
wenzelm@36277
     5
text {* 3rd Main Lemma *}
wenzelm@36277
     6
wenzelm@36277
     7
lemma Cut_a_redu_elim:
wenzelm@53015
     8
  assumes a: "Cut <a>.M (x).N \<longrightarrow>\<^sub>a R"
wenzelm@53015
     9
  shows "(\<exists>M'. R = Cut <a>.M' (x).N \<and> M \<longrightarrow>\<^sub>a M') \<or>
wenzelm@53015
    10
         (\<exists>N'. R = Cut <a>.M (x).N' \<and> N \<longrightarrow>\<^sub>a N') \<or>
wenzelm@53015
    11
         (Cut <a>.M (x).N \<longrightarrow>\<^sub>c R) \<or>
wenzelm@53015
    12
         (Cut <a>.M (x).N \<longrightarrow>\<^sub>l R)"
wenzelm@36277
    13
using a
wenzelm@36277
    14
apply(erule_tac a_redu.cases)
wenzelm@36277
    15
apply(simp_all)
wenzelm@36277
    16
apply(simp_all add: trm.inject)
wenzelm@36277
    17
apply(rule disjI1)
wenzelm@36277
    18
apply(auto simp add: alpha)[1]
wenzelm@36277
    19
apply(rule_tac x="[(a,aa)]\<bullet>M'" in exI)
wenzelm@36277
    20
apply(perm_simp add: fresh_left calc_atm a_redu.eqvt fresh_a_redu)
wenzelm@36277
    21
apply(rule_tac x="[(a,aa)]\<bullet>M'" in exI)
wenzelm@36277
    22
apply(perm_simp add: fresh_left calc_atm a_redu.eqvt fresh_a_redu)
wenzelm@36277
    23
apply(rule disjI2)
wenzelm@36277
    24
apply(rule disjI1)
wenzelm@36277
    25
apply(auto simp add: alpha)[1]
wenzelm@36277
    26
apply(rule_tac x="[(x,xa)]\<bullet>N'" in exI)
wenzelm@36277
    27
apply(perm_simp add: fresh_left calc_atm a_redu.eqvt fresh_a_redu)
wenzelm@36277
    28
apply(rule_tac x="[(x,xa)]\<bullet>N'" in exI)
wenzelm@36277
    29
apply(perm_simp add: fresh_left calc_atm a_redu.eqvt fresh_a_redu)
wenzelm@36277
    30
done
wenzelm@36277
    31
wenzelm@36277
    32
lemma Cut_c_redu_elim:
wenzelm@53015
    33
  assumes a: "Cut <a>.M (x).N \<longrightarrow>\<^sub>c R"
wenzelm@36277
    34
  shows "(R = M{a:=(x).N} \<and> \<not>fic M a) \<or>
wenzelm@36277
    35
         (R = N{x:=<a>.M} \<and> \<not>fin N x)"
wenzelm@36277
    36
using a
wenzelm@36277
    37
apply(erule_tac c_redu.cases)
wenzelm@36277
    38
apply(simp_all)
wenzelm@36277
    39
apply(simp_all add: trm.inject)
wenzelm@36277
    40
apply(rule disjI1)
wenzelm@36277
    41
apply(auto simp add: alpha)[1]
wenzelm@36277
    42
apply(simp add: subst_rename fresh_atm)
wenzelm@36277
    43
apply(simp add: subst_rename fresh_atm)
wenzelm@36277
    44
apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2))
wenzelm@36277
    45
apply(perm_simp)
wenzelm@36277
    46
apply(simp add: subst_rename fresh_atm fresh_prod)
wenzelm@36277
    47
apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2))
wenzelm@36277
    48
apply(perm_simp)
wenzelm@36277
    49
apply(rule disjI2)
wenzelm@36277
    50
apply(auto simp add: alpha)[1]
wenzelm@36277
    51
apply(simp add: subst_rename fresh_atm)
wenzelm@36277
    52
apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1))
wenzelm@36277
    53
apply(perm_simp)
wenzelm@36277
    54
apply(simp add: subst_rename fresh_atm fresh_prod)
wenzelm@36277
    55
apply(simp add: subst_rename fresh_atm fresh_prod)
wenzelm@36277
    56
apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1))
wenzelm@36277
    57
apply(perm_simp)
wenzelm@36277
    58
done
wenzelm@36277
    59
wenzelm@36277
    60
lemma not_fic_crename_aux:
wenzelm@36277
    61
  assumes a: "fic M c" "c\<sharp>(a,b)"
wenzelm@36277
    62
  shows "fic (M[a\<turnstile>c>b]) c" 
wenzelm@36277
    63
using a
wenzelm@36277
    64
apply(nominal_induct M avoiding: c a b rule: trm.strong_induct)
wenzelm@36277
    65
apply(auto dest!: fic_elims intro!: fic.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh)
wenzelm@36277
    66
done
wenzelm@36277
    67
wenzelm@36277
    68
lemma not_fic_crename:
wenzelm@36277
    69
  assumes a: "\<not>(fic (M[a\<turnstile>c>b]) c)" "c\<sharp>(a,b)"
wenzelm@36277
    70
  shows "\<not>(fic M c)" 
wenzelm@36277
    71
using a
wenzelm@36277
    72
apply(auto dest:  not_fic_crename_aux)
wenzelm@36277
    73
done
wenzelm@36277
    74
wenzelm@36277
    75
lemma not_fin_crename_aux:
wenzelm@36277
    76
  assumes a: "fin M y"
wenzelm@36277
    77
  shows "fin (M[a\<turnstile>c>b]) y" 
wenzelm@36277
    78
using a
wenzelm@36277
    79
apply(nominal_induct M avoiding: a b rule: trm.strong_induct)
wenzelm@36277
    80
apply(auto dest!: fin_elims intro!: fin.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh)
wenzelm@36277
    81
done
wenzelm@36277
    82
wenzelm@36277
    83
lemma not_fin_crename:
wenzelm@36277
    84
  assumes a: "\<not>(fin (M[a\<turnstile>c>b]) y)" 
wenzelm@36277
    85
  shows "\<not>(fin M y)" 
wenzelm@36277
    86
using a
wenzelm@36277
    87
apply(auto dest:  not_fin_crename_aux)
wenzelm@36277
    88
done
wenzelm@36277
    89
wenzelm@36277
    90
lemma crename_fresh_interesting1:
wenzelm@36277
    91
  fixes c::"coname"
wenzelm@36277
    92
  assumes a: "c\<sharp>(M[a\<turnstile>c>b])" "c\<sharp>(a,b)"
wenzelm@36277
    93
  shows "c\<sharp>M"
wenzelm@36277
    94
using a
wenzelm@36277
    95
apply(nominal_induct M avoiding: c a b rule: trm.strong_induct)
wenzelm@36277
    96
apply(auto split: if_splits simp add: abs_fresh)
wenzelm@36277
    97
done
wenzelm@36277
    98
wenzelm@36277
    99
lemma crename_fresh_interesting2:
wenzelm@36277
   100
  fixes x::"name"
wenzelm@36277
   101
  assumes a: "x\<sharp>(M[a\<turnstile>c>b])" 
wenzelm@36277
   102
  shows "x\<sharp>M"
wenzelm@36277
   103
using a
wenzelm@36277
   104
apply(nominal_induct M avoiding: x a b rule: trm.strong_induct)
wenzelm@36277
   105
apply(auto split: if_splits simp add: abs_fresh abs_supp fin_supp fresh_atm)
wenzelm@36277
   106
done
wenzelm@36277
   107
wenzelm@36277
   108
wenzelm@36277
   109
lemma fic_crename:
wenzelm@36277
   110
  assumes a: "fic (M[a\<turnstile>c>b]) c" "c\<sharp>(a,b)"
wenzelm@36277
   111
  shows "fic M c" 
wenzelm@36277
   112
using a
wenzelm@36277
   113
apply(nominal_induct M avoiding: c a b rule: trm.strong_induct)
wenzelm@36277
   114
apply(auto dest!: fic_elims intro!: fic.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh
wenzelm@36277
   115
           split: if_splits)
wenzelm@36277
   116
apply(auto dest: crename_fresh_interesting1 simp add: fresh_prod fresh_atm)
wenzelm@36277
   117
done
wenzelm@36277
   118
wenzelm@36277
   119
lemma fin_crename:
wenzelm@36277
   120
  assumes a: "fin (M[a\<turnstile>c>b]) x"
wenzelm@36277
   121
  shows "fin M x" 
wenzelm@36277
   122
using a
wenzelm@36277
   123
apply(nominal_induct M avoiding: x a b rule: trm.strong_induct)
wenzelm@36277
   124
apply(auto dest!: fin_elims intro!: fin.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh
wenzelm@36277
   125
           split: if_splits)
wenzelm@36277
   126
apply(auto dest: crename_fresh_interesting2 simp add: fresh_prod fresh_atm)
wenzelm@36277
   127
done
wenzelm@36277
   128
wenzelm@36277
   129
lemma crename_Cut:
wenzelm@36277
   130
  assumes a: "R[a\<turnstile>c>b] = Cut <c>.M (x).N" "c\<sharp>(a,b,N,R)" "x\<sharp>(M,R)"
wenzelm@36277
   131
  shows "\<exists>M' N'. R = Cut <c>.M' (x).N' \<and> M'[a\<turnstile>c>b] = M \<and> N'[a\<turnstile>c>b] = N \<and> c\<sharp>N' \<and> x\<sharp>M'"
wenzelm@36277
   132
using a
wenzelm@36277
   133
apply(nominal_induct R avoiding: a b c x M N rule: trm.strong_induct)
wenzelm@36277
   134
apply(auto split: if_splits)
wenzelm@36277
   135
apply(simp add: trm.inject)
wenzelm@36277
   136
apply(auto simp add: alpha)
wenzelm@36277
   137
apply(rule_tac x="[(name,x)]\<bullet>trm2" in exI)
wenzelm@36277
   138
apply(perm_simp)
wenzelm@36277
   139
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
   140
apply(drule sym)
wenzelm@36277
   141
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
   142
apply(simp add: eqvts calc_atm)
wenzelm@36277
   143
apply(rule_tac x="[(coname,c)]\<bullet>trm1" in exI)
wenzelm@36277
   144
apply(perm_simp)
wenzelm@36277
   145
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
   146
apply(drule sym)
wenzelm@36277
   147
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
wenzelm@36277
   148
apply(simp add: eqvts calc_atm)
wenzelm@36277
   149
apply(auto simp add: fresh_atm)[1]
wenzelm@36277
   150
apply(rule_tac x="[(coname,c)]\<bullet>trm1" in exI)
wenzelm@36277
   151
apply(perm_simp)
wenzelm@36277
   152
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
   153
apply(rule_tac x="[(name,x)]\<bullet>trm2" in exI)
wenzelm@36277
   154
apply(perm_simp)
wenzelm@36277
   155
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
   156
apply(drule sym)
wenzelm@36277
   157
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
wenzelm@36277
   158
apply(simp add: eqvts calc_atm)
wenzelm@36277
   159
apply(auto simp add: fresh_atm)[1]
wenzelm@36277
   160
apply(drule sym)
wenzelm@36277
   161
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
   162
apply(simp add: eqvts calc_atm)
wenzelm@36277
   163
apply(drule sym)
wenzelm@36277
   164
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
   165
apply(simp add: eqvts calc_atm)
wenzelm@36277
   166
done
wenzelm@36277
   167
wenzelm@36277
   168
lemma crename_NotR:
wenzelm@36277
   169
  assumes a: "R[a\<turnstile>c>b] = NotR (x).N c" "x\<sharp>R" "c\<sharp>(a,b)"
wenzelm@36277
   170
  shows "\<exists>N'. (R = NotR (x).N' c) \<and> N'[a\<turnstile>c>b] = N" 
wenzelm@36277
   171
using a
wenzelm@36277
   172
apply(nominal_induct R avoiding: a b c x N rule: trm.strong_induct)
wenzelm@36277
   173
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
wenzelm@36277
   174
apply(rule_tac x="[(name,x)]\<bullet>trm" in exI)
wenzelm@36277
   175
apply(perm_simp)
wenzelm@36277
   176
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
   177
apply(drule sym)
wenzelm@36277
   178
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
   179
apply(simp add: eqvts calc_atm)
wenzelm@36277
   180
done
wenzelm@36277
   181
wenzelm@36277
   182
lemma crename_NotR':
wenzelm@36277
   183
  assumes a: "R[a\<turnstile>c>b] = NotR (x).N c" "x\<sharp>R" "c\<sharp>a"
wenzelm@36277
   184
  shows "(\<exists>N'. (R = NotR (x).N' c) \<and> N'[a\<turnstile>c>b] = N) \<or> (\<exists>N'. (R = NotR (x).N' a) \<and> b=c \<and> N'[a\<turnstile>c>b] = N)"
wenzelm@36277
   185
using a
wenzelm@36277
   186
apply(nominal_induct R avoiding: a b c x N rule: trm.strong_induct)
wenzelm@36277
   187
apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject)
wenzelm@36277
   188
apply(rule_tac x="[(name,x)]\<bullet>trm" in exI)
wenzelm@36277
   189
apply(perm_simp)
wenzelm@36277
   190
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
   191
apply(drule sym)
wenzelm@36277
   192
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
   193
apply(simp add: eqvts calc_atm)
wenzelm@36277
   194
apply(rule_tac x="[(name,x)]\<bullet>trm" in exI)
wenzelm@36277
   195
apply(perm_simp)
wenzelm@36277
   196
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
   197
apply(drule sym)
wenzelm@36277
   198
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
   199
apply(simp add: eqvts calc_atm)
wenzelm@36277
   200
done
wenzelm@36277
   201
wenzelm@36277
   202
lemma crename_NotR_aux:
wenzelm@36277
   203
  assumes a: "R[a\<turnstile>c>b] = NotR (x).N c" 
wenzelm@36277
   204
  shows "(a=c \<and> a=b) \<or> (a\<noteq>c)" 
wenzelm@36277
   205
using a
wenzelm@36277
   206
apply(nominal_induct R avoiding: a b c x N rule: trm.strong_induct)
wenzelm@36277
   207
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
wenzelm@36277
   208
done
wenzelm@36277
   209
wenzelm@36277
   210
lemma crename_NotL:
wenzelm@36277
   211
  assumes a: "R[a\<turnstile>c>b] = NotL <c>.N y" "c\<sharp>(R,a,b)"
wenzelm@36277
   212
  shows "\<exists>N'. (R = NotL <c>.N' y) \<and> N'[a\<turnstile>c>b] = N" 
wenzelm@36277
   213
using a
wenzelm@36277
   214
apply(nominal_induct R avoiding: a b c y N rule: trm.strong_induct)
wenzelm@36277
   215
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
wenzelm@36277
   216
apply(rule_tac x="[(coname,c)]\<bullet>trm" in exI)
wenzelm@36277
   217
apply(perm_simp)
wenzelm@36277
   218
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
   219
apply(drule sym)
wenzelm@36277
   220
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
wenzelm@36277
   221
apply(simp add: eqvts calc_atm)
wenzelm@36277
   222
done
wenzelm@36277
   223
wenzelm@36277
   224
lemma crename_AndL1:
wenzelm@36277
   225
  assumes a: "R[a\<turnstile>c>b] = AndL1 (x).N y" "x\<sharp>R"
wenzelm@36277
   226
  shows "\<exists>N'. (R = AndL1 (x).N' y) \<and> N'[a\<turnstile>c>b] = N" 
wenzelm@36277
   227
using a
wenzelm@36277
   228
apply(nominal_induct R avoiding: a b x y N rule: trm.strong_induct)
wenzelm@36277
   229
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
wenzelm@36277
   230
apply(rule_tac x="[(name1,x)]\<bullet>trm" in exI)
wenzelm@36277
   231
apply(perm_simp)
wenzelm@36277
   232
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
   233
apply(drule sym)
wenzelm@36277
   234
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
   235
apply(simp add: eqvts calc_atm)
wenzelm@36277
   236
done
wenzelm@36277
   237
wenzelm@36277
   238
lemma crename_AndL2:
wenzelm@36277
   239
  assumes a: "R[a\<turnstile>c>b] = AndL2 (x).N y" "x\<sharp>R"
wenzelm@36277
   240
  shows "\<exists>N'. (R = AndL2 (x).N' y) \<and> N'[a\<turnstile>c>b] = N" 
wenzelm@36277
   241
using a
wenzelm@36277
   242
apply(nominal_induct R avoiding: a b x y N rule: trm.strong_induct)
wenzelm@36277
   243
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
wenzelm@36277
   244
apply(rule_tac x="[(name1,x)]\<bullet>trm" in exI)
wenzelm@36277
   245
apply(perm_simp)
wenzelm@36277
   246
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
   247
apply(drule sym)
wenzelm@36277
   248
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
   249
apply(simp add: eqvts calc_atm)
wenzelm@36277
   250
done
wenzelm@36277
   251
wenzelm@36277
   252
lemma crename_AndR_aux:
wenzelm@36277
   253
  assumes a: "R[a\<turnstile>c>b] = AndR <c>.M <d>.N e" 
wenzelm@36277
   254
  shows "(a=e \<and> a=b) \<or> (a\<noteq>e)" 
wenzelm@36277
   255
using a
wenzelm@36277
   256
apply(nominal_induct R avoiding: a b c d e M N rule: trm.strong_induct)
wenzelm@36277
   257
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
wenzelm@36277
   258
done
wenzelm@36277
   259
wenzelm@36277
   260
lemma crename_AndR:
wenzelm@36277
   261
  assumes a: "R[a\<turnstile>c>b] = AndR <c>.M <d>.N e" "c\<sharp>(a,b,d,e,N,R)" "d\<sharp>(a,b,c,e,M,R)" "e\<sharp>(a,b)"
wenzelm@36277
   262
  shows "\<exists>M' N'. R = AndR <c>.M' <d>.N' e \<and> M'[a\<turnstile>c>b] = M \<and> N'[a\<turnstile>c>b] = N \<and> c\<sharp>N' \<and> d\<sharp>M'"
wenzelm@36277
   263
using a
wenzelm@36277
   264
apply(nominal_induct R avoiding: a b c d e M N rule: trm.strong_induct)
wenzelm@36277
   265
apply(auto split: if_splits simp add: trm.inject alpha)
wenzelm@36277
   266
apply(simp add: fresh_atm fresh_prod)
wenzelm@36277
   267
apply(rule_tac x="[(coname2,d)]\<bullet>trm2" in exI)
wenzelm@36277
   268
apply(perm_simp)
wenzelm@36277
   269
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
wenzelm@36277
   270
apply(rule_tac x="[(coname1,c)]\<bullet>trm1" in exI)
wenzelm@36277
   271
apply(perm_simp)
wenzelm@36277
   272
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
wenzelm@36277
   273
apply(rule_tac x="[(coname1,c)]\<bullet>trm1" in exI)
wenzelm@36277
   274
apply(perm_simp)
wenzelm@36277
   275
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
wenzelm@36277
   276
apply(rule_tac x="[(coname2,d)]\<bullet>trm2" in exI)
wenzelm@36277
   277
apply(perm_simp)
wenzelm@36277
   278
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
wenzelm@36277
   279
apply(rule_tac x="[(coname1,c)]\<bullet>trm1" in exI)
wenzelm@36277
   280
apply(perm_simp)
wenzelm@36277
   281
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
wenzelm@36277
   282
apply(rule_tac x="[(coname1,c)]\<bullet>trm1" in exI)
wenzelm@36277
   283
apply(perm_simp)
wenzelm@36277
   284
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
wenzelm@36277
   285
apply(rule_tac x="[(coname2,d)]\<bullet>trm2" in exI)
wenzelm@36277
   286
apply(perm_simp)
wenzelm@36277
   287
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
wenzelm@36277
   288
apply(drule sym)
wenzelm@36277
   289
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
wenzelm@36277
   290
apply(simp add: eqvts calc_atm)
wenzelm@36277
   291
apply(drule_tac s="trm2[a\<turnstile>c>b]" in  sym)
wenzelm@36277
   292
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
wenzelm@36277
   293
apply(simp add: eqvts calc_atm)
wenzelm@36277
   294
done
wenzelm@36277
   295
wenzelm@36277
   296
lemma crename_AndR':
wenzelm@36277
   297
  assumes a: "R[a\<turnstile>c>b] = AndR <c>.M <d>.N e" "c\<sharp>(a,b,d,e,N,R)" "d\<sharp>(a,b,c,e,M,R)" "e\<sharp>a"
wenzelm@36277
   298
  shows "(\<exists>M' N'. R = AndR <c>.M' <d>.N' e \<and> M'[a\<turnstile>c>b] = M \<and> N'[a\<turnstile>c>b] = N \<and> c\<sharp>N' \<and> d\<sharp>M') \<or>
wenzelm@36277
   299
         (\<exists>M' N'. R = AndR <c>.M' <d>.N' a \<and> b=e \<and> M'[a\<turnstile>c>b] = M \<and> N'[a\<turnstile>c>b] = N \<and> c\<sharp>N' \<and> d\<sharp>M')"
wenzelm@36277
   300
using a
wenzelm@36277
   301
apply(nominal_induct R avoiding: a b c d e M N rule: trm.strong_induct)
wenzelm@36277
   302
apply(auto split: if_splits simp add: trm.inject alpha)[1]
wenzelm@36277
   303
apply(auto split: if_splits simp add: trm.inject alpha)[1]
wenzelm@36277
   304
apply(auto split: if_splits simp add: trm.inject alpha)[1]
wenzelm@36277
   305
apply(auto split: if_splits simp add: trm.inject alpha)[1]
wenzelm@36277
   306
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm trm.inject alpha)[1]
wenzelm@36277
   307
apply(case_tac "coname3=a")
wenzelm@36277
   308
apply(simp)
wenzelm@36277
   309
apply(rule_tac x="[(coname1,c)]\<bullet>trm1" in exI)
wenzelm@36277
   310
apply(perm_simp)
wenzelm@36277
   311
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
wenzelm@36277
   312
apply(rule_tac x="[(coname2,d)]\<bullet>trm2" in exI)
wenzelm@36277
   313
apply(perm_simp)
wenzelm@36277
   314
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm trm.inject alpha split: if_splits)[1]
wenzelm@36277
   315
apply(drule sym)
wenzelm@36277
   316
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
wenzelm@36277
   317
apply(simp add: eqvts calc_atm)
wenzelm@36277
   318
apply(drule_tac s="trm2[a\<turnstile>c>e]" in  sym)
wenzelm@36277
   319
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
wenzelm@36277
   320
apply(simp add: eqvts calc_atm)
wenzelm@36277
   321
apply(simp)
wenzelm@36277
   322
apply(rule_tac x="[(coname1,c)]\<bullet>trm1" in exI)
wenzelm@36277
   323
apply(perm_simp)
wenzelm@36277
   324
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
   325
apply(rule_tac x="[(coname2,d)]\<bullet>trm2" in exI)
wenzelm@36277
   326
apply(perm_simp)
wenzelm@36277
   327
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm trm.inject alpha split: if_splits)[1]
wenzelm@36277
   328
apply(drule sym)
wenzelm@36277
   329
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
wenzelm@36277
   330
apply(simp add: eqvts calc_atm)
wenzelm@36277
   331
apply(drule_tac s="trm2[a\<turnstile>c>b]" in  sym)
wenzelm@36277
   332
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
wenzelm@36277
   333
apply(simp add: eqvts calc_atm)
wenzelm@36277
   334
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
wenzelm@36277
   335
done
wenzelm@36277
   336
wenzelm@36277
   337
lemma crename_OrR1_aux:
wenzelm@36277
   338
  assumes a: "R[a\<turnstile>c>b] = OrR1 <c>.M e" 
wenzelm@36277
   339
  shows "(a=e \<and> a=b) \<or> (a\<noteq>e)" 
wenzelm@36277
   340
using a
wenzelm@36277
   341
apply(nominal_induct R avoiding: a b c e M rule: trm.strong_induct)
wenzelm@36277
   342
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
wenzelm@36277
   343
done
wenzelm@36277
   344
wenzelm@36277
   345
lemma crename_OrR1:
wenzelm@36277
   346
  assumes a: "R[a\<turnstile>c>b] = OrR1 <c>.N d" "c\<sharp>(R,a,b)" "d\<sharp>(a,b)"
wenzelm@36277
   347
  shows "\<exists>N'. (R = OrR1 <c>.N' d) \<and> N'[a\<turnstile>c>b] = N" 
wenzelm@36277
   348
using a
wenzelm@36277
   349
apply(nominal_induct R avoiding: a b c d N rule: trm.strong_induct)
wenzelm@36277
   350
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
wenzelm@36277
   351
apply(rule_tac x="[(coname1,c)]\<bullet>trm" in exI)
wenzelm@36277
   352
apply(perm_simp)
wenzelm@36277
   353
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
   354
apply(drule sym)
wenzelm@36277
   355
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
wenzelm@36277
   356
apply(simp add: eqvts calc_atm)
wenzelm@36277
   357
done
wenzelm@36277
   358
wenzelm@36277
   359
lemma crename_OrR1':
wenzelm@36277
   360
  assumes a: "R[a\<turnstile>c>b] = OrR1 <c>.N d" "c\<sharp>(R,a,b)" "d\<sharp>a"
wenzelm@36277
   361
  shows "(\<exists>N'. (R = OrR1 <c>.N' d) \<and> N'[a\<turnstile>c>b] = N) \<or>
wenzelm@36277
   362
         (\<exists>N'. (R = OrR1 <c>.N' a) \<and> b=d \<and> N'[a\<turnstile>c>b] = N)" 
wenzelm@36277
   363
using a
wenzelm@36277
   364
apply(nominal_induct R avoiding: a b c d N rule: trm.strong_induct)
wenzelm@36277
   365
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
wenzelm@36277
   366
apply(rule_tac x="[(coname1,c)]\<bullet>trm" in exI)
wenzelm@36277
   367
apply(perm_simp)
wenzelm@36277
   368
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
   369
apply(drule sym)
wenzelm@36277
   370
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
wenzelm@36277
   371
apply(simp add: eqvts calc_atm)
wenzelm@36277
   372
apply(rule_tac x="[(coname1,c)]\<bullet>trm" in exI)
wenzelm@36277
   373
apply(perm_simp)
wenzelm@36277
   374
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
   375
apply(drule sym)
wenzelm@36277
   376
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
wenzelm@36277
   377
apply(simp add: eqvts calc_atm)
wenzelm@36277
   378
done
wenzelm@36277
   379
wenzelm@36277
   380
lemma crename_OrR2_aux:
wenzelm@36277
   381
  assumes a: "R[a\<turnstile>c>b] = OrR2 <c>.M e" 
wenzelm@36277
   382
  shows "(a=e \<and> a=b) \<or> (a\<noteq>e)" 
wenzelm@36277
   383
using a
wenzelm@36277
   384
apply(nominal_induct R avoiding: a b c e M rule: trm.strong_induct)
wenzelm@36277
   385
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
wenzelm@36277
   386
done
wenzelm@36277
   387
wenzelm@36277
   388
lemma crename_OrR2:
wenzelm@36277
   389
  assumes a: "R[a\<turnstile>c>b] = OrR2 <c>.N d" "c\<sharp>(R,a,b)" "d\<sharp>(a,b)"
wenzelm@36277
   390
  shows "\<exists>N'. (R = OrR2 <c>.N' d) \<and> N'[a\<turnstile>c>b] = N" 
wenzelm@36277
   391
using a
wenzelm@36277
   392
apply(nominal_induct R avoiding: a b c d N rule: trm.strong_induct)
wenzelm@36277
   393
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
wenzelm@36277
   394
apply(rule_tac x="[(coname1,c)]\<bullet>trm" in exI)
wenzelm@36277
   395
apply(perm_simp)
wenzelm@36277
   396
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
   397
apply(drule sym)
wenzelm@36277
   398
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
wenzelm@36277
   399
apply(simp add: eqvts calc_atm)
wenzelm@36277
   400
done
wenzelm@36277
   401
wenzelm@36277
   402
lemma crename_OrR2':
wenzelm@36277
   403
  assumes a: "R[a\<turnstile>c>b] = OrR2 <c>.N d" "c\<sharp>(R,a,b)" "d\<sharp>a"
wenzelm@36277
   404
  shows "(\<exists>N'. (R = OrR2 <c>.N' d) \<and> N'[a\<turnstile>c>b] = N) \<or>
wenzelm@36277
   405
         (\<exists>N'. (R = OrR2 <c>.N' a) \<and> b=d \<and> N'[a\<turnstile>c>b] = N)" 
wenzelm@36277
   406
using a
wenzelm@36277
   407
apply(nominal_induct R avoiding: a b c d N rule: trm.strong_induct)
wenzelm@36277
   408
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
wenzelm@36277
   409
apply(rule_tac x="[(coname1,c)]\<bullet>trm" in exI)
wenzelm@36277
   410
apply(perm_simp)
wenzelm@36277
   411
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
   412
apply(drule sym)
wenzelm@36277
   413
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
wenzelm@36277
   414
apply(simp add: eqvts calc_atm)
wenzelm@36277
   415
apply(rule_tac x="[(coname1,c)]\<bullet>trm" in exI)
wenzelm@36277
   416
apply(perm_simp)
wenzelm@36277
   417
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
   418
apply(drule sym)
wenzelm@36277
   419
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
wenzelm@36277
   420
apply(simp add: eqvts calc_atm)
wenzelm@36277
   421
done
wenzelm@36277
   422
wenzelm@36277
   423
lemma crename_OrL:
wenzelm@36277
   424
  assumes a: "R[a\<turnstile>c>b] = OrL (x).M (y).N z" "x\<sharp>(y,z,N,R)" "y\<sharp>(x,z,M,R)"
wenzelm@36277
   425
  shows "\<exists>M' N'. R = OrL (x).M' (y).N' z \<and> M'[a\<turnstile>c>b] = M \<and> N'[a\<turnstile>c>b] = N \<and> x\<sharp>N' \<and> y\<sharp>M'"
wenzelm@36277
   426
using a
wenzelm@36277
   427
apply(nominal_induct R avoiding: a b x y z M N rule: trm.strong_induct)
wenzelm@36277
   428
apply(auto split: if_splits simp add: trm.inject alpha)
wenzelm@36277
   429
apply(rule_tac x="[(name2,y)]\<bullet>trm2" in exI)
wenzelm@36277
   430
apply(perm_simp)
wenzelm@36277
   431
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
wenzelm@36277
   432
apply(rule_tac x="[(name1,x)]\<bullet>trm1" in exI)
wenzelm@36277
   433
apply(perm_simp)
wenzelm@36277
   434
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
wenzelm@36277
   435
apply(rule_tac x="[(name1,x)]\<bullet>trm1" in exI)
wenzelm@36277
   436
apply(perm_simp)
wenzelm@36277
   437
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
wenzelm@36277
   438
apply(rule_tac x="[(name2,y)]\<bullet>trm2" in exI)
wenzelm@36277
   439
apply(perm_simp)
wenzelm@36277
   440
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
wenzelm@36277
   441
apply(drule sym)
wenzelm@36277
   442
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
   443
apply(simp add: eqvts calc_atm)
wenzelm@36277
   444
apply(drule_tac s="trm2[a\<turnstile>c>b]" in  sym)
wenzelm@36277
   445
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
   446
apply(simp add: eqvts calc_atm)
wenzelm@36277
   447
done
wenzelm@36277
   448
wenzelm@36277
   449
lemma crename_ImpL:
wenzelm@36277
   450
  assumes a: "R[a\<turnstile>c>b] = ImpL <c>.M (y).N z" "c\<sharp>(a,b,N,R)" "y\<sharp>(z,M,R)"
wenzelm@36277
   451
  shows "\<exists>M' N'. R = ImpL <c>.M' (y).N' z \<and> M'[a\<turnstile>c>b] = M \<and> N'[a\<turnstile>c>b] = N \<and> c\<sharp>N' \<and> y\<sharp>M'"
wenzelm@36277
   452
using a
wenzelm@36277
   453
apply(nominal_induct R avoiding: a b c y z M N rule: trm.strong_induct)
wenzelm@36277
   454
apply(auto split: if_splits simp add: trm.inject alpha)
wenzelm@36277
   455
apply(rule_tac x="[(name1,y)]\<bullet>trm2" in exI)
wenzelm@36277
   456
apply(perm_simp)
wenzelm@36277
   457
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
wenzelm@36277
   458
apply(rule_tac x="[(coname,c)]\<bullet>trm1" in exI)
wenzelm@36277
   459
apply(perm_simp)
wenzelm@36277
   460
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
wenzelm@36277
   461
apply(rule_tac x="[(coname,c)]\<bullet>trm1" in exI)
wenzelm@36277
   462
apply(perm_simp)
wenzelm@36277
   463
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
wenzelm@36277
   464
apply(rule_tac x="[(name1,y)]\<bullet>trm2" in exI)
wenzelm@36277
   465
apply(perm_simp)
wenzelm@36277
   466
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
wenzelm@36277
   467
apply(drule sym)
wenzelm@36277
   468
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
wenzelm@36277
   469
apply(simp add: eqvts calc_atm)
wenzelm@36277
   470
apply(drule_tac s="trm2[a\<turnstile>c>b]" in  sym)
wenzelm@36277
   471
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
   472
apply(simp add: eqvts calc_atm)
wenzelm@36277
   473
done
wenzelm@36277
   474
wenzelm@36277
   475
lemma crename_ImpR_aux:
wenzelm@36277
   476
  assumes a: "R[a\<turnstile>c>b] = ImpR (x).<c>.M e" 
wenzelm@36277
   477
  shows "(a=e \<and> a=b) \<or> (a\<noteq>e)" 
wenzelm@36277
   478
using a
wenzelm@36277
   479
apply(nominal_induct R avoiding: x a b c e M rule: trm.strong_induct)
wenzelm@36277
   480
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
wenzelm@36277
   481
done
wenzelm@36277
   482
wenzelm@36277
   483
lemma crename_ImpR:
wenzelm@36277
   484
  assumes a: "R[a\<turnstile>c>b] = ImpR (x).<c>.N d" "c\<sharp>(R,a,b)" "d\<sharp>(a,b)" "x\<sharp>R" 
wenzelm@36277
   485
  shows "\<exists>N'. (R = ImpR (x).<c>.N' d) \<and> N'[a\<turnstile>c>b] = N" 
wenzelm@36277
   486
using a
wenzelm@36277
   487
apply(nominal_induct R avoiding: a b x c d N rule: trm.strong_induct)
wenzelm@36277
   488
apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_perm alpha abs_fresh trm.inject)
wenzelm@36277
   489
apply(rule_tac x="[(name,x)]\<bullet>trm" in exI)
wenzelm@36277
   490
apply(perm_simp)
wenzelm@36277
   491
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
   492
apply(rule_tac x="[(name,x)]\<bullet>[(coname1, c)]\<bullet>trm" in exI)
wenzelm@36277
   493
apply(perm_simp)
wenzelm@36277
   494
apply(simp add: abs_supp fin_supp abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
   495
apply(drule sym)
wenzelm@36277
   496
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
wenzelm@36277
   497
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
   498
apply(simp add: eqvts calc_atm)
wenzelm@36277
   499
done
wenzelm@36277
   500
wenzelm@36277
   501
lemma crename_ImpR':
wenzelm@36277
   502
  assumes a: "R[a\<turnstile>c>b] = ImpR (x).<c>.N d" "c\<sharp>(R,a,b)" "x\<sharp>R" "d\<sharp>a"
wenzelm@36277
   503
  shows "(\<exists>N'. (R = ImpR (x).<c>.N' d) \<and> N'[a\<turnstile>c>b] = N) \<or>
wenzelm@36277
   504
         (\<exists>N'. (R = ImpR (x).<c>.N' a) \<and> b=d \<and> N'[a\<turnstile>c>b] = N)" 
wenzelm@36277
   505
using a
wenzelm@36277
   506
apply(nominal_induct R avoiding: x a b c d N rule: trm.strong_induct)
wenzelm@36277
   507
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject abs_perm calc_atm)
wenzelm@36277
   508
apply(rule_tac x="[(name,x)]\<bullet>[(coname1,c)]\<bullet>trm" in exI)
wenzelm@36277
   509
apply(perm_simp)
wenzelm@36277
   510
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod abs_supp fin_supp)
wenzelm@36277
   511
apply(drule sym)
wenzelm@36277
   512
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
wenzelm@36277
   513
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
   514
apply(simp add: eqvts calc_atm)
wenzelm@36277
   515
apply(rule_tac x="[(name,x)]\<bullet>[(coname1,c)]\<bullet>trm" in exI)
wenzelm@36277
   516
apply(perm_simp)
wenzelm@36277
   517
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod abs_supp fin_supp)
wenzelm@36277
   518
apply(drule sym)
wenzelm@36277
   519
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
wenzelm@36277
   520
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
   521
apply(simp add: eqvts calc_atm)
wenzelm@36277
   522
done
wenzelm@36277
   523
wenzelm@36277
   524
lemma crename_ax2:
wenzelm@36277
   525
  assumes a: "N[a\<turnstile>c>b] = Ax x c"
wenzelm@36277
   526
  shows "\<exists>d. N = Ax x d"
wenzelm@36277
   527
using a
wenzelm@36277
   528
apply(nominal_induct N avoiding: a b rule: trm.strong_induct)
wenzelm@36277
   529
apply(auto split: if_splits)
wenzelm@36277
   530
apply(simp add: trm.inject)
wenzelm@36277
   531
done
wenzelm@36277
   532
wenzelm@36277
   533
lemma crename_interesting1:
wenzelm@36277
   534
  assumes a: "distinct [a,b,c]"
wenzelm@36277
   535
  shows "M[a\<turnstile>c>c][c\<turnstile>c>b] = M[c\<turnstile>c>b][a\<turnstile>c>b]"
wenzelm@36277
   536
using a
wenzelm@36277
   537
apply(nominal_induct M avoiding: a c b rule: trm.strong_induct)
wenzelm@36277
   538
apply(auto simp add: rename_fresh simp add: trm.inject alpha)
wenzelm@36277
   539
apply(blast)
wenzelm@36277
   540
apply(rotate_tac 12)
wenzelm@36277
   541
apply(drule_tac x="a" in meta_spec)
wenzelm@36277
   542
apply(rotate_tac 15)
wenzelm@36277
   543
apply(drule_tac x="c" in meta_spec)
wenzelm@36277
   544
apply(rotate_tac 15)
wenzelm@36277
   545
apply(drule_tac x="b" in meta_spec)
wenzelm@36277
   546
apply(blast)
wenzelm@36277
   547
apply(blast)
wenzelm@36277
   548
apply(blast)
wenzelm@36277
   549
done
wenzelm@36277
   550
wenzelm@36277
   551
lemma crename_interesting2:
wenzelm@36277
   552
  assumes a: "a\<noteq>c" "a\<noteq>d" "a\<noteq>b" "c\<noteq>d" "b\<noteq>c"
wenzelm@36277
   553
  shows "M[a\<turnstile>c>b][c\<turnstile>c>d] = M[c\<turnstile>c>d][a\<turnstile>c>b]"
wenzelm@36277
   554
using a
wenzelm@36277
   555
apply(nominal_induct M avoiding: a c b d rule: trm.strong_induct)
wenzelm@36277
   556
apply(auto simp add: rename_fresh simp add: trm.inject alpha)
wenzelm@36277
   557
done
wenzelm@36277
   558
wenzelm@36277
   559
lemma crename_interesting3:
wenzelm@36277
   560
  shows "M[a\<turnstile>c>c][x\<turnstile>n>y] = M[x\<turnstile>n>y][a\<turnstile>c>c]"
wenzelm@36277
   561
apply(nominal_induct M avoiding: a c x y rule: trm.strong_induct)
wenzelm@36277
   562
apply(auto simp add: rename_fresh simp add: trm.inject alpha)
wenzelm@36277
   563
done
wenzelm@36277
   564
wenzelm@36277
   565
lemma crename_credu:
wenzelm@53015
   566
  assumes a: "(M[a\<turnstile>c>b]) \<longrightarrow>\<^sub>c M'"
wenzelm@53015
   567
  shows "\<exists>M0. M0[a\<turnstile>c>b]=M' \<and> M \<longrightarrow>\<^sub>c M0"
wenzelm@36277
   568
using a
wenzelm@36277
   569
apply(nominal_induct M\<equiv>"M[a\<turnstile>c>b]" M' avoiding: M a b rule: c_redu.strong_induct)
wenzelm@36277
   570
apply(drule sym)
wenzelm@36277
   571
apply(drule crename_Cut)
wenzelm@36277
   572
apply(simp)
wenzelm@36277
   573
apply(simp)
wenzelm@36277
   574
apply(auto)
wenzelm@36277
   575
apply(rule_tac x="M'{a:=(x).N'}" in exI)
wenzelm@36277
   576
apply(rule conjI)
wenzelm@36277
   577
apply(simp add: fresh_atm abs_fresh subst_comm fresh_prod)
wenzelm@36277
   578
apply(rule c_redu.intros)
wenzelm@36277
   579
apply(auto dest: not_fic_crename)[1]
wenzelm@36277
   580
apply(simp add: abs_fresh)
wenzelm@36277
   581
apply(simp add: abs_fresh)
wenzelm@36277
   582
apply(drule sym)
wenzelm@36277
   583
apply(drule crename_Cut)
wenzelm@36277
   584
apply(simp)
wenzelm@36277
   585
apply(simp)
wenzelm@36277
   586
apply(auto)
wenzelm@36277
   587
apply(rule_tac x="N'{x:=<a>.M'}" in exI)
wenzelm@36277
   588
apply(rule conjI)
wenzelm@36277
   589
apply(simp add: fresh_atm abs_fresh subst_comm fresh_prod)
wenzelm@36277
   590
apply(rule c_redu.intros)
wenzelm@36277
   591
apply(auto dest: not_fin_crename)[1]
wenzelm@36277
   592
apply(simp add: abs_fresh)
wenzelm@36277
   593
apply(simp add: abs_fresh)
wenzelm@36277
   594
done
wenzelm@36277
   595
wenzelm@36277
   596
lemma crename_lredu:
wenzelm@53015
   597
  assumes a: "(M[a\<turnstile>c>b]) \<longrightarrow>\<^sub>l M'"
wenzelm@53015
   598
  shows "\<exists>M0. M0[a\<turnstile>c>b]=M' \<and> M \<longrightarrow>\<^sub>l M0"
wenzelm@36277
   599
using a
wenzelm@36277
   600
apply(nominal_induct M\<equiv>"M[a\<turnstile>c>b]" M' avoiding: M a b rule: l_redu.strong_induct)
wenzelm@36277
   601
apply(drule sym)
wenzelm@36277
   602
apply(drule crename_Cut)
wenzelm@36277
   603
apply(simp add: fresh_prod fresh_atm)
wenzelm@36277
   604
apply(simp)
wenzelm@36277
   605
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
wenzelm@36277
   606
apply(case_tac "aa=ba")
wenzelm@36277
   607
apply(simp add: crename_id)
wenzelm@36277
   608
apply(rule l_redu.intros)
wenzelm@36277
   609
apply(simp)
wenzelm@36277
   610
apply(simp add: fresh_atm)
wenzelm@36277
   611
apply(assumption)
wenzelm@36277
   612
apply(frule crename_ax2)
wenzelm@36277
   613
apply(auto)[1]
wenzelm@36277
   614
apply(case_tac "d=aa")
wenzelm@36277
   615
apply(simp add: trm.inject)
wenzelm@36277
   616
apply(rule_tac x="M'[a\<turnstile>c>aa]" in exI)
wenzelm@36277
   617
apply(rule conjI)
wenzelm@36277
   618
apply(rule crename_interesting1)
wenzelm@36277
   619
apply(simp)
wenzelm@36277
   620
apply(rule l_redu.intros)
wenzelm@36277
   621
apply(simp)
wenzelm@36277
   622
apply(simp add: fresh_atm)
wenzelm@36277
   623
apply(auto dest: fic_crename simp add: fresh_prod fresh_atm)[1]
wenzelm@36277
   624
apply(simp add: trm.inject)
wenzelm@36277
   625
apply(rule_tac x="M'[a\<turnstile>c>b]" in exI)
wenzelm@36277
   626
apply(rule conjI)
wenzelm@36277
   627
apply(rule crename_interesting2)
wenzelm@36277
   628
apply(simp)
wenzelm@36277
   629
apply(simp)
wenzelm@36277
   630
apply(simp)
wenzelm@36277
   631
apply(simp)
wenzelm@36277
   632
apply(simp)
wenzelm@36277
   633
apply(rule l_redu.intros)
wenzelm@36277
   634
apply(simp)
wenzelm@36277
   635
apply(simp add: fresh_atm)
wenzelm@36277
   636
apply(auto dest: fic_crename simp add: fresh_prod fresh_atm)[1]
wenzelm@36277
   637
apply(drule sym)
wenzelm@36277
   638
apply(drule crename_Cut)
wenzelm@36277
   639
apply(simp add: fresh_prod fresh_atm)
wenzelm@36277
   640
apply(simp add: fresh_prod fresh_atm)
wenzelm@36277
   641
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
wenzelm@36277
   642
apply(case_tac "aa=b")
wenzelm@36277
   643
apply(simp add: crename_id)
wenzelm@36277
   644
apply(rule l_redu.intros)
wenzelm@36277
   645
apply(simp)
wenzelm@36277
   646
apply(simp add: fresh_atm)
wenzelm@36277
   647
apply(assumption)
wenzelm@36277
   648
apply(frule crename_ax2)
wenzelm@36277
   649
apply(auto)[1]
wenzelm@36277
   650
apply(case_tac "d=aa")
wenzelm@36277
   651
apply(simp add: trm.inject)
wenzelm@36277
   652
apply(simp add: trm.inject)
wenzelm@36277
   653
apply(rule_tac x="N'[x\<turnstile>n>y]" in exI)
wenzelm@36277
   654
apply(rule conjI)
wenzelm@36277
   655
apply(rule sym)
wenzelm@36277
   656
apply(rule crename_interesting3)
wenzelm@36277
   657
apply(rule l_redu.intros)
wenzelm@36277
   658
apply(simp)
wenzelm@36277
   659
apply(simp add: fresh_atm)
wenzelm@36277
   660
apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
wenzelm@36277
   661
(* LNot *)
wenzelm@36277
   662
apply(drule sym)
wenzelm@36277
   663
apply(drule crename_Cut)
wenzelm@36277
   664
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
   665
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
   666
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
wenzelm@36277
   667
apply(drule crename_NotR)
wenzelm@36277
   668
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
   669
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
   670
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
wenzelm@36277
   671
apply(drule crename_NotL)
wenzelm@36277
   672
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
   673
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
wenzelm@36277
   674
apply(rule_tac x="Cut <b>.N'b (x).N'a" in exI)
wenzelm@36277
   675
apply(simp add: fresh_atm)[1]
wenzelm@36277
   676
apply(rule l_redu.intros)
wenzelm@36277
   677
apply(auto simp add: fresh_prod intro: crename_fresh_interesting2)[1]
wenzelm@36277
   678
apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting2)[1]
wenzelm@36277
   679
apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
wenzelm@36277
   680
apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
wenzelm@36277
   681
apply(simp add: fresh_atm)
wenzelm@36277
   682
apply(simp add: fresh_atm)
wenzelm@36277
   683
(* LAnd1 *)
wenzelm@36277
   684
apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
wenzelm@36277
   685
apply(drule sym)
wenzelm@36277
   686
apply(drule crename_Cut)
wenzelm@36277
   687
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
   688
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
   689
apply(auto)[1]
wenzelm@36277
   690
apply(drule crename_AndR)
wenzelm@36277
   691
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
   692
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
   693
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
wenzelm@36277
   694
apply(drule crename_AndL1)
wenzelm@36277
   695
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
   696
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
wenzelm@36277
   697
apply(rule_tac x="Cut <a1>.M'a (x).N'a" in exI)
wenzelm@36277
   698
apply(simp add: fresh_atm)[1]
wenzelm@36277
   699
apply(rule l_redu.intros)
wenzelm@36277
   700
apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: crename_fresh_interesting1)[1]
wenzelm@36277
   701
apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting2)[1]
wenzelm@36277
   702
apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
wenzelm@36277
   703
apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
wenzelm@36277
   704
apply(simp add: fresh_atm)
wenzelm@36277
   705
apply(simp add: fresh_atm)
wenzelm@36277
   706
(* LAnd2 *)
wenzelm@36277
   707
apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
wenzelm@36277
   708
apply(drule sym)
wenzelm@36277
   709
apply(drule crename_Cut)
wenzelm@36277
   710
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
   711
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
   712
apply(auto)[1]
wenzelm@36277
   713
apply(drule crename_AndR)
wenzelm@36277
   714
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
   715
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
   716
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
wenzelm@36277
   717
apply(drule crename_AndL2)
wenzelm@36277
   718
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
   719
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
wenzelm@36277
   720
apply(rule_tac x="Cut <a2>.N'b (x).N'a" in exI)
wenzelm@36277
   721
apply(simp add: fresh_atm)[1]
wenzelm@36277
   722
apply(rule l_redu.intros)
wenzelm@36277
   723
apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: crename_fresh_interesting1)[1]
wenzelm@36277
   724
apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting2)[1]
wenzelm@36277
   725
apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
wenzelm@36277
   726
apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
wenzelm@36277
   727
apply(simp add: fresh_atm)
wenzelm@36277
   728
apply(simp add: fresh_atm)
wenzelm@36277
   729
(* LOr1 *)
wenzelm@36277
   730
apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
wenzelm@36277
   731
apply(drule sym)
wenzelm@36277
   732
apply(drule crename_Cut)
wenzelm@36277
   733
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
   734
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
   735
apply(auto)[1]
wenzelm@36277
   736
apply(drule crename_OrL)
wenzelm@36277
   737
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
   738
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
   739
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
wenzelm@36277
   740
apply(drule crename_OrR1)
wenzelm@36277
   741
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
   742
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
wenzelm@36277
   743
apply(auto)
wenzelm@36277
   744
apply(rule_tac x="Cut <a>.N' (x1).M'a" in exI)
wenzelm@36277
   745
apply(rule conjI)
wenzelm@36277
   746
apply(simp add: abs_fresh fresh_atm)[1]
wenzelm@36277
   747
apply(rule l_redu.intros)
wenzelm@36277
   748
apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: crename_fresh_interesting1)[1]
wenzelm@36277
   749
apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting2)[1]
wenzelm@36277
   750
apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
wenzelm@36277
   751
apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
wenzelm@36277
   752
apply(simp add: fresh_atm)
wenzelm@36277
   753
apply(simp add: fresh_atm)
wenzelm@36277
   754
(* LOr2 *)
wenzelm@36277
   755
apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
wenzelm@36277
   756
apply(drule sym)
wenzelm@36277
   757
apply(drule crename_Cut)
wenzelm@36277
   758
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
   759
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
   760
apply(auto)[1]
wenzelm@36277
   761
apply(drule crename_OrL)
wenzelm@36277
   762
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
   763
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
   764
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
wenzelm@36277
   765
apply(drule crename_OrR2)
wenzelm@36277
   766
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
   767
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
wenzelm@36277
   768
apply(auto)
wenzelm@36277
   769
apply(rule_tac x="Cut <a>.N' (x2).N'a" in exI)
wenzelm@36277
   770
apply(rule conjI)
wenzelm@36277
   771
apply(simp add: abs_fresh fresh_atm)[1]
wenzelm@36277
   772
apply(rule l_redu.intros)
wenzelm@36277
   773
apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: crename_fresh_interesting1)[1]
wenzelm@36277
   774
apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting2)[1]
wenzelm@36277
   775
apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
wenzelm@36277
   776
apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
wenzelm@36277
   777
apply(simp add: fresh_atm)
wenzelm@36277
   778
apply(simp add: fresh_atm)
wenzelm@36277
   779
(* ImpL *)
wenzelm@36277
   780
apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
wenzelm@36277
   781
apply(drule sym)
wenzelm@36277
   782
apply(drule crename_Cut)
wenzelm@36277
   783
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
   784
apply(simp add: fresh_prod abs_fresh fresh_atm abs_supp fin_supp)
wenzelm@36277
   785
apply(auto)[1]
wenzelm@36277
   786
apply(drule crename_ImpL)
wenzelm@36277
   787
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
   788
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
   789
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
wenzelm@36277
   790
apply(drule crename_ImpR)
wenzelm@36277
   791
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
   792
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
   793
apply(simp)
wenzelm@36277
   794
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
wenzelm@36277
   795
apply(rule_tac x="Cut <a>.(Cut <c>.M'a (x).N') (y).N'a" in exI)
wenzelm@36277
   796
apply(rule conjI)
wenzelm@36277
   797
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
   798
apply(rule l_redu.intros)
wenzelm@36277
   799
apply(auto simp add: fresh_atm abs_fresh abs_supp fin_supp fresh_prod intro: crename_fresh_interesting2)[1]
wenzelm@36277
   800
apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: crename_fresh_interesting1)[1]
wenzelm@36277
   801
apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: crename_fresh_interesting2)[1]
wenzelm@36277
   802
apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: crename_fresh_interesting1)[1]
wenzelm@36277
   803
apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: crename_fresh_interesting1)[1]
wenzelm@36277
   804
apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: crename_fresh_interesting1)[1]
wenzelm@36277
   805
done
wenzelm@36277
   806
wenzelm@36277
   807
lemma crename_aredu:
wenzelm@53015
   808
  assumes a: "(M[a\<turnstile>c>b]) \<longrightarrow>\<^sub>a M'" "a\<noteq>b"
wenzelm@53015
   809
  shows "\<exists>M0. M0[a\<turnstile>c>b]=M' \<and> M \<longrightarrow>\<^sub>a M0"
wenzelm@36277
   810
using a
wenzelm@36277
   811
apply(nominal_induct "M[a\<turnstile>c>b]" M' avoiding: M a b rule: a_redu.strong_induct)
wenzelm@36277
   812
apply(drule  crename_lredu)
wenzelm@36277
   813
apply(blast)
wenzelm@36277
   814
apply(drule  crename_credu)
wenzelm@36277
   815
apply(blast)
wenzelm@36277
   816
(* Cut *)
wenzelm@36277
   817
apply(drule sym)
wenzelm@36277
   818
apply(drule crename_Cut)
wenzelm@36277
   819
apply(simp)
wenzelm@36277
   820
apply(simp)
wenzelm@36277
   821
apply(auto)[1]
wenzelm@36277
   822
apply(drule_tac x="M'a" in meta_spec)
wenzelm@36277
   823
apply(drule_tac x="aa" in meta_spec)
wenzelm@36277
   824
apply(drule_tac x="b" in meta_spec)
wenzelm@36277
   825
apply(auto)[1]
wenzelm@36277
   826
apply(rule_tac x="Cut <a>.M0 (x).N'" in exI)
wenzelm@36277
   827
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
   828
apply(rule conjI)
wenzelm@36277
   829
apply(rule trans)
wenzelm@36277
   830
apply(rule crename.simps)
wenzelm@36277
   831
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
   832
apply(drule crename_fresh_interesting2)
wenzelm@36277
   833
apply(simp add: fresh_a_redu)
wenzelm@36277
   834
apply(simp)
wenzelm@36277
   835
apply(auto)[1]
wenzelm@36277
   836
apply(drule sym)
wenzelm@36277
   837
apply(drule crename_Cut)
wenzelm@36277
   838
apply(simp)
wenzelm@36277
   839
apply(simp)
wenzelm@36277
   840
apply(auto)[1]
wenzelm@36277
   841
apply(drule_tac x="N'a" in meta_spec)
wenzelm@36277
   842
apply(drule_tac x="aa" in meta_spec)
wenzelm@36277
   843
apply(drule_tac x="b" in meta_spec)
wenzelm@36277
   844
apply(auto)[1]
wenzelm@36277
   845
apply(rule_tac x="Cut <a>.M' (x).M0" in exI)
wenzelm@36277
   846
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
   847
apply(rule conjI)
wenzelm@36277
   848
apply(rule trans)
wenzelm@36277
   849
apply(rule crename.simps)
wenzelm@36277
   850
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
wenzelm@36277
   851
apply(drule crename_fresh_interesting1)
wenzelm@36277
   852
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
   853
apply(simp add: fresh_a_redu)
wenzelm@36277
   854
apply(simp)
wenzelm@36277
   855
apply(simp)
wenzelm@36277
   856
apply(auto)[1]
wenzelm@36277
   857
(* NotL *)
wenzelm@36277
   858
apply(drule sym)
wenzelm@36277
   859
apply(drule crename_NotL)
wenzelm@36277
   860
apply(simp)
wenzelm@36277
   861
apply(auto)[1]
wenzelm@36277
   862
apply(drule_tac x="N'" in meta_spec)
wenzelm@36277
   863
apply(drule_tac x="aa" in meta_spec)
wenzelm@36277
   864
apply(drule_tac x="b" in meta_spec)
wenzelm@36277
   865
apply(auto)[1]
wenzelm@36277
   866
apply(rule_tac x="NotL <a>.M0 x" in exI)
wenzelm@36277
   867
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
   868
apply(auto)[1]
wenzelm@36277
   869
(* NotR *)
wenzelm@36277
   870
apply(drule sym)
wenzelm@36277
   871
apply(frule crename_NotR_aux)
wenzelm@36277
   872
apply(erule disjE)
wenzelm@36277
   873
apply(auto)[1]
wenzelm@36277
   874
apply(drule crename_NotR')
wenzelm@36277
   875
apply(simp)
wenzelm@36277
   876
apply(simp add: fresh_atm)
wenzelm@36277
   877
apply(erule disjE)
wenzelm@36277
   878
apply(auto)[1]
wenzelm@36277
   879
apply(drule_tac x="N'" in meta_spec)
wenzelm@36277
   880
apply(drule_tac x="aa" in meta_spec)
wenzelm@36277
   881
apply(drule_tac x="b" in meta_spec)
wenzelm@36277
   882
apply(auto)[1]
wenzelm@36277
   883
apply(rule_tac x="NotR (x).M0 a" in exI)
wenzelm@36277
   884
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
   885
apply(auto)[1]
wenzelm@36277
   886
apply(auto)[1]
wenzelm@36277
   887
apply(drule_tac x="N'" in meta_spec)
wenzelm@36277
   888
apply(drule_tac x="aa" in meta_spec)
wenzelm@36277
   889
apply(drule_tac x="a" in meta_spec)
wenzelm@36277
   890
apply(auto)[1]
wenzelm@36277
   891
apply(rule_tac x="NotR (x).M0 aa" in exI)
wenzelm@36277
   892
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
   893
apply(auto)[1]
wenzelm@36277
   894
(* AndR *)
wenzelm@36277
   895
apply(drule sym)
wenzelm@36277
   896
apply(frule crename_AndR_aux)
wenzelm@36277
   897
apply(erule disjE)
wenzelm@36277
   898
apply(auto)[1]
wenzelm@36277
   899
apply(drule crename_AndR')
wenzelm@36277
   900
apply(simp add: fresh_prod fresh_atm)
wenzelm@36277
   901
apply(simp add: fresh_atm)
wenzelm@36277
   902
apply(simp add: fresh_atm)
wenzelm@36277
   903
apply(erule disjE)
wenzelm@36277
   904
apply(auto)[1]
wenzelm@36277
   905
apply(drule_tac x="M'a" in meta_spec)
wenzelm@36277
   906
apply(drule_tac x="aa" in meta_spec)
wenzelm@36277
   907
apply(drule_tac x="ba" in meta_spec)
wenzelm@36277
   908
apply(auto)[1]
wenzelm@36277
   909
apply(rule_tac x="AndR <a>.M0 <b>.N' c" in exI)
wenzelm@36277
   910
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
   911
apply(auto)[1]
wenzelm@36277
   912
apply(rule trans)
wenzelm@36277
   913
apply(rule crename.simps)
wenzelm@36277
   914
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
   915
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
   916
apply(auto intro: fresh_a_redu)[1]
wenzelm@36277
   917
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
   918
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
   919
apply(auto)[1]
wenzelm@36277
   920
apply(drule_tac x="M'a" in meta_spec)
wenzelm@36277
   921
apply(drule_tac x="aa" in meta_spec)
wenzelm@36277
   922
apply(drule_tac x="c" in meta_spec)
wenzelm@36277
   923
apply(auto)[1]
wenzelm@36277
   924
apply(rule_tac x="AndR <a>.M0 <b>.N' aa" in exI)
wenzelm@36277
   925
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
   926
apply(auto)[1]
wenzelm@36277
   927
apply(rule trans)
wenzelm@36277
   928
apply(rule crename.simps)
wenzelm@36277
   929
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
   930
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
   931
apply(auto intro: fresh_a_redu)[1]
wenzelm@36277
   932
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
   933
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
   934
apply(drule sym)
wenzelm@36277
   935
apply(frule crename_AndR_aux)
wenzelm@36277
   936
apply(erule disjE)
wenzelm@36277
   937
apply(auto)[1]
wenzelm@36277
   938
apply(drule crename_AndR')
wenzelm@36277
   939
apply(simp add: fresh_prod fresh_atm)
wenzelm@36277
   940
apply(simp add: fresh_atm)
wenzelm@36277
   941
apply(simp add: fresh_atm)
wenzelm@36277
   942
apply(erule disjE)
wenzelm@36277
   943
apply(auto)[1]
wenzelm@36277
   944
apply(drule_tac x="N'a" in meta_spec)
wenzelm@36277
   945
apply(drule_tac x="aa" in meta_spec)
wenzelm@36277
   946
apply(drule_tac x="ba" in meta_spec)
wenzelm@36277
   947
apply(auto)[1]
wenzelm@36277
   948
apply(rule_tac x="AndR <a>.M' <b>.M0 c" in exI)
wenzelm@36277
   949
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
   950
apply(auto)[1]
wenzelm@36277
   951
apply(rule trans)
wenzelm@36277
   952
apply(rule crename.simps)
wenzelm@36277
   953
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
wenzelm@36277
   954
apply(auto intro: fresh_a_redu)[1]
wenzelm@36277
   955
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
   956
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
   957
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
   958
apply(auto)[1]
wenzelm@36277
   959
apply(drule_tac x="N'a" in meta_spec)
wenzelm@36277
   960
apply(drule_tac x="aa" in meta_spec)
wenzelm@36277
   961
apply(drule_tac x="c" in meta_spec)
wenzelm@36277
   962
apply(auto)[1]
wenzelm@36277
   963
apply(rule_tac x="AndR <a>.M' <b>.M0 aa" in exI)
wenzelm@36277
   964
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
   965
apply(auto)[1]
wenzelm@36277
   966
apply(rule trans)
wenzelm@36277
   967
apply(rule crename.simps)
wenzelm@36277
   968
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
wenzelm@36277
   969
apply(auto intro: fresh_a_redu)[1]
wenzelm@36277
   970
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
   971
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
   972
apply(simp)
wenzelm@36277
   973
(* AndL1 *)
wenzelm@36277
   974
apply(drule sym)
wenzelm@36277
   975
apply(drule crename_AndL1)
wenzelm@36277
   976
apply(simp)
wenzelm@36277
   977
apply(auto)[1]
wenzelm@36277
   978
apply(drule_tac x="N'" in meta_spec)
wenzelm@36277
   979
apply(drule_tac x="a" in meta_spec)
wenzelm@36277
   980
apply(drule_tac x="b" in meta_spec)
wenzelm@36277
   981
apply(auto)[1]
wenzelm@36277
   982
apply(rule_tac x="AndL1 (x).M0 y" in exI)
wenzelm@36277
   983
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
   984
apply(auto)[1]
wenzelm@36277
   985
(* AndL2 *)
wenzelm@36277
   986
apply(drule sym)
wenzelm@36277
   987
apply(drule crename_AndL2)
wenzelm@36277
   988
apply(simp)
wenzelm@36277
   989
apply(auto)[1]
wenzelm@36277
   990
apply(drule_tac x="N'" in meta_spec)
wenzelm@36277
   991
apply(drule_tac x="a" in meta_spec)
wenzelm@36277
   992
apply(drule_tac x="b" in meta_spec)
wenzelm@36277
   993
apply(auto)[1]
wenzelm@36277
   994
apply(rule_tac x="AndL2 (x).M0 y" in exI)
wenzelm@36277
   995
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
   996
apply(auto)[1]
wenzelm@36277
   997
(* OrL *)
wenzelm@36277
   998
apply(drule sym)
wenzelm@36277
   999
apply(drule crename_OrL)
wenzelm@36277
  1000
apply(simp)
wenzelm@36277
  1001
apply(auto simp add: fresh_atm fresh_prod)[1]
wenzelm@36277
  1002
apply(auto simp add: fresh_atm fresh_prod)[1]
wenzelm@36277
  1003
apply(auto)[1]
wenzelm@36277
  1004
apply(drule_tac x="M'a" in meta_spec)
wenzelm@36277
  1005
apply(drule_tac x="a" in meta_spec)
wenzelm@36277
  1006
apply(drule_tac x="b" in meta_spec)
wenzelm@36277
  1007
apply(auto)[1]
wenzelm@36277
  1008
apply(rule_tac x="OrL (x).M0 (y).N' z" in exI)
wenzelm@36277
  1009
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  1010
apply(auto)[1]
wenzelm@36277
  1011
apply(rule trans)
wenzelm@36277
  1012
apply(rule crename.simps)
wenzelm@36277
  1013
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
wenzelm@36277
  1014
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  1015
apply(auto intro: fresh_a_redu)[1]
wenzelm@36277
  1016
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  1017
apply(simp)
wenzelm@36277
  1018
apply(drule sym)
wenzelm@36277
  1019
apply(drule crename_OrL)
wenzelm@36277
  1020
apply(simp)
wenzelm@36277
  1021
apply(auto simp add: fresh_atm fresh_prod)[1]
wenzelm@36277
  1022
apply(auto simp add: fresh_atm fresh_prod)[1]
wenzelm@36277
  1023
apply(auto)[1]
wenzelm@36277
  1024
apply(drule_tac x="N'a" in meta_spec)
wenzelm@36277
  1025
apply(drule_tac x="a" in meta_spec)
wenzelm@36277
  1026
apply(drule_tac x="b" in meta_spec)
wenzelm@36277
  1027
apply(auto)[1]
wenzelm@36277
  1028
apply(rule_tac x="OrL (x).M' (y).M0 z" in exI)
wenzelm@36277
  1029
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  1030
apply(auto)[1]
wenzelm@36277
  1031
apply(rule trans)
wenzelm@36277
  1032
apply(rule crename.simps)
wenzelm@36277
  1033
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
wenzelm@36277
  1034
apply(auto intro: fresh_a_redu)[1]
wenzelm@36277
  1035
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  1036
apply(simp)
wenzelm@36277
  1037
apply(simp)
wenzelm@36277
  1038
(* OrR1 *)
wenzelm@36277
  1039
apply(drule sym)
wenzelm@36277
  1040
apply(frule crename_OrR1_aux)
wenzelm@36277
  1041
apply(erule disjE)
wenzelm@36277
  1042
apply(auto)[1]
wenzelm@36277
  1043
apply(drule crename_OrR1')
wenzelm@36277
  1044
apply(simp)
wenzelm@36277
  1045
apply(simp add: fresh_atm)
wenzelm@36277
  1046
apply(erule disjE)
wenzelm@36277
  1047
apply(auto)[1]
wenzelm@36277
  1048
apply(drule_tac x="N'" in meta_spec)
wenzelm@36277
  1049
apply(drule_tac x="aa" in meta_spec)
wenzelm@36277
  1050
apply(drule_tac x="ba" in meta_spec)
wenzelm@36277
  1051
apply(auto)[1]
wenzelm@36277
  1052
apply(rule_tac x="OrR1 <a>.M0 b" in exI)
wenzelm@36277
  1053
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  1054
apply(auto)[1]
wenzelm@36277
  1055
apply(auto)[1]
wenzelm@36277
  1056
apply(drule_tac x="N'" in meta_spec)
wenzelm@36277
  1057
apply(drule_tac x="aa" in meta_spec)
wenzelm@36277
  1058
apply(drule_tac x="b" in meta_spec)
wenzelm@36277
  1059
apply(auto)[1]
wenzelm@36277
  1060
apply(rule_tac x="OrR1 <a>.M0 aa" in exI)
wenzelm@36277
  1061
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  1062
apply(auto)[1]
wenzelm@36277
  1063
(* OrR2 *)
wenzelm@36277
  1064
apply(drule sym)
wenzelm@36277
  1065
apply(frule crename_OrR2_aux)
wenzelm@36277
  1066
apply(erule disjE)
wenzelm@36277
  1067
apply(auto)[1]
wenzelm@36277
  1068
apply(drule crename_OrR2')
wenzelm@36277
  1069
apply(simp)
wenzelm@36277
  1070
apply(simp add: fresh_atm)
wenzelm@36277
  1071
apply(erule disjE)
wenzelm@36277
  1072
apply(auto)[1]
wenzelm@36277
  1073
apply(drule_tac x="N'" in meta_spec)
wenzelm@36277
  1074
apply(drule_tac x="aa" in meta_spec)
wenzelm@36277
  1075
apply(drule_tac x="ba" in meta_spec)
wenzelm@36277
  1076
apply(auto)[1]
wenzelm@36277
  1077
apply(rule_tac x="OrR2 <a>.M0 b" in exI)
wenzelm@36277
  1078
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  1079
apply(auto)[1]
wenzelm@36277
  1080
apply(auto)[1]
wenzelm@36277
  1081
apply(drule_tac x="N'" in meta_spec)
wenzelm@36277
  1082
apply(drule_tac x="aa" in meta_spec)
wenzelm@36277
  1083
apply(drule_tac x="b" in meta_spec)
wenzelm@36277
  1084
apply(auto)[1]
wenzelm@36277
  1085
apply(rule_tac x="OrR2 <a>.M0 aa" in exI)
wenzelm@36277
  1086
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  1087
apply(auto)[1]
wenzelm@36277
  1088
(* ImpL *)
wenzelm@36277
  1089
apply(drule sym)
wenzelm@36277
  1090
apply(drule crename_ImpL)
wenzelm@36277
  1091
apply(simp)
wenzelm@36277
  1092
apply(simp)
wenzelm@36277
  1093
apply(auto)[1]
wenzelm@36277
  1094
apply(drule_tac x="M'a" in meta_spec)
wenzelm@36277
  1095
apply(drule_tac x="aa" in meta_spec)
wenzelm@36277
  1096
apply(drule_tac x="b" in meta_spec)
wenzelm@36277
  1097
apply(auto)[1]
wenzelm@36277
  1098
apply(rule_tac x="ImpL <a>.M0 (x).N' y" in exI)
wenzelm@36277
  1099
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  1100
apply(auto)[1]
wenzelm@36277
  1101
apply(rule trans)
wenzelm@36277
  1102
apply(rule crename.simps)
wenzelm@36277
  1103
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
wenzelm@36277
  1104
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  1105
apply(auto intro: fresh_a_redu)[1]
wenzelm@36277
  1106
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  1107
apply(drule sym)
wenzelm@36277
  1108
apply(drule crename_ImpL)
wenzelm@36277
  1109
apply(simp)
wenzelm@36277
  1110
apply(simp)
wenzelm@36277
  1111
apply(auto)[1]
wenzelm@36277
  1112
apply(drule_tac x="N'a" in meta_spec)
wenzelm@36277
  1113
apply(drule_tac x="aa" in meta_spec)
wenzelm@36277
  1114
apply(drule_tac x="b" in meta_spec)
wenzelm@36277
  1115
apply(auto)[1]
wenzelm@36277
  1116
apply(rule_tac x="ImpL <a>.M' (x).M0 y" in exI)
wenzelm@36277
  1117
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  1118
apply(auto)[1]
wenzelm@36277
  1119
apply(rule trans)
wenzelm@36277
  1120
apply(rule crename.simps)
wenzelm@36277
  1121
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
wenzelm@36277
  1122
apply(auto intro: fresh_a_redu)[1]
wenzelm@36277
  1123
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  1124
apply(simp)
wenzelm@36277
  1125
(* ImpR *)
wenzelm@36277
  1126
apply(drule sym)
wenzelm@36277
  1127
apply(frule crename_ImpR_aux)
wenzelm@36277
  1128
apply(erule disjE)
wenzelm@36277
  1129
apply(auto)[1]
wenzelm@36277
  1130
apply(drule crename_ImpR')
wenzelm@36277
  1131
apply(simp)
wenzelm@36277
  1132
apply(simp add: fresh_atm)
wenzelm@36277
  1133
apply(simp add: fresh_atm)
wenzelm@36277
  1134
apply(erule disjE)
wenzelm@36277
  1135
apply(auto)[1]
wenzelm@36277
  1136
apply(drule_tac x="N'" in meta_spec)
wenzelm@36277
  1137
apply(drule_tac x="aa" in meta_spec)
wenzelm@36277
  1138
apply(drule_tac x="ba" in meta_spec)
wenzelm@36277
  1139
apply(auto)[1]
wenzelm@36277
  1140
apply(rule_tac x="ImpR (x).<a>.M0 b" in exI)
wenzelm@36277
  1141
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  1142
apply(auto)[1]
wenzelm@36277
  1143
apply(auto)[1]
wenzelm@36277
  1144
apply(drule_tac x="N'" in meta_spec)
wenzelm@36277
  1145
apply(drule_tac x="aa" in meta_spec)
wenzelm@36277
  1146
apply(drule_tac x="b" in meta_spec)
wenzelm@36277
  1147
apply(auto)[1]
wenzelm@36277
  1148
apply(rule_tac x="ImpR (x).<a>.M0 aa" in exI)
wenzelm@36277
  1149
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  1150
apply(auto)[1]
wenzelm@36277
  1151
done
wenzelm@36277
  1152
wenzelm@36277
  1153
lemma SNa_preserved_renaming1:
wenzelm@36277
  1154
  assumes a: "SNa M"
wenzelm@36277
  1155
  shows "SNa (M[a\<turnstile>c>b])"
wenzelm@36277
  1156
using a
wenzelm@36277
  1157
apply(induct rule: SNa_induct)
wenzelm@36277
  1158
apply(case_tac "a=b")
wenzelm@36277
  1159
apply(simp add: crename_id)
wenzelm@36277
  1160
apply(rule SNaI)
wenzelm@36277
  1161
apply(drule crename_aredu)
wenzelm@36277
  1162
apply(blast)+
wenzelm@36277
  1163
done
wenzelm@36277
  1164
wenzelm@36277
  1165
lemma nrename_interesting1:
wenzelm@36277
  1166
  assumes a: "distinct [x,y,z]"
wenzelm@36277
  1167
  shows "M[x\<turnstile>n>z][z\<turnstile>n>y] = M[z\<turnstile>n>y][x\<turnstile>n>y]"
wenzelm@36277
  1168
using a
wenzelm@36277
  1169
apply(nominal_induct M avoiding: x y z rule: trm.strong_induct)
wenzelm@36277
  1170
apply(auto simp add: rename_fresh simp add: trm.inject alpha)
wenzelm@36277
  1171
apply(blast)
wenzelm@36277
  1172
apply(blast)
wenzelm@36277
  1173
apply(rotate_tac 12)
wenzelm@36277
  1174
apply(drule_tac x="x" in meta_spec)
wenzelm@36277
  1175
apply(rotate_tac 15)
wenzelm@36277
  1176
apply(drule_tac x="y" in meta_spec)
wenzelm@36277
  1177
apply(rotate_tac 15)
wenzelm@36277
  1178
apply(drule_tac x="z" in meta_spec)
wenzelm@36277
  1179
apply(blast)
wenzelm@36277
  1180
apply(rotate_tac 11)
wenzelm@36277
  1181
apply(drule_tac x="x" in meta_spec)
wenzelm@36277
  1182
apply(rotate_tac 14)
wenzelm@36277
  1183
apply(drule_tac x="y" in meta_spec)
wenzelm@36277
  1184
apply(rotate_tac 14)
wenzelm@36277
  1185
apply(drule_tac x="z" in meta_spec)
wenzelm@36277
  1186
apply(blast)
wenzelm@36277
  1187
done
wenzelm@36277
  1188
wenzelm@36277
  1189
lemma nrename_interesting2:
wenzelm@36277
  1190
  assumes a: "x\<noteq>z" "x\<noteq>u" "x\<noteq>y" "z\<noteq>u" "y\<noteq>z"
wenzelm@36277
  1191
  shows "M[x\<turnstile>n>y][z\<turnstile>n>u] = M[z\<turnstile>n>u][x\<turnstile>n>y]"
wenzelm@36277
  1192
using a
wenzelm@36277
  1193
apply(nominal_induct M avoiding: x y z u rule: trm.strong_induct)
wenzelm@36277
  1194
apply(auto simp add: rename_fresh simp add: trm.inject alpha)
wenzelm@36277
  1195
done
wenzelm@36277
  1196
wenzelm@36277
  1197
lemma not_fic_nrename_aux:
wenzelm@36277
  1198
  assumes a: "fic M c" 
wenzelm@36277
  1199
  shows "fic (M[x\<turnstile>n>y]) c" 
wenzelm@36277
  1200
using a
wenzelm@36277
  1201
apply(nominal_induct M avoiding: c x y rule: trm.strong_induct)
wenzelm@36277
  1202
apply(auto dest!: fic_elims intro!: fic.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh)
wenzelm@36277
  1203
done
wenzelm@36277
  1204
wenzelm@36277
  1205
lemma not_fic_nrename:
wenzelm@36277
  1206
  assumes a: "\<not>(fic (M[x\<turnstile>n>y]) c)" 
wenzelm@36277
  1207
  shows "\<not>(fic M c)" 
wenzelm@36277
  1208
using a
wenzelm@36277
  1209
apply(auto dest:  not_fic_nrename_aux)
wenzelm@36277
  1210
done
wenzelm@36277
  1211
wenzelm@36277
  1212
lemma fin_nrename:
wenzelm@36277
  1213
  assumes a: "fin M z" "z\<sharp>(x,y)"
wenzelm@36277
  1214
  shows "fin (M[x\<turnstile>n>y]) z" 
wenzelm@36277
  1215
using a
wenzelm@36277
  1216
apply(nominal_induct M avoiding: x y z rule: trm.strong_induct)
wenzelm@36277
  1217
apply(auto dest!: fin_elims intro!: fin.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh
wenzelm@36277
  1218
           split: if_splits)
wenzelm@36277
  1219
done
wenzelm@36277
  1220
wenzelm@36277
  1221
lemma nrename_fresh_interesting1:
wenzelm@36277
  1222
  fixes z::"name"
wenzelm@36277
  1223
  assumes a: "z\<sharp>(M[x\<turnstile>n>y])" "z\<sharp>(x,y)"
wenzelm@36277
  1224
  shows "z\<sharp>M"
wenzelm@36277
  1225
using a
wenzelm@36277
  1226
apply(nominal_induct M avoiding: x y z rule: trm.strong_induct)
wenzelm@36277
  1227
apply(auto split: if_splits simp add: abs_fresh abs_supp fin_supp)
wenzelm@36277
  1228
done
wenzelm@36277
  1229
wenzelm@36277
  1230
lemma nrename_fresh_interesting2:
wenzelm@36277
  1231
  fixes c::"coname"
wenzelm@36277
  1232
  assumes a: "c\<sharp>(M[x\<turnstile>n>y])" 
wenzelm@36277
  1233
  shows "c\<sharp>M"
wenzelm@36277
  1234
using a
wenzelm@36277
  1235
apply(nominal_induct M avoiding: x y c rule: trm.strong_induct)
wenzelm@36277
  1236
apply(auto split: if_splits simp add: abs_fresh abs_supp fin_supp fresh_atm)
wenzelm@36277
  1237
done
wenzelm@36277
  1238
wenzelm@36277
  1239
lemma fin_nrename2:
wenzelm@36277
  1240
  assumes a: "fin (M[x\<turnstile>n>y]) z" "z\<sharp>(x,y)"
wenzelm@36277
  1241
  shows "fin M z" 
wenzelm@36277
  1242
using a
wenzelm@36277
  1243
apply(nominal_induct M avoiding: x y z rule: trm.strong_induct)
wenzelm@36277
  1244
apply(auto dest!: fin_elims intro!: fin.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh
wenzelm@36277
  1245
           split: if_splits)
wenzelm@36277
  1246
apply(auto dest: nrename_fresh_interesting1 simp add: fresh_atm fresh_prod)
wenzelm@36277
  1247
done
wenzelm@36277
  1248
wenzelm@36277
  1249
lemma nrename_Cut:
wenzelm@36277
  1250
  assumes a: "R[x\<turnstile>n>y] = Cut <c>.M (z).N" "c\<sharp>(N,R)" "z\<sharp>(x,y,M,R)"
wenzelm@36277
  1251
  shows "\<exists>M' N'. R = Cut <c>.M' (z).N' \<and> M'[x\<turnstile>n>y] = M \<and> N'[x\<turnstile>n>y] = N \<and> c\<sharp>N' \<and> z\<sharp>M'"
wenzelm@36277
  1252
using a
wenzelm@36277
  1253
apply(nominal_induct R avoiding: c y x z M N rule: trm.strong_induct)
wenzelm@36277
  1254
apply(auto split: if_splits)
wenzelm@36277
  1255
apply(simp add: trm.inject)
wenzelm@36277
  1256
apply(auto simp add: alpha fresh_atm)
wenzelm@36277
  1257
apply(rule_tac x="[(coname,c)]\<bullet>trm1" in exI)
wenzelm@36277
  1258
apply(perm_simp)
wenzelm@36277
  1259
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
  1260
apply(rule_tac x="[(name,z)]\<bullet>trm2" in exI)
wenzelm@36277
  1261
apply(perm_simp)
wenzelm@36277
  1262
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
  1263
apply(rule conjI)
wenzelm@36277
  1264
apply(drule sym)
wenzelm@36277
  1265
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
wenzelm@36277
  1266
apply(simp add: eqvts calc_atm)
wenzelm@36277
  1267
apply(auto simp add: fresh_atm)[1]
wenzelm@36277
  1268
apply(drule sym)
wenzelm@36277
  1269
apply(drule sym)
wenzelm@36277
  1270
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
  1271
apply(simp add: eqvts calc_atm)
wenzelm@36277
  1272
done
wenzelm@36277
  1273
wenzelm@36277
  1274
lemma nrename_NotR:
wenzelm@36277
  1275
  assumes a: "R[x\<turnstile>n>y] = NotR (z).N c" "z\<sharp>(R,x,y)" 
wenzelm@36277
  1276
  shows "\<exists>N'. (R = NotR (z).N' c) \<and> N'[x\<turnstile>n>y] = N" 
wenzelm@36277
  1277
using a
wenzelm@36277
  1278
apply(nominal_induct R avoiding: x y c z N rule: trm.strong_induct)
wenzelm@36277
  1279
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
wenzelm@36277
  1280
apply(rule_tac x="[(name,z)]\<bullet>trm" in exI)
wenzelm@36277
  1281
apply(perm_simp)
wenzelm@36277
  1282
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
  1283
apply(drule sym)
wenzelm@36277
  1284
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
  1285
apply(simp add: eqvts calc_atm)
wenzelm@36277
  1286
done
wenzelm@36277
  1287
wenzelm@36277
  1288
lemma nrename_NotL:
wenzelm@36277
  1289
  assumes a: "R[x\<turnstile>n>y] = NotL <c>.N z" "c\<sharp>R" "z\<sharp>(x,y)"
wenzelm@36277
  1290
  shows "\<exists>N'. (R = NotL <c>.N' z) \<and> N'[x\<turnstile>n>y] = N" 
wenzelm@36277
  1291
using a
wenzelm@36277
  1292
apply(nominal_induct R avoiding: x y c z N rule: trm.strong_induct)
wenzelm@36277
  1293
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
wenzelm@36277
  1294
apply(rule_tac x="[(coname,c)]\<bullet>trm" in exI)
wenzelm@36277
  1295
apply(perm_simp)
wenzelm@36277
  1296
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
  1297
apply(drule sym)
wenzelm@36277
  1298
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
wenzelm@36277
  1299
apply(simp add: eqvts calc_atm)
wenzelm@36277
  1300
done
wenzelm@36277
  1301
wenzelm@36277
  1302
lemma nrename_NotL':
wenzelm@36277
  1303
  assumes a: "R[x\<turnstile>n>y] = NotL <c>.N u" "c\<sharp>R" "x\<noteq>y" 
wenzelm@36277
  1304
  shows "(\<exists>N'. (R = NotL <c>.N' u) \<and> N'[x\<turnstile>n>y] = N) \<or> (\<exists>N'. (R = NotL <c>.N' x) \<and> y=u \<and> N'[x\<turnstile>n>y] = N)"
wenzelm@36277
  1305
using a
wenzelm@36277
  1306
apply(nominal_induct R avoiding: y u c x N rule: trm.strong_induct)
wenzelm@36277
  1307
apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject)
wenzelm@36277
  1308
apply(rule_tac x="[(coname,c)]\<bullet>trm" in exI)
wenzelm@36277
  1309
apply(perm_simp)
wenzelm@36277
  1310
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
  1311
apply(drule sym)
wenzelm@36277
  1312
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
wenzelm@36277
  1313
apply(simp add: eqvts calc_atm)
wenzelm@36277
  1314
apply(rule_tac x="[(coname,c)]\<bullet>trm" in exI)
wenzelm@36277
  1315
apply(perm_simp)
wenzelm@36277
  1316
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
  1317
apply(drule sym)
wenzelm@36277
  1318
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
wenzelm@36277
  1319
apply(simp add: eqvts calc_atm)
wenzelm@36277
  1320
done
wenzelm@36277
  1321
wenzelm@36277
  1322
lemma nrename_NotL_aux:
wenzelm@36277
  1323
  assumes a: "R[x\<turnstile>n>y] = NotL <c>.N u" 
wenzelm@36277
  1324
  shows "(x=u \<and> x=y) \<or> (x\<noteq>u)" 
wenzelm@36277
  1325
using a
wenzelm@36277
  1326
apply(nominal_induct R avoiding: y u c x N rule: trm.strong_induct)
wenzelm@36277
  1327
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
wenzelm@36277
  1328
done
wenzelm@36277
  1329
wenzelm@36277
  1330
lemma nrename_AndL1:
wenzelm@36277
  1331
  assumes a: "R[x\<turnstile>n>y] = AndL1 (z).N u" "z\<sharp>(R,x,y)" "u\<sharp>(x,y)"
wenzelm@36277
  1332
  shows "\<exists>N'. (R = AndL1 (z).N' u) \<and> N'[x\<turnstile>n>y] = N" 
wenzelm@36277
  1333
using a
wenzelm@36277
  1334
apply(nominal_induct R avoiding: z u x y N rule: trm.strong_induct)
wenzelm@36277
  1335
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
wenzelm@36277
  1336
apply(rule_tac x="[(name1,z)]\<bullet>trm" in exI)
wenzelm@36277
  1337
apply(perm_simp)
wenzelm@36277
  1338
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
  1339
apply(drule sym)
wenzelm@36277
  1340
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
  1341
apply(simp add: eqvts calc_atm)
wenzelm@36277
  1342
done
wenzelm@36277
  1343
wenzelm@36277
  1344
lemma nrename_AndL1':
wenzelm@36277
  1345
  assumes a: "R[x\<turnstile>n>y] = AndL1 (v).N u" "v\<sharp>(R,u,x,y)" "x\<noteq>y" 
wenzelm@36277
  1346
  shows "(\<exists>N'. (R = AndL1 (v).N' u) \<and> N'[x\<turnstile>n>y] = N) \<or> (\<exists>N'. (R = AndL1 (v).N' x) \<and> y=u \<and> N'[x\<turnstile>n>y] = N)"
wenzelm@36277
  1347
using a
wenzelm@36277
  1348
apply(nominal_induct R avoiding: y u v x N rule: trm.strong_induct)
wenzelm@36277
  1349
apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject)
wenzelm@36277
  1350
apply(rule_tac x="[(name1,v)]\<bullet>trm" in exI)
wenzelm@36277
  1351
apply(perm_simp)
wenzelm@36277
  1352
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
  1353
apply(drule sym)
wenzelm@36277
  1354
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
  1355
apply(simp add: eqvts calc_atm)
wenzelm@36277
  1356
apply(rule_tac x="[(name1,v)]\<bullet>trm" in exI)
wenzelm@36277
  1357
apply(perm_simp)
wenzelm@36277
  1358
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
  1359
apply(drule sym)
wenzelm@36277
  1360
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
  1361
apply(simp add: eqvts calc_atm)
wenzelm@36277
  1362
done
wenzelm@36277
  1363
wenzelm@36277
  1364
lemma nrename_AndL1_aux:
wenzelm@36277
  1365
  assumes a: "R[x\<turnstile>n>y] = AndL1 (v).N u" 
wenzelm@36277
  1366
  shows "(x=u \<and> x=y) \<or> (x\<noteq>u)" 
wenzelm@36277
  1367
using a
wenzelm@36277
  1368
apply(nominal_induct R avoiding: y u v x N rule: trm.strong_induct)
wenzelm@36277
  1369
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
wenzelm@36277
  1370
done
wenzelm@36277
  1371
wenzelm@36277
  1372
lemma nrename_AndL2:
wenzelm@36277
  1373
  assumes a: "R[x\<turnstile>n>y] = AndL2 (z).N u" "z\<sharp>(R,x,y)" "u\<sharp>(x,y)"
wenzelm@36277
  1374
  shows "\<exists>N'. (R = AndL2 (z).N' u) \<and> N'[x\<turnstile>n>y] = N" 
wenzelm@36277
  1375
using a
wenzelm@36277
  1376
apply(nominal_induct R avoiding: z u x y N rule: trm.strong_induct)
wenzelm@36277
  1377
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
wenzelm@36277
  1378
apply(rule_tac x="[(name1,z)]\<bullet>trm" in exI)
wenzelm@36277
  1379
apply(perm_simp)
wenzelm@36277
  1380
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
  1381
apply(drule sym)
wenzelm@36277
  1382
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
  1383
apply(simp add: eqvts calc_atm)
wenzelm@36277
  1384
done
wenzelm@36277
  1385
wenzelm@36277
  1386
lemma nrename_AndL2':
wenzelm@36277
  1387
  assumes a: "R[x\<turnstile>n>y] = AndL2 (v).N u" "v\<sharp>(R,u,x,y)" "x\<noteq>y" 
wenzelm@36277
  1388
  shows "(\<exists>N'. (R = AndL2 (v).N' u) \<and> N'[x\<turnstile>n>y] = N) \<or> (\<exists>N'. (R = AndL2 (v).N' x) \<and> y=u \<and> N'[x\<turnstile>n>y] = N)"
wenzelm@36277
  1389
using a
wenzelm@36277
  1390
apply(nominal_induct R avoiding: y u v x N rule: trm.strong_induct)
wenzelm@36277
  1391
apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject)
wenzelm@36277
  1392
apply(rule_tac x="[(name1,v)]\<bullet>trm" in exI)
wenzelm@36277
  1393
apply(perm_simp)
wenzelm@36277
  1394
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
  1395
apply(drule sym)
wenzelm@36277
  1396
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
  1397
apply(simp add: eqvts calc_atm)
wenzelm@36277
  1398
apply(rule_tac x="[(name1,v)]\<bullet>trm" in exI)
wenzelm@36277
  1399
apply(perm_simp)
wenzelm@36277
  1400
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
  1401
apply(drule sym)
wenzelm@36277
  1402
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
  1403
apply(simp add: eqvts calc_atm)
wenzelm@36277
  1404
done
wenzelm@36277
  1405
wenzelm@36277
  1406
lemma nrename_AndL2_aux:
wenzelm@36277
  1407
  assumes a: "R[x\<turnstile>n>y] = AndL2 (v).N u" 
wenzelm@36277
  1408
  shows "(x=u \<and> x=y) \<or> (x\<noteq>u)" 
wenzelm@36277
  1409
using a
wenzelm@36277
  1410
apply(nominal_induct R avoiding: y u v x N rule: trm.strong_induct)
wenzelm@36277
  1411
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
wenzelm@36277
  1412
done
wenzelm@36277
  1413
wenzelm@36277
  1414
lemma nrename_AndR:
wenzelm@36277
  1415
  assumes a: "R[x\<turnstile>n>y] = AndR <c>.M <d>.N e" "c\<sharp>(d,e,N,R)" "d\<sharp>(c,e,M,R)" 
wenzelm@36277
  1416
  shows "\<exists>M' N'. R = AndR <c>.M' <d>.N' e \<and> M'[x\<turnstile>n>y] = M \<and> N'[x\<turnstile>n>y] = N \<and> c\<sharp>N' \<and> d\<sharp>M'"
wenzelm@36277
  1417
using a
wenzelm@36277
  1418
apply(nominal_induct R avoiding: x y c d e M N rule: trm.strong_induct)
wenzelm@36277
  1419
apply(auto split: if_splits simp add: trm.inject alpha)
wenzelm@36277
  1420
apply(simp add: fresh_atm fresh_prod)
wenzelm@36277
  1421
apply(rule_tac x="[(coname1,c)]\<bullet>trm1" in exI)
wenzelm@36277
  1422
apply(perm_simp)
wenzelm@36277
  1423
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
wenzelm@36277
  1424
apply(rule_tac x="[(coname1,c)]\<bullet>trm1" in exI)
wenzelm@36277
  1425
apply(perm_simp)
wenzelm@36277
  1426
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
wenzelm@36277
  1427
apply(rule_tac x="[(coname2,d)]\<bullet>trm2" in exI)
wenzelm@36277
  1428
apply(perm_simp)
wenzelm@36277
  1429
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
wenzelm@36277
  1430
apply(drule sym)
wenzelm@36277
  1431
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
wenzelm@36277
  1432
apply(simp add: eqvts calc_atm)
wenzelm@36277
  1433
apply(drule_tac s="trm2[x\<turnstile>n>y]" in  sym)
wenzelm@36277
  1434
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
wenzelm@36277
  1435
apply(simp add: eqvts calc_atm)
wenzelm@36277
  1436
done
wenzelm@36277
  1437
wenzelm@36277
  1438
lemma nrename_OrR1:
wenzelm@36277
  1439
  assumes a: "R[x\<turnstile>n>y] = OrR1 <c>.N d" "c\<sharp>(R,d)" 
wenzelm@36277
  1440
  shows "\<exists>N'. (R = OrR1 <c>.N' d) \<and> N'[x\<turnstile>n>y] = N" 
wenzelm@36277
  1441
using a
wenzelm@36277
  1442
apply(nominal_induct R avoiding: x y c d N rule: trm.strong_induct)
wenzelm@36277
  1443
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
wenzelm@36277
  1444
apply(rule_tac x="[(coname1,c)]\<bullet>trm" in exI)
wenzelm@36277
  1445
apply(perm_simp)
wenzelm@36277
  1446
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
  1447
apply(drule sym)
wenzelm@36277
  1448
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
wenzelm@36277
  1449
apply(simp add: eqvts calc_atm)
wenzelm@36277
  1450
done
wenzelm@36277
  1451
wenzelm@36277
  1452
lemma nrename_OrR2:
wenzelm@36277
  1453
  assumes a: "R[x\<turnstile>n>y] = OrR2 <c>.N d" "c\<sharp>(R,d)" 
wenzelm@36277
  1454
  shows "\<exists>N'. (R = OrR2 <c>.N' d) \<and> N'[x\<turnstile>n>y] = N" 
wenzelm@36277
  1455
using a
wenzelm@36277
  1456
apply(nominal_induct R avoiding: x y c d N rule: trm.strong_induct)
wenzelm@36277
  1457
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
wenzelm@36277
  1458
apply(rule_tac x="[(coname1,c)]\<bullet>trm" in exI)
wenzelm@36277
  1459
apply(perm_simp)
wenzelm@36277
  1460
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
  1461
apply(drule sym)
wenzelm@36277
  1462
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
wenzelm@36277
  1463
apply(simp add: eqvts calc_atm)
wenzelm@36277
  1464
done
wenzelm@36277
  1465
wenzelm@36277
  1466
lemma nrename_OrL:
wenzelm@36277
  1467
  assumes a: "R[u\<turnstile>n>v] = OrL (x).M (y).N z" "x\<sharp>(y,z,u,v,N,R)" "y\<sharp>(x,z,u,v,M,R)" "z\<sharp>(u,v)"
wenzelm@36277
  1468
  shows "\<exists>M' N'. R = OrL (x).M' (y).N' z \<and> M'[u\<turnstile>n>v] = M \<and> N'[u\<turnstile>n>v] = N \<and> x\<sharp>N' \<and> y\<sharp>M'"
wenzelm@36277
  1469
using a
wenzelm@36277
  1470
apply(nominal_induct R avoiding: u v x y z M N rule: trm.strong_induct)
wenzelm@36277
  1471
apply(auto split: if_splits simp add: trm.inject alpha fresh_prod fresh_atm)
wenzelm@36277
  1472
apply(rule_tac x="[(name1,x)]\<bullet>trm1" in exI)
wenzelm@36277
  1473
apply(perm_simp)
wenzelm@36277
  1474
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
wenzelm@36277
  1475
apply(rule_tac x="[(name2,y)]\<bullet>trm2" in exI)
wenzelm@36277
  1476
apply(perm_simp)
wenzelm@36277
  1477
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
wenzelm@36277
  1478
apply(drule sym)
wenzelm@36277
  1479
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
  1480
apply(simp add: eqvts calc_atm)
wenzelm@36277
  1481
apply(drule_tac s="trm2[u\<turnstile>n>v]" in  sym)
wenzelm@36277
  1482
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
  1483
apply(simp add: eqvts calc_atm)
wenzelm@36277
  1484
done
wenzelm@36277
  1485
wenzelm@36277
  1486
lemma nrename_OrL':
wenzelm@36277
  1487
  assumes a: "R[x\<turnstile>n>y] = OrL (v).M (w).N u" "v\<sharp>(R,N,u,x,y)" "w\<sharp>(R,M,u,x,y)" "x\<noteq>y" 
wenzelm@36277
  1488
  shows "(\<exists>M' N'. (R = OrL (v).M' (w).N' u) \<and> M'[x\<turnstile>n>y] = M \<and> N'[x\<turnstile>n>y] = N) \<or> 
wenzelm@36277
  1489
         (\<exists>M' N'. (R = OrL (v).M' (w).N' x) \<and> y=u \<and> M'[x\<turnstile>n>y] = M \<and> N'[x\<turnstile>n>y] = N)"
wenzelm@36277
  1490
using a
wenzelm@36277
  1491
apply(nominal_induct R avoiding: y x u v w M N rule: trm.strong_induct)
wenzelm@36277
  1492
apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject)
wenzelm@36277
  1493
apply(rule_tac x="[(name1,v)]\<bullet>trm1" in exI)
wenzelm@36277
  1494
apply(perm_simp)
wenzelm@36277
  1495
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
  1496
apply(rule_tac x="[(name2,w)]\<bullet>trm2" in exI)
wenzelm@36277
  1497
apply(perm_simp)
wenzelm@36277
  1498
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
  1499
apply(rule conjI)
wenzelm@36277
  1500
apply(drule sym)
wenzelm@36277
  1501
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
  1502
apply(simp add: eqvts calc_atm)
wenzelm@36277
  1503
apply(drule_tac s="trm2[x\<turnstile>n>u]" in sym)
wenzelm@36277
  1504
apply(drule_tac pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
  1505
apply(simp add: eqvts calc_atm)
wenzelm@36277
  1506
apply(rule_tac x="[(name1,v)]\<bullet>trm1" in exI)
wenzelm@36277
  1507
apply(perm_simp)
wenzelm@36277
  1508
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
  1509
apply(rule_tac x="[(name2,w)]\<bullet>trm2" in exI)
wenzelm@36277
  1510
apply(perm_simp)
wenzelm@36277
  1511
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
  1512
apply(rule conjI)
wenzelm@36277
  1513
apply(drule sym)
wenzelm@36277
  1514
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
  1515
apply(simp add: eqvts calc_atm)
wenzelm@36277
  1516
apply(drule_tac s="trm2[x\<turnstile>n>y]" in sym)
wenzelm@36277
  1517
apply(drule_tac pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
  1518
apply(simp add: eqvts calc_atm)
wenzelm@36277
  1519
done
wenzelm@36277
  1520
wenzelm@36277
  1521
lemma nrename_OrL_aux:
wenzelm@36277
  1522
  assumes a: "R[x\<turnstile>n>y] = OrL (v).M (w).N u" 
wenzelm@36277
  1523
  shows "(x=u \<and> x=y) \<or> (x\<noteq>u)" 
wenzelm@36277
  1524
using a
wenzelm@36277
  1525
apply(nominal_induct R avoiding: y x w u v M N rule: trm.strong_induct)
wenzelm@36277
  1526
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
wenzelm@36277
  1527
done
wenzelm@36277
  1528
wenzelm@36277
  1529
lemma nrename_ImpL:
wenzelm@36277
  1530
  assumes a: "R[x\<turnstile>n>y] = ImpL <c>.M (u).N z" "c\<sharp>(N,R)" "u\<sharp>(y,x,z,M,R)" "z\<sharp>(x,y)"
wenzelm@36277
  1531
  shows "\<exists>M' N'. R = ImpL <c>.M' (u).N' z \<and> M'[x\<turnstile>n>y] = M \<and> N'[x\<turnstile>n>y] = N \<and> c\<sharp>N' \<and> u\<sharp>M'"
wenzelm@36277
  1532
using a
wenzelm@36277
  1533
apply(nominal_induct R avoiding: u x c y z M N rule: trm.strong_induct)
wenzelm@36277
  1534
apply(auto split: if_splits simp add: trm.inject alpha fresh_prod fresh_atm)
wenzelm@36277
  1535
apply(rule_tac x="[(coname,c)]\<bullet>trm1" in exI)
wenzelm@36277
  1536
apply(perm_simp)
wenzelm@36277
  1537
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
wenzelm@36277
  1538
apply(rule_tac x="[(name1,u)]\<bullet>trm2" in exI)
wenzelm@36277
  1539
apply(perm_simp)
wenzelm@36277
  1540
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
wenzelm@36277
  1541
apply(drule sym)
wenzelm@36277
  1542
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
wenzelm@36277
  1543
apply(simp add: eqvts calc_atm)
wenzelm@36277
  1544
apply(drule_tac s="trm2[x\<turnstile>n>y]" in  sym)
wenzelm@36277
  1545
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
  1546
apply(simp add: eqvts calc_atm fresh_prod fresh_atm)
wenzelm@36277
  1547
done
wenzelm@36277
  1548
wenzelm@36277
  1549
lemma nrename_ImpL':
wenzelm@36277
  1550
  assumes a: "R[x\<turnstile>n>y] = ImpL <c>.M (w).N u" "c\<sharp>(R,N)" "w\<sharp>(R,M,u,x,y)" "x\<noteq>y" 
wenzelm@36277
  1551
  shows "(\<exists>M' N'. (R = ImpL <c>.M' (w).N' u) \<and> M'[x\<turnstile>n>y] = M \<and> N'[x\<turnstile>n>y] = N) \<or> 
wenzelm@36277
  1552
         (\<exists>M' N'. (R = ImpL <c>.M' (w).N' x) \<and> y=u \<and> M'[x\<turnstile>n>y] = M \<and> N'[x\<turnstile>n>y] = N)"
wenzelm@36277
  1553
using a
wenzelm@36277
  1554
apply(nominal_induct R avoiding: y x u c w M N rule: trm.strong_induct)
wenzelm@36277
  1555
apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject)
wenzelm@36277
  1556
apply(rule_tac x="[(coname,c)]\<bullet>trm1" in exI)
wenzelm@36277
  1557
apply(perm_simp)
wenzelm@36277
  1558
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
  1559
apply(rule_tac x="[(name1,w)]\<bullet>trm2" in exI)
wenzelm@36277
  1560
apply(perm_simp)
wenzelm@36277
  1561
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
  1562
apply(rule conjI)
wenzelm@36277
  1563
apply(drule sym)
wenzelm@36277
  1564
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
wenzelm@36277
  1565
apply(simp add: eqvts calc_atm)
wenzelm@36277
  1566
apply(drule_tac s="trm2[x\<turnstile>n>u]" in sym)
wenzelm@36277
  1567
apply(drule_tac pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
  1568
apply(simp add: eqvts calc_atm)
wenzelm@36277
  1569
apply(rule_tac x="[(coname,c)]\<bullet>trm1" in exI)
wenzelm@36277
  1570
apply(perm_simp)
wenzelm@36277
  1571
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
  1572
apply(rule_tac x="[(name1,w)]\<bullet>trm2" in exI)
wenzelm@36277
  1573
apply(perm_simp)
wenzelm@36277
  1574
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
  1575
apply(rule conjI)
wenzelm@36277
  1576
apply(drule sym)
wenzelm@36277
  1577
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
wenzelm@36277
  1578
apply(simp add: eqvts calc_atm)
wenzelm@36277
  1579
apply(drule_tac s="trm2[x\<turnstile>n>y]" in sym)
wenzelm@36277
  1580
apply(drule_tac pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
  1581
apply(simp add: eqvts calc_atm)
wenzelm@36277
  1582
done
wenzelm@36277
  1583
wenzelm@36277
  1584
lemma nrename_ImpL_aux:
wenzelm@36277
  1585
  assumes a: "R[x\<turnstile>n>y] = ImpL <c>.M (w).N u" 
wenzelm@36277
  1586
  shows "(x=u \<and> x=y) \<or> (x\<noteq>u)" 
wenzelm@36277
  1587
using a
wenzelm@36277
  1588
apply(nominal_induct R avoiding: y x w u c M N rule: trm.strong_induct)
wenzelm@36277
  1589
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
wenzelm@36277
  1590
done
wenzelm@36277
  1591
wenzelm@36277
  1592
lemma nrename_ImpR:
wenzelm@36277
  1593
  assumes a: "R[u\<turnstile>n>v] = ImpR (x).<c>.N d" "c\<sharp>(R,d)" "x\<sharp>(R,u,v)" 
wenzelm@36277
  1594
  shows "\<exists>N'. (R = ImpR (x).<c>.N' d) \<and> N'[u\<turnstile>n>v] = N" 
wenzelm@36277
  1595
using a
wenzelm@36277
  1596
apply(nominal_induct R avoiding: u v x c d N rule: trm.strong_induct)
wenzelm@36277
  1597
apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_perm alpha abs_fresh trm.inject)
wenzelm@36277
  1598
apply(rule_tac x="[(name,x)]\<bullet>trm" in exI)
wenzelm@36277
  1599
apply(perm_simp)
wenzelm@36277
  1600
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
  1601
apply(rule_tac x="[(name,x)]\<bullet>[(coname1, c)]\<bullet>trm" in exI)
wenzelm@36277
  1602
apply(perm_simp)
wenzelm@36277
  1603
apply(simp add: abs_supp fin_supp abs_fresh fresh_left calc_atm fresh_prod)
wenzelm@36277
  1604
apply(drule sym)
wenzelm@36277
  1605
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
wenzelm@36277
  1606
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
wenzelm@36277
  1607
apply(simp add: eqvts calc_atm)
wenzelm@36277
  1608
done
wenzelm@36277
  1609
wenzelm@36277
  1610
lemma nrename_credu:
wenzelm@53015
  1611
  assumes a: "(M[x\<turnstile>n>y]) \<longrightarrow>\<^sub>c M'"
wenzelm@53015
  1612
  shows "\<exists>M0. M0[x\<turnstile>n>y]=M' \<and> M \<longrightarrow>\<^sub>c M0"
wenzelm@36277
  1613
using a
wenzelm@36277
  1614
apply(nominal_induct M\<equiv>"M[x\<turnstile>n>y]" M' avoiding: M x y rule: c_redu.strong_induct)
wenzelm@36277
  1615
apply(drule sym)
wenzelm@36277
  1616
apply(drule nrename_Cut)
wenzelm@36277
  1617
apply(simp)
wenzelm@36277
  1618
apply(simp)
wenzelm@36277
  1619
apply(auto)
wenzelm@36277
  1620
apply(rule_tac x="M'{a:=(x).N'}" in exI)
wenzelm@36277
  1621
apply(rule conjI)
wenzelm@36277
  1622
apply(simp add: fresh_atm abs_fresh subst_comm fresh_prod)
wenzelm@36277
  1623
apply(rule c_redu.intros)
wenzelm@36277
  1624
apply(auto dest: not_fic_nrename)[1]
wenzelm@36277
  1625
apply(simp add: abs_fresh)
wenzelm@36277
  1626
apply(simp add: abs_fresh)
wenzelm@36277
  1627
apply(drule sym)
wenzelm@36277
  1628
apply(drule nrename_Cut)
wenzelm@36277
  1629
apply(simp)
wenzelm@36277
  1630
apply(simp)
wenzelm@36277
  1631
apply(auto)
wenzelm@36277
  1632
apply(rule_tac x="N'{x:=<a>.M'}" in exI)
wenzelm@36277
  1633
apply(rule conjI)
wenzelm@36277
  1634
apply(simp add: fresh_atm abs_fresh subst_comm fresh_prod)
wenzelm@36277
  1635
apply(rule c_redu.intros)
wenzelm@36277
  1636
apply(auto)
wenzelm@36277
  1637
apply(drule_tac x="xa" and y="y" in fin_nrename)
wenzelm@36277
  1638
apply(auto simp add: fresh_prod abs_fresh)
wenzelm@36277
  1639
done
wenzelm@36277
  1640
wenzelm@36277
  1641
lemma nrename_ax2:
wenzelm@36277
  1642
  assumes a: "N[x\<turnstile>n>y] = Ax z c"
wenzelm@36277
  1643
  shows "\<exists>z. N = Ax z c"
wenzelm@36277
  1644
using a
wenzelm@36277
  1645
apply(nominal_induct N avoiding: x y rule: trm.strong_induct)
wenzelm@36277
  1646
apply(auto split: if_splits)
wenzelm@36277
  1647
apply(simp add: trm.inject)
wenzelm@36277
  1648
done
wenzelm@36277
  1649
wenzelm@36277
  1650
lemma fic_nrename:
wenzelm@36277
  1651
  assumes a: "fic (M[x\<turnstile>n>y]) c" 
wenzelm@36277
  1652
  shows "fic M c" 
wenzelm@36277
  1653
using a
wenzelm@36277
  1654
apply(nominal_induct M avoiding: c x y rule: trm.strong_induct)
wenzelm@36277
  1655
apply(auto dest!: fic_elims intro!: fic.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh
wenzelm@36277
  1656
           split: if_splits)
wenzelm@36277
  1657
apply(auto dest: nrename_fresh_interesting2 simp add: fresh_prod fresh_atm)
wenzelm@36277
  1658
done
wenzelm@36277
  1659
wenzelm@36277
  1660
lemma nrename_lredu:
wenzelm@53015
  1661
  assumes a: "(M[x\<turnstile>n>y]) \<longrightarrow>\<^sub>l M'"
wenzelm@53015
  1662
  shows "\<exists>M0. M0[x\<turnstile>n>y]=M' \<and> M \<longrightarrow>\<^sub>l M0"
wenzelm@36277
  1663
using a
wenzelm@36277
  1664
apply(nominal_induct M\<equiv>"M[x\<turnstile>n>y]" M' avoiding: M x y rule: l_redu.strong_induct)
wenzelm@36277
  1665
apply(drule sym)
wenzelm@36277
  1666
apply(drule nrename_Cut)
wenzelm@36277
  1667
apply(simp add: fresh_prod fresh_atm)
wenzelm@36277
  1668
apply(simp)
wenzelm@36277
  1669
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
wenzelm@36277
  1670
apply(case_tac "xa=y")
wenzelm@36277
  1671
apply(simp add: nrename_id)
wenzelm@36277
  1672
apply(rule l_redu.intros)
wenzelm@36277
  1673
apply(simp)
wenzelm@36277
  1674
apply(simp add: fresh_atm)
wenzelm@36277
  1675
apply(assumption)
wenzelm@36277
  1676
apply(frule nrename_ax2)
wenzelm@36277
  1677
apply(auto)[1]
wenzelm@36277
  1678
apply(case_tac "z=xa")
wenzelm@36277
  1679
apply(simp add: trm.inject)
wenzelm@36277
  1680
apply(simp)
wenzelm@36277
  1681
apply(rule_tac x="M'[a\<turnstile>c>b]" in exI)
wenzelm@36277
  1682
apply(rule conjI)
wenzelm@36277
  1683
apply(rule crename_interesting3)
wenzelm@36277
  1684
apply(rule l_redu.intros)
wenzelm@36277
  1685
apply(simp)
wenzelm@36277
  1686
apply(simp add: fresh_atm)
wenzelm@36277
  1687
apply(auto dest: fic_nrename simp add: fresh_prod fresh_atm)[1]
wenzelm@36277
  1688
apply(drule sym)
wenzelm@36277
  1689
apply(drule nrename_Cut)
wenzelm@36277
  1690
apply(simp add: fresh_prod fresh_atm)
wenzelm@36277
  1691
apply(simp add: fresh_prod fresh_atm)
wenzelm@36277
  1692
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
wenzelm@36277
  1693
apply(case_tac "xa=ya")
wenzelm@36277
  1694
apply(simp add: nrename_id)
wenzelm@36277
  1695
apply(rule l_redu.intros)
wenzelm@36277
  1696
apply(simp)
wenzelm@36277
  1697
apply(simp add: fresh_atm)
wenzelm@36277
  1698
apply(assumption)
wenzelm@36277
  1699
apply(frule nrename_ax2)
wenzelm@36277
  1700
apply(auto)[1]
wenzelm@36277
  1701
apply(case_tac "z=xa")
wenzelm@36277
  1702
apply(simp add: trm.inject)
wenzelm@36277
  1703
apply(rule_tac x="N'[x\<turnstile>n>xa]" in exI)
wenzelm@36277
  1704
apply(rule conjI)
wenzelm@36277
  1705
apply(rule nrename_interesting1)
wenzelm@36277
  1706
apply(auto)[1]
wenzelm@36277
  1707
apply(rule l_redu.intros)
wenzelm@36277
  1708
apply(simp)
wenzelm@36277
  1709
apply(simp add: fresh_atm)
wenzelm@36277
  1710
apply(auto dest: fin_nrename2 simp add: fresh_prod fresh_atm)[1]
wenzelm@36277
  1711
apply(simp add: trm.inject)
wenzelm@36277
  1712
apply(rule_tac x="N'[x\<turnstile>n>y]" in exI)
wenzelm@36277
  1713
apply(rule conjI)
wenzelm@36277
  1714
apply(rule nrename_interesting2)
wenzelm@36277
  1715
apply(simp_all)
wenzelm@36277
  1716
apply(rule l_redu.intros)
wenzelm@36277
  1717
apply(simp)
wenzelm@36277
  1718
apply(simp add: fresh_atm)
wenzelm@36277
  1719
apply(auto dest: fin_nrename2 simp add: fresh_prod fresh_atm)[1]
wenzelm@36277
  1720
(* LNot *)
wenzelm@36277
  1721
apply(drule sym)
wenzelm@36277
  1722
apply(drule nrename_Cut)
wenzelm@36277
  1723
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1724
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1725
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
wenzelm@36277
  1726
apply(drule nrename_NotR)
wenzelm@36277
  1727
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1728
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
wenzelm@36277
  1729
apply(drule nrename_NotL)
wenzelm@36277
  1730
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1731
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1732
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
wenzelm@36277
  1733
apply(rule_tac x="Cut <b>.N'b (x).N'a" in exI)
wenzelm@36277
  1734
apply(simp add: fresh_atm)[1]
wenzelm@36277
  1735
apply(rule l_redu.intros)
wenzelm@36277
  1736
apply(auto simp add: fresh_prod fresh_atm intro: nrename_fresh_interesting1)[1]
wenzelm@36277
  1737
apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
wenzelm@36277
  1738
apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting2)[1]
wenzelm@36277
  1739
apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting2)[1]
wenzelm@36277
  1740
apply(simp add: fresh_atm)
wenzelm@36277
  1741
apply(simp add: fresh_atm)
wenzelm@36277
  1742
(* LAnd1 *)
wenzelm@36277
  1743
apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
wenzelm@36277
  1744
apply(drule sym)
wenzelm@36277
  1745
apply(drule nrename_Cut)
wenzelm@36277
  1746
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1747
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1748
apply(auto)[1]
wenzelm@36277
  1749
apply(drule nrename_AndR)
wenzelm@36277
  1750
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1751
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1752
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
wenzelm@36277
  1753
apply(drule nrename_AndL1)
wenzelm@36277
  1754
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1755
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1756
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
wenzelm@36277
  1757
apply(rule_tac x="Cut <a1>.M'a (x).N'b" in exI)
wenzelm@36277
  1758
apply(simp add: fresh_atm)[1]
wenzelm@36277
  1759
apply(rule l_redu.intros)
wenzelm@36277
  1760
apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: nrename_fresh_interesting2)[1]
wenzelm@36277
  1761
apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
wenzelm@36277
  1762
apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
wenzelm@36277
  1763
apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
wenzelm@36277
  1764
apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
wenzelm@36277
  1765
apply(simp add: fresh_atm)
wenzelm@36277
  1766
(* LAnd2 *)
wenzelm@36277
  1767
apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
wenzelm@36277
  1768
apply(drule sym)
wenzelm@36277
  1769
apply(drule nrename_Cut)
wenzelm@36277
  1770
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1771
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1772
apply(auto)[1]
wenzelm@36277
  1773
apply(drule nrename_AndR)
wenzelm@36277
  1774
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1775
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1776
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
wenzelm@36277
  1777
apply(drule nrename_AndL2)
wenzelm@36277
  1778
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1779
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1780
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
wenzelm@36277
  1781
apply(rule_tac x="Cut <a2>.N'a (x).N'b" in exI)
wenzelm@36277
  1782
apply(simp add: fresh_atm)[1]
wenzelm@36277
  1783
apply(rule l_redu.intros)
wenzelm@36277
  1784
apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: nrename_fresh_interesting2)[1]
wenzelm@36277
  1785
apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
wenzelm@36277
  1786
apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
wenzelm@36277
  1787
apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
wenzelm@36277
  1788
apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
wenzelm@36277
  1789
apply(simp add: fresh_atm)
wenzelm@36277
  1790
(* LOr1 *)
wenzelm@36277
  1791
apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
wenzelm@36277
  1792
apply(drule sym)
wenzelm@36277
  1793
apply(drule nrename_Cut)
wenzelm@36277
  1794
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1795
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1796
apply(auto)[1]
wenzelm@36277
  1797
apply(drule nrename_OrL)
wenzelm@36277
  1798
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1799
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1800
apply(simp add: fresh_prod fresh_atm)
wenzelm@36277
  1801
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
wenzelm@36277
  1802
apply(drule nrename_OrR1)
wenzelm@36277
  1803
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1804
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
wenzelm@36277
  1805
apply(rule_tac x="Cut <a>.N' (x1).M'a" in exI)
wenzelm@36277
  1806
apply(rule conjI)
wenzelm@36277
  1807
apply(simp add: abs_fresh fresh_atm)[1]
wenzelm@36277
  1808
apply(rule l_redu.intros)
wenzelm@36277
  1809
apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: nrename_fresh_interesting2)[1]
wenzelm@36277
  1810
apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
wenzelm@36277
  1811
apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
wenzelm@36277
  1812
apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
wenzelm@36277
  1813
apply(simp add: fresh_atm)
wenzelm@36277
  1814
apply(simp add: fresh_atm)
wenzelm@36277
  1815
(* LOr2 *)
wenzelm@36277
  1816
apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
wenzelm@36277
  1817
apply(drule sym)
wenzelm@36277
  1818
apply(drule nrename_Cut)
wenzelm@36277
  1819
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1820
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1821
apply(auto)[1]
wenzelm@36277
  1822
apply(drule nrename_OrL)
wenzelm@36277
  1823
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1824
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1825
apply(simp add: fresh_prod fresh_atm)
wenzelm@36277
  1826
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
wenzelm@36277
  1827
apply(drule nrename_OrR2)
wenzelm@36277
  1828
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1829
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
wenzelm@36277
  1830
apply(rule_tac x="Cut <a>.N' (x2).N'a" in exI)
wenzelm@36277
  1831
apply(rule conjI)
wenzelm@36277
  1832
apply(simp add: abs_fresh fresh_atm)[1]
wenzelm@36277
  1833
apply(rule l_redu.intros)
wenzelm@36277
  1834
apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: nrename_fresh_interesting2)[1]
wenzelm@36277
  1835
apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
wenzelm@36277
  1836
apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
wenzelm@36277
  1837
apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
wenzelm@36277
  1838
apply(simp add: fresh_atm)
wenzelm@36277
  1839
apply(simp add: fresh_atm)
wenzelm@36277
  1840
(* ImpL *)
wenzelm@36277
  1841
apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
wenzelm@36277
  1842
apply(drule sym) 
wenzelm@36277
  1843
apply(drule nrename_Cut)
wenzelm@36277
  1844
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1845
apply(simp add: fresh_prod abs_fresh fresh_atm abs_supp fin_supp)
wenzelm@36277
  1846
apply(auto)[1]
wenzelm@36277
  1847
apply(drule nrename_ImpL)
wenzelm@36277
  1848
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1849
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1850
apply(simp add: fresh_prod fresh_atm)
wenzelm@36277
  1851
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
wenzelm@36277
  1852
apply(drule nrename_ImpR)
wenzelm@36277
  1853
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1854
apply(simp add: fresh_prod abs_fresh fresh_atm)
wenzelm@36277
  1855
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
wenzelm@36277
  1856
apply(rule_tac x="Cut <a>.(Cut <c>.M'a (x).N') (y).N'a" in exI)
wenzelm@36277
  1857
apply(rule conjI)
wenzelm@36277
  1858
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  1859
apply(rule l_redu.intros)
wenzelm@36277
  1860
apply(auto simp add: fresh_atm abs_fresh abs_supp fin_supp fresh_prod intro: nrename_fresh_interesting1)[1]
wenzelm@36277
  1861
apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: nrename_fresh_interesting2)[1]
wenzelm@36277
  1862
apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: nrename_fresh_interesting1)[1]
wenzelm@36277
  1863
apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: nrename_fresh_interesting2)[1]
wenzelm@36277
  1864
apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: nrename_fresh_interesting2)[1]
wenzelm@36277
  1865
apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: nrename_fresh_interesting2)[1]
wenzelm@36277
  1866
done
wenzelm@36277
  1867
wenzelm@36277
  1868
lemma nrename_aredu:
wenzelm@53015
  1869
  assumes a: "(M[x\<turnstile>n>y]) \<longrightarrow>\<^sub>a M'" "x\<noteq>y"
wenzelm@53015
  1870
  shows "\<exists>M0. M0[x\<turnstile>n>y]=M' \<and> M \<longrightarrow>\<^sub>a M0"
wenzelm@36277
  1871
using a
wenzelm@36277
  1872
apply(nominal_induct "M[x\<turnstile>n>y]" M' avoiding: M x y rule: a_redu.strong_induct)
wenzelm@36277
  1873
apply(drule  nrename_lredu)
wenzelm@36277
  1874
apply(blast)
wenzelm@36277
  1875
apply(drule  nrename_credu)
wenzelm@36277
  1876
apply(blast)
wenzelm@36277
  1877
(* Cut *)
wenzelm@36277
  1878
apply(drule sym)
wenzelm@36277
  1879
apply(drule nrename_Cut)
wenzelm@36277
  1880
apply(simp)
wenzelm@36277
  1881
apply(simp)
wenzelm@36277
  1882
apply(auto)[1]
wenzelm@36277
  1883
apply(drule_tac x="M'a" in meta_spec)
wenzelm@36277
  1884
apply(drule_tac x="xa" in meta_spec)
wenzelm@36277
  1885
apply(drule_tac x="y" in meta_spec)
wenzelm@36277
  1886
apply(auto)[1]
wenzelm@36277
  1887
apply(rule_tac x="Cut <a>.M0 (x).N'" in exI)
wenzelm@36277
  1888
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  1889
apply(rule conjI)
wenzelm@36277
  1890
apply(rule trans)
wenzelm@36277
  1891
apply(rule nrename.simps)
wenzelm@36277
  1892
apply(drule nrename_fresh_interesting2)
wenzelm@36277
  1893
apply(simp add: fresh_a_redu)
wenzelm@36277
  1894
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  1895
apply(drule nrename_fresh_interesting1)
wenzelm@36277
  1896
apply(simp add: fresh_prod fresh_atm)
wenzelm@36277
  1897
apply(simp add: fresh_a_redu)
wenzelm@36277
  1898
apply(simp)
wenzelm@36277
  1899
apply(auto)[1]
wenzelm@36277
  1900
apply(drule sym)
wenzelm@36277
  1901
apply(drule nrename_Cut)
wenzelm@36277
  1902
apply(simp)
wenzelm@36277
  1903
apply(simp)
wenzelm@36277
  1904
apply(auto)[1]
wenzelm@36277
  1905
apply(drule_tac x="N'a" in meta_spec)
wenzelm@36277
  1906
apply(drule_tac x="xa" in meta_spec)
wenzelm@36277
  1907
apply(drule_tac x="y" in meta_spec)
wenzelm@36277
  1908
apply(auto)[1]
wenzelm@36277
  1909
apply(rule_tac x="Cut <a>.M' (x).M0" in exI)
wenzelm@36277
  1910
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  1911
apply(rule conjI)
wenzelm@36277
  1912
apply(rule trans)
wenzelm@36277
  1913
apply(rule nrename.simps)
wenzelm@36277
  1914
apply(simp add: fresh_a_redu)
wenzelm@36277
  1915
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
wenzelm@36277
  1916
apply(simp)
wenzelm@36277
  1917
apply(auto)[1]
wenzelm@36277
  1918
(* NotL *)
wenzelm@36277
  1919
apply(drule sym)
wenzelm@36277
  1920
apply(frule nrename_NotL_aux)
wenzelm@36277
  1921
apply(erule disjE)
wenzelm@36277
  1922
apply(auto)[1]
wenzelm@36277
  1923
apply(drule nrename_NotL')
wenzelm@36277
  1924
apply(simp)
wenzelm@36277
  1925
apply(simp add: fresh_atm)
wenzelm@36277
  1926
apply(erule disjE)
wenzelm@36277
  1927
apply(auto)[1]
wenzelm@36277
  1928
apply(drule_tac x="N'" in meta_spec)
wenzelm@36277
  1929
apply(drule_tac x="xa" in meta_spec)
wenzelm@36277
  1930
apply(drule_tac x="y" in meta_spec)
wenzelm@36277
  1931
apply(auto)[1]
wenzelm@36277
  1932
apply(rule_tac x="NotL <a>.M0 x" in exI)
wenzelm@36277
  1933
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  1934
apply(auto)[1]
wenzelm@36277
  1935
apply(auto)[1]
wenzelm@36277
  1936
apply(drule_tac x="N'" in meta_spec)
wenzelm@36277
  1937
apply(drule_tac x="xa" in meta_spec)
wenzelm@36277
  1938
apply(drule_tac x="x" in meta_spec)
wenzelm@36277
  1939
apply(auto)[1]
wenzelm@36277
  1940
apply(rule_tac x="NotL <a>.M0 xa" in exI)
wenzelm@36277
  1941
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  1942
apply(auto)[1]
wenzelm@36277
  1943
(* NotR *)
wenzelm@36277
  1944
apply(drule sym)
wenzelm@36277
  1945
apply(drule nrename_NotR)
wenzelm@36277
  1946
apply(simp)
wenzelm@36277
  1947
apply(auto)[1]
wenzelm@36277
  1948
apply(drule_tac x="N'" in meta_spec)
wenzelm@36277
  1949
apply(drule_tac x="xa" in meta_spec)
wenzelm@36277
  1950
apply(drule_tac x="y" in meta_spec)
wenzelm@36277
  1951
apply(auto)[1]
wenzelm@36277
  1952
apply(rule_tac x="NotR (x).M0 a" in exI)
wenzelm@36277
  1953
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  1954
apply(auto)[1]
wenzelm@36277
  1955
(* AndR *)
wenzelm@36277
  1956
apply(drule sym)
wenzelm@36277
  1957
apply(drule nrename_AndR)
wenzelm@36277
  1958
apply(simp)
wenzelm@36277
  1959
apply(auto simp add: fresh_atm fresh_prod)[1]
wenzelm@36277
  1960
apply(auto simp add: fresh_atm fresh_prod)[1]
wenzelm@36277
  1961
apply(auto)[1]
wenzelm@36277
  1962
apply(drule_tac x="M'a" in meta_spec)
wenzelm@36277
  1963
apply(drule_tac x="x" in meta_spec)
wenzelm@36277
  1964
apply(drule_tac x="y" in meta_spec)
wenzelm@36277
  1965
apply(auto)[1]
wenzelm@36277
  1966
apply(rule_tac x="AndR <a>.M0 <b>.N' c" in exI)
wenzelm@36277
  1967
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  1968
apply(auto)[1]
wenzelm@36277
  1969
apply(rule trans)
wenzelm@36277
  1970
apply(rule nrename.simps)
wenzelm@36277
  1971
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
wenzelm@36277
  1972
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  1973
apply(auto intro: fresh_a_redu)[1]
wenzelm@36277
  1974
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  1975
apply(simp)
wenzelm@36277
  1976
apply(drule sym)
wenzelm@36277
  1977
apply(drule nrename_AndR)
wenzelm@36277
  1978
apply(simp)
wenzelm@36277
  1979
apply(auto simp add: fresh_atm fresh_prod)[1]
wenzelm@36277
  1980
apply(auto simp add: fresh_atm fresh_prod)[1]
wenzelm@36277
  1981
apply(auto)[1]
wenzelm@36277
  1982
apply(drule_tac x="N'a" in meta_spec)
wenzelm@36277
  1983
apply(drule_tac x="x" in meta_spec)
wenzelm@36277
  1984
apply(drule_tac x="y" in meta_spec)
wenzelm@36277
  1985
apply(auto)[1]
wenzelm@36277
  1986
apply(rule_tac x="AndR <a>.M' <b>.M0 c" in exI)
wenzelm@36277
  1987
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  1988
apply(auto)[1]
wenzelm@36277
  1989
apply(rule trans)
wenzelm@36277
  1990
apply(rule nrename.simps)
wenzelm@36277
  1991
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
wenzelm@36277
  1992
apply(auto intro: fresh_a_redu)[1]
wenzelm@36277
  1993
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  1994
apply(simp)
wenzelm@36277
  1995
apply(simp)
wenzelm@36277
  1996
(* AndL1 *)
wenzelm@36277
  1997
apply(drule sym)
wenzelm@36277
  1998
apply(frule nrename_AndL1_aux)
wenzelm@36277
  1999
apply(erule disjE)
wenzelm@36277
  2000
apply(auto)[1]
wenzelm@36277
  2001
apply(drule nrename_AndL1')
wenzelm@36277
  2002
apply(simp)
wenzelm@36277
  2003
apply(simp add: fresh_atm)
wenzelm@36277
  2004
apply(erule disjE)
wenzelm@36277
  2005
apply(auto)[1]
wenzelm@36277
  2006
apply(drule_tac x="N'" in meta_spec)
wenzelm@36277
  2007
apply(drule_tac x="xa" in meta_spec)
wenzelm@36277
  2008
apply(drule_tac x="ya" in meta_spec)
wenzelm@36277
  2009
apply(auto)[1]
wenzelm@36277
  2010
apply(rule_tac x="AndL1 (x).M0 y" in exI)
wenzelm@36277
  2011
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  2012
apply(auto)[1]
wenzelm@36277
  2013
apply(auto)[1]
wenzelm@36277
  2014
apply(drule_tac x="N'" in meta_spec)
wenzelm@36277
  2015
apply(drule_tac x="xa" in meta_spec)
wenzelm@36277
  2016
apply(drule_tac x="y" in meta_spec)
wenzelm@36277
  2017
apply(auto)[1]
wenzelm@36277
  2018
apply(rule_tac x="AndL1 (x).M0 xa" in exI)
wenzelm@36277
  2019
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  2020
apply(auto)[1]
wenzelm@36277
  2021
(* AndL2 *)
wenzelm@36277
  2022
apply(drule sym)
wenzelm@36277
  2023
apply(frule nrename_AndL2_aux)
wenzelm@36277
  2024
apply(erule disjE)
wenzelm@36277
  2025
apply(auto)[1]
wenzelm@36277
  2026
apply(drule nrename_AndL2')
wenzelm@36277
  2027
apply(simp)
wenzelm@36277
  2028
apply(simp add: fresh_atm)
wenzelm@36277
  2029
apply(erule disjE)
wenzelm@36277
  2030
apply(auto)[1]
wenzelm@36277
  2031
apply(drule_tac x="N'" in meta_spec)
wenzelm@36277
  2032
apply(drule_tac x="xa" in meta_spec)
wenzelm@36277
  2033
apply(drule_tac x="ya" in meta_spec)
wenzelm@36277
  2034
apply(auto)[1]
wenzelm@36277
  2035
apply(rule_tac x="AndL2 (x).M0 y" in exI)
wenzelm@36277
  2036
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  2037
apply(auto)[1]
wenzelm@36277
  2038
apply(auto)[1]
wenzelm@36277
  2039
apply(drule_tac x="N'" in meta_spec)
wenzelm@36277
  2040
apply(drule_tac x="xa" in meta_spec)
wenzelm@36277
  2041
apply(drule_tac x="y" in meta_spec)
wenzelm@36277
  2042
apply(auto)[1]
wenzelm@36277
  2043
apply(rule_tac x="AndL2 (x).M0 xa" in exI)
wenzelm@36277
  2044
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
wenzelm@36277
  2045
apply(auto)[1]
wenzelm@36277
  2046
(* OrL *)
wenzelm@36277
  2047
apply(drule sym)
wenzelm@36277
  2048
apply(frule nrename_OrL_aux)
wenzelm@36277
  2049
apply(erule disjE)
wenzelm@36277
  2050
apply(auto)[1]
wenzelm@36277
  2051
apply(drule nrename_OrL')
wenzelm@36277
  2052
apply(simp add: fresh_prod fresh_atm)
wenzelm@36277
  2053
apply(simp add: fresh_atm)
wenzelm@36277
  2054
apply(simp add: fresh_atm)
wenzelm@36277
  2055
apply(erule disjE)
wenzelm@36277
  2056
apply(auto)[1]