12 inductive |
12 inductive |
13 alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100) |
13 alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100) |
14 where |
14 where |
15 a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)" |
15 a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)" |
16 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2" |
16 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2" |
17 | a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a\<sharp>s\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s" |
17 | a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a\<sharp>[b].s\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s" |
18 |
18 |
19 quotient lam = rlam / alpha |
19 quotient lam = rlam / alpha |
20 apply - |
20 apply - |
21 sorry |
21 sorry |
22 |
22 |
23 print_quotients |
23 print_quotients |
24 |
24 |
25 local_setup {* |
25 quotient_def (for lam) |
26 old_make_const_def @{binding Var} @{term "rVar"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #> |
26 Var :: "name \<Rightarrow> lam" |
27 old_make_const_def @{binding App} @{term "rApp"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #> |
27 where |
28 old_make_const_def @{binding Lam} @{term "rLam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd |
28 "Var \<equiv> rVar" |
29 *} |
29 |
|
30 quotient_def (for lam) |
|
31 App :: "lam \<Rightarrow> lam \<Rightarrow> lam" |
|
32 where |
|
33 "App \<equiv> rApp" |
|
34 |
|
35 quotient_def (for lam) |
|
36 Lam :: "name \<Rightarrow> lam \<Rightarrow> lam" |
|
37 where |
|
38 "Lam \<equiv> rLam" |
30 |
39 |
31 thm Var_def |
40 thm Var_def |
32 thm App_def |
41 thm App_def |
33 thm Lam_def |
42 thm Lam_def |
|
43 |
|
44 (* definition of overloaded permutation function *) |
|
45 (* for the lifted type lam *) |
|
46 overloading |
|
47 perm_lam \<equiv> "perm :: 'x prm \<Rightarrow> lam \<Rightarrow> lam" (unchecked) |
|
48 begin |
|
49 |
|
50 quotient_def (for lam) |
|
51 perm_lam :: "'x prm \<Rightarrow> lam \<Rightarrow> lam" |
|
52 where |
|
53 "perm_lam \<equiv> (perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam)" |
|
54 |
|
55 end |
|
56 |
|
57 thm perm_lam_def |
|
58 |
|
59 (* lemmas that need to lift *) |
|
60 lemma |
|
61 fixes pi::"'x prm" |
|
62 shows "(pi\<bullet>Var a) = Var (pi\<bullet>a)" |
|
63 sorry |
|
64 |
|
65 lemma |
|
66 fixes pi::"'x prm" |
|
67 shows "(pi\<bullet>App t1 t2) = App (pi\<bullet>t1) (pi\<bullet>t2)" |
|
68 sorry |
|
69 |
|
70 lemma |
|
71 fixes pi::"'x prm" |
|
72 shows "(pi\<bullet>Lam a t) = Lam (pi\<bullet>a) (pi\<bullet>t)" |
|
73 sorry |
34 |
74 |
35 lemma real_alpha: |
75 lemma real_alpha: |
36 assumes "t = ([(a,b)]\<bullet>s)" "a\<sharp>s" |
76 assumes "t = ([(a,b)]\<bullet>s)" "a\<sharp>s" |
37 shows "Lam a t = Lam b s" |
77 shows "Lam a t = Lam b s" |
38 sorry |
78 sorry |
41 |
81 |
42 |
82 |
43 |
83 |
44 (* Construction Site code *) |
84 (* Construction Site code *) |
45 |
85 |
46 lemma perm_rsp: "op = ===> alpha ===> alpha op \<bullet> op \<bullet>" sorry |
86 lemma perm_rsp: "op = ===> alpha ===> alpha op \<bullet> op \<bullet>" |
47 lemma fresh_rsp: "op = ===> (alpha ===> op =) fresh fresh" sorry |
87 apply(auto) |
48 lemma rLam_rsp: "op = ===> (alpha ===> alpha) rLam rLam" sorry |
88 (* this is propably true if some type conditions are imposed ;o) *) |
|
89 sorry |
|
90 |
|
91 lemma fresh_rsp: "op = ===> (alpha ===> op =) fresh fresh" |
|
92 apply(auto) |
|
93 (* this is probably only true if some type conditions are imposed *) |
|
94 sorry |
|
95 |
|
96 lemma rLam_rsp: "op = ===> (alpha ===> alpha) rLam rLam" |
|
97 apply(auto) |
|
98 apply(rule a3) |
|
99 apply(rule_tac t="[(x,x)]\<bullet>y" and s="y" in subst) |
|
100 apply(rule sym) |
|
101 apply(rule trans) |
|
102 apply(rule pt_name3) |
|
103 apply(rule at_ds1[OF at_name_inst]) |
|
104 apply(simp add: pt_name1) |
|
105 apply(assumption) |
|
106 apply(simp add: abs_fresh) |
|
107 done |
49 |
108 |
50 ML {* val defs = @{thms Var_def App_def Lam_def} *} |
109 ML {* val defs = @{thms Var_def App_def Lam_def} *} |
51 ML {* val consts = [@{const_name "rVar"}, @{const_name "rApp"}, @{const_name "rLam"}]; *} |
110 ML {* val consts = [@{const_name "rVar"}, @{const_name "rApp"}, @{const_name "rLam"}]; *} |
52 |
111 |
53 ML {* val rty = @{typ "rlam"} *} |
112 ML {* val rty = @{typ "rlam"} *} |