| author | Christian Urban <christian dot urban at kcl dot ac dot uk> |
| Mon, 19 May 2014 12:45:26 +0100 | |
| changeset 3235 | 5ebd327ffb96 |
| parent 3197 | 25d11b449e92 |
| child 3236 | e2da10806a34 |
| permissions | -rw-r--r-- |
|
2436
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2311
diff
changeset
|
1 |
theory LetRec |
|
2454
9ffee4eb1ae1
renamed NewParser to Nominal2
Christian Urban <urbanc@in.tum.de>
parents:
2438
diff
changeset
|
2 |
imports "../Nominal2" |
|
1596
c69d9fb16785
Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
3 |
begin |
|
c69d9fb16785
Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
4 |
|
|
2311
4da5c5c29009
work on transitivity proof
Christian Urban <urbanc@in.tum.de>
parents:
2120
diff
changeset
|
5 |
atom_decl name |
| 2056 | 6 |
|
|
2436
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2311
diff
changeset
|
7 |
nominal_datatype let_rec: |
|
2438
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
parents:
2436
diff
changeset
|
8 |
trm = |
| 2056 | 9 |
Var "name" |
|
2438
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
parents:
2436
diff
changeset
|
10 |
| 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:
2877
diff
changeset
|
11 |
| Lam x::"name" t::"trm" binds (set) x in t |
|
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents:
2877
diff
changeset
|
12 |
| Let_Rec bp::"bp" t::"trm" binds (set) "bn bp" in bp t |
|
1946
3395e87d94b8
tuned and made to compile
Christian Urban <urbanc@in.tum.de>
parents:
1773
diff
changeset
|
13 |
and bp = |
|
2438
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
parents:
2436
diff
changeset
|
14 |
Bp "name" "trm" |
|
1596
c69d9fb16785
Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
15 |
binder |
|
2438
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
parents:
2436
diff
changeset
|
16 |
bn::"bp \<Rightarrow> atom set" |
|
1596
c69d9fb16785
Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
17 |
where |
|
2438
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
parents:
2436
diff
changeset
|
18 |
"bn (Bp x t) = {atom x}"
|
|
1596
c69d9fb16785
Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
19 |
|
|
2436
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2311
diff
changeset
|
20 |
thm let_rec.distinct |
|
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2311
diff
changeset
|
21 |
thm let_rec.induct |
|
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2311
diff
changeset
|
22 |
thm let_rec.exhaust |
|
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2311
diff
changeset
|
23 |
thm let_rec.fv_defs |
|
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2311
diff
changeset
|
24 |
thm let_rec.bn_defs |
|
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2311
diff
changeset
|
25 |
thm let_rec.perm_simps |
|
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2311
diff
changeset
|
26 |
thm let_rec.eq_iff |
|
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2311
diff
changeset
|
27 |
thm let_rec.fv_bn_eqvt |
|
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2311
diff
changeset
|
28 |
thm let_rec.size_eqvt |
|
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
parents:
2067
diff
changeset
|
29 |
|
| 2877 | 30 |
|
|
3235
5ebd327ffb96
changed nominal_primrec into the more appropriate nominal_function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3197
diff
changeset
|
31 |
nominal_function |
| 2877 | 32 |
height_trm :: "trm \<Rightarrow> nat" |
33 |
and height_bp :: "bp \<Rightarrow> nat" |
|
34 |
where |
|
35 |
"height_trm (Var x) = 1" |
|
36 |
| "height_trm (App l r) = max (height_trm l) (height_trm r)" |
|
37 |
| "height_trm (Lam v b) = 1 + (height_trm b)" |
|
38 |
| "height_trm (Let_Rec bp b) = max (height_bp bp) (height_trm b)" |
|
39 |
| "height_bp (Bp v t) = height_trm t" |
|
|
3197
25d11b449e92
definition of an auxiliary graph in nominal-primrec definitions
Christian Urban <urbanc@in.tum.de>
parents:
3192
diff
changeset
|
40 |
apply (simp add: eqvt_def height_trm_height_bp_graph_aux_def) |
|
25d11b449e92
definition of an auxiliary graph in nominal-primrec definitions
Christian Urban <urbanc@in.tum.de>
parents:
3192
diff
changeset
|
41 |
apply(rule TrueI) |
|
3192
14c7d7e29c44
added a simproc for alpha-equivalence to the simplifier
Christian Urban <urbanc@in.tum.de>
parents:
3183
diff
changeset
|
42 |
using [[simproc del: alpha_set]] |
| 2877 | 43 |
apply auto |
44 |
apply (case_tac x) |
|
45 |
apply (case_tac a rule: let_rec.exhaust(1)) |
|
|
3192
14c7d7e29c44
added a simproc for alpha-equivalence to the simplifier
Christian Urban <urbanc@in.tum.de>
parents:
3183
diff
changeset
|
46 |
using [[simproc del: alpha_set]] |
| 2877 | 47 |
apply auto |
48 |
apply (case_tac b rule: let_rec.exhaust(2)) |
|
49 |
apply blast |
|
50 |
apply (erule Abs_set_fcb) |
|
|
3183
313e6f2cdd89
added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often
Christian Urban <urbanc@in.tum.de>
parents:
2975
diff
changeset
|
51 |
apply (simp_all add: pure_fresh)[2] |
|
313e6f2cdd89
added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often
Christian Urban <urbanc@in.tum.de>
parents:
2975
diff
changeset
|
52 |
apply (simp only: eqvt_at_def) |
|
313e6f2cdd89
added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often
Christian Urban <urbanc@in.tum.de>
parents:
2975
diff
changeset
|
53 |
apply(perm_simp) |
|
313e6f2cdd89
added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often
Christian Urban <urbanc@in.tum.de>
parents:
2975
diff
changeset
|
54 |
apply(simp) |
| 2877 | 55 |
apply (simp add: Abs_eq_iff2) |
56 |
apply (simp add: alphas) |
|
57 |
apply clarify |
|
58 |
apply (rule trans) |
|
59 |
apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
|
60 |
apply (simp add: pure_supp fresh_star_def) |
|
| 2971 | 61 |
apply(simp add: eqvt_at_def) |
| 2877 | 62 |
done |
63 |
||
|
2975
c62e26830420
preliminary version of automatically generation the eqvt-lemmas for functions defined with nominal_primrec
Christian Urban <urbanc@in.tum.de>
parents:
2974
diff
changeset
|
64 |
termination (eqvt) by lexicographic_order |
|
2974
b95a2065aa10
generated the partial eqvt-theorem for functions
Christian Urban <urbanc@in.tum.de>
parents:
2973
diff
changeset
|
65 |
|
|
2975
c62e26830420
preliminary version of automatically generation the eqvt-lemmas for functions defined with nominal_primrec
Christian Urban <urbanc@in.tum.de>
parents:
2974
diff
changeset
|
66 |
thm height_trm_height_bp.eqvt |
|
2974
b95a2065aa10
generated the partial eqvt-theorem for functions
Christian Urban <urbanc@in.tum.de>
parents:
2973
diff
changeset
|
67 |
|
|
2067
ace7775cbd04
Experiments with equivariance.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2056
diff
changeset
|
68 |
|
|
1596
c69d9fb16785
Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
69 |
end |
|
c69d9fb16785
Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
70 |
|
|
c69d9fb16785
Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
71 |
|
|
c69d9fb16785
Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
72 |