| author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
| Wed, 06 Jul 2011 07:42:12 +0900 | |
| changeset 2953 | 80f01215d1a6 |
| parent 2950 | 0911cb7bf696 |
| permissions | -rw-r--r-- |
| 2573 | 1 |
theory Foo2 |
2 |
imports "../Nominal2" |
|
3 |
begin |
|
4 |
||
5 |
(* |
|
6 |
Contrived example that has more than one |
|
7 |
binding clause |
|
8 |
*) |
|
9 |
||
10 |
atom_decl name |
|
11 |
||
|
2630
8268b277d240
automated all strong induction lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2629
diff
changeset
|
12 |
|
| 2573 | 13 |
nominal_datatype foo: trm = |
14 |
Var "name" |
|
15 |
| 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:
2630
diff
changeset
|
16 |
| 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:
2630
diff
changeset
|
17 |
| Let1 a1::"assg" t1::"trm" a2::"assg" t2::"trm" binds "bn a1" in t1, binds "bn a2" in t2 |
|
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents:
2630
diff
changeset
|
18 |
| Let2 x::"name" y::"name" t1::"trm" t2::"trm" binds x y in t1, binds y in t2 |
| 2573 | 19 |
and assg = |
20 |
As_Nil |
|
21 |
| As "name" x::"name" t::"trm" "assg" |
|
22 |
binder |
|
23 |
bn::"assg \<Rightarrow> atom list" |
|
24 |
where |
|
|
2611
3d101f2f817c
simple cases for strong inducts done; infrastructure for the difficult ones is there
Christian Urban <urbanc@in.tum.de>
parents:
2609
diff
changeset
|
25 |
"bn (As x y t a) = [atom x] @ bn a" |
| 2573 | 26 |
| "bn (As_Nil) = []" |
27 |
||
|
2628
16ffbc8442ca
generated goals for strong induction theorems.
Christian Urban <urbanc@in.tum.de>
parents:
2626
diff
changeset
|
28 |
|
|
2598
b136721eedb2
automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents:
2594
diff
changeset
|
29 |
thm foo.bn_defs |
|
b136721eedb2
automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents:
2594
diff
changeset
|
30 |
thm foo.permute_bn |
|
2593
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2592
diff
changeset
|
31 |
thm foo.perm_bn_alpha |
| 2573 | 32 |
thm foo.perm_bn_simps |
|
2593
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2592
diff
changeset
|
33 |
thm foo.bn_finite |
| 2573 | 34 |
|
35 |
thm foo.distinct |
|
36 |
thm foo.induct |
|
37 |
thm foo.inducts |
|
|
2630
8268b277d240
automated all strong induction lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2629
diff
changeset
|
38 |
thm foo.strong_induct |
| 2573 | 39 |
thm foo.exhaust |
|
2626
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents:
2616
diff
changeset
|
40 |
thm foo.strong_exhaust |
| 2573 | 41 |
thm foo.fv_defs |
42 |
thm foo.bn_defs |
|
43 |
thm foo.perm_simps |
|
|
2607
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
parents:
2603
diff
changeset
|
44 |
thm foo.eq_iff |
| 2573 | 45 |
thm foo.fv_bn_eqvt |
46 |
thm foo.size_eqvt |
|
47 |
thm foo.supports |
|
48 |
thm foo.fsupp |
|
49 |
thm foo.supp |
|
50 |
thm foo.fresh |
|
|
2630
8268b277d240
automated all strong induction lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2629
diff
changeset
|
51 |
thm foo.size |
|
2629
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
parents:
2628
diff
changeset
|
52 |
|
|
2584
1eac050a36f4
completely different method fro deriving the exhaust lemma
Christian Urban <urbanc@in.tum.de>
parents:
2579
diff
changeset
|
53 |
|
| 2573 | 54 |
end |
55 |
||
56 |
||
57 |