| author | Christian Urban <urbanc@in.tum.de> |
| Sat, 02 Jul 2011 00:27:47 +0100 | |
| changeset 2931 | aaef9dec5e1d |
| parent 2616 | dd7490fdd998 |
| child 2950 | 0911cb7bf696 |
| permissions | -rw-r--r-- |
|
2481
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2480
diff
changeset
|
1 |
theory Multi_Recs |
|
2454
9ffee4eb1ae1
renamed NewParser to Nominal2
Christian Urban <urbanc@in.tum.de>
parents:
2436
diff
changeset
|
2 |
imports "../Nominal2" |
|
1655
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
3 |
begin |
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
4 |
|
|
2481
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2480
diff
changeset
|
5 |
(* |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2480
diff
changeset
|
6 |
multiple recursive binders |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2480
diff
changeset
|
7 |
|
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2480
diff
changeset
|
8 |
example 7 from Peter Sewell's bestiary |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2480
diff
changeset
|
9 |
|
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2480
diff
changeset
|
10 |
*) |
|
1655
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
11 |
|
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
12 |
atom_decl name |
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
13 |
|
|
2481
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2480
diff
changeset
|
14 |
nominal_datatype multi_recs: exp = |
|
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
parents:
2043
diff
changeset
|
15 |
Var name |
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
parents:
2043
diff
changeset
|
16 |
| Unit |
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
parents:
2043
diff
changeset
|
17 |
| Pair exp exp |
|
2436
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2120
diff
changeset
|
18 |
| LetRec l::"lrbs" e::"exp" bind (set) "bs l" in l e |
|
1655
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
19 |
and lrb = |
|
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
parents:
2043
diff
changeset
|
20 |
Assign name exp |
|
1655
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
21 |
and lrbs = |
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
22 |
Single lrb |
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
23 |
| More lrb lrbs |
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
24 |
binder |
|
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
parents:
2043
diff
changeset
|
25 |
b :: "lrb \<Rightarrow> atom set" and |
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
parents:
2043
diff
changeset
|
26 |
bs :: "lrbs \<Rightarrow> atom set" |
|
1655
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
27 |
where |
|
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
parents:
2043
diff
changeset
|
28 |
"b (Assign x e) = {atom x}"
|
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
parents:
2043
diff
changeset
|
29 |
| "bs (Single a) = b a" |
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
parents:
2043
diff
changeset
|
30 |
| "bs (More a as) = (b a) \<union> (bs as)" |
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
parents:
2043
diff
changeset
|
31 |
|
|
2481
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2480
diff
changeset
|
32 |
thm multi_recs.distinct |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2480
diff
changeset
|
33 |
thm multi_recs.induct |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2480
diff
changeset
|
34 |
thm multi_recs.inducts |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2480
diff
changeset
|
35 |
thm multi_recs.exhaust |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2480
diff
changeset
|
36 |
thm multi_recs.fv_defs |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2480
diff
changeset
|
37 |
thm multi_recs.bn_defs |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2480
diff
changeset
|
38 |
thm multi_recs.perm_simps |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2480
diff
changeset
|
39 |
thm multi_recs.eq_iff |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2480
diff
changeset
|
40 |
thm multi_recs.fv_bn_eqvt |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2480
diff
changeset
|
41 |
thm multi_recs.size_eqvt |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2480
diff
changeset
|
42 |
thm multi_recs.supports |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2480
diff
changeset
|
43 |
thm multi_recs.fsupp |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2480
diff
changeset
|
44 |
thm multi_recs.supp |
|
1655
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
45 |
|
|
2615
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
46 |
thm multi_recs.bn_defs |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
47 |
thm multi_recs.permute_bn |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
48 |
thm multi_recs.perm_bn_alpha |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
49 |
thm multi_recs.perm_bn_simps |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
50 |
thm multi_recs.bn_finite |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
51 |
|
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
52 |
|
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
53 |
lemma at_set_avoiding5: |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
54 |
assumes "finite xs" |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
55 |
and "finite (supp c)" |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
56 |
shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp p = xs \<union> p \<bullet> xs" |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
57 |
using assms |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
58 |
apply(erule_tac c="c" in at_set_avoiding) |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
59 |
apply(auto) |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
60 |
done |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
61 |
|
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
62 |
lemma |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
63 |
fixes c::"'a::fs" |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
64 |
assumes a: "\<And>lrbs exp. \<lbrakk>bs lrbs \<sharp>* c; y = LetRec lrbs exp\<rbrakk> \<Longrightarrow> P" |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
65 |
shows "y = LetRec lrbs exp \<Longrightarrow> P" |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
66 |
apply - |
|
2616
dd7490fdd998
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
Christian Urban <urbanc@in.tum.de>
parents:
2615
diff
changeset
|
67 |
apply(subgoal_tac "\<exists>p. ((p \<bullet> (bs lrbs)) \<sharp>* (c, bs lrbs, lrbs, exp))") |
|
2615
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
68 |
apply(erule exE) |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
69 |
apply(simp add: fresh_star_Pair) |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
70 |
apply(erule conjE)+ |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
71 |
apply(simp add: multi_recs.fv_bn_eqvt) |
|
2616
dd7490fdd998
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
Christian Urban <urbanc@in.tum.de>
parents:
2615
diff
changeset
|
72 |
using Abs_rename_set' |
|
2615
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
73 |
apply - |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
74 |
apply(drule_tac x="p" in meta_spec) |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
75 |
apply(drule_tac x="bs lrbs" in meta_spec) |
|
2616
dd7490fdd998
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
Christian Urban <urbanc@in.tum.de>
parents:
2615
diff
changeset
|
76 |
apply(drule_tac x="(lrbs, exp)" in meta_spec) |
|
2615
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
77 |
apply(drule meta_mp) |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
78 |
apply(simp add: multi_recs.fv_bn_eqvt fresh_star_Pair) |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
79 |
apply(drule meta_mp) |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
80 |
apply(simp add: multi_recs.bn_finite) |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
81 |
apply(erule exE) |
|
2616
dd7490fdd998
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
Christian Urban <urbanc@in.tum.de>
parents:
2615
diff
changeset
|
82 |
apply(erule conjE) |
|
dd7490fdd998
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
Christian Urban <urbanc@in.tum.de>
parents:
2615
diff
changeset
|
83 |
apply(rotate_tac 6) |
|
dd7490fdd998
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
Christian Urban <urbanc@in.tum.de>
parents:
2615
diff
changeset
|
84 |
apply(drule sym) |
|
2615
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
85 |
apply(simp add: multi_recs.fv_bn_eqvt) |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
86 |
apply(rule a) |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
87 |
apply(assumption) |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
88 |
apply(clarify) |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
89 |
apply(simp (no_asm) only: multi_recs.eq_iff) |
|
2616
dd7490fdd998
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
Christian Urban <urbanc@in.tum.de>
parents:
2615
diff
changeset
|
90 |
apply(rule at_set_avoiding1) |
|
2615
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
91 |
apply(simp add: multi_recs.bn_finite) |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
92 |
apply(simp add: supp_Pair finite_supp) |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
93 |
apply(rule finite_sets_supp) |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
94 |
apply(simp add: multi_recs.bn_finite) |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
95 |
done |
|
d5713db7e146
one interesting case done
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
96 |
|
|
1655
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
97 |
end |
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
98 |
|
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
99 |
|
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
100 |