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>
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
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
+ − 10
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
+ − 11
Ax "name" "coname"
2311
+ − 12
| Cut n::"coname" t1::"trm" c::"coname" t2::"trm" bind n in t1, bind c in t2
+ − 13
| AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind c1 in t1, bind c2 in t2
+ − 14
| AndL1 n::"name" t::"trm" "name" bind n in t
+ − 15
| AndL2 n::"name" t::"trm" "name" bind n in t
+ − 16
| ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" bind c in t1, bind n in t2
+ − 17
| 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
+ − 18
2436
+ − 19
thm trm.distinct
+ − 20
thm trm.induct
+ − 21
thm trm.exhaust
+ − 22
thm trm.fv_defs
+ − 23
thm trm.bn_defs
+ − 24
thm trm.perm_simps
+ − 25
thm trm.eq_iff
+ − 26
thm trm.fv_bn_eqvt
+ − 27
thm trm.size_eqvt
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
+ − 28
2434
+ − 29
1866
+ − 30
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
+ − 31
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
+ − 32
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
+ − 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
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