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>
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 |