| author | Christian Urban <urbanc@in.tum.de> |
| Sun, 08 Aug 2010 10:12:38 +0800 | |
| changeset 2392 | 9294d7cec5e2 |
| parent 2311 | 4da5c5c29009 |
| child 2434 | 92dc6cfa3a95 |
| permissions | -rw-r--r-- |
|
1792
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
theory Classical |
|
2008
1bddffddc03f
attempted to remove dependency on (old) Fv and (old) Parser; lifting still uses Fv.thy; the examples do not work at the moment (with equivp proofs failing)
Christian Urban <urbanc@in.tum.de>
parents:
1866
diff
changeset
|
2 |
imports "../NewParser" |
|
1792
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
begin |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
|
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
(* example from my Urban's PhD *) |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
6 |
|
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
atom_decl name |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
8 |
atom_decl coname |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
|
|
2308
387fcbd33820
fixed problem with bn_info
Christian Urban <urbanc@in.tum.de>
parents:
2120
diff
changeset
|
10 |
declare [[STEPS = 9]] |
|
2031
d361a4699176
Added cheats to classical
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2008
diff
changeset
|
11 |
|
|
1792
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
12 |
nominal_datatype trm = |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
Ax "name" "coname" |
|
2311
4da5c5c29009
work on transitivity proof
Christian Urban <urbanc@in.tum.de>
parents:
2308
diff
changeset
|
14 |
| Cut n::"coname" t1::"trm" c::"coname" t2::"trm" bind n in t1, bind c in t2 |
|
4da5c5c29009
work on transitivity proof
Christian Urban <urbanc@in.tum.de>
parents:
2308
diff
changeset
|
15 |
| AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind c1 in t1, bind c2 in t2 |
|
4da5c5c29009
work on transitivity proof
Christian Urban <urbanc@in.tum.de>
parents:
2308
diff
changeset
|
16 |
| AndL1 n::"name" t::"trm" "name" bind n in t |
|
4da5c5c29009
work on transitivity proof
Christian Urban <urbanc@in.tum.de>
parents:
2308
diff
changeset
|
17 |
| AndL2 n::"name" t::"trm" "name" bind n in t |
|
4da5c5c29009
work on transitivity proof
Christian Urban <urbanc@in.tum.de>
parents:
2308
diff
changeset
|
18 |
| ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" bind c in t1, bind n in t2 |
|
4da5c5c29009
work on transitivity proof
Christian Urban <urbanc@in.tum.de>
parents:
2308
diff
changeset
|
19 |
| ImpR c::"coname" n::"name" t::"trm" "coname" bind n c in t |
|
1792
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
20 |
|
|
2308
387fcbd33820
fixed problem with bn_info
Christian Urban <urbanc@in.tum.de>
parents:
2120
diff
changeset
|
21 |
thm alpha_trm_raw.intros[no_vars] |
|
1792
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
22 |
|
|
2308
387fcbd33820
fixed problem with bn_info
Christian Urban <urbanc@in.tum.de>
parents:
2120
diff
changeset
|
23 |
(* |
|
1792
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
24 |
thm trm.fv |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
25 |
thm trm.eq_iff |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
26 |
thm trm.bn |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
27 |
thm trm.perm |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
28 |
thm trm.induct |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
29 |
thm trm.distinct |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
30 |
thm trm.fv[simplified trm.supp] |
|
2308
387fcbd33820
fixed problem with bn_info
Christian Urban <urbanc@in.tum.de>
parents:
2120
diff
changeset
|
31 |
*) |
|
1866
6d4e4bf9bce6
automatic proofs for equivariance of alphas
Christian Urban <urbanc@in.tum.de>
parents:
1792
diff
changeset
|
32 |
|
|
1792
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
33 |
|
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
34 |
end |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
35 |
|
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
36 |
|
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
37 |