| author | Christian Urban <urbanc@in.tum.de> |
| Tue, 21 Dec 2010 10:28:08 +0000 | |
| changeset 2616 | dd7490fdd998 |
| parent 2611 | 3d101f2f817c |
| child 2626 | d1bdc281be2b |
| 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 |
||
12 |
nominal_datatype foo: trm = |
|
13 |
Var "name" |
|
14 |
| App "trm" "trm" |
|
15 |
| Lam x::"name" t::"trm" bind x in t |
|
16 |
| Let1 a1::"assg" t1::"trm" a2::"assg" t2::"trm" bind "bn a1" in t1, bind "bn a2" in t2 |
|
17 |
| Let2 x::"name" y::"name" t1::"trm" t2::"trm" bind x y in t1, bind y in t2 |
|
18 |
and assg = |
|
19 |
As_Nil |
|
20 |
| As "name" x::"name" t::"trm" "assg" |
|
21 |
binder |
|
22 |
bn::"assg \<Rightarrow> atom list" |
|
23 |
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
|
24 |
"bn (As x y t a) = [atom x] @ bn a" |
| 2573 | 25 |
| "bn (As_Nil) = []" |
26 |
||
|
2603
90779aefbf1a
first tests about exhaust
Christian Urban <urbanc@in.tum.de>
parents:
2602
diff
changeset
|
27 |
|
|
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
|
28 |
|
|
3d101f2f817c
simple cases for strong inducts done; infrastructure for the difficult ones is there
Christian Urban <urbanc@in.tum.de>
parents:
2609
diff
changeset
|
29 |
|
|
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:
2611
diff
changeset
|
30 |
|
|
2598
b136721eedb2
automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents:
2594
diff
changeset
|
31 |
thm foo.bn_defs |
|
b136721eedb2
automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents:
2594
diff
changeset
|
32 |
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
|
33 |
thm foo.perm_bn_alpha |
| 2573 | 34 |
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
|
35 |
thm foo.bn_finite |
| 2573 | 36 |
|
|
2600
ca6b4bc7a871
kept the nested structure of constructors (belonging to one datatype)
Christian Urban <urbanc@in.tum.de>
parents:
2599
diff
changeset
|
37 |
|
| 2573 | 38 |
thm foo.distinct |
39 |
thm foo.induct |
|
40 |
thm foo.inducts |
|
41 |
thm foo.exhaust |
|
42 |
thm foo.fv_defs |
|
43 |
thm foo.bn_defs |
|
44 |
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
|
45 |
thm foo.eq_iff |
| 2573 | 46 |
thm foo.fv_bn_eqvt |
47 |
thm foo.size_eqvt |
|
48 |
thm foo.supports |
|
49 |
thm foo.fsupp |
|
50 |
thm foo.supp |
|
51 |
thm foo.fresh |
|
52 |
||
|
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:
2611
diff
changeset
|
53 |
lemma at_set_avoiding5: |
|
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:
2611
diff
changeset
|
54 |
assumes "finite xs" |
|
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:
2611
diff
changeset
|
55 |
and "finite (supp c)" |
|
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:
2611
diff
changeset
|
56 |
shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp p = xs \<union> p \<bullet> xs" |
|
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:
2611
diff
changeset
|
57 |
using assms |
|
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:
2611
diff
changeset
|
58 |
apply(erule_tac c="c" in at_set_avoiding) |
|
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:
2611
diff
changeset
|
59 |
apply(auto) |
|
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:
2611
diff
changeset
|
60 |
done |
|
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:
2611
diff
changeset
|
61 |
|
|
2609
666ffc8a92a9
freshness theorem in strong exhausts; (temporarily includes a cheat_tac to make all tests go through)
Christian Urban <urbanc@in.tum.de>
parents:
2608
diff
changeset
|
62 |
|
|
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:
2611
diff
changeset
|
63 |
lemma Abs_rename_lst3: |
|
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:
2611
diff
changeset
|
64 |
fixes x::"'a::fs" |
|
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:
2611
diff
changeset
|
65 |
assumes a: "(p \<bullet> (set bs)) \<sharp>* (bs, x)" |
|
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:
2611
diff
changeset
|
66 |
shows "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> p \<bullet> bs = q \<bullet> bs" |
|
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:
2611
diff
changeset
|
67 |
proof - |
|
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:
2611
diff
changeset
|
68 |
from a have "p \<bullet> (set bs) \<inter> (set bs) = {}" using at_fresh_star_inter
|
|
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:
2611
diff
changeset
|
69 |
by (simp add: fresh_star_Pair fresh_star_set) |
|
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:
2611
diff
changeset
|
70 |
with list_renaming_perm |
|
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:
2611
diff
changeset
|
71 |
obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by metis |
|
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:
2611
diff
changeset
|
72 |
have "[bs]lst. x = q \<bullet> ([bs]lst. x)" |
|
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:
2611
diff
changeset
|
73 |
apply(rule perm_supp_eq[symmetric]) |
|
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:
2611
diff
changeset
|
74 |
using a ** |
|
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:
2611
diff
changeset
|
75 |
unfolding fresh_star_Pair |
|
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:
2611
diff
changeset
|
76 |
unfolding Abs_fresh_star_iff |
|
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:
2611
diff
changeset
|
77 |
unfolding fresh_star_def |
|
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:
2611
diff
changeset
|
78 |
by auto |
|
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:
2611
diff
changeset
|
79 |
also have "\<dots> = [q \<bullet> bs]lst. (q \<bullet> x)" by simp |
|
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:
2611
diff
changeset
|
80 |
also have "\<dots> = [p \<bullet> bs]lst. (q \<bullet> x)" using * by simp |
|
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:
2611
diff
changeset
|
81 |
finally have "[bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x)" . |
|
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:
2611
diff
changeset
|
82 |
then show "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> p \<bullet> bs = q \<bullet> bs" |
|
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:
2611
diff
changeset
|
83 |
using * ** by metis |
|
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:
2611
diff
changeset
|
84 |
qed |
|
2584
1eac050a36f4
completely different method fro deriving the exhaust lemma
Christian Urban <urbanc@in.tum.de>
parents:
2579
diff
changeset
|
85 |
|
|
2586
3ebc7ecfb0dd
disabled the Foo examples, because of heavy work
Christian Urban <urbanc@in.tum.de>
parents:
2585
diff
changeset
|
86 |
|
|
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:
2611
diff
changeset
|
87 |
lemma |
|
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:
2611
diff
changeset
|
88 |
fixes c::"'a::fs" |
|
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:
2611
diff
changeset
|
89 |
assumes a: "\<And>assg1 trm1 assg2 trm2. \<lbrakk>((set (bn assg1)) \<union> (set (bn assg2))) \<sharp>* c; y = Let1 assg1 trm1 assg2 trm2\<rbrakk> \<Longrightarrow> P" |
|
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:
2611
diff
changeset
|
90 |
shows "y = Let1 assg1 trm1 assg2 trm2 \<Longrightarrow> P" |
|
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:
2611
diff
changeset
|
91 |
apply - |
|
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:
2611
diff
changeset
|
92 |
apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2) \<and> |
|
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:
2611
diff
changeset
|
93 |
supp p = (set (bn assg1)) \<union> (set (bn assg2)) \<union> (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2))))") |
|
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:
2611
diff
changeset
|
94 |
defer |
|
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:
2611
diff
changeset
|
95 |
apply(rule at_set_avoiding5) |
|
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:
2611
diff
changeset
|
96 |
apply(simp add: foo.bn_finite) |
|
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:
2611
diff
changeset
|
97 |
apply(simp add: supp_Pair finite_supp) |
|
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:
2611
diff
changeset
|
98 |
apply(erule exE) |
|
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:
2611
diff
changeset
|
99 |
apply(perm_simp add: foo.permute_bn) |
|
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:
2611
diff
changeset
|
100 |
apply(simp add: fresh_star_Pair) |
|
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:
2611
diff
changeset
|
101 |
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:
2611
diff
changeset
|
102 |
thm Abs_rename_lst |
|
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:
2611
diff
changeset
|
103 |
apply(insert Abs_rename_lst)[1] |
|
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:
2611
diff
changeset
|
104 |
apply(drule_tac x="p" in meta_spec) |
|
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:
2611
diff
changeset
|
105 |
apply(drule_tac x="bn assg1" in meta_spec) |
|
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:
2611
diff
changeset
|
106 |
apply(drule_tac x="trm1" in meta_spec) |
|
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:
2611
diff
changeset
|
107 |
apply(insert Abs_rename_lst)[1] |
|
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:
2611
diff
changeset
|
108 |
apply(drule_tac x="p" in meta_spec) |
|
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:
2611
diff
changeset
|
109 |
apply(drule_tac x="bn assg2" in meta_spec) |
|
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:
2611
diff
changeset
|
110 |
apply(drule_tac x="trm2" in meta_spec) |
|
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:
2611
diff
changeset
|
111 |
apply(drule meta_mp) |
|
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:
2611
diff
changeset
|
112 |
apply(perm_simp add: foo.permute_bn) |
|
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:
2611
diff
changeset
|
113 |
apply(simp add: fresh_star_Pair fresh_star_Un) |
|
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:
2611
diff
changeset
|
114 |
apply(drule meta_mp) |
|
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:
2611
diff
changeset
|
115 |
apply(perm_simp add: foo.permute_bn) |
|
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:
2611
diff
changeset
|
116 |
apply(simp add: fresh_star_Pair fresh_star_Un) |
|
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:
2611
diff
changeset
|
117 |
apply(erule exE)+ |
|
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:
2611
diff
changeset
|
118 |
apply(rule a) |
|
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:
2611
diff
changeset
|
119 |
apply(assumption) |
|
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:
2611
diff
changeset
|
120 |
apply(simp only: foo.eq_iff) |
|
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:
2611
diff
changeset
|
121 |
apply(perm_simp add: foo.permute_bn) |
|
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:
2611
diff
changeset
|
122 |
apply(rule conjI) |
|
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:
2611
diff
changeset
|
123 |
apply(rule refl) |
|
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:
2611
diff
changeset
|
124 |
apply(rule conjI) |
|
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:
2611
diff
changeset
|
125 |
apply(rule foo.perm_bn_alpha) |
|
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:
2611
diff
changeset
|
126 |
apply(rule conjI) |
|
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:
2611
diff
changeset
|
127 |
apply(perm_simp add: foo.permute_bn) |
|
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:
2611
diff
changeset
|
128 |
apply(rule refl) |
|
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:
2611
diff
changeset
|
129 |
apply(rule foo.perm_bn_alpha) |
|
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:
2611
diff
changeset
|
130 |
done |
|
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:
2611
diff
changeset
|
131 |
|
|
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:
2611
diff
changeset
|
132 |
lemma |
|
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:
2611
diff
changeset
|
133 |
fixes c::"'a::fs" |
|
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:
2611
diff
changeset
|
134 |
assumes a: "\<And>assg1 trm1 assg2 trm2. \<lbrakk>((set (bn assg1)) \<union> (set (bn assg2))) \<sharp>* c; y = Let1 assg1 trm1 assg2 trm2\<rbrakk> \<Longrightarrow> P" |
|
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:
2611
diff
changeset
|
135 |
shows "y = Let1 assg1 trm1 assg2 trm2 \<Longrightarrow> P" |
|
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:
2611
diff
changeset
|
136 |
apply - |
|
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:
2611
diff
changeset
|
137 |
apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2) \<and> |
|
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:
2611
diff
changeset
|
138 |
supp p = (set (bn assg1)) \<union> (set (bn assg2)) \<union> (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2))))") |
|
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:
2611
diff
changeset
|
139 |
defer |
|
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:
2611
diff
changeset
|
140 |
apply(rule at_set_avoiding5) |
|
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:
2611
diff
changeset
|
141 |
apply(simp add: foo.bn_finite) |
|
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:
2611
diff
changeset
|
142 |
apply(simp add: supp_Pair finite_supp) |
|
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:
2611
diff
changeset
|
143 |
apply(erule exE) |
|
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:
2611
diff
changeset
|
144 |
apply(perm_simp add: foo.permute_bn) |
|
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:
2611
diff
changeset
|
145 |
apply(simp add: fresh_star_Pair) |
|
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:
2611
diff
changeset
|
146 |
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:
2611
diff
changeset
|
147 |
apply(insert Abs_rename_lst3)[1] |
|
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:
2611
diff
changeset
|
148 |
apply(drule_tac x="p" in meta_spec) |
|
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:
2611
diff
changeset
|
149 |
apply(drule_tac x="bn assg1" in meta_spec) |
|
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:
2611
diff
changeset
|
150 |
apply(drule_tac x="trm1" in meta_spec) |
|
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:
2611
diff
changeset
|
151 |
apply(insert Abs_rename_lst3)[1] |
|
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:
2611
diff
changeset
|
152 |
apply(drule_tac x="p" in meta_spec) |
|
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:
2611
diff
changeset
|
153 |
apply(drule_tac x="bn assg2" in meta_spec) |
|
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:
2611
diff
changeset
|
154 |
apply(drule_tac x="trm2" in meta_spec) |
|
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:
2611
diff
changeset
|
155 |
apply(drule meta_mp) |
|
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:
2611
diff
changeset
|
156 |
apply(perm_simp add: foo.permute_bn) |
|
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:
2611
diff
changeset
|
157 |
apply(simp add: fresh_star_Pair fresh_star_Un) |
|
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:
2611
diff
changeset
|
158 |
apply(drule meta_mp) |
|
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:
2611
diff
changeset
|
159 |
apply(perm_simp add: foo.permute_bn) |
|
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:
2611
diff
changeset
|
160 |
apply(simp add: fresh_star_Pair fresh_star_Un) |
|
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:
2611
diff
changeset
|
161 |
apply(erule exE)+ |
|
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:
2611
diff
changeset
|
162 |
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:
2611
diff
changeset
|
163 |
apply(simp add: foo.permute_bn) |
|
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:
2611
diff
changeset
|
164 |
apply(rule a) |
|
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:
2611
diff
changeset
|
165 |
apply(assumption) |
|
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:
2611
diff
changeset
|
166 |
apply(clarify) |
|
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:
2611
diff
changeset
|
167 |
apply(simp (no_asm) only: foo.eq_iff) |
|
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:
2611
diff
changeset
|
168 |
apply(rule conjI) |
|
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:
2611
diff
changeset
|
169 |
apply(assumption) |
|
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:
2611
diff
changeset
|
170 |
apply(rule conjI) |
|
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:
2611
diff
changeset
|
171 |
apply(rule foo.perm_bn_alpha) |
|
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:
2611
diff
changeset
|
172 |
apply(rule conjI) |
|
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:
2611
diff
changeset
|
173 |
apply(assumption) |
|
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:
2611
diff
changeset
|
174 |
apply(rule foo.perm_bn_alpha) |
|
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:
2611
diff
changeset
|
175 |
done |
|
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:
2611
diff
changeset
|
176 |
|
|
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:
2611
diff
changeset
|
177 |
|
|
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:
2611
diff
changeset
|
178 |
lemma |
|
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:
2611
diff
changeset
|
179 |
fixes c::"'a::fs" |
|
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:
2611
diff
changeset
|
180 |
assumes a: "\<And>assg1 trm1 assg2 trm2. \<lbrakk>((set (bn assg1)) \<union> (set (bn assg2))) \<sharp>* c; y = Let1 assg1 trm1 assg2 trm2\<rbrakk> \<Longrightarrow> P" |
|
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:
2611
diff
changeset
|
181 |
shows "y = Let1 assg1 trm1 assg2 trm2 \<Longrightarrow> P" |
|
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:
2611
diff
changeset
|
182 |
apply - |
|
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:
2611
diff
changeset
|
183 |
apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2) \<and> |
|
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:
2611
diff
changeset
|
184 |
supp p = (set (bn assg1)) \<union> (set (bn assg2)) \<union> (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2))))") |
|
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:
2611
diff
changeset
|
185 |
defer |
|
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:
2611
diff
changeset
|
186 |
apply(rule at_set_avoiding5) |
|
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:
2611
diff
changeset
|
187 |
apply(simp add: foo.bn_finite) |
|
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:
2611
diff
changeset
|
188 |
apply(simp add: supp_Pair finite_supp) |
|
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:
2611
diff
changeset
|
189 |
apply(erule exE) |
|
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:
2611
diff
changeset
|
190 |
apply(simp add: fresh_star_Pair) |
|
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:
2611
diff
changeset
|
191 |
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:
2611
diff
changeset
|
192 |
apply(simp (no_asm_use) only: foo.permute_bn set_eqvt union_eqvt) |
|
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:
2611
diff
changeset
|
193 |
apply(rule a) |
|
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:
2611
diff
changeset
|
194 |
apply(assumption) |
|
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:
2611
diff
changeset
|
195 |
apply(clarify) |
|
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:
2611
diff
changeset
|
196 |
apply(simp (no_asm) only: foo.eq_iff) |
|
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:
2611
diff
changeset
|
197 |
apply(rule conjI) |
|
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:
2611
diff
changeset
|
198 |
apply(rule trans) |
|
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:
2611
diff
changeset
|
199 |
apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
|
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:
2611
diff
changeset
|
200 |
apply(rule fresh_star_supp_conv) |
|
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:
2611
diff
changeset
|
201 |
apply(simp (no_asm_use) add: fresh_star_def) |
|
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:
2611
diff
changeset
|
202 |
apply(simp (no_asm_use) add: Abs_fresh_iff)[1] |
|
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:
2611
diff
changeset
|
203 |
apply(rule ballI) |
|
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:
2611
diff
changeset
|
204 |
apply(auto simp add: fresh_Pair)[1] |
|
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:
2611
diff
changeset
|
205 |
apply(simp (no_asm_use) only: permute_Abs) |
|
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:
2611
diff
changeset
|
206 |
apply(simp (no_asm_use) only: multi_recs.fv_bn_eqvt) |
|
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:
2611
diff
changeset
|
207 |
apply(simp) |
|
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:
2611
diff
changeset
|
208 |
apply(rule at_set_avoiding5) |
|
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:
2611
diff
changeset
|
209 |
apply(simp add: multi_recs.bn_finite) |
|
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:
2611
diff
changeset
|
210 |
apply(simp add: supp_Pair finite_supp) |
|
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:
2611
diff
changeset
|
211 |
apply(rule finite_sets_supp) |
|
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:
2611
diff
changeset
|
212 |
apply(simp add: multi_recs.bn_finite) |
|
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:
2611
diff
changeset
|
213 |
done |
|
2600
ca6b4bc7a871
kept the nested structure of constructors (belonging to one datatype)
Christian Urban <urbanc@in.tum.de>
parents:
2599
diff
changeset
|
214 |
|
|
2590
98dc38c250bb
added abs_rename_res lemma
Christian Urban <urbanc@in.tum.de>
parents:
2589
diff
changeset
|
215 |
|
|
2586
3ebc7ecfb0dd
disabled the Foo examples, because of heavy work
Christian Urban <urbanc@in.tum.de>
parents:
2585
diff
changeset
|
216 |
|
|
2588
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
217 |
lemma test6: |
|
2584
1eac050a36f4
completely different method fro deriving the exhaust lemma
Christian Urban <urbanc@in.tum.de>
parents:
2579
diff
changeset
|
218 |
fixes c::"'a::fs" |
|
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
|
219 |
assumes "\<And>name. y = Var name \<Longrightarrow> P" |
|
3d101f2f817c
simple cases for strong inducts done; infrastructure for the difficult ones is there
Christian Urban <urbanc@in.tum.de>
parents:
2609
diff
changeset
|
220 |
and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
|
2592
98236fbd8aa6
updated to Isabelle 2nd December
Christian Urban <urbanc@in.tum.de>
parents:
2591
diff
changeset
|
221 |
and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P"
|
|
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
|
222 |
and "\<And>a1 trm1 a2 trm2. \<lbrakk>((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c; y = Let1 a1 trm1 a2 trm2\<rbrakk> \<Longrightarrow> P" |
|
2588
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
223 |
and "\<exists>x1 x2 trm1 trm2. {atom x1, atom x2} \<sharp>* c \<and> y = Let2 x1 x2 trm1 trm2 \<Longrightarrow> P"
|
|
2584
1eac050a36f4
completely different method fro deriving the exhaust lemma
Christian Urban <urbanc@in.tum.de>
parents:
2579
diff
changeset
|
224 |
shows "P" |
|
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
|
225 |
apply(rule_tac y="y" in foo.exhaust(1)) |
|
2588
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
226 |
apply(rule assms(1)) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
227 |
apply(assumption) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
228 |
apply(rule assms(2)) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
229 |
apply(assumption) |
|
2598
b136721eedb2
automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents:
2594
diff
changeset
|
230 |
(* lam case *) |
|
2609
666ffc8a92a9
freshness theorem in strong exhausts; (temporarily includes a cheat_tac to make all tests go through)
Christian Urban <urbanc@in.tum.de>
parents:
2608
diff
changeset
|
231 |
apply(subgoal_tac "\<exists>p. (p \<bullet> {atom name}) \<sharp>* (c, name, trm)")
|
|
2584
1eac050a36f4
completely different method fro deriving the exhaust lemma
Christian Urban <urbanc@in.tum.de>
parents:
2579
diff
changeset
|
232 |
apply(erule exE) |
|
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
|
233 |
apply(insert Abs_rename_lst)[1] |
|
2588
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
234 |
apply(drule_tac x="p" in meta_spec) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
235 |
apply(drule_tac x="[atom name]" in meta_spec) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
236 |
apply(drule_tac x="trm" in meta_spec) |
|
2591
35c570891a3a
isarfied some of the high-level proofs
Christian Urban <urbanc@in.tum.de>
parents:
2590
diff
changeset
|
237 |
apply(simp only: fresh_star_Pair set.simps) |
|
2588
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
238 |
apply(drule meta_mp) |
|
2609
666ffc8a92a9
freshness theorem in strong exhausts; (temporarily includes a cheat_tac to make all tests go through)
Christian Urban <urbanc@in.tum.de>
parents:
2608
diff
changeset
|
239 |
apply(simp add: fresh_star_def fresh_Nil fresh_Cons fresh_atom_at_base) |
|
2588
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
240 |
apply(erule exE) |
|
2592
98236fbd8aa6
updated to Isabelle 2nd December
Christian Urban <urbanc@in.tum.de>
parents:
2591
diff
changeset
|
241 |
apply(rule assms(3)) |
|
2584
1eac050a36f4
completely different method fro deriving the exhaust lemma
Christian Urban <urbanc@in.tum.de>
parents:
2579
diff
changeset
|
242 |
apply(perm_simp) |
|
2588
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
243 |
apply(erule conjE)+ |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
244 |
apply(assumption) |
|
2592
98236fbd8aa6
updated to Isabelle 2nd December
Christian Urban <urbanc@in.tum.de>
parents:
2591
diff
changeset
|
245 |
apply(clarify) |
|
98236fbd8aa6
updated to Isabelle 2nd December
Christian Urban <urbanc@in.tum.de>
parents:
2591
diff
changeset
|
246 |
apply(simp (no_asm) add: foo.eq_iff) |
|
98236fbd8aa6
updated to Isabelle 2nd December
Christian Urban <urbanc@in.tum.de>
parents:
2591
diff
changeset
|
247 |
apply(perm_simp) |
|
98236fbd8aa6
updated to Isabelle 2nd December
Christian Urban <urbanc@in.tum.de>
parents:
2591
diff
changeset
|
248 |
apply(assumption) |
|
2589
9781db0e2196
completed proofs in Foo2
Christian Urban <urbanc@in.tum.de>
parents:
2588
diff
changeset
|
249 |
apply(rule at_set_avoiding1) |
|
9781db0e2196
completed proofs in Foo2
Christian Urban <urbanc@in.tum.de>
parents:
2588
diff
changeset
|
250 |
apply(simp) |
|
9781db0e2196
completed proofs in Foo2
Christian Urban <urbanc@in.tum.de>
parents:
2588
diff
changeset
|
251 |
apply(simp add: finite_supp) |
|
2598
b136721eedb2
automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents:
2594
diff
changeset
|
252 |
(* let1 case *) |
|
2588
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
253 |
apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2)") |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
254 |
apply(erule exE) |
|
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
|
255 |
apply(perm_simp add: foo.permute_bn) |
|
3d101f2f817c
simple cases for strong inducts done; infrastructure for the difficult ones is there
Christian Urban <urbanc@in.tum.de>
parents:
2609
diff
changeset
|
256 |
apply(simp add: fresh_star_Pair) |
|
3d101f2f817c
simple cases for strong inducts done; infrastructure for the difficult ones is there
Christian Urban <urbanc@in.tum.de>
parents:
2609
diff
changeset
|
257 |
apply(erule conjE)+ |
|
3d101f2f817c
simple cases for strong inducts done; infrastructure for the difficult ones is there
Christian Urban <urbanc@in.tum.de>
parents:
2609
diff
changeset
|
258 |
apply(insert Abs_rename_lst)[1] |
|
2588
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
259 |
apply(drule_tac x="p" in meta_spec) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
260 |
apply(drule_tac x="bn assg1" in meta_spec) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
261 |
apply(drule_tac x="trm1" in meta_spec) |
|
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
|
262 |
apply(insert Abs_rename_lst)[1] |
|
2588
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
263 |
apply(drule_tac x="p" in meta_spec) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
264 |
apply(drule_tac x="bn assg2" in meta_spec) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
265 |
apply(drule_tac x="trm2" in meta_spec) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
266 |
apply(drule meta_mp) |
|
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:
2611
diff
changeset
|
267 |
apply(perm_simp add: foo.permute_bn) |
|
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:
2611
diff
changeset
|
268 |
apply(simp add: fresh_star_Pair fresh_star_Un) |
|
2588
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
269 |
apply(drule meta_mp) |
|
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:
2611
diff
changeset
|
270 |
apply(perm_simp add: foo.permute_bn) |
|
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:
2611
diff
changeset
|
271 |
apply(simp add: fresh_star_Pair fresh_star_Un) |
|
2588
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
272 |
apply(erule exE)+ |
|
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
|
273 |
apply(rule assms(4)) |
|
3d101f2f817c
simple cases for strong inducts done; infrastructure for the difficult ones is there
Christian Urban <urbanc@in.tum.de>
parents:
2609
diff
changeset
|
274 |
apply(assumption) |
|
3d101f2f817c
simple cases for strong inducts done; infrastructure for the difficult ones is there
Christian Urban <urbanc@in.tum.de>
parents:
2609
diff
changeset
|
275 |
apply(simp add: foo.eq_iff refl) |
|
2588
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
276 |
apply(rule conjI) |
|
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:
2611
diff
changeset
|
277 |
apply(perm_simp add: foo.permute_bn) |
|
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
|
278 |
apply(rule refl) |
|
2584
1eac050a36f4
completely different method fro deriving the exhaust lemma
Christian Urban <urbanc@in.tum.de>
parents:
2579
diff
changeset
|
279 |
apply(rule conjI) |
|
2594
515e5496171c
automated alpha_perm_bn theorems
Christian Urban <urbanc@in.tum.de>
parents:
2593
diff
changeset
|
280 |
apply(rule foo.perm_bn_alpha) |
|
2588
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
281 |
apply(rule conjI) |
|
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:
2611
diff
changeset
|
282 |
apply(perm_simp add: foo.permute_bn) |
|
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
|
283 |
apply(rule refl) |
|
2594
515e5496171c
automated alpha_perm_bn theorems
Christian Urban <urbanc@in.tum.de>
parents:
2593
diff
changeset
|
284 |
apply(rule foo.perm_bn_alpha) |
|
2589
9781db0e2196
completed proofs in Foo2
Christian Urban <urbanc@in.tum.de>
parents:
2588
diff
changeset
|
285 |
apply(rule at_set_avoiding1) |
|
9781db0e2196
completed proofs in Foo2
Christian Urban <urbanc@in.tum.de>
parents:
2588
diff
changeset
|
286 |
apply(simp) |
|
9781db0e2196
completed proofs in Foo2
Christian Urban <urbanc@in.tum.de>
parents:
2588
diff
changeset
|
287 |
apply(simp add: finite_supp) |
|
2598
b136721eedb2
automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents:
2594
diff
changeset
|
288 |
(* let2 case *) |
|
2588
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
289 |
apply(subgoal_tac "\<exists>p. (p \<bullet> ({atom name1} \<union> {atom name2})) \<sharp>* (c, atom name1, atom name2, trm1, trm2)")
|
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
290 |
apply(erule exE) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
291 |
apply(rule assms(5)) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
292 |
apply(simp only:) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
293 |
apply(simp only: foo.eq_iff) |
|
2591
35c570891a3a
isarfied some of the high-level proofs
Christian Urban <urbanc@in.tum.de>
parents:
2590
diff
changeset
|
294 |
apply(insert Abs_rename_list)[1] |
|
2588
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
295 |
apply(drule_tac x="p" in meta_spec) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
296 |
apply(drule_tac x="[atom name1] @ [atom name2]" in meta_spec) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
297 |
apply(drule_tac x="trm1" in meta_spec) |
|
2591
35c570891a3a
isarfied some of the high-level proofs
Christian Urban <urbanc@in.tum.de>
parents:
2590
diff
changeset
|
298 |
apply(insert Abs_rename_list)[1] |
|
2588
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
299 |
apply(drule_tac x="p" in meta_spec) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
300 |
apply(drule_tac x="[atom name2]" in meta_spec) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
301 |
apply(drule_tac x="trm2" in meta_spec) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
302 |
apply(drule meta_mp) |
|
2591
35c570891a3a
isarfied some of the high-level proofs
Christian Urban <urbanc@in.tum.de>
parents:
2590
diff
changeset
|
303 |
apply(simp only: union_eqvt fresh_star_Pair fresh_star_list fresh_star_Un, simp) |
|
35c570891a3a
isarfied some of the high-level proofs
Christian Urban <urbanc@in.tum.de>
parents:
2590
diff
changeset
|
304 |
apply(auto)[1] |
|
35c570891a3a
isarfied some of the high-level proofs
Christian Urban <urbanc@in.tum.de>
parents:
2590
diff
changeset
|
305 |
apply(perm_simp) |
|
35c570891a3a
isarfied some of the high-level proofs
Christian Urban <urbanc@in.tum.de>
parents:
2590
diff
changeset
|
306 |
apply(auto simp add: fresh_star_def)[1] |
|
35c570891a3a
isarfied some of the high-level proofs
Christian Urban <urbanc@in.tum.de>
parents:
2590
diff
changeset
|
307 |
apply(perm_simp) |
|
35c570891a3a
isarfied some of the high-level proofs
Christian Urban <urbanc@in.tum.de>
parents:
2590
diff
changeset
|
308 |
apply(auto simp add: fresh_star_def)[1] |
|
35c570891a3a
isarfied some of the high-level proofs
Christian Urban <urbanc@in.tum.de>
parents:
2590
diff
changeset
|
309 |
apply(perm_simp) |
|
35c570891a3a
isarfied some of the high-level proofs
Christian Urban <urbanc@in.tum.de>
parents:
2590
diff
changeset
|
310 |
apply(auto simp add: fresh_star_def)[1] |
|
2588
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
311 |
apply(drule meta_mp) |
|
2591
35c570891a3a
isarfied some of the high-level proofs
Christian Urban <urbanc@in.tum.de>
parents:
2590
diff
changeset
|
312 |
apply(perm_simp) |
|
35c570891a3a
isarfied some of the high-level proofs
Christian Urban <urbanc@in.tum.de>
parents:
2590
diff
changeset
|
313 |
apply(auto simp add: fresh_star_def fresh_Pair fresh_Nil fresh_Cons)[1] |
|
2588
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
314 |
apply(erule exE)+ |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
315 |
apply(rule exI)+ |
|
2598
b136721eedb2
automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents:
2594
diff
changeset
|
316 |
apply(perm_simp add: foo.permute_bn) |
|
2588
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
317 |
apply(rule conjI) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
318 |
prefer 2 |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
319 |
apply(rule conjI) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
320 |
apply(assumption) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
321 |
apply(assumption) |
|
2591
35c570891a3a
isarfied some of the high-level proofs
Christian Urban <urbanc@in.tum.de>
parents:
2590
diff
changeset
|
322 |
apply(simp add: fresh_star_Pair) |
|
2588
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
323 |
apply(simp add: fresh_star_def) |
|
2589
9781db0e2196
completed proofs in Foo2
Christian Urban <urbanc@in.tum.de>
parents:
2588
diff
changeset
|
324 |
apply(rule at_set_avoiding1) |
|
9781db0e2196
completed proofs in Foo2
Christian Urban <urbanc@in.tum.de>
parents:
2588
diff
changeset
|
325 |
apply(simp) |
|
9781db0e2196
completed proofs in Foo2
Christian Urban <urbanc@in.tum.de>
parents:
2588
diff
changeset
|
326 |
apply(simp add: finite_supp) |
|
9781db0e2196
completed proofs in Foo2
Christian Urban <urbanc@in.tum.de>
parents:
2588
diff
changeset
|
327 |
done |
|
2584
1eac050a36f4
completely different method fro deriving the exhaust lemma
Christian Urban <urbanc@in.tum.de>
parents:
2579
diff
changeset
|
328 |
|
|
2585
385add25dedf
slightly simplified the Foo2 tests and hint at a general lemma
Christian Urban <urbanc@in.tum.de>
parents:
2584
diff
changeset
|
329 |
lemma test5: |
|
385add25dedf
slightly simplified the Foo2 tests and hint at a general lemma
Christian Urban <urbanc@in.tum.de>
parents:
2584
diff
changeset
|
330 |
fixes c::"'a::fs" |
|
385add25dedf
slightly simplified the Foo2 tests and hint at a general lemma
Christian Urban <urbanc@in.tum.de>
parents:
2584
diff
changeset
|
331 |
assumes "\<And>name. y = Var name \<Longrightarrow> P" |
|
385add25dedf
slightly simplified the Foo2 tests and hint at a general lemma
Christian Urban <urbanc@in.tum.de>
parents:
2584
diff
changeset
|
332 |
and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
|
385add25dedf
slightly simplified the Foo2 tests and hint at a general lemma
Christian Urban <urbanc@in.tum.de>
parents:
2584
diff
changeset
|
333 |
and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P"
|
|
2588
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
334 |
and "\<And>a1 trm1 a2 trm2. \<lbrakk>((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c; y = Let1 a1 trm1 a2 trm2\<rbrakk> \<Longrightarrow> P" |
|
2585
385add25dedf
slightly simplified the Foo2 tests and hint at a general lemma
Christian Urban <urbanc@in.tum.de>
parents:
2584
diff
changeset
|
335 |
and "\<And>x1 x2 trm1 trm2. \<lbrakk>{atom x1, atom x2} \<sharp>* c; y = Let2 x1 x2 trm1 trm2\<rbrakk> \<Longrightarrow> P"
|
|
385add25dedf
slightly simplified the Foo2 tests and hint at a general lemma
Christian Urban <urbanc@in.tum.de>
parents:
2584
diff
changeset
|
336 |
shows "P" |
|
2588
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
337 |
apply(rule_tac y="y" in test6) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
338 |
apply(erule exE)+ |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
339 |
apply(rule assms(1)) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
340 |
apply(assumption) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
341 |
apply(erule exE)+ |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
342 |
apply(rule assms(2)) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
343 |
apply(assumption) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
344 |
apply(rule assms(3)) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
345 |
apply(auto)[2] |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
346 |
apply(erule exE)+ |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
347 |
apply(rule assms(4)) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
348 |
apply(auto)[2] |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
349 |
apply(erule exE)+ |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
350 |
apply(rule assms(5)) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
351 |
apply(auto)[2] |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
352 |
done |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
353 |
|
|
2585
385add25dedf
slightly simplified the Foo2 tests and hint at a general lemma
Christian Urban <urbanc@in.tum.de>
parents:
2584
diff
changeset
|
354 |
|
|
2588
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
355 |
lemma strong_induct: |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
356 |
fixes c :: "'a :: fs" |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
357 |
and assg :: assg and trm :: trm |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
358 |
assumes a0: "\<And>name c. P1 c (Var name)" |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
359 |
and a1: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (App trm1 trm2)" |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
360 |
and a2: "\<And>name trm c. (\<And>d. P1 d trm) \<Longrightarrow> P1 c (Lam name trm)" |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
361 |
and a3: "\<And>a1 t1 a2 t2 c. |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
362 |
\<lbrakk>((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c; \<And>d. P2 c a1; \<And>d. P1 d t1; \<And>d. P2 d a2; \<And>d. P1 d t2\<rbrakk> |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
363 |
\<Longrightarrow> P1 c (Let1 a1 t1 a2 t2)" |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
364 |
and a4: "\<And>n1 n2 t1 t2 c. |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
365 |
\<lbrakk>{atom n1, atom n2} \<sharp>* c; \<And>d. P1 d t1; \<And>d. P1 d t2\<rbrakk> \<Longrightarrow> P1 c (Let2 n1 n2 t1 t2)"
|
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
366 |
and a5: "\<And>c. P2 c As_Nil" |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
367 |
and a6: "\<And>name1 name2 trm assg c. \<lbrakk>\<And>d. P1 d trm; \<And>d. P2 d assg\<rbrakk> \<Longrightarrow> P2 c (As name1 name2 trm assg)" |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
368 |
shows "P1 c trm" "P2 c assg" |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
369 |
using assms |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
370 |
apply(induction_schema) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
371 |
apply(rule_tac y="trm" and c="c" in test5) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
372 |
apply(simp_all)[5] |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
373 |
apply(rule_tac y="assg" in foo.exhaust(2)) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
374 |
apply(simp_all)[2] |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
375 |
apply(relation "measure (sum_case (size o snd) (size o snd))") |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
376 |
apply(simp_all add: foo.size) |
|
8f5420681039
completed the strong exhausts rules for Foo2 using general lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2586
diff
changeset
|
377 |
done |
|
2584
1eac050a36f4
completely different method fro deriving the exhaust lemma
Christian Urban <urbanc@in.tum.de>
parents:
2579
diff
changeset
|
378 |
|
| 2573 | 379 |
end |
380 |
||
381 |
||
382 |