| author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
| Sat, 27 Mar 2010 08:17:43 +0100 | |
| changeset 1672 | 94b8b70f7bc0 |
| parent 1595 | aeed597d2043 |
| permissions | -rw-r--r-- |
|
1595
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
1 |
theory TestMorePerm |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
2 |
imports "Parser" |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
3 |
begin |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
4 |
|
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
5 |
(* Since there are more permutations, we do not know how to prove equivalence |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
6 |
(it is probably not true with the way alpha is defined now) so *) |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
7 |
ML {* val _ = cheat_equivp := true *}
|
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
8 |
|
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
9 |
|
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
10 |
atom_decl name |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
11 |
|
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
12 |
(* example from my PHD *) |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
13 |
|
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
14 |
atom_decl coname |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
15 |
|
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
16 |
nominal_datatype phd = |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
17 |
Ax "name" "coname" |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
18 |
| Cut n::"coname" t1::"phd" c::"coname" t2::"phd" bind n in t1, bind c in t2 |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
19 |
| AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname" bind c1 in t1, bind c2 in t2 |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
20 |
| AndL1 n::"name" t::"phd" "name" bind n in t |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
21 |
| AndL2 n::"name" t::"phd" "name" bind n in t |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
22 |
| ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name" bind c in t1, bind n in t2 |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
23 |
| ImpR c::"coname" n::"name" t::"phd" "coname" bind n in t, bind c in t |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
24 |
|
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
25 |
thm phd.fv |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
26 |
thm phd.eq_iff |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
27 |
thm phd.bn |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
28 |
thm phd.perm |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
29 |
thm phd.induct |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
30 |
thm phd.distinct |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
31 |
thm phd.fv[simplified phd.supp] |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
32 |
|
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
33 |
text {* weirdo example from Peter Sewell's bestiary *}
|
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
34 |
|
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
35 |
nominal_datatype weird = |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
36 |
WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird" |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
37 |
bind x in p1, bind x in p2, bind y in p2, bind y in p3 |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
38 |
| WV "name" |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
39 |
| WP "weird" "weird" |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
40 |
|
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
41 |
thm permute_weird_raw.simps[no_vars] |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
42 |
thm alpha_weird_raw.intros[no_vars] |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
43 |
thm fv_weird_raw.simps[no_vars] |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
44 |
|
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
45 |
|
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
46 |
end |
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
47 |
|
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
48 |
|
|
aeed597d2043
Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
49 |