|
1 theory Term6 |
|
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" |
|
3 begin |
|
4 |
|
5 atom_decl name |
|
6 |
|
7 (* example with a bn function defined over the type itself, NOT respectful. *) |
|
8 |
|
9 datatype rtrm6 = |
|
10 rVr6 "name" |
|
11 | rLm6 "name" "rtrm6" --"bind name in rtrm6" |
|
12 | rLt6 "rtrm6" "rtrm6" --"bind (bv6 left) in (right)" |
|
13 |
|
14 primrec |
|
15 rbv6 |
|
16 where |
|
17 "rbv6 (rVr6 n) = {}" |
|
18 | "rbv6 (rLm6 n t) = {atom n} \<union> rbv6 t" |
|
19 | "rbv6 (rLt6 l r) = rbv6 l \<union> rbv6 r" |
|
20 |
|
21 setup {* snd o define_raw_perms ["rtrm6"] ["Term6.rtrm6"] *} |
|
22 print_theorems |
|
23 |
|
24 local_setup {* snd o define_fv_alpha "Term6.rtrm6" [ |
|
25 [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv6}, 0)]]]] *} |
|
26 notation alpha_rtrm6 ("_ \<approx>6 _" [100, 100] 100) |
|
27 thm alpha_rtrm6.intros |
|
28 |
|
29 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_inj}, []), (build_alpha_inj @{thms alpha_rtrm6.intros} @{thms rtrm6.distinct rtrm6.inject} @{thms alpha_rtrm6.cases} ctxt)) ctxt)) *} |
|
30 thm alpha6_inj |
|
31 |
|
32 local_setup {* |
|
33 snd o (build_eqvts @{binding rbv6_eqvt} [@{term rbv6}] [@{term "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"}] (@{thms rbv6.simps permute_rtrm6.simps}) @{thm rtrm6.induct}) |
|
34 *} |
|
35 |
|
36 local_setup {* |
|
37 snd o build_eqvts @{binding fv_rtrm6_eqvt} [@{term fv_rtrm6}] [@{term "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"}] (@{thms fv_rtrm6.simps permute_rtrm6.simps}) @{thm rtrm6.induct} |
|
38 *} |
|
39 |
|
40 local_setup {* |
|
41 (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_eqvt}, []), |
|
42 build_alpha_eqvts [@{term alpha_rtrm6}] [@{term "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"}] @{thms permute_rtrm6.simps alpha6_inj} @{thm alpha_rtrm6.induct} ctxt) ctxt)) |
|
43 *} |
|
44 |
|
45 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_equivp}, []), |
|
46 (build_equivps [@{term alpha_rtrm6}] @{thm rtrm6.induct} @{thm alpha_rtrm6.induct} @{thms rtrm6.inject} @{thms alpha6_inj} @{thms rtrm6.distinct} @{thms alpha_rtrm6.cases} @{thms alpha6_eqvt} ctxt)) ctxt)) *} |
|
47 thm alpha6_equivp |
|
48 |
|
49 quotient_type |
|
50 trm6 = rtrm6 / alpha_rtrm6 |
|
51 by (auto intro: alpha6_equivp) |
|
52 |
|
53 local_setup {* |
|
54 (fn ctxt => ctxt |
|
55 |> snd o (Quotient_Def.quotient_lift_const ("Vr6", @{term rVr6})) |
|
56 |> snd o (Quotient_Def.quotient_lift_const ("Lm6", @{term rLm6})) |
|
57 |> snd o (Quotient_Def.quotient_lift_const ("Lt6", @{term rLt6})) |
|
58 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm6", @{term fv_rtrm6})) |
|
59 |> snd o (Quotient_Def.quotient_lift_const ("bv6", @{term rbv6}))) |
|
60 *} |
|
61 print_theorems |
|
62 |
|
63 lemma [quot_respect]: |
|
64 "(op = ===> alpha_rtrm6 ===> alpha_rtrm6) permute permute" |
|
65 by (auto simp add: alpha6_eqvt) |
|
66 |
|
67 (* Definitely not true , see lemma below *) |
|
68 lemma [quot_respect]:"(alpha_rtrm6 ===> op =) rbv6 rbv6" |
|
69 apply simp apply clarify |
|
70 apply (erule alpha_rtrm6.induct) |
|
71 oops |
|
72 |
|
73 lemma "(a :: name) \<noteq> b \<Longrightarrow> \<not> (alpha_rtrm6 ===> op =) rbv6 rbv6" |
|
74 apply simp |
|
75 apply (rule_tac x="rLm6 (a::name) (rVr6 (a :: name))" in exI) |
|
76 apply (rule_tac x="rLm6 (b::name) (rVr6 (b :: name))" in exI) |
|
77 apply simp |
|
78 apply (simp add: alpha6_inj) |
|
79 apply (rule_tac x="(a \<leftrightarrow> b)" in exI) |
|
80 apply (simp add: alpha_gen fresh_star_def) |
|
81 apply (simp add: alpha6_inj) |
|
82 done |
|
83 |
|
84 lemma fv6_rsp: "x \<approx>6 y \<Longrightarrow> fv_rtrm6 x = fv_rtrm6 y" |
|
85 apply (induct_tac x y rule: alpha_rtrm6.induct) |
|
86 apply simp_all |
|
87 apply (erule exE) |
|
88 apply (simp_all add: alpha_gen) |
|
89 done |
|
90 |
|
91 lemma [quot_respect]:"(alpha_rtrm6 ===> op =) fv_rtrm6 fv_rtrm6" |
|
92 by (simp add: fv6_rsp) |
|
93 |
|
94 lemma [quot_respect]: |
|
95 "(op = ===> alpha_rtrm6) rVr6 rVr6" |
|
96 "(op = ===> alpha_rtrm6 ===> alpha_rtrm6) rLm6 rLm6" |
|
97 apply auto |
|
98 apply (simp_all add: alpha6_inj) |
|
99 apply (rule_tac x="0::perm" in exI) |
|
100 apply (simp add: alpha_gen fv6_rsp fresh_star_def fresh_zero_perm) |
|
101 done |
|
102 |
|
103 lemma [quot_respect]: |
|
104 "(alpha_rtrm6 ===> alpha_rtrm6 ===> alpha_rtrm6) rLt6 rLt6" |
|
105 apply auto |
|
106 apply (simp_all add: alpha6_inj) |
|
107 apply (rule_tac [!] x="0::perm" in exI) |
|
108 apply (simp_all add: alpha_gen fresh_star_def fresh_zero_perm) |
|
109 (* needs rbv6_rsp *) |
|
110 oops |
|
111 |
|
112 instantiation trm6 :: pt begin |
|
113 |
|
114 quotient_definition |
|
115 "permute_trm6 :: perm \<Rightarrow> trm6 \<Rightarrow> trm6" |
|
116 is |
|
117 "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6" |
|
118 |
|
119 instance |
|
120 apply default |
|
121 sorry |
|
122 end |
|
123 |
|
124 lemma lifted_induct: |
|
125 "\<lbrakk>x1 = x2; \<And>name namea. name = namea \<Longrightarrow> P (Vr6 name) (Vr6 namea); |
|
126 \<And>name rtrm6 namea rtrm6a. |
|
127 \<lbrakk>True; |
|
128 \<exists>pi. fv_trm6 rtrm6 - {atom name} = fv_trm6 rtrm6a - {atom namea} \<and> |
|
129 (fv_trm6 rtrm6 - {atom name}) \<sharp>* pi \<and> pi \<bullet> rtrm6 = rtrm6a \<and> P (pi \<bullet> rtrm6) rtrm6a\<rbrakk> |
|
130 \<Longrightarrow> P (Lm6 name rtrm6) (Lm6 namea rtrm6a); |
|
131 \<And>rtrm61 rtrm61a rtrm62 rtrm62a. |
|
132 \<lbrakk>rtrm61 = rtrm61a; P rtrm61 rtrm61a; |
|
133 \<exists>pi. fv_trm6 rtrm62 - bv6 rtrm61 = fv_trm6 rtrm62a - bv6 rtrm61a \<and> |
|
134 (fv_trm6 rtrm62 - bv6 rtrm61) \<sharp>* pi \<and> pi \<bullet> rtrm62 = rtrm62a \<and> P (pi \<bullet> rtrm62) rtrm62a\<rbrakk> |
|
135 \<Longrightarrow> P (Lt6 rtrm61 rtrm62) (Lt6 rtrm61a rtrm62a)\<rbrakk> |
|
136 \<Longrightarrow> P x1 x2" |
|
137 apply (lifting alpha_rtrm6.induct[unfolded alpha_gen]) |
|
138 apply injection |
|
139 (* notice unsolvable goals: (alpha_rtrm6 ===> op =) rbv6 rbv6 *) |
|
140 oops |
|
141 |
|
142 lemma lifted_inject_a3: |
|
143 "(Lt6 rtrm61 rtrm62 = Lt6 rtrm61a rtrm62a) = |
|
144 (rtrm61 = rtrm61a \<and> |
|
145 (\<exists>pi. fv_trm6 rtrm62 - bv6 rtrm61 = fv_trm6 rtrm62a - bv6 rtrm61a \<and> |
|
146 (fv_trm6 rtrm62 - bv6 rtrm61) \<sharp>* pi \<and> pi \<bullet> rtrm62 = rtrm62a))" |
|
147 apply(lifting alpha6_inj(3)[unfolded alpha_gen]) |
|
148 apply injection |
|
149 (* notice unsolvable goals: (alpha_rtrm6 ===> op =) rbv6 rbv6 *) |
|
150 oops |
|
151 |
|
152 |
|
153 |
|
154 |
|
155 end |