|
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
|
12 |
|
|
2573
|
13 |
nominal_datatype foo: trm =
|
|
|
14 |
Var "name"
|
|
|
15 |
| App "trm" "trm"
|
|
|
16 |
| Lam x::"name" t::"trm" bind x in t
|
|
|
17 |
| Let1 a1::"assg" t1::"trm" a2::"assg" t2::"trm" bind "bn a1" in t1, bind "bn a2" in t2
|
|
|
18 |
| Let2 x::"name" y::"name" t1::"trm" t2::"trm" bind x y in t1, bind y in t2
|
|
|
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>
diff
changeset
|
25 |
"bn (As x y t a) = [atom x] @ bn a"
|
|
2573
|
26 |
| "bn (As_Nil) = []"
|
|
|
27 |
|
|
2628
|
28 |
|
|
2598
|
29 |
thm foo.bn_defs
|
|
|
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>
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>
diff
changeset
|
33 |
thm foo.bn_finite
|
|
2573
|
34 |
|
|
|
35 |
thm foo.distinct
|
|
|
36 |
thm foo.induct
|
|
|
37 |
thm foo.inducts
|
|
2630
|
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>
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>
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
|
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>
diff
changeset
|
52 |
|
|
2584
|
53 |
|
|
2573
|
54 |
end
|
|
|
55 |
|
|
|
56 |
|
|
|
57 |
|