author | urbanc |
Tue, 06 Mar 2007 15:28:22 +0100 | |
changeset 22418 | 49e2d9744ae1 |
parent 22232 | 340cb955008e |
child 22542 | 8279a25ad0ae |
permissions | -rw-r--r-- |
19500 | 1 |
(* $Id$ *) |
18425 | 2 |
|
18661 | 3 |
theory Class |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
4 |
imports "../Nominal" |
18425 | 5 |
begin |
18395 | 6 |
|
18881 | 7 |
section {* Term-Calculus from Urban's PhD *} |
8 |
||
18395 | 9 |
atom_decl name coname |
10 |
||
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
11 |
text {* types *} |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
12 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
13 |
nominal_datatype ty = |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
14 |
PROP "string" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
15 |
| NOT "ty" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
16 |
| AND "ty" "ty" ("_ AND _" [100,100] 100) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
17 |
| OR "ty" "ty" ("_ OR _" [100,100] 100) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
18 |
| IMP "ty" "ty" ("_ IMPL _" [100,100] 100) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
19 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
20 |
text {* terms *} |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
21 |
|
18881 | 22 |
nominal_datatype trm = |
23 |
Ax "name" "coname" |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
24 |
| Cut "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" ("Cut <_>._ (_)._" [100,100,100,100] 100) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
25 |
| NotR "\<guillemotleft>name\<guillemotright>trm" "coname" ("NotR (_)._ _" [100,100,100] 100) |
18881 | 26 |
| NotL "\<guillemotleft>coname\<guillemotright>trm" "name" ("NotL <_>._ _" [100,100,100] 100) |
27 |
| AndR "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>coname\<guillemotright>trm" "coname" ("AndR <_>._ <_>._ _" [100,100,100,100,100] 100) |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
28 |
| AndL1 "\<guillemotleft>name\<guillemotright>trm" "name" ("AndL1 (_)._ _" [100,100,100] 100) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
29 |
| AndL2 "\<guillemotleft>name\<guillemotright>trm" "name" ("AndL2 (_)._ _" [100,100,100] 100) |
18881 | 30 |
| OrR1 "\<guillemotleft>coname\<guillemotright>trm" "coname" ("OrR1 <_>._ _" [100,100,100] 100) |
31 |
| OrR2 "\<guillemotleft>coname\<guillemotright>trm" "coname" ("OrR2 <_>._ _" [100,100,100] 100) |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
32 |
| OrL "\<guillemotleft>name\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name" ("OrL (_)._ (_)._ _" [100,100,100,100,100] 100) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
33 |
| ImpR "\<guillemotleft>name\<guillemotright>(\<guillemotleft>coname\<guillemotright>trm)" "coname" ("ImpR (_).<_>._ _" [100,100,100,100] 100) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
34 |
| ImpL "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name" ("ImpL <_>._ (_)._ _" [100,100,100,100,100] 100) |
19319
7e1f85ceb1a2
added the first two simple proofs of the recursion
urbanc
parents:
18881
diff
changeset
|
35 |
|
18881 | 36 |
text {* Induction principles *} |
18395 | 37 |
|
18881 | 38 |
thm trm.induct_weak --"weak" |
39 |
thm trm.induct --"strong" |
|
40 |
thm trm.induct' --"strong with explicit context (rarely needed)" |
|
41 |
||
42 |
text {* named terms *} |
|
43 |
||
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
44 |
nominal_datatype ntrm = Na "\<guillemotleft>name\<guillemotright>trm" ("((_):_)" [100,100] 100) |
18881 | 45 |
|
46 |
text {* conamed terms *} |
|
18395 | 47 |
|
22232 | 48 |
nominal_datatype ctrm = Co "\<guillemotleft>coname\<guillemotright>trm" ("(<_>:_)" [100,100] 100) |
49 |
||
50 |
text {* renaming functions *} |
|
51 |
||
52 |
consts |
|
53 |
nrename :: "trm \<Rightarrow> name \<Rightarrow> name \<Rightarrow> trm" ("_[_\<turnstile>n>_]" [100,100,100] 100) |
|
54 |
crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm" ("_[_\<turnstile>c>_]" [100,100,100] 100) |
|
55 |
||
56 |
nominal_primrec (freshness_context: "(d::coname,e::coname)") |
|
57 |
"(Ax x a)[d\<turnstile>c>e] = (if a=d then Ax x e else Ax x a)" |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
58 |
"\<lbrakk>a\<sharp>(d,e,N);x\<sharp>M\<rbrakk> \<Longrightarrow> (Cut <a>.M (x).N)[d\<turnstile>c>e] = Cut <a>.(M[d\<turnstile>c>e]) (x).(N[d\<turnstile>c>e])" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
59 |
"(NotR (x).M a)[d\<turnstile>c>e] = (if a=d then NotR (x).(M[d\<turnstile>c>e]) e else NotR (x).(M[d\<turnstile>c>e]) a)" |
22232 | 60 |
"a\<sharp>(d,e) \<Longrightarrow> (NotL <a>.M x)[d\<turnstile>c>e] = (NotL <a>.(M[d\<turnstile>c>e]) x)" |
61 |
"\<lbrakk>a\<sharp>(d,e,N,c);b\<sharp>(d,e,M,c);b\<noteq>a\<rbrakk> \<Longrightarrow> (AndR <a>.M <b>.N c)[d\<turnstile>c>e] = |
|
62 |
(if c=d then AndR <a>.(M[d\<turnstile>c>e]) <b>.(N[d \<turnstile>c>e]) e else AndR <a>.(M[d\<turnstile>c>e]) <b>.(N[d\<turnstile>c>e]) c)" |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
63 |
"x\<sharp>y \<Longrightarrow> (AndL1 (x).M y)[d\<turnstile>c>e] = AndL1 (x).(M[d\<turnstile>c>e]) y" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
64 |
"x\<sharp>y \<Longrightarrow> (AndL2 (x).M y)[d\<turnstile>c>e] = AndL2 (x).(M[d\<turnstile>c>e]) y" |
22232 | 65 |
"a\<sharp>(d,e,b) \<Longrightarrow> (OrR1 <a>.M b)[d\<turnstile>c>e] = (if b=d then OrR1 <a>.(M[d\<turnstile>c>e]) e else OrR1 <a>.(M[d\<turnstile>c>e]) b)" |
66 |
"a\<sharp>(d,e,b) \<Longrightarrow> (OrR2 <a>.M b)[d\<turnstile>c>e] = (if b=d then OrR2 <a>.(M[d\<turnstile>c>e]) e else OrR2 <a>.(M[d\<turnstile>c>e]) b)" |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
67 |
"\<lbrakk>x\<sharp>(N,z);y\<sharp>(M,z);y\<noteq>x\<rbrakk> \<Longrightarrow> (OrL (x).M (y).N z)[d\<turnstile>c>e] = OrL (x).(M[d\<turnstile>c>e]) (y).(N[d\<turnstile>c>e]) z" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
68 |
"a\<sharp>(d,e,b) \<Longrightarrow> (ImpR (x).<a>.M b)[d\<turnstile>c>e] = |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
69 |
(if b=d then ImpR (x).<a>.(M[d\<turnstile>c>e]) e else ImpR (x).<a>.(M[d\<turnstile>c>e]) b)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
70 |
"\<lbrakk>a\<sharp>(d,e,N);x\<sharp>(M,y)\<rbrakk> \<Longrightarrow> (ImpL <a>.M (x).N y)[d\<turnstile>c>e] = ImpL <a>.(M[d\<turnstile>c>e]) (x).(N[d\<turnstile>c>e]) y" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
71 |
apply(finite_guess)+ |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
72 |
apply(rule TrueI)+ |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
73 |
apply(simp add: abs_fresh abs_supp fin_supp)+ |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
74 |
apply(fresh_guess)+ |
22232 | 75 |
done |
76 |
||
77 |
nominal_primrec (freshness_context: "(u::name,v::name)") |
|
78 |
"(Ax x a)[u\<turnstile>n>v] = (if x=u then Ax v a else Ax x a)" |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
79 |
"\<lbrakk>a\<sharp>N;x\<sharp>(u,v,M)\<rbrakk> \<Longrightarrow> (Cut <a>.M (x).N)[u\<turnstile>n>v] = Cut <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v])" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
80 |
"x\<sharp>(u,v) \<Longrightarrow> (NotR (x).M a)[u\<turnstile>n>v] = NotR (x).(M[u\<turnstile>n>v]) a" |
22232 | 81 |
"(NotL <a>.M x)[u\<turnstile>n>v] = (if x=u then NotL <a>.(M[u\<turnstile>n>v]) v else NotL <a>.(M[u\<turnstile>n>v]) x)" |
82 |
"\<lbrakk>a\<sharp>(N,c);b\<sharp>(M,c);b\<noteq>a\<rbrakk> \<Longrightarrow> (AndR <a>.M <b>.N c)[u\<turnstile>n>v] = AndR <a>.(M[u\<turnstile>n>v]) <b>.(N[u\<turnstile>n>v]) c" |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
83 |
"x\<sharp>(u,v,y) \<Longrightarrow> (AndL1 (x).M y)[u\<turnstile>n>v] = (if y=u then AndL1 (x).(M[u\<turnstile>n>v]) v else AndL1 (x).(M[u\<turnstile>n>v]) y)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
84 |
"x\<sharp>(u,v,y) \<Longrightarrow> (AndL2 (x).M y)[u\<turnstile>n>v] = (if y=u then AndL2 (x).(M[u\<turnstile>n>v]) v else AndL2 (x).(M[u\<turnstile>n>v]) y)" |
22232 | 85 |
"a\<sharp>b \<Longrightarrow> (OrR1 <a>.M b)[u\<turnstile>n>v] = OrR1 <a>.(M[u\<turnstile>n>v]) b" |
86 |
"a\<sharp>b \<Longrightarrow> (OrR2 <a>.M b)[u\<turnstile>n>v] = OrR2 <a>.(M[u\<turnstile>n>v]) b" |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
87 |
"\<lbrakk>x\<sharp>(u,v,N,z);y\<sharp>(u,v,M,z);y\<noteq>x\<rbrakk> \<Longrightarrow> (OrL (x).M (y).N z)[u\<turnstile>n>v] = |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
88 |
(if z=u then OrL (x).(M[u\<turnstile>n>v]) (y).(N[u\<turnstile>n>v]) v else OrL (x).(M[u\<turnstile>n>v]) (y).(N[u\<turnstile>n>v]) z)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
89 |
"\<lbrakk>a\<sharp>b; x\<sharp>(u,v)\<rbrakk> \<Longrightarrow> (ImpR (x).<a>.M b)[u\<turnstile>n>v] = ImpR (x).<a>.(M[u\<turnstile>n>v]) b" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
90 |
"\<lbrakk>a\<sharp>N;x\<sharp>(u,v,M,y)\<rbrakk> \<Longrightarrow> (ImpL <a>.M (x).N y)[u\<turnstile>n>v] = |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
91 |
(if y=u then ImpL <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v]) v else ImpL <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v]) y)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
92 |
apply(finite_guess)+ |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
93 |
apply(rule TrueI)+ |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
94 |
apply(simp add: abs_fresh abs_supp fs_name1 fs_coname1)+ |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
95 |
apply(fresh_guess)+ |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
96 |
done |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
97 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
98 |
lemmas eq_bij = pt_bij[OF pt_name_inst, OF at_name_inst] pt_bij[OF pt_coname_inst, OF at_coname_inst] |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
99 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
100 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
101 |
lemma crename_name_eqvt[eqvt]: |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
102 |
fixes pi::"name prm" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
103 |
shows "pi\<bullet>(M[d\<turnstile>c>e]) = (pi\<bullet>M)[(pi\<bullet>d)\<turnstile>c>(pi\<bullet>e)]" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
104 |
apply(nominal_induct M avoiding: d e rule: trm.induct) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
105 |
apply(auto simp add: fresh_bij eq_bij) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
106 |
done |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
107 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
108 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
109 |
lemma crename_coname_eqvt[eqvt]: |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
110 |
fixes pi::"coname prm" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
111 |
shows "pi\<bullet>(M[d\<turnstile>c>e]) = (pi\<bullet>M)[(pi\<bullet>d)\<turnstile>c>(pi\<bullet>e)]" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
112 |
apply(nominal_induct M avoiding: d e rule: trm.induct) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
113 |
apply(auto simp add: fresh_bij eq_bij) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
114 |
done |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
115 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
116 |
lemma nrename_name_eqvt[eqvt]: |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
117 |
fixes pi::"name prm" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
118 |
shows "pi\<bullet>(M[x\<turnstile>n>y]) = (pi\<bullet>M)[(pi\<bullet>x)\<turnstile>n>(pi\<bullet>y)]" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
119 |
apply(nominal_induct M avoiding: x y rule: trm.induct) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
120 |
apply(auto simp add: fresh_bij eq_bij) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
121 |
done |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
122 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
123 |
lemma nrename_coname_eqvt[eqvt]: |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
124 |
fixes pi::"coname prm" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
125 |
shows "pi\<bullet>(M[x\<turnstile>n>y]) = (pi\<bullet>M)[(pi\<bullet>x)\<turnstile>n>(pi\<bullet>y)]" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
126 |
apply(nominal_induct M avoiding: x y rule: trm.induct) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
127 |
apply(auto simp add: fresh_bij eq_bij) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
128 |
done |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
129 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
130 |
text {* substitution functions *} |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
131 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
132 |
consts |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
133 |
substn :: "trm \<Rightarrow> name \<Rightarrow> coname \<Rightarrow> trm \<Rightarrow> trm" ("_[_:=<_>._]" [100,100,100,100] 100) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
134 |
substc :: "trm \<Rightarrow> coname \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_[_:=(_)._]" [100,100,100,100] 100) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
135 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
136 |
nominal_primrec (freshness_context: "(y::name,c::coname,P::trm)") |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
137 |
"(Ax x a)[y:=<c>.P] = (if x=y then P[c\<turnstile>c>a] else Ax x a)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
138 |
"\<lbrakk>a\<sharp>(c,P,N);x\<sharp>(y,c,P,M)\<rbrakk> \<Longrightarrow> |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
139 |
(Cut <a>.M (x).N)[y:=<c>.P] = Cut <a>.(M[y:=<c>.P]) (x).(N[y:=<c>.P])" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
140 |
"x\<sharp>(y,c,P) \<Longrightarrow> |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
141 |
(NotR (x).M a)[y:=<c>.P] = NotR (x).(M[y:=<c>.P]) a" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
142 |
"a\<sharp>(c,P)\<Longrightarrow> |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
143 |
(NotL <a>.M x)[y:=<c>.P] = (if x=y then Cut <c>.P (x).(NotL <a>. (M[y:=<c>.P]) x) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
144 |
else NotL <a>. (M[y:=<c>.P]) x)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
145 |
"\<lbrakk>a\<sharp>(c,P,N,d);b\<sharp>(c,P,M,d);b\<noteq>a\<rbrakk> \<Longrightarrow> |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
146 |
(AndR <a>.M <b>.N d)[y:=<c>.P] = AndR <a>.(M[y:=<c>.P]) <b>.(N[y:=<c>.P]) d" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
147 |
"x\<sharp>(y,c,P,z) \<Longrightarrow> |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
148 |
(AndL1 (x).M z)[y:=<c>.P] = (if z=y then Cut <c>.P (z).AndL1 (x).(M[y:=<c>.P]) z |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
149 |
else AndL1 (x).(M[y:=<c>.P]) z)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
150 |
"x\<sharp>(y,c,P,z) \<Longrightarrow> |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
151 |
(AndL2 (x).M z)[y:=<c>.P] = (if z=y then Cut <c>.P (z).AndL2 (x).(M[y:=<c>.P]) z |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
152 |
else AndL2 (x).(M[y:=<c>.P]) z)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
153 |
"a\<sharp>(c,P,b) \<Longrightarrow> |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
154 |
(OrR1 <a>.M b)[y:=<c>.P] = OrR1 <a>.(M[y:=<c>.P]) b" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
155 |
"a\<sharp>(c,P,b) \<Longrightarrow> |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
156 |
(OrR2 <a>.M b)[y:=<c>.P] = OrR2 <a>.(M[y:=<c>.P]) b" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
157 |
"\<lbrakk>x\<sharp>(y,N,c,P,z);u\<sharp>(y,M,c,P,z);x\<noteq>u\<rbrakk> \<Longrightarrow> |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
158 |
(OrL (x).M (u).N z)[y:=<c>.P] = (if z=y then Cut <c>.P (z).(OrL (x).(M[y:=<c>.P]) (u).(N[y:=<c>.P]) z) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
159 |
else OrL (x).(M[y:=<c>.P]) (u).(N[y:=<c>.P]) z)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
160 |
"\<lbrakk>a\<sharp>(b,c,P); x\<sharp>(y,c,P)\<rbrakk> \<Longrightarrow> |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
161 |
(ImpR (x).<a>.M b)[y:=<c>.P] = ImpR (x).<a>.(M[y:=<c>.P]) b" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
162 |
"\<lbrakk>a\<sharp>(N,c,P);x\<sharp>(y,c,P,M,z)\<rbrakk> \<Longrightarrow> |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
163 |
(ImpL <a>.M (x).N z)[y:=<c>.P] = (if y=z then Cut <c>.P (z).(ImpL <a>.(M[y:=<c>.P]) (x).(N[y:=<c>.P]) z) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
164 |
else ImpL <a>.(M[y:=<c>.P]) (x).(N[y:=<c>.P]) z)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
165 |
apply(finite_guess)+ |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
166 |
apply(rule TrueI)+ |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
167 |
apply(simp add: abs_fresh abs_supp fs_name1 fs_coname1)+ |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
168 |
apply(fresh_guess)+ |
22232 | 169 |
done |
18881 | 170 |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
171 |
text {* typing contexts *} |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
172 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
173 |
types |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
174 |
ctxtn = "(name\<times>ty) list" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
175 |
ctxtc = "(coname\<times>ty) list" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
176 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
177 |
inductive2 |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
178 |
validc :: "ctxtc \<Rightarrow> bool" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
179 |
where |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
180 |
vc1[intro]: "validc []" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
181 |
| vc2[intro]: "\<lbrakk>a\<sharp>\<Delta>; validc \<Delta>\<rbrakk> \<Longrightarrow> validc ((a,T)#\<Delta>)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
182 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
183 |
inductive2 |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
184 |
validn :: "ctxtn \<Rightarrow> bool" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
185 |
where |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
186 |
vn1[intro]: "validn []" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
187 |
| vn2[intro]: "\<lbrakk>x\<sharp>\<Gamma>; validn \<Gamma>\<rbrakk> \<Longrightarrow> validn ((x,T)#\<Gamma>)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
188 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
189 |
text {* typing relation *} |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
190 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
191 |
inductive2 |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
192 |
typing :: "ctxtn \<Rightarrow> trm \<Rightarrow> ctxtc \<Rightarrow> bool" ("_ \<turnstile> _ \<turnstile> _" [100,100,100] 100) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
193 |
where |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
194 |
"\<lbrakk>validn \<Gamma>;validc \<Delta>; (x,B)\<in>set \<Gamma>; (a,B)\<in>set \<Delta>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Ax x a \<turnstile> \<Delta>" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
195 |
| "\<lbrakk>x\<sharp>\<Gamma>; ((x,B)#\<Gamma>) \<turnstile> M \<turnstile> \<Delta>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> NotR (x).M a \<turnstile> ((a,NOT B)#\<Delta>)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
196 |
| "\<lbrakk>a\<sharp>\<Delta>; \<Gamma> \<turnstile> M \<turnstile> ((a,B)#\<Delta>)\<rbrakk> \<Longrightarrow> ((x,NOT B)#\<Gamma>) \<turnstile> NotL <a>.M x \<turnstile> \<Delta>" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
197 |
| "\<lbrakk>x\<sharp>\<Gamma>; ((x,B1)#\<Gamma>) \<turnstile> M \<turnstile> \<Delta>\<rbrakk> \<Longrightarrow> ((y,B1 AND B2)#\<Gamma>) \<turnstile> AndL1 (x).M y \<turnstile> \<Delta>" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
198 |
| "\<lbrakk>x\<sharp>\<Gamma>; ((x,B2)#\<Gamma>) \<turnstile> M \<turnstile> \<Delta>\<rbrakk> \<Longrightarrow> ((y,B1 AND B2)#\<Gamma>) \<turnstile> AndL2 (x).M y \<turnstile> \<Delta>" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
199 |
| "\<lbrakk>a\<sharp>\<Delta>;b\<sharp>\<Delta>; \<Gamma> \<turnstile> M \<turnstile> ((a,B)#\<Delta>); \<Gamma> \<turnstile> N \<turnstile> ((b,C)#\<Delta>)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> AndR <a>.M <b>.N c \<turnstile> ((c,B AND C)#\<Delta>)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
200 |
| "\<lbrakk>x\<sharp>\<Gamma>;y\<sharp>\<Gamma>; ((x,B)#\<Gamma>) \<turnstile> M \<turnstile> \<Delta>; ((y,C)#\<Gamma>) \<turnstile> N \<turnstile> \<Delta>\<rbrakk> \<Longrightarrow> ((z,B OR C)#\<Gamma>) \<turnstile> OrL (x).M (y).N z \<turnstile> \<Delta>" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
201 |
| "\<lbrakk>a\<sharp>\<Delta>; \<Gamma> \<turnstile> M \<turnstile> ((a,B1)#\<Delta>)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> OrR1 <a>.M b \<turnstile> ((b,B1 OR B2)#\<Delta>)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
202 |
| "\<lbrakk>a\<sharp>\<Delta>; \<Gamma> \<turnstile> M \<turnstile> ((a,B2)#\<Delta>)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> OrR2 <a>.M b \<turnstile> ((b,B1 OR B2)#\<Delta>)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
203 |
| "\<lbrakk>a\<sharp>\<Delta>;x\<sharp>\<Gamma>; \<Gamma> \<turnstile> M \<turnstile> ((a,B)#\<Delta>); ((x,C)#\<Gamma>) \<turnstile> N \<turnstile> \<Delta>\<rbrakk> \<Longrightarrow> ((y,B IMPL C)#\<Gamma>) \<turnstile> ImpL <a>.M (x).N y \<turnstile> \<Delta>" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
204 |
| "\<lbrakk>a\<sharp>\<Delta>;x\<sharp>\<Gamma>; ((x,B)#\<Gamma>) \<turnstile> M \<turnstile> ((a,C)#\<Delta>)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> ImpR (x).<a>.M b \<turnstile> ((b,B IMPL C)#\<Delta>)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
205 |
| "\<lbrakk>a\<sharp>\<Delta>1;x\<sharp>\<Gamma>2; validn(\<Gamma>1@\<Gamma>2); validc (\<Delta>1@\<Delta>2); \<Gamma>1 \<turnstile> M \<turnstile> ((a,B)#\<Delta>1); ((x,B)#\<Gamma>2) \<turnstile> N \<turnstile> \<Delta>2\<rbrakk> |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
206 |
\<Longrightarrow> (\<Gamma>1@\<Gamma>2) \<turnstile> Cut <a>.M (x).N \<turnstile> (\<Delta>1@\<Delta>2)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
207 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
208 |
text {* relations about freshly introducing a name or coname *} |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
209 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
210 |
inductive2 |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
211 |
fin :: "trm \<times> name \<Rightarrow> bool" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
212 |
where |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
213 |
"fin (Ax x a,x)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
214 |
| "x\<sharp>M \<Longrightarrow> fin (NotL <a>.M x,x)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
215 |
| "y\<sharp>[x].M \<Longrightarrow> fin (AndL1 (x).M y,y)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
216 |
| "y\<sharp>[x].M \<Longrightarrow> fin (AndL2 (x).M y,y)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
217 |
| "\<lbrakk>z\<sharp>[x].M;z\<sharp>[y].N\<rbrakk> \<Longrightarrow> fin (OrL (x).M (y).N z,z)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
218 |
| "\<lbrakk>y\<sharp>M;y\<sharp>[x].N\<rbrakk> \<Longrightarrow> fin (ImpL <a>.M (x).N y,y)" |
18395 | 219 |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
220 |
inductive2 |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
221 |
fic :: "trm \<times> coname \<Rightarrow> bool" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
222 |
where |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
223 |
"fic (Ax x a,a)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
224 |
| "a\<sharp>M \<Longrightarrow> fic (NotR (x).M a,a)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
225 |
| "\<lbrakk>c\<sharp>[a].M;c\<sharp>[b].N\<rbrakk> \<Longrightarrow> fic (AndR <a>.M <b>.N c,c)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
226 |
| "b\<sharp>[a].M \<Longrightarrow> fic (OrR1 <a>.M b,b)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
227 |
| "b\<sharp>[a].M \<Longrightarrow> fic (OrR2 <a>.M b,b)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
228 |
| "\<lbrakk>b\<sharp>[a].M\<rbrakk> \<Longrightarrow> fic (ImpR (x).<a>.M b,b)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
229 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
230 |
text {* cut-reductions *} |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
231 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
232 |
inductive2 |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
233 |
red :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<longrightarrow>\<^isub>c _" [100,100] 100) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
234 |
where |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
235 |
"fic (M,a) \<Longrightarrow> Cut <a>.M (x).(Ax x b) \<longrightarrow>\<^isub>c M[a\<turnstile>c>b]" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
236 |
| "fin (M,x) \<Longrightarrow> Cut <a>.(Ax y a) (x).M \<longrightarrow>\<^isub>c M[x\<turnstile>n>y]" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
237 |
| "\<lbrakk>fic (NotR (x).M a,a); fin (NotL <b>.N y,y)\<rbrakk> \<Longrightarrow> |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
238 |
Cut <a>.(NotR (x).M a) (y).(NotL <b>.N y) \<longrightarrow>\<^isub>c Cut <b>.N (x).M" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
239 |
| "\<lbrakk>fic (AndR <a1>.M1 <a2>.M2 b,b); fin (AndL1 (x).N y,y)\<rbrakk> \<Longrightarrow> |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
240 |
Cut <b>.(AndR <a1>.M1 <a2>.M2 b) (y).(AndL1 (x).N y) \<longrightarrow>\<^isub>c Cut <a1>.M1 (x).N" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
241 |
| "\<lbrakk>fic (AndR <a1>.M1 <a2>.M2 b,b); fin (AndL2 (x).N y,y)\<rbrakk> \<Longrightarrow> |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
242 |
Cut <b>.(AndR <a1>.M1 <a2>.M2 b) (y).(AndL2 (x).N y) \<longrightarrow>\<^isub>c Cut <a2>.M2 (x).N" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
243 |
| "\<lbrakk>fic (AndR <a1>.M1 <a2>.M2 b,b); fin (AndL1 (x).N y,y)\<rbrakk> \<Longrightarrow> |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
244 |
Cut <b>.(AndR <a1>.M1 <a2>.M2 b) (y).(AndL1 (x).N y) \<longrightarrow>\<^isub>c Cut <a1>.M1 (x).N" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
245 |
| "\<lbrakk>fic (OrR1 <a>.M b,b); fin (OrL (x1).N1 (x2).N2 y,y)\<rbrakk> \<Longrightarrow> |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
246 |
Cut <b>.(OrR1 <a>.M b) (y).(OrL (x1).N1 (x2).N2 y) \<longrightarrow>\<^isub>c Cut <a>.M (x1).N1" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
247 |
| "\<lbrakk>fic (OrR2 <a>.M b,b); fin (OrL (x1).N1 (x2).N2 y,y)\<rbrakk> \<Longrightarrow> |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
248 |
Cut <b>.(OrR2 <a>.M b) (y).(OrL (x1).N1 (x2).N2 y) \<longrightarrow>\<^isub>c Cut <a>.M (x2).N2" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
249 |
| "\<lbrakk>fin (ImpL <c>.N (y).P z,z); fic (ImpR (x).<a>.M b,b)\<rbrakk> \<Longrightarrow> |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
250 |
Cut <b>.(ImpR (x).<a>.M b) (z).(ImpL <c>.N (y).P z) \<longrightarrow>\<^isub>c Cut <a>.(Cut <c>.N (x).M) (y).P" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
251 |
| "\<lbrakk>fin (ImpL <c>.N (y).P z,z); fic (ImpR (x).<a>.M b,b)\<rbrakk> \<Longrightarrow> |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
252 |
Cut <b>.(ImpR (x).<a>.M b) (z).(ImpL <c>.N (y).P z) \<longrightarrow>\<^isub>c Cut <a>.N (x).(Cut <a>.M (y).P)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
253 |
| "\<not>fic (M,a) \<Longrightarrow> Cut <a>.M (x).N \<longrightarrow>\<^isub>c M[a:=(x).N]" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
254 |
| "\<not>fin (N,x) \<Longrightarrow> Cut <a>.M (x).N \<longrightarrow>\<^isub>c N[x:=<a>.M]" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
255 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
256 |
text {* PROOFS *} |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
257 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
258 |
lemma validn_eqvt[eqvt]: |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
259 |
fixes pi1:: "name prm" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
260 |
and pi2:: "coname prm" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
261 |
assumes a: "validn \<Gamma>" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
262 |
shows "validn (pi1\<bullet>\<Gamma>)" and "validn (pi2\<bullet>\<Gamma>)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
263 |
using a by (induct) (auto simp add: fresh_bij) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
264 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
265 |
lemma validc_eqvt[eqvt]: |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
266 |
fixes pi1:: "name prm" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
267 |
and pi2:: "coname prm" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
268 |
assumes a: "validc \<Delta>" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
269 |
shows "validc (pi1\<bullet>\<Delta>)" and "validc (pi2\<bullet>\<Delta>)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
270 |
using a by (induct) (auto simp add: fresh_bij) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
271 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
272 |
text {* Weakening Lemma *} |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
273 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
274 |
abbreviation |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
275 |
"subn" :: "ctxtn \<Rightarrow> ctxtn \<Rightarrow> bool" (" _ \<lless>n _ " [80,80] 80) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
276 |
where |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
277 |
"\<Gamma>1 \<lless>n \<Gamma>2 \<equiv> \<forall>x B. (x,B)\<in>set \<Gamma>1 \<longrightarrow> (x,B)\<in>set \<Gamma>2" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
278 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
279 |
abbreviation |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
280 |
"subc" :: "ctxtc \<Rightarrow> ctxtc \<Rightarrow> bool" (" _ \<lless>c _ " [80,80] 80) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
281 |
where |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
282 |
"\<Delta>1 \<lless>c \<Delta>2 \<equiv> \<forall>a B. (a,B)\<in>set \<Delta>1 \<longrightarrow> (a,B)\<in>set \<Delta>2" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22232
diff
changeset
|
283 |
|
19500 | 284 |
|
285 |
end |
|
286 |