author | urbanc |
Tue, 06 Mar 2007 15:28:22 +0100 | |
changeset 22418 | 49e2d9744ae1 |
parent 22271 | 51a80e238b29 |
child 22541 | c33b542394f3 |
permissions | -rw-r--r-- |
21087 | 1 |
(* $Id$ *) |
20606
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
2 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
3 |
(* A challenge suggested by Adam Chlipala *) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
4 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
5 |
theory Compile |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
6 |
imports "../Nominal" |
20606
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
7 |
begin |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
8 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
9 |
atom_decl name |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
10 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
11 |
nominal_datatype data = DNat |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
12 |
| DProd "data" "data" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
13 |
| DSum "data" "data" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
14 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
15 |
nominal_datatype ty = Data "data" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
16 |
| Arrow "ty" "ty" ("_\<rightarrow>_" [100,100] 100) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
17 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
18 |
nominal_datatype trm = Var "name" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
19 |
| Lam "\<guillemotleft>name\<guillemotright>trm" ("Lam [_]._" [100,100] 100) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
20 |
| App "trm" "trm" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
21 |
| Const "nat" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
22 |
| Pr "trm" "trm" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
23 |
| Fst "trm" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
24 |
| Snd "trm" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
25 |
| InL "trm" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
26 |
| InR "trm" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
27 |
| Case "trm" "\<guillemotleft>name\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
28 |
("Case _ of inl _ \<rightarrow> _ | inr _ \<rightarrow> _" [100,100,100,100,100] 100) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
29 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
30 |
nominal_datatype dataI = OneI | NatI |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
31 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
32 |
nominal_datatype tyI = DataI "dataI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
33 |
| ArrowI "tyI" "tyI" ("_\<rightarrow>_" [100,100] 100) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
34 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
35 |
nominal_datatype trmI = IVar "name" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
36 |
| ILam "\<guillemotleft>name\<guillemotright>trmI" ("ILam [_]._" [100,100] 100) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
37 |
| IApp "trmI" "trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
38 |
| IUnit |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
39 |
| INat "nat" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
40 |
| ISucc "trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
41 |
| IAss "trmI" "trmI" ("_\<mapsto>_" [100,100] 100) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
42 |
| IRef "trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
43 |
| ISeq "trmI" "trmI" ("_;;_" [100,100] 100) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
44 |
| Iif "trmI" "trmI" "trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
45 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
46 |
text {* valid contexts *} |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
47 |
|
22271 | 48 |
inductive2 valid :: "(name\<times>'a::pt_name) list \<Rightarrow> bool" |
49 |
where |
|
50 |
v1[intro]: "valid []" |
|
51 |
| v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)" (* maybe dom of \<Gamma> *) |
|
20606
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
52 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
53 |
text {* typing judgements for trms *} |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
54 |
|
22271 | 55 |
inductive2 typing :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80) |
56 |
where |
|
57 |
t0[intro]: "\<lbrakk>valid \<Gamma>; (x,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var x : \<tau>" |
|
58 |
| t1[intro]: "\<lbrakk>\<Gamma> \<turnstile> e1 : \<tau>1\<rightarrow>\<tau>2; \<Gamma> \<turnstile> e2 : \<tau>1\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App e1 e2 : \<tau>2" |
|
59 |
| t2[intro]: "\<lbrakk>x\<sharp>\<Gamma>;((x,\<tau>1)#\<Gamma>) \<turnstile> t : \<tau>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : \<tau>1\<rightarrow>\<tau>2" |
|
60 |
| t3[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n : Data(DNat)" |
|
61 |
| t4[intro]: "\<lbrakk>\<Gamma> \<turnstile> e1 : Data(\<sigma>1); \<Gamma> \<turnstile> e2 : Data(\<sigma>2)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Pr e1 e2 : Data (DProd \<sigma>1 \<sigma>2)" |
|
62 |
| t5[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(DProd \<sigma>1 \<sigma>2)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Fst e : Data(\<sigma>1)" |
|
63 |
| t6[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(DProd \<sigma>1 \<sigma>2)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Snd e : Data(\<sigma>2)" |
|
64 |
| t7[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(\<sigma>1)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> InL e : Data(DSum \<sigma>1 \<sigma>2)" |
|
65 |
| t8[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(\<sigma>2)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> InR e : Data(DSum \<sigma>1 \<sigma>2)" |
|
66 |
| t9[intro]: "\<lbrakk>x1\<sharp>\<Gamma>; x2\<sharp>\<Gamma>; \<Gamma> \<turnstile> e: Data(DSum \<sigma>1 \<sigma>2); |
|
20606
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
67 |
((x1,Data(\<sigma>1))#\<Gamma>) \<turnstile> e1 : \<tau>; ((x2,Data(\<sigma>2))#\<Gamma>) \<turnstile> e2 : \<tau>\<rbrakk> |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
68 |
\<Longrightarrow> \<Gamma> \<turnstile> (Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2) : \<tau>" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
69 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
70 |
text {* typing judgements for Itrms *} |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
71 |
|
22271 | 72 |
inductive2 Ityping :: "(name\<times>tyI) list\<Rightarrow>trmI\<Rightarrow>tyI\<Rightarrow>bool" (" _ I\<turnstile> _ : _ " [80,80,80] 80) |
73 |
where |
|
74 |
t0[intro]: "\<lbrakk>valid \<Gamma>; (x,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> I\<turnstile> IVar x : \<tau>" |
|
75 |
| t1[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e1 : \<tau>1\<rightarrow>\<tau>2; \<Gamma> I\<turnstile> e2 : \<tau>1\<rbrakk>\<Longrightarrow> \<Gamma> I\<turnstile> IApp e1 e2 : \<tau>2" |
|
76 |
| t2[intro]: "\<lbrakk>x\<sharp>\<Gamma>;((x,\<tau>1)#\<Gamma>) I\<turnstile> t : \<tau>2\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> ILam [x].t : \<tau>1\<rightarrow>\<tau>2" |
|
77 |
| t3[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> I\<turnstile> IUnit : DataI(OneI)" |
|
78 |
| t4[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> I\<turnstile> INat(n) : DataI(NatI)" |
|
79 |
| t5[intro]: "\<Gamma> I\<turnstile> e : DataI(NatI) \<Longrightarrow> \<Gamma> I\<turnstile> ISucc(e) : DataI(NatI)" |
|
80 |
| t6[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e : DataI(NatI)\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> IRef e : DataI (NatI)" |
|
81 |
| t7[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e1 : DataI(NatI); \<Gamma> I\<turnstile> e2 : DataI(NatI)\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> e1\<mapsto>e2 : DataI(OneI)" |
|
82 |
| t8[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e1 : DataI(NatI); \<Gamma> I\<turnstile> e2 : \<tau>\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> e1;;e2 : \<tau>" |
|
83 |
| t9[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e: DataI(NatI); \<Gamma> I\<turnstile> e1 : \<tau>; \<Gamma> I\<turnstile> e2 : \<tau>\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> Iif e e1 e2 : \<tau>" |
|
20606
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
84 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
85 |
text {* capture-avoiding substitution *} |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
86 |
|
21543 | 87 |
consts |
88 |
subst :: "'a \<Rightarrow> name \<Rightarrow> 'a \<Rightarrow> 'a" ("_[_::=_]" [100,100,100] 100) |
|
20606
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
89 |
|
21543 | 90 |
nominal_primrec |
91 |
"(Var x)[y::=t'] = (if x=y then t' else (Var x))" |
|
92 |
"(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])" |
|
93 |
"\<lbrakk>x\<sharp>y; x\<sharp>t'\<rbrakk> \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])" |
|
94 |
"(Const n)[y::=t'] = Const n" |
|
95 |
"(Pr e1 e2)[y::=t'] = Pr (e1[y::=t']) (e2[y::=t'])" |
|
96 |
"(Fst e)[y::=t'] = Fst (e[y::=t'])" |
|
97 |
"(Snd e)[y::=t'] = Snd (e[y::=t'])" |
|
98 |
"(InL e)[y::=t'] = InL (e[y::=t'])" |
|
99 |
"(InR e)[y::=t'] = InR (e[y::=t'])" |
|
100 |
"\<lbrakk>z\<noteq>x; x\<sharp>y; x\<sharp>e; x\<sharp>e2; z\<sharp>y; z\<sharp>e; z\<sharp>e1; x\<sharp>t'; z\<sharp>t'\<rbrakk> \<Longrightarrow> |
|
101 |
(Case e of inl x \<rightarrow> e1 | inr z \<rightarrow> e2)[y::=t'] = |
|
102 |
(Case (e[y::=t']) of inl x \<rightarrow> (e1[y::=t']) | inr z \<rightarrow> (e2[y::=t']))" |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
103 |
apply(finite_guess)+ |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
104 |
apply(rule TrueI)+ |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
105 |
apply(simp add: abs_fresh)+ |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
106 |
apply(fresh_guess)+ |
21543 | 107 |
done |
20606
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
108 |
|
21543 | 109 |
nominal_primrec (Isubst) |
110 |
"(IVar x)[y::=t'] = (if x=y then t' else (IVar x))" |
|
111 |
"(IApp t1 t2)[y::=t'] = IApp (t1[y::=t']) (t2[y::=t'])" |
|
112 |
"\<lbrakk>x\<sharp>y; x\<sharp>t'\<rbrakk> \<Longrightarrow> (ILam [x].t)[y::=t'] = ILam [x].(t[y::=t'])" |
|
113 |
"(INat n)[y::=t'] = INat n" |
|
114 |
"(IUnit)[y::=t'] = IUnit" |
|
115 |
"(ISucc e)[y::=t'] = ISucc (e[y::=t'])" |
|
116 |
"(IAss e1 e2)[y::=t'] = IAss (e1[y::=t']) (e2[y::=t'])" |
|
117 |
"(IRef e)[y::=t'] = IRef (e[y::=t'])" |
|
118 |
"(ISeq e1 e2)[y::=t'] = ISeq (e1[y::=t']) (e2[y::=t'])" |
|
119 |
"(Iif e e1 e2)[y::=t'] = Iif (e[y::=t']) (e1[y::=t']) (e2[y::=t'])" |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
120 |
apply(finite_guess)+ |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
121 |
apply(rule TrueI)+ |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
122 |
apply(simp add: abs_fresh)+ |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
123 |
apply(fresh_guess)+ |
21543 | 124 |
done |
20606
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
125 |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
126 |
lemma Isubst_eqvt[eqvt]: |
20606
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
127 |
fixes pi::"name prm" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
128 |
and t1::"trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
129 |
and t2::"trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
130 |
and x::"name" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
131 |
shows "pi\<bullet>(t1[x::=t2]) = ((pi\<bullet>t1)[(pi\<bullet>x)::=(pi\<bullet>t2)])" |
21543 | 132 |
apply (nominal_induct t1 avoiding: x t2 rule: trmI.induct) |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
133 |
apply (simp_all add: Isubst.simps eqvt fresh_bij) |
20606
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
134 |
done |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
135 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
136 |
lemma Isubst_supp: |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
137 |
fixes t1::"trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
138 |
and t2::"trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
139 |
and x::"name" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
140 |
shows "((supp (t1[x::=t2]))::name set) \<subseteq> (supp t2)\<union>((supp t1)-{x})" |
21543 | 141 |
apply (nominal_induct t1 avoiding: x t2 rule: trmI.induct) |
142 |
apply (auto simp add: Isubst.simps trmI.supp supp_atm abs_supp supp_nat) |
|
143 |
apply blast+ |
|
144 |
done |
|
20606
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
145 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
146 |
lemma Isubst_fresh: |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
147 |
fixes x::"name" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
148 |
and y::"name" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
149 |
and t1::"trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
150 |
and t2::"trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
151 |
assumes a: "x\<sharp>[y].t1" "x\<sharp>t2" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
152 |
shows "x\<sharp>(t1[y::=t2])" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
153 |
using a |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
154 |
apply(auto simp add: fresh_def Isubst_supp) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
155 |
apply(drule rev_subsetD) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
156 |
apply(rule Isubst_supp) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
157 |
apply(simp add: abs_supp) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
158 |
done |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
159 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
160 |
text {* big-step evaluation for trms *} |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
161 |
|
22271 | 162 |
inductive2 big :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<Down> _" [80,80] 80) |
163 |
where |
|
164 |
b0[intro]: "Lam [x].e \<Down> Lam [x].e" |
|
165 |
| b1[intro]: "\<lbrakk>e1\<Down>Lam [x].e; e2\<Down>e2'; e[x::=e2']\<Down>e'\<rbrakk> \<Longrightarrow> App e1 e2 \<Down> e'" |
|
166 |
| b2[intro]: "Const n \<Down> Const n" |
|
167 |
| b3[intro]: "\<lbrakk>e1\<Down>e1'; e2\<Down>e2'\<rbrakk> \<Longrightarrow> Pr e1 e2 \<Down> Pr e1' e2'" |
|
168 |
| b4[intro]: "e\<Down>Pr e1 e2 \<Longrightarrow> Fst e\<Down>e1" |
|
169 |
| b5[intro]: "e\<Down>Pr e1 e2 \<Longrightarrow> Snd e\<Down>e2" |
|
170 |
| b6[intro]: "e\<Down>e' \<Longrightarrow> InL e \<Down> InL e'" |
|
171 |
| b7[intro]: "e\<Down>e' \<Longrightarrow> InR e \<Down> InR e'" |
|
172 |
| b8[intro]: "\<lbrakk>e\<Down>InL e'; e1[x::=e']\<Down>e''\<rbrakk> \<Longrightarrow> Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2 \<Down> e''" |
|
173 |
| b9[intro]: "\<lbrakk>e\<Down>InR e'; e2[x::=e']\<Down>e''\<rbrakk> \<Longrightarrow> Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2 \<Down> e''" |
|
20606
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
174 |
|
22271 | 175 |
inductive2 Ibig :: "((nat\<Rightarrow>nat)\<times>trmI)\<Rightarrow>((nat\<Rightarrow>nat)\<times>trmI)\<Rightarrow>bool" ("_ I\<Down> _" [80,80] 80) |
176 |
where |
|
177 |
m0[intro]: "(m,ILam [x].e) I\<Down> (m,ILam [x].e)" |
|
178 |
| m1[intro]: "\<lbrakk>(m,e1)I\<Down>(m',ILam [x].e); (m',e2)I\<Down>(m'',e3); (m'',e[x::=e3])I\<Down>(m''',e4)\<rbrakk> |
|
20606
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
179 |
\<Longrightarrow> (m,IApp e1 e2) I\<Down> (m''',e4)" |
22271 | 180 |
| m2[intro]: "(m,IUnit) I\<Down> (m,IUnit)" |
181 |
| m3[intro]: "(m,INat(n))I\<Down>(m,INat(n))" |
|
182 |
| m4[intro]: "(m,e)I\<Down>(m',INat(n)) \<Longrightarrow> (m,ISucc(e))I\<Down>(m',INat(n+1))" |
|
183 |
| m5[intro]: "(m,e)I\<Down>(m',INat(n)) \<Longrightarrow> (m,IRef(e))I\<Down>(m',INat(m' n))" |
|
184 |
| m6[intro]: "\<lbrakk>(m,e1)I\<Down>(m',INat(n1)); (m',e2)I\<Down>(m'',INat(n2))\<rbrakk> \<Longrightarrow> (m,e1\<mapsto>e2)I\<Down>(m''(n1:=n2),IUnit)" |
|
185 |
| m7[intro]: "\<lbrakk>(m,e1)I\<Down>(m',IUnit); (m',e2)I\<Down>(m'',e)\<rbrakk> \<Longrightarrow> (m,e1;;e2)I\<Down>(m'',e)" |
|
186 |
| m8[intro]: "\<lbrakk>(m,e)I\<Down>(m',INat(n)); n\<noteq>0; (m',e1)I\<Down>(m'',e)\<rbrakk> \<Longrightarrow> (m,Iif e e1 e2)I\<Down>(m'',e)" |
|
187 |
| m9[intro]: "\<lbrakk>(m,e)I\<Down>(m',INat(0)); (m',e2)I\<Down>(m'',e)\<rbrakk> \<Longrightarrow> (m,Iif e e1 e2)I\<Down>(m'',e)" |
|
20606
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
188 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
189 |
text {* Translation functions *} |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
190 |
|
21543 | 191 |
consts trans :: "trm \<Rightarrow> trmI" |
20606
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
192 |
|
21543 | 193 |
nominal_primrec |
194 |
"trans (Var x) = (IVar x)" |
|
195 |
"trans (App e1 e2) = IApp (trans e1) (trans e2)" |
|
196 |
"trans (Lam [x].e) = ILam [x].(trans e)" |
|
197 |
"trans (Const n) = INat n" |
|
198 |
"trans (Pr e1 e2) = |
|
199 |
(let limit = IRef(INat 0) in |
|
200 |
let v1 = (trans e1) in |
|
201 |
let v2 = (trans e2) in |
|
202 |
(((ISucc limit)\<mapsto>v1);;(ISucc(ISucc limit)\<mapsto>v2));;(INat 0 \<mapsto> ISucc(ISucc(limit))))" |
|
203 |
"trans (Fst e) = IRef (ISucc (trans e))" |
|
204 |
"trans (Snd e) = IRef (ISucc (ISucc (trans e)))" |
|
205 |
"trans (InL e) = |
|
206 |
(let limit = IRef(INat 0) in |
|
207 |
let v = (trans e) in |
|
208 |
(((ISucc limit)\<mapsto>INat(0));;(ISucc(ISucc limit)\<mapsto>v));;(INat 0 \<mapsto> ISucc(ISucc(limit))))" |
|
209 |
"trans (InR e) = |
|
210 |
(let limit = IRef(INat 0) in |
|
211 |
let v = (trans e) in |
|
212 |
(((ISucc limit)\<mapsto>INat(1));;(ISucc(ISucc limit)\<mapsto>v));;(INat 0 \<mapsto> ISucc(ISucc(limit))))" |
|
213 |
"\<lbrakk>x2\<noteq>x1; x1\<sharp>e; x1\<sharp>e2; x2\<sharp>e; x2\<sharp>e1\<rbrakk> \<Longrightarrow> |
|
214 |
trans (Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2) = |
|
215 |
(let v = (trans e) in |
|
216 |
let v1 = (trans e1) in |
|
217 |
let v2 = (trans e2) in |
|
218 |
Iif (IRef (ISucc v)) (v2[x2::=IRef (ISucc (ISucc v))]) (v1[x1::=IRef (ISucc (ISucc v))]))" |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
219 |
apply(finite_guess add: Let_def)+ |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
220 |
apply(rule TrueI)+ |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
221 |
apply(simp add: abs_fresh Isubst_fresh)+ |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
222 |
apply(fresh_guess add: Let_def)+ |
21543 | 223 |
done |
20606
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
224 |
|
21543 | 225 |
consts trans_type :: "ty \<Rightarrow> tyI" |
226 |
||
227 |
nominal_primrec |
|
228 |
"trans_type (Data \<sigma>) = DataI(NatI)" |
|
229 |
"trans_type (\<tau>1\<rightarrow>\<tau>2) = (trans_type \<tau>1)\<rightarrow>(trans_type \<tau>2)" |
|
230 |
by (rule TrueI)+ |
|
20606
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
231 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
232 |
end |