equal
deleted
inserted
replaced
1 theory Terms |
1 theory Terms |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "../../Attic/Prove" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 text {* primrec seems to be genarally faster than fun *} |
7 text {* primrec seems to be genarally faster than fun *} |
35 print_theorems |
35 print_theorems |
36 notation |
36 notation |
37 alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and |
37 alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and |
38 alpha_bp ("_ \<approx>1b _" [100, 100] 100) |
38 alpha_bp ("_ \<approx>1b _" [100, 100] 100) |
39 thm alpha_rtrm1_alpha_bp.intros |
39 thm alpha_rtrm1_alpha_bp.intros |
|
40 |
|
41 prove {* build_alpha_inj_gl @{thms alpha_rtrm1_alpha_bp.intros} @{context} *} |
|
42 sorry |
40 |
43 |
41 lemma alpha1_inj: |
44 lemma alpha1_inj: |
42 "(rVr1 a \<approx>1 rVr1 b) = (a = b)" |
45 "(rVr1 a \<approx>1 rVr1 b) = (a = b)" |
43 "(rAp1 t1 s1 \<approx>1 rAp1 t2 s2) = (t1 \<approx>1 t2 \<and> s1 \<approx>1 s2)" |
46 "(rAp1 t1 s1 \<approx>1 rAp1 t2 s2) = (t1 \<approx>1 t2 \<and> s1 \<approx>1 s2)" |
44 "(rLm1 aa t \<approx>1 rLm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen alpha_rtrm1 fv_rtrm1 pi ({atom ab}, s)))" |
47 "(rLm1 aa t \<approx>1 rLm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen alpha_rtrm1 fv_rtrm1 pi ({atom ab}, s)))" |