26 | "bv1 (BVr x) = {atom x}" |
26 | "bv1 (BVr x) = {atom x}" |
27 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)" |
27 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)" |
28 |
28 |
29 (* needs to be calculated by the package *) |
29 (* needs to be calculated by the package *) |
30 primrec |
30 primrec |
31 fv_trm1 and fv_bp |
31 rfv_trm1 and rfv_bp |
32 where |
32 where |
33 "fv_trm1 (Vr1 x) = {atom x}" |
33 "rfv_trm1 (rVr1 x) = {atom x}" |
34 | "fv_trm1 (Ap1 t1 t2) = (fv_trm1 t1) \<union> (fv_trm1 t2)" |
34 | "rfv_trm1 (rAp1 t1 t2) = (rfv_trm1 t1) \<union> (rfv_trm1 t2)" |
35 | "fv_trm1 (Lm1 x t) = (fv_trm1 t) - {atom x}" |
35 | "rfv_trm1 (rLm1 x t) = (rfv_trm1 t) - {atom x}" |
36 | "fv_trm1 (Lt1 bp t1 t2) = (fv_trm1 t1) \<union> (fv_trm1 t2 - bv1 bp)" |
36 | "rfv_trm1 (rLt1 bp t1 t2) = (rfv_trm1 t1) \<union> (rfv_trm1 t2 - bv1 bp)" |
37 | "fv_bp (BUnit) = {}" |
37 | "rfv_bp (BUnit) = {}" |
38 | "fv_bp (BVr x) = {atom x}" |
38 | "rfv_bp (BVr x) = {atom x}" |
39 | "fv_bp (BPr b1 b2) = (fv_bp b1) \<union> (fv_bp b2)" |
39 | "rfv_bp (BPr b1 b2) = (rfv_bp b1) \<union> (rfv_bp b2)" |
40 |
40 |
41 (* needs to be stated by the package *) |
41 (* needs to be stated by the package *) |
42 instantiation |
42 instantiation |
43 trm1 and bp :: pt |
43 rtrm1 and bp :: pt |
44 begin |
44 begin |
45 |
45 |
46 primrec |
46 primrec |
47 permute_trm1 and permute_bp |
47 permute_rtrm1 and permute_bp |
48 where |
48 where |
49 "permute_trm1 pi (Vr1 a) = Vr1 (pi \<bullet> a)" |
49 "permute_rtrm1 pi (rVr1 a) = rVr1 (pi \<bullet> a)" |
50 | "permute_trm1 pi (Ap1 t1 t2) = Ap1 (permute_trm1 pi t1) (permute_trm1 pi t2)" |
50 | "permute_rtrm1 pi (rAp1 t1 t2) = rAp1 (permute_rtrm1 pi t1) (permute_rtrm1 pi t2)" |
51 | "permute_trm1 pi (Lm1 a t) = Lm1 (pi \<bullet> a) (permute_trm1 pi t)" |
51 | "permute_rtrm1 pi (rLm1 a t) = rLm1 (pi \<bullet> a) (permute_rtrm1 pi t)" |
52 | "permute_trm1 pi (Lt1 bp t1 t2) = Lt1 (permute_bp pi bp) (permute_trm1 pi t1) (permute_trm1 pi t2)" |
52 | "permute_rtrm1 pi (rLt1 bp t1 t2) = rLt1 (permute_bp pi bp) (permute_rtrm1 pi t1) (permute_rtrm1 pi t2)" |
53 | "permute_bp pi (BUnit) = BUnit" |
53 | "permute_bp pi (BUnit) = BUnit" |
54 | "permute_bp pi (BVr a) = BVr (pi \<bullet> a)" |
54 | "permute_bp pi (BVr a) = BVr (pi \<bullet> a)" |
55 | "permute_bp pi (BPr bp1 bp2) = BPr (permute_bp pi bp1) (permute_bp pi bp2)" |
55 | "permute_bp pi (BPr bp1 bp2) = BPr (permute_bp pi bp1) (permute_bp pi bp2)" |
56 |
56 |
57 lemma pt_trm1_bp_zero: |
57 lemma pt_rtrm1_bp_zero: |
58 fixes t::trm1 |
58 fixes t::rtrm1 |
59 and b::bp |
59 and b::bp |
60 shows "0 \<bullet> t = t" |
60 shows "0 \<bullet> t = t" |
61 and "0 \<bullet> b = b" |
61 and "0 \<bullet> b = b" |
62 apply(induct t and b rule: trm1_bp.inducts) |
62 apply(induct t and b rule: rtrm1_bp.inducts) |
63 apply(simp_all) |
63 apply(simp_all) |
64 done |
64 done |
65 |
65 |
66 lemma pt_trm1_bp_plus: |
66 lemma pt_rtrm1_bp_plus: |
67 fixes t::trm1 |
67 fixes t::rtrm1 |
68 and b::bp |
68 and b::bp |
69 shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)" |
69 shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)" |
70 and "((p + q) \<bullet> b) = p \<bullet> (q \<bullet> b)" |
70 and "((p + q) \<bullet> b) = p \<bullet> (q \<bullet> b)" |
71 apply(induct t and b rule: trm1_bp.inducts) |
71 apply(induct t and b rule: rtrm1_bp.inducts) |
72 apply(simp_all) |
72 apply(simp_all) |
73 done |
73 done |
74 |
74 |
75 instance |
75 instance |
76 apply default |
76 apply default |
77 apply(simp_all add: pt_trm1_bp_zero pt_trm1_bp_plus) |
77 apply(simp_all add: pt_rtrm1_bp_zero pt_rtrm1_bp_plus) |
78 done |
78 done |
79 |
79 |
80 end |
80 end |
81 |
81 |
82 inductive |
82 inductive |
83 alpha1 :: "trm1 \<Rightarrow> trm1 \<Rightarrow> bool" ("_ \<approx>1 _" [100, 100] 100) |
83 alpha1 :: "rtrm1 \<Rightarrow> rtrm1 \<Rightarrow> bool" ("_ \<approx>1 _" [100, 100] 100) |
84 where |
84 where |
85 a1: "a = b \<Longrightarrow> (Vr1 a) \<approx>1 (Vr1 b)" |
85 a1: "a = b \<Longrightarrow> (rVr1 a) \<approx>1 (rVr1 b)" |
86 | a2: "\<lbrakk>t1 \<approx>1 t2; s1 \<approx>1 s2\<rbrakk> \<Longrightarrow> Ap1 t1 s1 \<approx>1 Ap1 t2 s2" |
86 | a2: "\<lbrakk>t1 \<approx>1 t2; s1 \<approx>1 s2\<rbrakk> \<Longrightarrow> rAp1 t1 s1 \<approx>1 rAp1 t2 s2" |
87 | a3: "\<exists>pi. (fv_trm1 t - {atom a} = fv_trm1 s - {atom b} \<and> |
87 | a3: "(\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 rfv_trm1 pi ({atom ab}, s))) \<Longrightarrow> rLm1 aa t \<approx>1 rLm1 ab s" |
88 (fv_trm1 t - {atom a})\<sharp>* pi \<and> |
88 | a4: "t1 \<approx>1 t2 \<Longrightarrow> (\<exists>pi. (((bv1 b1), s1) \<approx>gen alpha1 rfv_trm1 pi ((bv1 b2), s2))) \<Longrightarrow> rLt1 b1 t1 s1 \<approx>1 rLt1 b2 t2 s2" |
89 (pi \<bullet> t) \<approx>1 s \<and> (pi \<bullet> a) = b) |
89 |
90 \<Longrightarrow> Lm1 a t \<approx>1 Lm1 b s" |
90 lemma alpha_inj: |
91 | a4: "\<exists>pi.(t1 \<approx>1 t2 \<and> |
91 "(rVr1 a \<approx>1 rVr1 b) = (a = b)" |
92 (fv_trm1 s1 - fv_bp b1 = fv_trm1 s2 - fv_bp b2) \<and> |
92 "(rAp1 t1 s1 \<approx>1 rAp1 t2 s2) = (t1 \<approx>1 t2 \<and> s1 \<approx>1 s2)" |
93 (fv_trm1 s1 - fv_bp b1) \<sharp>* pi \<and> |
93 "(rLm1 aa t \<approx>1 rLm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 rfv_trm1 pi ({atom ab}, s)))" |
94 (pi \<bullet> s1 = s2) (* Optional: \<and> (pi \<bullet> b1 = b2) *)) |
94 "(rLt1 b1 t1 s1 \<approx>1 rLt1 b2 t2 s2) = (t1 \<approx>1 t2 \<and> (\<exists>pi. (((bv1 b1), s1) \<approx>gen alpha1 rfv_trm1 pi ((bv1 b2), s2))))" |
95 \<Longrightarrow> Lt1 b1 t1 s1 \<approx>1 Lt1 b2 t2 s2" |
95 apply - |
|
96 apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros) |
|
97 apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros) |
|
98 apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros) |
|
99 apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros) |
|
100 done |
|
101 |
|
102 lemma rfv1_eqvt[eqvt]: |
|
103 shows "(pi\<bullet>rfv_trm1 t) = rfv_trm1 (pi\<bullet>t)" |
|
104 sorry |
|
105 |
|
106 lemma alpha1_eqvt: |
|
107 shows "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)" |
|
108 sorry |
96 |
109 |
97 lemma alpha1_equivp: "equivp alpha1" |
110 lemma alpha1_equivp: "equivp alpha1" |
98 sorry |
111 sorry |
99 |
112 |
100 quotient_type qtrm1 = trm1 / alpha1 |
113 quotient_type trm1 = rtrm1 / alpha1 |
101 by (rule alpha1_equivp) |
114 by (rule alpha1_equivp) |
|
115 |
|
116 quotient_definition |
|
117 "Vr1 :: name \<Rightarrow> trm1" |
|
118 as |
|
119 "rVr1" |
102 |
120 |
103 |
121 |
104 section {*** lets with single assignments ***} |
122 section {*** lets with single assignments ***} |
105 |
123 |
106 datatype trm2 = |
124 datatype trm2 = |