| author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
| Wed, 10 Mar 2010 11:39:28 +0100 | |
| changeset 1391 | ebfbcadeac5e |
| parent 1288 | 0203cd5cfd6c |
| child 1399 | 40e1646ff934 |
| permissions | -rw-r--r-- |
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
1 |
theory Term5 |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
2 |
imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
3 |
begin |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
4 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
5 |
atom_decl name |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
6 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
7 |
datatype rtrm5 = |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
8 |
rVr5 "name" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
9 |
| rAp5 "rtrm5" "rtrm5" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
10 |
| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
11 |
and rlts = |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
12 |
rLnil |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
13 |
| rLcons "name" "rtrm5" "rlts" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
14 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
15 |
primrec |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
16 |
rbv5 |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
17 |
where |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
18 |
"rbv5 rLnil = {}"
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
19 |
| "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
20 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
21 |
|
|
1277
6eacf60ce41d
Permutation and FV_Alpha interface change.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1270
diff
changeset
|
22 |
setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term5.rtrm5") 2 *}
|
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
23 |
print_theorems |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
24 |
|
|
1391
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
25 |
local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term5.rtrm5")
|
|
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
26 |
[[[], [], [(SOME (@{term rbv5}, true), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [0, 2]])] *}
|
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
27 |
print_theorems |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
28 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
29 |
notation |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
30 |
alpha_rtrm5 ("_ \<approx>5 _" [100, 100] 100) and
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
31 |
alpha_rlts ("_ \<approx>l _" [100, 100] 100)
|
|
1391
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
32 |
thm alpha_rtrm5_alpha_rlts_alpha_rbv5.intros |
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
33 |
|
|
1391
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
34 |
local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} ctxt)) ctxt)) *}
|
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
35 |
thm alpha5_inj |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
36 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
37 |
lemma rbv5_eqvt[eqvt]: |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
38 |
"pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
39 |
apply (induct x) |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
40 |
apply (simp_all add: eqvts atom_eqvt) |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
41 |
done |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
42 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
43 |
lemma fv_rtrm5_rlts_eqvt[eqvt]: |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
44 |
"pi \<bullet> (fv_rtrm5 x) = fv_rtrm5 (pi \<bullet> x)" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
45 |
"pi \<bullet> (fv_rlts l) = fv_rlts (pi \<bullet> l)" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
46 |
apply (induct x and l) |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
47 |
apply (simp_all add: eqvts atom_eqvt) |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
48 |
done |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
49 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
50 |
lemma alpha5_eqvt: |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
51 |
"xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
52 |
"xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)" |
|
1391
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
53 |
"alpha_rbv5 a b c \<Longrightarrow> True" |
|
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
54 |
apply (induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) |
|
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
55 |
apply (simp_all add: alpha5_inj) |
|
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
56 |
apply (erule exE) |
|
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
57 |
apply (rule_tac x="pi" in exI) |
|
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
58 |
apply clarify |
|
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
59 |
apply (simp add: alpha_gen fv_rtrm5_rlts_eqvt[symmetric] rbv5_eqvt[symmetric]) |
|
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
60 |
apply (subst eqvts[symmetric]) |
|
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
61 |
apply (subst eqvts[symmetric]) |
|
1288
0203cd5cfd6c
The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1287
diff
changeset
|
62 |
sorry |
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
63 |
|
|
1288
0203cd5cfd6c
The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1287
diff
changeset
|
64 |
lemma alpha5_equivp: |
|
0203cd5cfd6c
The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1287
diff
changeset
|
65 |
"equivp alpha_rtrm5" |
|
0203cd5cfd6c
The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1287
diff
changeset
|
66 |
"equivp alpha_rlts" |
|
0203cd5cfd6c
The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1287
diff
changeset
|
67 |
sorry |
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
68 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
69 |
quotient_type |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
70 |
trm5 = rtrm5 / alpha_rtrm5 |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
71 |
and |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
72 |
lts = rlts / alpha_rlts |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
73 |
by (auto intro: alpha5_equivp) |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
74 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
75 |
local_setup {*
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
76 |
(fn ctxt => ctxt |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
77 |
|> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5}))
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
78 |
|> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5}))
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
79 |
|> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5}))
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
80 |
|> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil}))
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
81 |
|> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons}))
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
82 |
|> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5}))
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
83 |
|> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts}))
|
|
1391
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
84 |
|> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5}))
|
|
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
85 |
|> snd o (Quotient_Def.quotient_lift_const ("alpha_bv5", @{term alpha_rbv5})))
|
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
86 |
*} |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
87 |
print_theorems |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
88 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
89 |
lemma alpha5_rfv: |
|
1391
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
90 |
"(t \<approx>5 s \<longrightarrow> fv_rtrm5 t = fv_rtrm5 s) \<and> (l \<approx>l m \<longrightarrow> fv_rlts l = fv_rlts m) \<and> (alpha_rbv5 a b c \<longrightarrow> True)" |
|
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
91 |
apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) |
|
1288
0203cd5cfd6c
The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1287
diff
changeset
|
92 |
apply(simp_all) |
|
0203cd5cfd6c
The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1287
diff
changeset
|
93 |
apply(simp add: alpha_gen) |
|
0203cd5cfd6c
The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1287
diff
changeset
|
94 |
apply(erule conjE)+ |
|
0203cd5cfd6c
The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1287
diff
changeset
|
95 |
apply(erule exE) |
|
0203cd5cfd6c
The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1287
diff
changeset
|
96 |
apply(erule conjE)+ |
|
0203cd5cfd6c
The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1287
diff
changeset
|
97 |
apply(simp_all) |
|
1391
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
98 |
sorry |
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
99 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
100 |
lemma bv_list_rsp: |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
101 |
shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y" |
|
1391
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
102 |
apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) |
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
103 |
apply(simp_all) |
|
1288
0203cd5cfd6c
The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1287
diff
changeset
|
104 |
apply(clarify) |
|
0203cd5cfd6c
The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1287
diff
changeset
|
105 |
apply simp |
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
106 |
done |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
107 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
108 |
lemma [quot_respect]: |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
109 |
"(alpha_rlts ===> op =) fv_rlts fv_rlts" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
110 |
"(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
111 |
"(alpha_rlts ===> op =) rbv5 rbv5" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
112 |
"(op = ===> alpha_rtrm5) rVr5 rVr5" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
113 |
"(alpha_rtrm5 ===> alpha_rtrm5 ===> alpha_rtrm5) rAp5 rAp5" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
114 |
"(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
115 |
"(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
116 |
"(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
117 |
"(op = ===> alpha_rlts ===> alpha_rlts) permute permute" |
|
1391
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
118 |
"(op = ===> alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5" |
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
119 |
apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp) |
|
1288
0203cd5cfd6c
The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1287
diff
changeset
|
120 |
apply (clarify) |
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
121 |
apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
|
1391
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
122 |
defer |
|
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
123 |
apply clarify |
|
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
124 |
apply (erule alpha_rlts.cases) |
|
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
125 |
apply (erule alpha_rlts.cases) |
|
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
126 |
apply (simp_all) |
|
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
127 |
defer |
|
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
128 |
apply (erule alpha_rlts.cases) |
|
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
129 |
apply (simp_all) |
|
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
130 |
defer |
|
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
131 |
apply clarify |
|
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
132 |
apply (simp add: alpha5_inj) |
|
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
133 |
sorry (* may be true? *) |
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
134 |
lemma |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
135 |
shows "(alpha_rlts ===> op =) rbv5 rbv5" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
136 |
by (simp add: bv_list_rsp) |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
137 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
138 |
lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted] |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
139 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
140 |
instantiation trm5 and lts :: pt |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
141 |
begin |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
142 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
143 |
quotient_definition |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
144 |
"permute_trm5 :: perm \<Rightarrow> trm5 \<Rightarrow> trm5" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
145 |
is |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
146 |
"permute :: perm \<Rightarrow> rtrm5 \<Rightarrow> rtrm5" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
147 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
148 |
quotient_definition |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
149 |
"permute_lts :: perm \<Rightarrow> lts \<Rightarrow> lts" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
150 |
is |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
151 |
"permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
152 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
153 |
instance by default |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
154 |
(simp_all add: permute_rtrm5_permute_rlts_zero[quot_lifted] permute_rtrm5_permute_rlts_append[quot_lifted]) |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
155 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
156 |
end |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
157 |
|
|
1391
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
158 |
lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted] |
|
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
159 |
lemmas bv5[simp] = rbv5.simps[quot_lifted] |
|
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
160 |
lemmas fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] |
|
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
161 |
lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
162 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
163 |
lemma lets_ok: |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
164 |
"(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
|
1288
0203cd5cfd6c
The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1287
diff
changeset
|
165 |
apply (simp add: alpha5_INJ) |
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
166 |
apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
1288
0203cd5cfd6c
The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1287
diff
changeset
|
167 |
apply (simp_all add: alpha_gen) |
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
168 |
apply (simp add: permute_trm5_lts fresh_star_def) |
|
1391
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
169 |
apply (metis flip_at_simps(1) supp_at_base supp_eqvt) |
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
170 |
done |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
171 |
|
|
1286
87894b5156f4
Example that shows that current alpha is wrong.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1277
diff
changeset
|
172 |
lemma lets_ok3: |
|
1288
0203cd5cfd6c
The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1287
diff
changeset
|
173 |
"x \<noteq> y \<Longrightarrow> |
|
0203cd5cfd6c
The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1287
diff
changeset
|
174 |
(Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
|
0203cd5cfd6c
The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1287
diff
changeset
|
175 |
(Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
|
0203cd5cfd6c
The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1287
diff
changeset
|
176 |
apply (simp add: permute_trm5_lts alpha_gen alpha5_INJ) |
|
1286
87894b5156f4
Example that shows that current alpha is wrong.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1277
diff
changeset
|
177 |
done |
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
178 |
|
|
1288
0203cd5cfd6c
The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1287
diff
changeset
|
179 |
|
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
180 |
lemma lets_not_ok1: |
|
1391
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
181 |
"(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) = |
|
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
182 |
(Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
|
1288
0203cd5cfd6c
The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1287
diff
changeset
|
183 |
apply (simp add: alpha5_INJ alpha_gen) |
|
1391
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
184 |
apply (rule_tac x="0::perm" in exI) |
|
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
185 |
apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1) eqvts) |
|
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
186 |
apply auto |
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
187 |
done |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
188 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
189 |
lemma distinct_helper: |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
190 |
shows "\<not>(rVr5 x \<approx>5 rAp5 y z)" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
191 |
apply auto |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
192 |
apply (erule alpha_rtrm5.cases) |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
193 |
apply (simp_all only: rtrm5.distinct) |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
194 |
done |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
195 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
196 |
lemma distinct_helper2: |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
197 |
shows "(Vr5 x) \<noteq> (Ap5 y z)" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
198 |
by (lifting distinct_helper) |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
199 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
200 |
lemma lets_nok: |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
201 |
"x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow> |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
202 |
(Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
203 |
(Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
204 |
apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def) |
|
1391
ebfbcadeac5e
Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1288
diff
changeset
|
205 |
apply (simp add: distinct_helper2 alpha5_INJ permute_trm5_lts) |
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
206 |
done |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
207 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
208 |
end |