| author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
| Fri, 24 Jun 2011 11:14:58 +0900 | |
| changeset 2896 | 59be22e05a0a |
| parent 2752 | 9f44608ea28d |
| permissions | -rw-r--r-- |
|
2726
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
1 |
theory Lambda_add |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
2 |
imports "Lambda" |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
3 |
begin |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
4 |
|
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
5 |
nominal_primrec |
|
2752
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents:
2739
diff
changeset
|
6 |
addlam :: "lam \<Rightarrow> lam" |
|
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents:
2739
diff
changeset
|
7 |
where |
|
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents:
2739
diff
changeset
|
8 |
"fv \<noteq> x \<Longrightarrow> addlam (Var x) = Lam [fv]. App (Var fv) (Var x)" |
|
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents:
2739
diff
changeset
|
9 |
| "addlam (App t1 t2) = App t1 t2" |
|
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents:
2739
diff
changeset
|
10 |
| "addlam (Lam [x]. t) = Lam [x].t" |
|
2896
59be22e05a0a
The examples in Lambda_add can be defined by nominal_function directly
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2752
diff
changeset
|
11 |
unfolding addlam_graph_def eqvt_def |
|
59be22e05a0a
The examples in Lambda_add can be defined by nominal_function directly
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2752
diff
changeset
|
12 |
apply perm_simp |
|
59be22e05a0a
The examples in Lambda_add can be defined by nominal_function directly
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2752
diff
changeset
|
13 |
apply auto |
|
59be22e05a0a
The examples in Lambda_add can be defined by nominal_function directly
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2752
diff
changeset
|
14 |
apply (case_tac x rule: lam.exhaust) |
|
59be22e05a0a
The examples in Lambda_add can be defined by nominal_function directly
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2752
diff
changeset
|
15 |
apply auto |
|
59be22e05a0a
The examples in Lambda_add can be defined by nominal_function directly
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2752
diff
changeset
|
16 |
apply (rule_tac x="name" and ?'a="name" in obtain_fresh) |
|
59be22e05a0a
The examples in Lambda_add can be defined by nominal_function directly
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2752
diff
changeset
|
17 |
apply (simp add: fresh_at_base) |
|
59be22e05a0a
The examples in Lambda_add can be defined by nominal_function directly
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2752
diff
changeset
|
18 |
apply (simp add: Abs1_eq_iff lam.fresh fresh_at_base) |
|
2726
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
19 |
done |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
20 |
|
|
2896
59be22e05a0a
The examples in Lambda_add can be defined by nominal_function directly
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2752
diff
changeset
|
21 |
termination by lexicographic_order |
| 2737 | 22 |
|
|
2726
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
23 |
end |