1600
|
1 |
theory ExPS3
|
2053
|
2 |
imports "../NewParser"
|
1600
|
3 |
begin
|
|
4 |
|
|
5 |
(* example 3 from Peter Sewell's bestiary *)
|
|
6 |
|
|
7 |
atom_decl name
|
|
8 |
|
2053
|
9 |
ML {* val _ = cheat_equivp := true *}
|
|
10 |
ML {* val _ = cheat_alpha_bn_rsp := true *}
|
|
11 |
|
1600
|
12 |
nominal_datatype exp =
|
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
13 |
Var "name"
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
14 |
| App "exp" "exp"
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
15 |
| Lam x::"name" e::"exp" bind_set x in e
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
16 |
| Let x::"name" p::"pat" e1::"exp" e2::"exp" bind_set x in e2, bind_set "bp p" in e1
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
17 |
and pat =
|
1600
|
18 |
PVar "name"
|
|
19 |
| PUnit
|
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
20 |
| PPair "pat" "pat"
|
1600
|
21 |
binder
|
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
22 |
bp :: "pat \<Rightarrow> atom set"
|
1600
|
23 |
where
|
1656
|
24 |
"bp (PVar x) = {atom x}"
|
|
25 |
| "bp (PUnit) = {}"
|
|
26 |
| "bp (PPair p1 p2) = bp p1 \<union> bp p2"
|
1600
|
27 |
|
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
28 |
thm exp_pat.fv
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
29 |
thm exp_pat.eq_iff
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
30 |
thm exp_pat.bn
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
31 |
thm exp_pat.perm
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
32 |
thm exp_pat.induct
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
33 |
thm exp_pat.distinct
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
34 |
thm exp_pat.fv
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
35 |
thm exp_pat.supp(1-2)
|
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
36 |
|
2120
2786ff1df475
fixed the examples for the new eqvt-procedure....temporarily disabled Manual/Term4.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
37 |
|
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
38 |
|
1600
|
39 |
|
|
40 |
end
|
|
41 |
|
|
42 |
|
|
43 |
|