| author | Cezary Kaliszyk <cezarykaliszyk@gmail.com> |
| Tue, 27 Mar 2012 14:56:06 +0200 | |
| changeset 3140 | 5179ff4806c5 |
| parent 2950 | 0911cb7bf696 |
| permissions | -rw-r--r-- |
|
2454
9ffee4eb1ae1
renamed NewParser to Nominal2
Christian Urban <urbanc@in.tum.de>
parents:
2436
diff
changeset
|
1 |
theory Ex1 |
|
9ffee4eb1ae1
renamed NewParser to Nominal2
Christian Urban <urbanc@in.tum.de>
parents:
2436
diff
changeset
|
2 |
imports "../Nominal2" |
|
2045
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
3 |
begin |
|
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
4 |
|
|
2454
9ffee4eb1ae1
renamed NewParser to Nominal2
Christian Urban <urbanc@in.tum.de>
parents:
2436
diff
changeset
|
5 |
(* free names in bar are bound in foo *) |
|
2045
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
6 |
|
|
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
7 |
atom_decl name |
|
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
8 |
|
|
2611
3d101f2f817c
simple cases for strong inducts done; infrastructure for the difficult ones is there
Christian Urban <urbanc@in.tum.de>
parents:
2593
diff
changeset
|
9 |
thm finite_sets_supp |
|
2561
7926f1cb45eb
respectfulness for permute_bn functions
Christian Urban <urbanc@in.tum.de>
parents:
2475
diff
changeset
|
10 |
|
|
2045
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
11 |
nominal_datatype foo = |
|
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
12 |
Foo0 "name" |
|
2950
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents:
2625
diff
changeset
|
13 |
| Foo1 b::"bar" f::"foo" binds (set) "bv b" in f |
|
2045
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
14 |
and bar = |
|
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
15 |
Bar0 "name" |
|
2950
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents:
2625
diff
changeset
|
16 |
| Bar1 "name" s::"name" b::"bar" binds (set) s in b |
|
2045
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
17 |
binder |
|
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
18 |
bv |
|
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
19 |
where |
|
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
20 |
"bv (Bar0 x) = {}"
|
|
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
21 |
| "bv (Bar1 v x b) = {atom v}"
|
|
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
22 |
|
|
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:
2561
diff
changeset
|
23 |
thm foo_bar.perm_bn_alpha |
|
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:
2561
diff
changeset
|
24 |
thm foo_bar.perm_bn_simps |
|
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:
2561
diff
changeset
|
25 |
thm foo_bar.bn_finite |
|
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:
2561
diff
changeset
|
26 |
|
|
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:
2561
diff
changeset
|
27 |
thm foo_bar.eq_iff |
|
2475
486d4647bb37
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
parents:
2454
diff
changeset
|
28 |
thm foo_bar.distinct |
|
486d4647bb37
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
parents:
2454
diff
changeset
|
29 |
thm foo_bar.induct |
|
486d4647bb37
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
parents:
2454
diff
changeset
|
30 |
thm foo_bar.inducts |
|
486d4647bb37
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
parents:
2454
diff
changeset
|
31 |
thm foo_bar.exhaust |
|
486d4647bb37
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
parents:
2454
diff
changeset
|
32 |
thm foo_bar.fv_defs |
|
486d4647bb37
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
parents:
2454
diff
changeset
|
33 |
thm foo_bar.bn_defs |
|
486d4647bb37
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
parents:
2454
diff
changeset
|
34 |
thm foo_bar.perm_simps |
|
486d4647bb37
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
parents:
2454
diff
changeset
|
35 |
thm foo_bar.eq_iff |
|
486d4647bb37
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
parents:
2454
diff
changeset
|
36 |
thm foo_bar.fv_bn_eqvt |
|
486d4647bb37
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
parents:
2454
diff
changeset
|
37 |
thm foo_bar.size_eqvt |
|
486d4647bb37
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
parents:
2454
diff
changeset
|
38 |
thm foo_bar.supports |
|
486d4647bb37
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
parents:
2454
diff
changeset
|
39 |
thm foo_bar.fsupp |
|
486d4647bb37
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
parents:
2454
diff
changeset
|
40 |
thm foo_bar.supp |
|
2454
9ffee4eb1ae1
renamed NewParser to Nominal2
Christian Urban <urbanc@in.tum.de>
parents:
2436
diff
changeset
|
41 |
|
|
9ffee4eb1ae1
renamed NewParser to Nominal2
Christian Urban <urbanc@in.tum.de>
parents:
2436
diff
changeset
|
42 |
lemma |
|
2625
478c5648e73f
moved generic functions into nominal_library
Christian Urban <urbanc@in.tum.de>
parents:
2611
diff
changeset
|
43 |
"supp (Foo1 (Bar1 v x (Bar0 x)) (Foo0 v)) = {}"
|
|
478c5648e73f
moved generic functions into nominal_library
Christian Urban <urbanc@in.tum.de>
parents:
2611
diff
changeset
|
44 |
apply(simp only: foo_bar.supp) |
|
2454
9ffee4eb1ae1
renamed NewParser to Nominal2
Christian Urban <urbanc@in.tum.de>
parents:
2436
diff
changeset
|
45 |
apply(simp only: foo_bar.bn_defs) |
|
9ffee4eb1ae1
renamed NewParser to Nominal2
Christian Urban <urbanc@in.tum.de>
parents:
2436
diff
changeset
|
46 |
apply(simp only: supp_at_base) |
|
9ffee4eb1ae1
renamed NewParser to Nominal2
Christian Urban <urbanc@in.tum.de>
parents:
2436
diff
changeset
|
47 |
apply(simp) |
|
9ffee4eb1ae1
renamed NewParser to Nominal2
Christian Urban <urbanc@in.tum.de>
parents:
2436
diff
changeset
|
48 |
done |
|
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
parents:
2045
diff
changeset
|
49 |
|
|
2045
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
50 |
end |
|
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
51 |
|
|
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
52 |