author | urbanc |
Tue, 19 Sep 2006 15:31:25 +0200 | |
changeset 20606 | fd9b0b78a7d3 |
child 20955 | 65a9a30b8ece |
permissions | -rw-r--r-- |
20606
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
1 |
(* $Id: *) |
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 |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
6 |
imports "Nominal" |
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 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
48 |
consts |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
49 |
ctxts :: "((name\<times>'a::pt_name) list) set" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
50 |
valid :: "(name\<times>'a::pt_name) list \<Rightarrow> bool" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
51 |
translations |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
52 |
"valid \<Gamma>" \<rightleftharpoons> "\<Gamma> \<in> ctxts" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
53 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
54 |
inductive ctxts |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
55 |
intros |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
56 |
v1[intro]: "valid []" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
57 |
v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
58 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
59 |
text {* typing judgements for trms *} |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
60 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
61 |
consts |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
62 |
typing :: "(((name\<times>ty) list)\<times>trm\<times>ty) set" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
63 |
syntax |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
64 |
"_typing_judge" :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
65 |
translations |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
66 |
"\<Gamma> \<turnstile> t : \<tau>" \<rightleftharpoons> "(\<Gamma>,t,\<tau>) \<in> typing" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
67 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
68 |
inductive typing |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
69 |
intros |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
70 |
t0[intro]: "\<lbrakk>valid \<Gamma>; (x,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var x : \<tau>" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
71 |
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" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
72 |
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" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
73 |
t3[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n : Data(DNat)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
74 |
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)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
75 |
t5[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(DProd \<sigma>1 \<sigma>2)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Fst e : Data(\<sigma>1)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
76 |
t6[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(DProd \<sigma>1 \<sigma>2)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Snd e : Data(\<sigma>2)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
77 |
t7[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(\<sigma>1)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> InL e : Data(DSum \<sigma>1 \<sigma>2)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
78 |
t8[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(\<sigma>2)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> InR e : Data(DSum \<sigma>1 \<sigma>2)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
79 |
t9[intro]: "\<lbrakk>x1\<sharp>\<Gamma>; x2\<sharp>\<Gamma>; \<Gamma> \<turnstile> e: Data(DSum \<sigma>1 \<sigma>2); |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
80 |
((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
|
81 |
\<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
|
82 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
83 |
text {* typing judgements for Itrms *} |
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 |
consts |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
86 |
Ityping :: "(((name\<times>tyI) list)\<times>trmI\<times>tyI) set" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
87 |
syntax |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
88 |
"_typing_judge" :: "(name\<times>tyI) list\<Rightarrow>trmI\<Rightarrow>tyI\<Rightarrow>bool" (" _ I\<turnstile> _ : _ " [80,80,80] 80) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
89 |
translations |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
90 |
"\<Gamma> I\<turnstile> t : \<tau>" \<rightleftharpoons> "(\<Gamma>,t,\<tau>) \<in> Ityping" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
91 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
92 |
inductive Ityping |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
93 |
intros |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
94 |
t0[intro]: "\<lbrakk>valid \<Gamma>; (x,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> I\<turnstile> IVar x : \<tau>" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
95 |
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" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
96 |
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" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
97 |
t3[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> I\<turnstile> IUnit : DataI(OneI)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
98 |
t4[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> I\<turnstile> INat(n) : DataI(NatI)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
99 |
t5[intro]: "\<Gamma> I\<turnstile> e : DataI(NatI) \<Longrightarrow> \<Gamma> I\<turnstile> ISucc(e) : DataI(NatI)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
100 |
t6[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e : DataI(NatI)\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> IRef e : DataI (NatI)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
101 |
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)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
102 |
t8[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e1 : DataI(NatI); \<Gamma> I\<turnstile> e2 : \<tau>\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> e1;;e2 : \<tau>" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
103 |
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>" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
104 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
105 |
text {* capture-avoiding substitution *} |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
106 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
107 |
consts |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
108 |
subst :: "'a \<Rightarrow> name \<Rightarrow> 'a \<Rightarrow> 'a" ("_[_::=_]" [100,100,100] 100) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
109 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
110 |
constdefs |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
111 |
subst_Var :: "name \<Rightarrow> trm \<Rightarrow> name \<Rightarrow> trm" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
112 |
"subst_Var x t' \<equiv> \<lambda>y. (if y=x then t' else (Var y))" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
113 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
114 |
subst_App :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
115 |
"subst_App x t' \<equiv> \<lambda>_ _ r1 r2. App r1 r2" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
116 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
117 |
subst_Lam :: "name \<Rightarrow> trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
118 |
"subst_Lam x t' \<equiv> \<lambda>a _ r. Lam [a].r" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
119 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
120 |
subst_Const :: "name \<Rightarrow> trm \<Rightarrow> nat \<Rightarrow> trm" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
121 |
"subst_Const x t' \<equiv> \<lambda>n. Const n" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
122 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
123 |
subst_Pr :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
124 |
"subst_Pr x t' \<equiv> \<lambda>_ _ r1 r2. Pr r1 r2" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
125 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
126 |
subst_Fst :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
127 |
"subst_Fst x t' \<equiv> \<lambda>_ r. Fst r" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
128 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
129 |
subst_Snd :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
130 |
"subst_Snd x t' \<equiv> \<lambda>_ r. Snd r" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
131 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
132 |
subst_InL :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
133 |
"subst_InL x t' \<equiv> \<lambda>_ r. InL r" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
134 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
135 |
subst_InR :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
136 |
"subst_InR x t' \<equiv> \<lambda>_ r. InR r" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
137 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
138 |
subst_Case :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
139 |
"subst_Case x t' \<equiv> \<lambda>_ x _ y _ r r1 r2. Case r of inl x \<rightarrow> r1 | inr y \<rightarrow> r2" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
140 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
141 |
defs(overloaded) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
142 |
subst_def: |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
143 |
"t[x::=t'] \<equiv> trm_rec (subst_Var x t') (subst_Lam x t') (subst_App x t') |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
144 |
(subst_Const x t') (subst_Pr x t') (subst_Fst x t') (subst_Snd x t') |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
145 |
(subst_InL x t') (subst_InR x t') (subst_Case x t') t" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
146 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
147 |
(* FIXME: the next two lemmas need to be in Nominal.thy *) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
148 |
lemma perm_if: |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
149 |
fixes pi::"'a prm" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
150 |
shows "pi\<bullet>(if b then c1 else c2) = (if (pi\<bullet>b) then (pi\<bullet>c1) else (pi\<bullet>c2))" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
151 |
apply(simp add: perm_fun_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
152 |
done |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
153 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
154 |
lemma eq_eqvt: |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
155 |
fixes pi::"name prm" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
156 |
and x::"'a::pt_name" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
157 |
shows "pi\<bullet>(x=y) = ((pi\<bullet>x)=(pi\<bullet>y))" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
158 |
apply(simp add: perm_bool perm_bij) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
159 |
done |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
160 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
161 |
lemma fin_supp_subst: |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
162 |
shows "finite ((supp (subst_Var x t))::name set)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
163 |
and "finite ((supp (subst_Lam x t))::name set)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
164 |
and "finite ((supp (subst_App x t))::name set)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
165 |
and "finite ((supp (subst_Const x t))::name set)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
166 |
and "finite ((supp (subst_Pr x t))::name set)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
167 |
and "finite ((supp (subst_Fst x t))::name set)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
168 |
and "finite ((supp (subst_Snd x t))::name set)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
169 |
and "finite ((supp (subst_InL x t))::name set)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
170 |
and "finite ((supp (subst_InR x t))::name set)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
171 |
and "finite ((supp (subst_Case x t))::name set)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
172 |
apply - |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
173 |
apply(finite_guess add: fs_name1 subst_Var_def perm_if eq_eqvt) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
174 |
apply(finite_guess add: fs_name1 subst_Lam_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
175 |
apply(finite_guess add: fs_name1 subst_App_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
176 |
apply(finite_guess add: fs_name1 subst_Const_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
177 |
apply(finite_guess add: fs_name1 subst_Pr_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
178 |
apply(finite_guess add: fs_name1 subst_Fst_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
179 |
apply(finite_guess add: fs_name1 subst_Snd_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
180 |
apply(finite_guess add: fs_name1 subst_InL_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
181 |
apply(finite_guess add: fs_name1 subst_InR_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
182 |
apply(finite_guess only: fs_name1 subst_Case_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
183 |
apply(perm_simp) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
184 |
apply(simp) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
185 |
done |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
186 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
187 |
lemma fcb_subst_Lam: |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
188 |
shows "x\<sharp>(subst_Lam y t') x t r" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
189 |
by (simp add: subst_Lam_def abs_fresh) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
190 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
191 |
lemma fcb_subst_Case: |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
192 |
assumes a: "x\<sharp>r" "x\<sharp>r2" "y\<sharp>r" "y\<sharp>r1" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
193 |
shows "x\<sharp>(subst_Case z t') e x e1 y e2 r r1 r2 \<and> y\<sharp>(subst_Case z t') e x e1 y e2 r r1 r2" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
194 |
using a |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
195 |
by (simp add: subst_Case_def abs_fresh) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
196 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
197 |
lemma subst: |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
198 |
shows "(Var x)[y::=t'] = (if x=y then t' else (Var x))" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
199 |
and "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
200 |
and "\<lbrakk>x\<sharp>y; x\<sharp>t'\<rbrakk> \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
201 |
and "(Const n)[y::=t'] = Const n" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
202 |
and "(Pr e1 e2)[y::=t'] = Pr (e1[y::=t']) (e2[y::=t'])" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
203 |
and "(Fst e)[y::=t'] = Fst (e[y::=t'])" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
204 |
and "(Snd e)[y::=t'] = Snd (e[y::=t'])" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
205 |
and "(InL e)[y::=t'] = InL (e[y::=t'])" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
206 |
and "(InR e)[y::=t'] = InR (e[y::=t'])" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
207 |
and "\<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> |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
208 |
\<Longrightarrow> (Case e of inl x \<rightarrow> e1 | inr z \<rightarrow> e2)[y::=t'] = |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
209 |
(Case (e[y::=t']) of inl x \<rightarrow> (e1[y::=t']) | inr z \<rightarrow> (e2[y::=t']))" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
210 |
apply(unfold subst_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
211 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
212 |
apply(rule trm.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
213 |
apply(rule fin_supp_subst)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
214 |
apply(simp add: fcb_subst_Lam) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
215 |
apply(simp add: fcb_subst_Case) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
216 |
apply(simp add: subst_Var_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
217 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
218 |
apply(rule trm.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
219 |
apply(rule fin_supp_subst)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
220 |
apply(simp add: fcb_subst_Lam) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
221 |
apply(simp add: fcb_subst_Case) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
222 |
apply(simp add: subst_App_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
223 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
224 |
apply(rule trm.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
225 |
apply(rule fin_supp_subst)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
226 |
apply(simp add: fcb_subst_Lam) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
227 |
apply(simp add: fcb_subst_Case) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
228 |
apply(fresh_guess add: fs_name1 subst_Var_def perm_if eq_eqvt) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
229 |
apply(fresh_guess add: fs_name1 subst_Lam_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
230 |
apply(fresh_guess add: fs_name1 subst_App_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
231 |
apply(fresh_guess add: fs_name1 subst_Const_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
232 |
apply(fresh_guess add: fs_name1 subst_Pr_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
233 |
apply(fresh_guess add: fs_name1 subst_Fst_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
234 |
apply(fresh_guess add: fs_name1 subst_Snd_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
235 |
apply(fresh_guess add: fs_name1 subst_InL_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
236 |
apply(fresh_guess add: fs_name1 subst_InR_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
237 |
apply(fresh_guess only: fs_name1 subst_Case_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
238 |
apply(perm_simp) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
239 |
apply(simp, simp) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
240 |
apply(simp add: subst_Lam_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
241 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
242 |
apply(rule trm.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
243 |
apply(rule fin_supp_subst)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
244 |
apply(simp add: fcb_subst_Lam) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
245 |
apply(simp add: fcb_subst_Case) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
246 |
apply(simp add: subst_Const_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
247 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
248 |
apply(rule trm.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
249 |
apply(rule fin_supp_subst)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
250 |
apply(simp add: fcb_subst_Lam) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
251 |
apply(simp add: fcb_subst_Case) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
252 |
apply(simp add: subst_Pr_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
253 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
254 |
apply(rule trm.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
255 |
apply(rule fin_supp_subst)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
256 |
apply(simp add: fcb_subst_Lam) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
257 |
apply(simp add: fcb_subst_Case) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
258 |
apply(simp add: subst_Fst_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
259 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
260 |
apply(rule trm.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
261 |
apply(rule fin_supp_subst)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
262 |
apply(simp add: fcb_subst_Lam) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
263 |
apply(simp add: fcb_subst_Case) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
264 |
apply(simp add: subst_Snd_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
265 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
266 |
apply(rule trm.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
267 |
apply(rule fin_supp_subst)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
268 |
apply(simp add: fcb_subst_Lam) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
269 |
apply(simp add: fcb_subst_Case) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
270 |
apply(simp add: subst_InL_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
271 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
272 |
apply(rule trm.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
273 |
apply(rule fin_supp_subst)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
274 |
apply(simp add: fcb_subst_Lam) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
275 |
apply(simp add: fcb_subst_Case) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
276 |
apply(simp add: subst_InR_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
277 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
278 |
apply(rule trm.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
279 |
apply(rule fin_supp_subst)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
280 |
apply(simp add: fcb_subst_Lam) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
281 |
apply(simp add: fcb_subst_Case) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
282 |
apply(fresh_guess add: fs_name1 subst_Var_def perm_if eq_eqvt) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
283 |
apply(fresh_guess add: fs_name1 subst_Var_def perm_if eq_eqvt) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
284 |
apply(fresh_guess add: fs_name1 subst_Lam_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
285 |
apply(fresh_guess add: fs_name1 subst_Lam_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
286 |
apply(fresh_guess add: fs_name1 subst_App_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
287 |
apply(fresh_guess add: fs_name1 subst_App_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
288 |
apply(fresh_guess add: fs_name1 subst_Const_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
289 |
apply(fresh_guess add: fs_name1 subst_Const_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
290 |
apply(fresh_guess add: fs_name1 subst_Pr_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
291 |
apply(fresh_guess add: fs_name1 subst_Pr_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
292 |
apply(fresh_guess add: fs_name1 subst_Fst_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
293 |
apply(fresh_guess add: fs_name1 subst_Fst_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
294 |
apply(fresh_guess add: fs_name1 subst_Snd_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
295 |
apply(fresh_guess add: fs_name1 subst_Snd_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
296 |
apply(fresh_guess add: fs_name1 subst_InL_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
297 |
apply(fresh_guess add: fs_name1 subst_InL_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
298 |
apply(fresh_guess add: fs_name1 subst_InR_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
299 |
apply(fresh_guess add: fs_name1 subst_InR_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
300 |
apply(fresh_guess only: fs_name1 subst_Case_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
301 |
apply(perm_simp) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
302 |
apply(simp, simp) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
303 |
apply(fresh_guess only: fs_name1 subst_Case_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
304 |
apply(perm_simp) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
305 |
apply(simp, simp) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
306 |
apply(assumption)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
307 |
apply(simp add: subst_Case_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
308 |
done |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
309 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
310 |
constdefs |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
311 |
subst_IVar :: "name \<Rightarrow> trmI \<Rightarrow> name \<Rightarrow> trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
312 |
"subst_IVar x t' \<equiv> \<lambda>y. (if y=x then t' else (IVar y))" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
313 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
314 |
subst_IApp :: "name \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
315 |
"subst_IApp x t' \<equiv> \<lambda>_ _ r1 r2. IApp r1 r2" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
316 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
317 |
subst_ILam :: "name \<Rightarrow> trmI \<Rightarrow> name \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
318 |
"subst_ILam x t' \<equiv> \<lambda>a _ r. ILam [a].r" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
319 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
320 |
subst_IUnit :: "name \<Rightarrow> trmI \<Rightarrow> trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
321 |
"subst_IUnit x t' \<equiv> IUnit" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
322 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
323 |
subst_INat :: "name \<Rightarrow> trmI \<Rightarrow> nat \<Rightarrow> trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
324 |
"subst_INat x t' \<equiv> \<lambda>n. INat n" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
325 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
326 |
subst_ISucc :: "name \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
327 |
"subst_ISucc x t' \<equiv> \<lambda>_ r. ISucc r" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
328 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
329 |
subst_IAss :: "name \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
330 |
"subst_IAss x t' \<equiv> \<lambda>_ _ r1 r2. r1\<mapsto>r2" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
331 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
332 |
subst_IRef :: "name \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
333 |
"subst_IRef x t' \<equiv> \<lambda>_ r. IRef r" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
334 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
335 |
subst_ISeq :: "name \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
336 |
"subst_ISeq x t' \<equiv> \<lambda>_ _ r1 r2. ISeq r1 r2" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
337 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
338 |
subst_Iif :: "name \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
339 |
"subst_Iif x t' \<equiv> \<lambda>_ _ _ r r1 r2. Iif r r1 r2" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
340 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
341 |
defs(overloaded) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
342 |
subst_trmI_def: |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
343 |
"t[x::=t'] \<equiv> trmI_rec (subst_IVar x t') (subst_ILam x t') (subst_IApp x t') |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
344 |
(subst_IUnit x t') (subst_INat x t') (subst_ISucc x t') (subst_IAss x t') |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
345 |
(subst_IRef x t') (subst_ISeq x t') (subst_Iif x t') t" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
346 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
347 |
lemma fin_supp_Isubst: |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
348 |
shows "finite ((supp (subst_IVar x t))::name set)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
349 |
and "finite ((supp (subst_ILam x t))::name set)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
350 |
and "finite ((supp (subst_IApp x t))::name set)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
351 |
and "finite ((supp (subst_INat x t))::name set)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
352 |
and "finite ((supp (subst_IUnit x t))::name set)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
353 |
and "finite ((supp (subst_ISucc x t))::name set)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
354 |
and "finite ((supp (subst_IAss x t))::name set)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
355 |
and "finite ((supp (subst_IRef x t))::name set)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
356 |
and "finite ((supp (subst_ISeq x t))::name set)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
357 |
and "finite ((supp (subst_Iif x t))::name set)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
358 |
apply - |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
359 |
apply(finite_guess add: fs_name1 subst_IVar_def perm_if eq_eqvt) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
360 |
apply(finite_guess add: fs_name1 subst_ILam_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
361 |
apply(finite_guess add: fs_name1 subst_IApp_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
362 |
apply(finite_guess add: fs_name1 subst_INat_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
363 |
apply(finite_guess add: fs_name1 subst_IUnit_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
364 |
apply(finite_guess add: fs_name1 subst_ISucc_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
365 |
apply(finite_guess add: fs_name1 subst_IAss_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
366 |
apply(finite_guess add: fs_name1 subst_IRef_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
367 |
apply(finite_guess add: fs_name1 subst_ISeq_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
368 |
apply(finite_guess only: fs_name1 subst_Iif_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
369 |
apply(perm_simp) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
370 |
apply(simp) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
371 |
done |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
372 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
373 |
lemma fcb_subst_ILam: |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
374 |
shows "x\<sharp>(subst_ILam y t') x t r" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
375 |
by (simp add: subst_ILam_def abs_fresh) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
376 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
377 |
lemma Isubst: |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
378 |
shows "(IVar x)[y::=t'] = (if x=y then t' else (IVar x))" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
379 |
and "(IApp t1 t2)[y::=t'] = IApp (t1[y::=t']) (t2[y::=t'])" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
380 |
and "\<lbrakk>x\<sharp>y; x\<sharp>t'\<rbrakk> \<Longrightarrow> (ILam [x].t)[y::=t'] = ILam [x].(t[y::=t'])" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
381 |
and "(INat n)[y::=t'] = INat n" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
382 |
and "(IUnit)[y::=t'] = IUnit" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
383 |
and "(ISucc e)[y::=t'] = ISucc (e[y::=t'])" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
384 |
and "(IAss e1 e2)[y::=t'] = IAss (e1[y::=t']) (e2[y::=t'])" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
385 |
and "(IRef e)[y::=t'] = IRef (e[y::=t'])" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
386 |
and "(ISeq e1 e2)[y::=t'] = ISeq (e1[y::=t']) (e2[y::=t'])" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
387 |
and "(Iif e e1 e2)[y::=t'] = Iif (e[y::=t']) (e1[y::=t']) (e2[y::=t'])" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
388 |
apply(unfold subst_trmI_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
389 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
390 |
apply(rule trmI.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
391 |
apply(rule fin_supp_Isubst)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
392 |
apply(simp add: fcb_subst_ILam) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
393 |
apply(simp add: subst_IVar_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
394 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
395 |
apply(rule trmI.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
396 |
apply(rule fin_supp_Isubst)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
397 |
apply(simp add: fcb_subst_ILam) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
398 |
apply(simp add: subst_IApp_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
399 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
400 |
apply(rule trmI.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
401 |
apply(rule fin_supp_Isubst)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
402 |
apply(simp add: fcb_subst_ILam) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
403 |
apply(fresh_guess add: fs_name1 subst_IVar_def perm_if eq_eqvt) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
404 |
apply(fresh_guess add: fs_name1 subst_ILam_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
405 |
apply(fresh_guess add: fs_name1 subst_IApp_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
406 |
apply(fresh_guess add: fs_name1 subst_IUnit_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
407 |
apply(fresh_guess add: fs_name1 subst_INat_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
408 |
apply(fresh_guess add: fs_name1 subst_ISucc_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
409 |
apply(fresh_guess add: fs_name1 subst_IAss_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
410 |
apply(fresh_guess add: fs_name1 subst_IRef_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
411 |
apply(fresh_guess add: fs_name1 subst_ISeq_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
412 |
apply(fresh_guess only: fs_name1 subst_Iif_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
413 |
apply(perm_simp) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
414 |
apply(simp, simp) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
415 |
apply(simp add: subst_ILam_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
416 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
417 |
apply(rule trmI.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
418 |
apply(rule fin_supp_Isubst)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
419 |
apply(simp add: fcb_subst_ILam) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
420 |
apply(simp add: subst_INat_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
421 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
422 |
apply(rule trmI.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
423 |
apply(rule fin_supp_Isubst)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
424 |
apply(simp add: fcb_subst_ILam) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
425 |
apply(simp add: subst_IUnit_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
426 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
427 |
apply(rule trmI.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
428 |
apply(rule fin_supp_Isubst)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
429 |
apply(simp add: fcb_subst_ILam) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
430 |
apply(simp add: subst_ISucc_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
431 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
432 |
apply(rule trmI.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
433 |
apply(rule fin_supp_Isubst)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
434 |
apply(simp add: fcb_subst_ILam) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
435 |
apply(simp add: subst_IAss_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
436 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
437 |
apply(rule trmI.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
438 |
apply(rule fin_supp_Isubst)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
439 |
apply(simp add: fcb_subst_ILam) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
440 |
apply(simp add: subst_IRef_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
441 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
442 |
apply(rule trmI.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
443 |
apply(rule fin_supp_Isubst)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
444 |
apply(simp add: fcb_subst_ILam) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
445 |
apply(simp add: subst_ISeq_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
446 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
447 |
apply(rule trmI.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
448 |
apply(rule fin_supp_Isubst)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
449 |
apply(simp add: fcb_subst_ILam) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
450 |
apply(simp add: subst_Iif_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
451 |
done |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
452 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
453 |
lemma Isubst_eqvt: |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
454 |
fixes pi::"name prm" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
455 |
and t1::"trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
456 |
and t2::"trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
457 |
and x::"name" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
458 |
shows "pi\<bullet>(t1[x::=t2]) = ((pi\<bullet>t1)[(pi\<bullet>x)::=(pi\<bullet>t2)])" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
459 |
apply(nominal_induct t1 avoiding: x t2 rule: trmI.induct) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
460 |
apply(simp_all add: Isubst perm_if eq_eqvt fresh_bij) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
461 |
done |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
462 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
463 |
lemma Isubst_supp: |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
464 |
fixes t1::"trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
465 |
and t2::"trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
466 |
and x::"name" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
467 |
shows "((supp (t1[x::=t2]))::name set) \<subseteq> (supp t2)\<union>((supp t1)-{x})" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
468 |
apply(nominal_induct t1 avoiding: x t2 rule: trmI.induct) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
469 |
apply(auto simp add: Isubst trmI.supp supp_atm abs_supp supp_nat) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
470 |
apply(blast)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
471 |
done |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
472 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
473 |
lemma Isubst_fresh: |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
474 |
fixes x::"name" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
475 |
and y::"name" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
476 |
and t1::"trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
477 |
and t2::"trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
478 |
assumes a: "x\<sharp>[y].t1" "x\<sharp>t2" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
479 |
shows "x\<sharp>(t1[y::=t2])" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
480 |
using a |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
481 |
apply(auto simp add: fresh_def Isubst_supp) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
482 |
apply(drule rev_subsetD) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
483 |
apply(rule Isubst_supp) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
484 |
apply(simp add: abs_supp) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
485 |
done |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
486 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
487 |
text {* big-step evaluation for trms *} |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
488 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
489 |
consts |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
490 |
big :: "(trm\<times>trm) set" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
491 |
syntax |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
492 |
"_big_judge" :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<Down> _" [80,80] 80) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
493 |
translations |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
494 |
"e1 \<Down> e2" \<rightleftharpoons> "(e1,e2) \<in> big" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
495 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
496 |
inductive big |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
497 |
intros |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
498 |
b0[intro]: "Lam [x].e \<Down> Lam [x].e" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
499 |
b1[intro]: "\<lbrakk>e1\<Down>Lam [x].e; e2\<Down>e2'; e[x::=e2']\<Down>e'\<rbrakk> \<Longrightarrow> App e1 e2 \<Down> e'" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
500 |
b2[intro]: "Const n \<Down> Const n" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
501 |
b3[intro]: "\<lbrakk>e1\<Down>e1'; e2\<Down>e2'\<rbrakk> \<Longrightarrow> Pr e1 e2 \<Down> Pr e1' e2'" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
502 |
b4[intro]: "e\<Down>Pr e1 e2 \<Longrightarrow> Fst e\<Down>e1" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
503 |
b5[intro]: "e\<Down>Pr e1 e2 \<Longrightarrow> Snd e\<Down>e2" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
504 |
b6[intro]: "e\<Down>e' \<Longrightarrow> InL e \<Down> InL e'" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
505 |
b7[intro]: "e\<Down>e' \<Longrightarrow> InR e \<Down> InR e'" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
506 |
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''" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
507 |
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''" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
508 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
509 |
consts |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
510 |
Ibig :: "(((nat\<Rightarrow>nat)\<times>trmI)\<times>((nat\<Rightarrow>nat)\<times>trmI)) set" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
511 |
syntax |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
512 |
"_Ibig_judge" :: "((nat\<Rightarrow>nat)\<times>trmI)\<Rightarrow>((nat\<Rightarrow>nat)\<times>trmI)\<Rightarrow>bool" ("_ I\<Down> _" [80,80] 80) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
513 |
translations |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
514 |
"(m,e1) I\<Down> (m',e2)" \<rightleftharpoons> "((m,e1),(m',e2)) \<in> Ibig" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
515 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
516 |
inductive Ibig |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
517 |
intros |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
518 |
m0[intro]: "(m,ILam [x].e) I\<Down> (m,ILam [x].e)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
519 |
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> |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
520 |
\<Longrightarrow> (m,IApp e1 e2) I\<Down> (m''',e4)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
521 |
m2[intro]: "(m,IUnit) I\<Down> (m,IUnit)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
522 |
m3[intro]: "(m,INat(n))I\<Down>(m,INat(n))" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
523 |
m4[intro]: "(m,e)I\<Down>(m',INat(n)) \<Longrightarrow> (m,ISucc(e))I\<Down>(m',INat(n+1))" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
524 |
m5[intro]: "(m,e)I\<Down>(m',INat(n)) \<Longrightarrow> (m,IRef(e))I\<Down>(m',INat(m' n))" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
525 |
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)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
526 |
m7[intro]: "\<lbrakk>(m,e1)I\<Down>(m',IUnit); (m',e2)I\<Down>(m'',e)\<rbrakk> \<Longrightarrow> (m,e1;;e2)I\<Down>(m'',e)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
527 |
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)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
528 |
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)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
529 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
530 |
text {* Translation functions *} |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
531 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
532 |
constdefs |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
533 |
trans_data :: "data \<Rightarrow> tyI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
534 |
"trans_data \<equiv> \<lambda>_. DataI(NatI)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
535 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
536 |
trans_arrow :: "ty \<Rightarrow> ty \<Rightarrow> tyI \<Rightarrow> tyI \<Rightarrow> tyI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
537 |
"trans_arrow \<equiv> \<lambda>_ _ r1 r2. ArrowI r1 r2" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
538 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
539 |
trans_type::"ty \<Rightarrow> tyI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
540 |
"trans_type \<tau> \<equiv> ty_rec (trans_data) (trans_arrow) \<tau>" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
541 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
542 |
lemma trans_type: |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
543 |
shows "trans_type (Data \<sigma>) = DataI(NatI)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
544 |
and "trans_type (\<tau>1\<rightarrow>\<tau>2) = (trans_type \<tau>1)\<rightarrow>(trans_type \<tau>2)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
545 |
apply(unfold trans_type_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
546 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
547 |
apply(rule ty.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
548 |
apply(simp add: trans_data_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
549 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
550 |
apply(rule ty.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
551 |
apply(simp add: trans_arrow_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
552 |
done |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
553 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
554 |
constdefs |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
555 |
trans_Var :: "name \<Rightarrow> trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
556 |
"trans_Var \<equiv> \<lambda>x. IVar x" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
557 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
558 |
trans_App :: "trm \<Rightarrow> trm \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
559 |
"trans_App \<equiv> \<lambda>_ _ r1 r2. IApp r1 r2" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
560 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
561 |
trans_Lam :: "name \<Rightarrow> trm \<Rightarrow> trmI \<Rightarrow> trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
562 |
"trans_Lam \<equiv> \<lambda>a _ r. ILam [a].r" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
563 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
564 |
trans_Const :: "nat \<Rightarrow> trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
565 |
"trans_Const \<equiv> \<lambda>n. INat n" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
566 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
567 |
trans_Pr :: "trm \<Rightarrow> trm \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
568 |
"trans_Pr \<equiv> \<lambda>_ _ r1 r2. |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
569 |
let limit = IRef(INat 0) in |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
570 |
let v1 = r1 in |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
571 |
let v2 = r2 in |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
572 |
(((ISucc limit)\<mapsto>v1);;(ISucc(ISucc limit)\<mapsto>v2));;(INat 0 \<mapsto> ISucc(ISucc(limit)))" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
573 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
574 |
trans_Fst :: "trm \<Rightarrow> trmI \<Rightarrow> trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
575 |
"trans_Fst \<equiv> \<lambda>_ r. IRef (ISucc r)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
576 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
577 |
trans_Snd :: "trm \<Rightarrow> trmI \<Rightarrow> trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
578 |
"trans_Snd \<equiv> \<lambda>_ r. IRef (ISucc (ISucc r))" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
579 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
580 |
trans_InL :: "trm \<Rightarrow> trmI \<Rightarrow> trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
581 |
"trans_InL \<equiv> \<lambda>_ r. |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
582 |
let limit = IRef(INat 0) in |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
583 |
let v = r in |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
584 |
(((ISucc limit)\<mapsto>INat(0));;(ISucc(ISucc limit)\<mapsto>v));;(INat 0 \<mapsto> ISucc(ISucc(limit)))" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
585 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
586 |
trans_InR :: "trm \<Rightarrow> trmI \<Rightarrow> trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
587 |
"trans_InR \<equiv> \<lambda>_ r. |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
588 |
let limit = IRef(INat 0) in |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
589 |
let v = r in |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
590 |
(((ISucc limit)\<mapsto>INat(1));;(ISucc(ISucc limit)\<mapsto>v));;(INat 0 \<mapsto> ISucc(ISucc(limit)))" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
591 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
592 |
trans_Case :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
593 |
"trans_Case \<equiv> \<lambda>_ x1 _ x2 _ r r1 r2. |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
594 |
let v = r in |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
595 |
let v1 = r1 in |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
596 |
let v2 = r2 in |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
597 |
Iif (IRef (ISucc v)) (v2[x2::=IRef (ISucc (ISucc v))]) (v1[x1::=IRef (ISucc (ISucc v))])" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
598 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
599 |
trans :: "trm \<Rightarrow> trmI" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
600 |
"trans t \<equiv> trm_rec (trans_Var) (trans_Lam) (trans_App) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
601 |
(trans_Const) (trans_Pr) (trans_Fst) (trans_Snd) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
602 |
(trans_InL) (trans_InR) (trans_Case) t" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
603 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
604 |
lemma fin_supp_trans: |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
605 |
shows "finite ((supp (trans_Var))::name set)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
606 |
and "finite ((supp (trans_Lam))::name set)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
607 |
and "finite ((supp (trans_App))::name set)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
608 |
and "finite ((supp (trans_Const))::name set)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
609 |
and "finite ((supp (trans_Pr))::name set)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
610 |
and "finite ((supp (trans_Fst))::name set)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
611 |
and "finite ((supp (trans_Snd))::name set)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
612 |
and "finite ((supp (trans_InL))::name set)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
613 |
and "finite ((supp (trans_InR))::name set)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
614 |
and "finite ((supp (trans_Case))::name set)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
615 |
apply - |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
616 |
apply(finite_guess add: fs_name1 trans_Var_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
617 |
apply(finite_guess add: fs_name1 trans_Lam_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
618 |
apply(finite_guess add: fs_name1 trans_App_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
619 |
apply(finite_guess add: fs_name1 trans_Const_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
620 |
apply(finite_guess add: fs_name1 trans_Pr_def Let_def perm_nat_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
621 |
apply(finite_guess add: fs_name1 trans_Fst_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
622 |
apply(finite_guess add: fs_name1 trans_Snd_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
623 |
apply(finite_guess add: fs_name1 trans_InL_def Let_def perm_nat_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
624 |
apply(finite_guess add: fs_name1 trans_InR_def Let_def perm_nat_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
625 |
apply(finite_guess add: fs_name1 trans_Case_def Let_def Isubst_eqvt) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
626 |
done |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
627 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
628 |
lemma fcb_trans_Lam: |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
629 |
shows "x\<sharp>(trans_Lam) x t r" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
630 |
by (simp add: trans_Lam_def abs_fresh) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
631 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
632 |
lemma fcb_trans_Case: |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
633 |
assumes a: "x\<sharp>r" "x\<sharp>r2" "y\<sharp>r" "y\<sharp>r1" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
634 |
shows "x\<sharp>(trans_Case) e x e1 y e2 r r1 r2 \<and> y\<sharp>(trans_Case) e x e1 y e2 r r1 r2" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
635 |
using a |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
636 |
by (simp add: trans_Case_def abs_fresh Isubst_fresh) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
637 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
638 |
lemma trans: |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
639 |
shows "trans (Var x) = (IVar x)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
640 |
and "trans (App e1 e2) = IApp (trans e1) (trans e2)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
641 |
and "trans (Lam [x].e) = ILam [x].(trans e)" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
642 |
and "trans (Const n) = INat n" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
643 |
and "trans (Pr e1 e2) = |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
644 |
(let limit = IRef(INat 0) in |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
645 |
let v1 = (trans e1) in |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
646 |
let v2 = (trans e2) in |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
647 |
(((ISucc limit)\<mapsto>v1);;(ISucc(ISucc limit)\<mapsto>v2));;(INat 0 \<mapsto> ISucc(ISucc(limit))))" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
648 |
and "trans (Fst e) = IRef (ISucc (trans e))" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
649 |
and "trans (Snd e) = IRef (ISucc (ISucc (trans e)))" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
650 |
and "trans (InL e) = |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
651 |
(let limit = IRef(INat 0) in |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
652 |
let v = (trans e) in |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
653 |
(((ISucc limit)\<mapsto>INat(0));;(ISucc(ISucc limit)\<mapsto>v));;(INat 0 \<mapsto> ISucc(ISucc(limit))))" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
654 |
and "trans (InR e) = |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
655 |
(let limit = IRef(INat 0) in |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
656 |
let v = (trans e) in |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
657 |
(((ISucc limit)\<mapsto>INat(1));;(ISucc(ISucc limit)\<mapsto>v));;(INat 0 \<mapsto> ISucc(ISucc(limit))))" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
658 |
and "\<lbrakk>x2\<noteq>x1; x1\<sharp>e; x1\<sharp>e2; x2\<sharp>e; x2\<sharp>e1\<rbrakk> \<Longrightarrow> |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
659 |
trans (Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2) = |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
660 |
(let v = (trans e) in |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
661 |
let v1 = (trans e1) in |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
662 |
let v2 = (trans e2) in |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
663 |
Iif (IRef (ISucc v)) (v2[x2::=IRef (ISucc (ISucc v))]) (v1[x1::=IRef (ISucc (ISucc v))]))" |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
664 |
apply(unfold trans_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
665 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
666 |
apply(rule trm.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
667 |
apply(rule fin_supp_trans)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
668 |
apply(simp add: fcb_trans_Lam) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
669 |
apply(simp add: fcb_trans_Case) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
670 |
apply(simp add: trans_Var_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
671 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
672 |
apply(rule trm.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
673 |
apply(rule fin_supp_trans)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
674 |
apply(simp add: fcb_trans_Lam) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
675 |
apply(simp add: fcb_trans_Case) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
676 |
apply(simp add: trans_App_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
677 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
678 |
apply(rule trm.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
679 |
apply(rule fin_supp_trans)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
680 |
apply(simp add: fcb_trans_Lam) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
681 |
apply(simp add: fcb_trans_Case) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
682 |
apply(fresh_guess add: fs_name1 trans_Var_def perm_if eq_eqvt) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
683 |
apply(fresh_guess add: fs_name1 trans_Lam_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
684 |
apply(fresh_guess add: fs_name1 trans_App_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
685 |
apply(fresh_guess add: fs_name1 trans_Const_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
686 |
apply(fresh_guess add: fs_name1 trans_Pr_def Let_def perm_nat_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
687 |
apply(fresh_guess add: fs_name1 trans_Fst_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
688 |
apply(fresh_guess add: fs_name1 trans_Snd_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
689 |
apply(fresh_guess add: fs_name1 trans_InL_def Let_def perm_nat_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
690 |
apply(fresh_guess add: fs_name1 trans_InR_def Let_def perm_nat_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
691 |
apply(fresh_guess add: fs_name1 trans_Case_def Let_def Isubst_eqvt) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
692 |
apply(simp add: trans_Lam_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
693 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
694 |
apply(rule trm.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
695 |
apply(rule fin_supp_trans)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
696 |
apply(simp add: fcb_trans_Lam) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
697 |
apply(simp add: fcb_trans_Case) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
698 |
apply(simp add: trans_Const_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
699 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
700 |
apply(rule trm.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
701 |
apply(rule fin_supp_trans)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
702 |
apply(simp add: fcb_trans_Lam) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
703 |
apply(simp add: fcb_trans_Case) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
704 |
apply(simp add: trans_Pr_def Let_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
705 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
706 |
apply(rule trm.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
707 |
apply(rule fin_supp_trans)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
708 |
apply(simp add: fcb_trans_Lam) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
709 |
apply(simp add: fcb_trans_Case) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
710 |
apply(simp add: trans_Fst_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
711 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
712 |
apply(rule trm.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
713 |
apply(rule fin_supp_trans)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
714 |
apply(simp add: fcb_trans_Lam) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
715 |
apply(simp add: fcb_trans_Case) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
716 |
apply(simp add: trans_Snd_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
717 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
718 |
apply(rule trm.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
719 |
apply(rule fin_supp_trans)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
720 |
apply(simp add: fcb_trans_Lam) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
721 |
apply(simp add: fcb_trans_Case) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
722 |
apply(simp add: trans_InL_def Let_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
723 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
724 |
apply(rule trm.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
725 |
apply(rule fin_supp_trans)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
726 |
apply(simp add: fcb_trans_Lam) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
727 |
apply(simp add: fcb_trans_Case) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
728 |
apply(simp add: trans_InR_def Let_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
729 |
apply(rule trans) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
730 |
apply(rule trm.recs[where P="\<lambda>_. True", simplified]) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
731 |
apply(rule fin_supp_trans)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
732 |
apply(simp add: fcb_trans_Lam) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
733 |
apply(simp add: fcb_trans_Case) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
734 |
apply(fresh_guess add: fs_name1 trans_Var_def perm_if eq_eqvt) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
735 |
apply(fresh_guess add: fs_name1 trans_Var_def perm_if eq_eqvt) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
736 |
apply(fresh_guess add: fs_name1 trans_Lam_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
737 |
apply(fresh_guess add: fs_name1 trans_Lam_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
738 |
apply(fresh_guess add: fs_name1 trans_App_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
739 |
apply(fresh_guess add: fs_name1 trans_App_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
740 |
apply(fresh_guess add: fs_name1 trans_Const_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
741 |
apply(fresh_guess add: fs_name1 trans_Const_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
742 |
apply(fresh_guess add: fs_name1 trans_Pr_def Let_def perm_nat_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
743 |
apply(fresh_guess add: fs_name1 trans_Pr_def Let_def perm_nat_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
744 |
apply(fresh_guess add: fs_name1 trans_Fst_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
745 |
apply(fresh_guess add: fs_name1 trans_Fst_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
746 |
apply(fresh_guess add: fs_name1 trans_Snd_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
747 |
apply(fresh_guess add: fs_name1 trans_Snd_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
748 |
apply(fresh_guess add: fs_name1 trans_InL_def Let_def perm_nat_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
749 |
apply(fresh_guess add: fs_name1 trans_InL_def Let_def perm_nat_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
750 |
apply(fresh_guess add: fs_name1 trans_InR_def Let_def perm_nat_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
751 |
apply(fresh_guess add: fs_name1 trans_InR_def Let_def perm_nat_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
752 |
apply(fresh_guess add: fs_name1 trans_Case_def Let_def Isubst_eqvt) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
753 |
apply(fresh_guess add: fs_name1 trans_Case_def Let_def Isubst_eqvt) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
754 |
apply(assumption)+ |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
755 |
apply(simp add: trans_Case_def Let_def) |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
756 |
done |
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
757 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
758 |
|
fd9b0b78a7d3
this file contains a compile-challenge suggested by Adam Chlipala;
urbanc
parents:
diff
changeset
|
759 |
end |