| author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
| Mon, 19 Dec 2011 16:39:20 +0900 | |
| changeset 3078 | abf147627b4b |
| parent 2950 | 0911cb7bf696 |
| child 3235 | 5ebd327ffb96 |
| permissions | -rw-r--r-- |
|
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
theory LetSimple1 |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
imports "../Nominal2" |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
begin |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
|
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
atom_decl name |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
6 |
|
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
nominal_datatype trm = |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
8 |
Var "name" |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
| App "trm" "trm" |
|
2950
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents:
2943
diff
changeset
|
10 |
| Let x::"name" "trm" t::"trm" binds x in t |
|
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
11 |
|
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
12 |
print_theorems |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
|
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
14 |
thm trm.fv_defs |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
15 |
thm trm.eq_iff |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
16 |
thm trm.bn_defs |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
17 |
thm trm.bn_inducts |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
18 |
thm trm.perm_simps |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
19 |
thm trm.induct |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
20 |
thm trm.inducts |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
21 |
thm trm.distinct |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
22 |
thm trm.supp |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
23 |
thm trm.fresh |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
24 |
thm trm.exhaust |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
25 |
thm trm.strong_exhaust |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
26 |
thm trm.perm_bn_simps |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
27 |
|
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
28 |
nominal_primrec |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
29 |
height_trm :: "trm \<Rightarrow> nat" |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
30 |
where |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
31 |
"height_trm (Var x) = 1" |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
32 |
| "height_trm (App l r) = max (height_trm l) (height_trm r)" |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
33 |
| "height_trm (Let x t s) = max (height_trm t) (height_trm s)" |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
34 |
apply (simp only: eqvt_def height_trm_graph_def) |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
35 |
apply (rule, perm_simp, rule, rule TrueI) |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
36 |
apply (case_tac x rule: trm.exhaust(1)) |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
37 |
apply (auto)[3] |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
38 |
apply(simp_all)[5] |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
39 |
apply (subgoal_tac "height_trm_sumC t = height_trm_sumC ta") |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
40 |
apply (subgoal_tac "height_trm_sumC s = height_trm_sumC sa") |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
41 |
apply simp |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
42 |
apply(simp) |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
43 |
apply(erule conjE) |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
44 |
apply(erule_tac c="()" in Abs_lst1_fcb2) |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
45 |
apply(simp_all add: fresh_star_def pure_fresh)[2] |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
46 |
apply(simp_all add: eqvt_at_def)[2] |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
47 |
apply(simp) |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
48 |
done |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
49 |
|
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
50 |
termination |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
51 |
by lexicographic_order |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
52 |
|
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
53 |
|
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
54 |
nominal_primrec (invariant "\<lambda>x (y::atom set). finite y") |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
55 |
frees_set :: "trm \<Rightarrow> atom set" |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
56 |
where |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
57 |
"frees_set (Var x) = {atom x}"
|
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
58 |
| "frees_set (App t1 t2) = frees_set t1 \<union> frees_set t2" |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
59 |
| "frees_set (Let x t s) = (frees_set s) - {atom x} \<union> (frees_set t)"
|
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
60 |
apply(simp add: eqvt_def frees_set_graph_def) |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
61 |
apply(rule, perm_simp, rule) |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
62 |
apply(erule frees_set_graph.induct) |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
63 |
apply(auto)[3] |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
64 |
apply(rule_tac y="x" in trm.exhaust) |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
65 |
apply(auto)[3] |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
66 |
apply(simp_all)[5] |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
67 |
apply(simp) |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
68 |
apply(erule conjE) |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
69 |
apply(subgoal_tac "frees_set_sumC s - {atom x} = frees_set_sumC sa - {atom xa}")
|
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
70 |
apply(simp) |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
71 |
apply(erule_tac c="()" in Abs_lst1_fcb2) |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
72 |
apply(simp add: fresh_minus_atom_set) |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
73 |
apply(simp add: fresh_star_def fresh_Unit) |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
74 |
apply(simp add: Diff_eqvt eqvt_at_def, perm_simp, rule refl) |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
75 |
apply(simp add: Diff_eqvt eqvt_at_def, perm_simp, rule refl) |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
76 |
done |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
77 |
|
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
78 |
termination |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
79 |
by lexicographic_order |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
80 |
|
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
81 |
|
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
82 |
nominal_primrec |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
83 |
subst :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_ [_ ::= _]" [90, 90, 90] 90)
|
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
84 |
where |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
85 |
"(Var x)[y ::= s] = (if x = y then s else (Var x))" |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
86 |
| "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
87 |
| "atom x \<sharp> (y, s) \<Longrightarrow> (Let x t t')[y ::= s] = Let x (t[y ::= s]) (t'[y ::= s])" |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
88 |
apply(simp add: eqvt_def subst_graph_def) |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
89 |
apply (rule, perm_simp, rule) |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
90 |
apply(rule TrueI) |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
91 |
apply(auto)[1] |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
92 |
apply(rule_tac y="a" and c="(aa, b)" in trm.strong_exhaust) |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
93 |
apply(blast)+ |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
94 |
apply(simp_all add: fresh_star_def fresh_Pair_elim)[1] |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
95 |
apply(blast) |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
96 |
apply(simp_all)[5] |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
97 |
apply(simp (no_asm_use)) |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
98 |
apply(simp) |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
99 |
apply(erule conjE)+ |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
100 |
apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2) |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
101 |
apply(simp add: Abs_fresh_iff) |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
102 |
apply(simp add: fresh_star_def fresh_Pair) |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
103 |
apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
104 |
apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
105 |
done |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
106 |
|
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
107 |
termination |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
108 |
by lexicographic_order |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
109 |
|
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
110 |
|
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
111 |
end |