| author | Christian Urban <urbanc@in.tum.de> |
| Sat, 17 Dec 2011 17:08:47 +0000 | |
| branch | Nominal2-Isabelle2011-1 |
| changeset 3071 | 11f6a561eb4b |
| parent 2971 | d629240f0f63 |
| permissions | -rw-r--r-- |
|
2436
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2120
diff
changeset
|
1 |
theory Let |
|
2454
9ffee4eb1ae1
renamed NewParser to Nominal2
Christian Urban <urbanc@in.tum.de>
parents:
2449
diff
changeset
|
2 |
imports "../Nominal2" |
| 1600 | 3 |
begin |
4 |
||
5 |
atom_decl name |
|
6 |
||
7 |
nominal_datatype trm = |
|
|
2436
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2120
diff
changeset
|
8 |
Var "name" |
|
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2120
diff
changeset
|
9 |
| App "trm" "trm" |
|
2950
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents:
2943
diff
changeset
|
10 |
| Lam x::"name" t::"trm" binds x in t |
|
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents:
2943
diff
changeset
|
11 |
| Let as::"assn" t::"trm" binds "bn as" in t |
| 2490 | 12 |
and assn = |
13 |
ANil |
|
14 |
| ACons "name" "trm" "assn" |
|
| 1600 | 15 |
binder |
16 |
bn |
|
17 |
where |
|
| 2490 | 18 |
"bn ANil = []" |
19 |
| "bn (ACons x t as) = (atom x) # (bn as)" |
|
20 |
||
| 2924 | 21 |
print_theorems |
22 |
||
23 |
thm alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.intros |
|
24 |
thm bn_raw.simps |
|
25 |
thm permute_bn_raw.simps |
|
26 |
thm trm_assn.perm_bn_alpha |
|
27 |
thm trm_assn.permute_bn |
|
28 |
||
| 2490 | 29 |
thm trm_assn.fv_defs |
| 2924 | 30 |
thm trm_assn.eq_iff |
| 2490 | 31 |
thm trm_assn.bn_defs |
| 2922 | 32 |
thm trm_assn.bn_inducts |
| 2490 | 33 |
thm trm_assn.perm_simps |
| 2956 | 34 |
thm trm_assn.permute_bn |
|
2492
5ac9a74d22fd
post-processed eq_iff and supp threormes according to the fv-supp equality
Christian Urban <urbanc@in.tum.de>
parents:
2490
diff
changeset
|
35 |
thm trm_assn.induct |
|
5ac9a74d22fd
post-processed eq_iff and supp threormes according to the fv-supp equality
Christian Urban <urbanc@in.tum.de>
parents:
2490
diff
changeset
|
36 |
thm trm_assn.inducts |
| 2490 | 37 |
thm trm_assn.distinct |
38 |
thm trm_assn.supp |
|
|
2493
2e174807c891
added postprocessed fresh-lemmas for constructors
Christian Urban <urbanc@in.tum.de>
parents:
2492
diff
changeset
|
39 |
thm trm_assn.fresh |
|
2617
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
2562
diff
changeset
|
40 |
thm trm_assn.exhaust |
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
2562
diff
changeset
|
41 |
thm trm_assn.strong_exhaust |
|
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
2926
diff
changeset
|
42 |
thm trm_assn.perm_bn_simps |
|
2494
11133eb76f61
added Foo1 to explore a contrived example
Christian Urban <urbanc@in.tum.de>
parents:
2493
diff
changeset
|
43 |
|
|
2670
3c493c951388
alpha_abs_let_stronger is not true in the same form
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2630
diff
changeset
|
44 |
|
|
2932
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2931
diff
changeset
|
45 |
end |