1792
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
theory Classical
|
2454
|
2 |
imports "../Nominal2"
|
1792
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
begin
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
|
2617
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
5 |
(* example from Urban's PhD *)
|
1792
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
6 |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
atom_decl name
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
8 |
atom_decl coname
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
10 |
nominal_datatype trm =
|
2889
|
11 |
Ax "name" "coname"
|
2891
304dfe6cc83a
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
12 |
| Cut c::"coname" t1::"trm" n::"name" t2::"trm" bind n in t1, bind c in t2
|
2889
|
13 |
("Cut <_>._ '(_')._" [100,100,100,100] 100)
|
|
14 |
| NotR n::"name" t::"trm" "coname" bind n in t
|
|
15 |
("NotR '(_')._ _" [100,100,100] 100)
|
|
16 |
| NotL c::"coname" t::"trm" "name" bind c in t
|
|
17 |
("NotL <_>._ _" [100,100,100] 100)
|
|
18 |
| AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind c1 in t1, bind c2 in t2
|
|
19 |
("AndR <_>._ <_>._ _" [100,100,100,100,100] 100)
|
|
20 |
| AndL1 n::"name" t::"trm" "name" bind n in t
|
|
21 |
("AndL1 '(_')._ _" [100,100,100] 100)
|
|
22 |
| AndL2 n::"name" t::"trm" "name" bind n in t
|
|
23 |
("AndL2 '(_')._ _" [100,100,100] 100)
|
|
24 |
| OrR1 c::"coname" t::"trm" "coname" bind c in t
|
|
25 |
("OrR1 <_>._ _" [100,100,100] 100)
|
|
26 |
| OrR2 c::"coname" t::"trm" "coname" bind c in t
|
|
27 |
("OrR2 <_>._ _" [100,100,100] 100)
|
|
28 |
| OrL n1::"name" t1::"trm" n2::"name" t2::"trm" "name" bind n1 in t1, bind n2 in t2
|
|
29 |
("OrL '(_')._ '(_')._ _" [100,100,100,100,100] 100)
|
|
30 |
| ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" bind c in t1, bind n in t2
|
|
31 |
("ImpL <_>._ '(_')._ _" [100,100,100,100,100] 100)
|
|
32 |
| ImpR c::"coname" n::"name" t::"trm" "coname" bind n c in t
|
|
33 |
("ImpR '(_').<_>._ _" [100,100,100,100] 100)
|
1792
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
34 |
|
2436
|
35 |
thm trm.distinct
|
|
36 |
thm trm.induct
|
|
37 |
thm trm.exhaust
|
2617
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
38 |
thm trm.strong_exhaust
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
39 |
thm trm.strong_exhaust[simplified]
|
2436
|
40 |
thm trm.fv_defs
|
|
41 |
thm trm.bn_defs
|
|
42 |
thm trm.perm_simps
|
|
43 |
thm trm.eq_iff
|
|
44 |
thm trm.fv_bn_eqvt
|
|
45 |
thm trm.size_eqvt
|
2617
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
46 |
thm trm.supp
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
47 |
thm trm.supp[simplified]
|
1792
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
48 |
|
2891
304dfe6cc83a
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
49 |
nominal_primrec (* (invariant "\<lambda>(_, e, d) y. atom e \<sharp> y \<and> atom d \<sharp> y") *)
|
2889
|
50 |
crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm" ("_[_\<turnstile>c>_]" [100,100,100] 100)
|
|
51 |
where
|
|
52 |
"(Ax x a)[d\<turnstile>c>e] = (if a=d then Ax x e else Ax x a)"
|
|
53 |
| "atom a \<sharp> (d, e) \<Longrightarrow> (Cut <a>.M (x).N)[d\<turnstile>c>e] = Cut <a>.(M[d\<turnstile>c>e]) (x).(N[d\<turnstile>c>e])"
|
|
54 |
| "(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)"
|
|
55 |
| "atom a \<sharp> (d, e) \<Longrightarrow> (NotL <a>.M x)[d\<turnstile>c>e] = (NotL <a>.(M[d\<turnstile>c>e]) x)"
|
|
56 |
| "\<lbrakk>atom a \<sharp> (d, e); atom b \<sharp> (d, e)\<rbrakk> \<Longrightarrow> (AndR <a>.M <b>.N c)[d\<turnstile>c>e] =
|
|
57 |
(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)"
|
|
58 |
| "(AndL1 (x).M y)[d\<turnstile>c>e] = AndL1 (x).(M[d\<turnstile>c>e]) y"
|
|
59 |
| "(AndL2 (x).M y)[d\<turnstile>c>e] = AndL2 (x).(M[d\<turnstile>c>e]) y"
|
|
60 |
| "atom a \<sharp> (d, e) \<Longrightarrow> (OrR1 <a>.M b)[d\<turnstile>c>e] =
|
|
61 |
(if b=d then OrR1 <a>.(M[d\<turnstile>c>e]) e else OrR1 <a>.(M[d\<turnstile>c>e]) b)"
|
|
62 |
| "atom a \<sharp> (d, e) \<Longrightarrow> (OrR2 <a>.M b)[d\<turnstile>c>e] =
|
|
63 |
(if b=d then OrR2 <a>.(M[d\<turnstile>c>e]) e else OrR2 <a>.(M[d\<turnstile>c>e]) b)"
|
|
64 |
| "(OrL (x).M (y).N z)[d\<turnstile>c>e] = OrL (x).(M[d\<turnstile>c>e]) (y).(N[d\<turnstile>c>e]) z"
|
|
65 |
| "atom a \<sharp> (d, e) \<Longrightarrow> (ImpR (x).<a>.M b)[d\<turnstile>c>e] =
|
|
66 |
(if b=d then ImpR (x).<a>.(M[d\<turnstile>c>e]) e else ImpR (x).<a>.(M[d\<turnstile>c>e]) b)"
|
|
67 |
| "atom a \<sharp> (d, e) \<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"
|
|
68 |
apply(simp only: eqvt_def)
|
|
69 |
apply(simp only: crename_graph_def)
|
|
70 |
apply (rule, perm_simp, rule)
|
2891
304dfe6cc83a
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
71 |
(*apply(erule crename_graph.induct)
|
304dfe6cc83a
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
72 |
apply(simp add: trm.fresh)*)
|
2889
|
73 |
apply(rule TrueI)
|
|
74 |
-- "covered all cases"
|
|
75 |
apply(case_tac x)
|
|
76 |
apply(rule_tac y="a" and c="(b, c)" in trm.strong_exhaust)
|
|
77 |
apply(simp)
|
|
78 |
apply(blast)
|
|
79 |
apply(simp add: fresh_star_def)
|
|
80 |
apply(blast)
|
|
81 |
apply(simp add: fresh_star_def)
|
|
82 |
apply(blast)
|
|
83 |
apply(simp add: fresh_star_def)
|
|
84 |
apply(blast)
|
|
85 |
apply(simp add: fresh_star_def)
|
|
86 |
apply(blast)
|
|
87 |
apply(simp add: fresh_star_def)
|
|
88 |
apply(blast)
|
|
89 |
apply(simp add: fresh_star_def)
|
|
90 |
apply(blast)
|
|
91 |
apply(simp add: fresh_star_def)
|
|
92 |
apply(blast)
|
|
93 |
apply(simp add: fresh_star_def)
|
|
94 |
apply(blast)
|
|
95 |
apply(simp add: fresh_star_def)
|
|
96 |
apply(metis)
|
|
97 |
apply(simp add: fresh_star_def)
|
|
98 |
apply(metis)
|
|
99 |
apply(simp add: fresh_star_def)
|
|
100 |
apply(metis)
|
2891
304dfe6cc83a
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
101 |
-- "compatibility"
|
2889
|
102 |
apply(simp_all)
|
2891
304dfe6cc83a
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
103 |
apply(rule conjI)
|
304dfe6cc83a
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
104 |
apply(erule conjE)+
|
304dfe6cc83a
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
105 |
apply(erule Abs_lst1_fcb)
|
304dfe6cc83a
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
106 |
apply(simp add: Abs_fresh_iff)
|
304dfe6cc83a
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
107 |
apply(simp add: Abs_fresh_iff)
|
304dfe6cc83a
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
108 |
apply(erule fresh_eqvt_at)
|
304dfe6cc83a
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
109 |
apply(simp add: finite_supp)
|
304dfe6cc83a
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
110 |
apply(simp add: fresh_Pair fresh_at_base(1))
|
304dfe6cc83a
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
111 |
apply(drule sym)
|
304dfe6cc83a
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
112 |
apply(drule sym)
|
304dfe6cc83a
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
113 |
apply(drule sym)
|
304dfe6cc83a
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
114 |
apply(drule sym)
|
304dfe6cc83a
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
115 |
apply(simp add: eqvt_at_def swap_fresh_fresh)
|
2889
|
116 |
oops
|
1792
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
117 |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
118 |
end
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
119 |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
120 |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
121 |
|