950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 1 theory Terms
1180
+ − 2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv"
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 3 begin
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 4
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 5 atom_decl name
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 6
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 7 text {* primrec seems to be genarally faster than fun *}
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 8
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 9 section {*** lets with binding patterns ***}
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 10
1028
+ − 11 datatype rtrm1 =
+ − 12 rVr1 "name"
+ − 13 | rAp1 "rtrm1" "rtrm1"
+ − 14 | rLm1 "name" "rtrm1" --"name is bound in trm1"
+ − 15 | rLt1 "bp" "rtrm1" "rtrm1" --"all variables in bp are bound in the 2nd trm1"
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 16 and bp =
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 17 BUnit
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 18 | BVr "name"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 19 | BPr "bp" "bp"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 20
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 21 (* to be given by the user *)
1029
+ − 22
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 23 primrec
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 24 bv1
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 25 where
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 26 "bv1 (BUnit) = {}"
957
+ − 27 | "bv1 (BVr x) = {atom x}"
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 28 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 29
1180
+ − 30 local_setup {* define_raw_fv "Terms.rtrm1"
+ − 31 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]],
+ − 32 [[], [[]], [[], []]]] *}
+ − 33 print_theorems
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 34
1171
+ − 35 setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *}
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 36
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 37 inductive
1028
+ − 38 alpha1 :: "rtrm1 \<Rightarrow> rtrm1 \<Rightarrow> bool" ("_ \<approx>1 _" [100, 100] 100)
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 39 where
1028
+ − 40 a1: "a = b \<Longrightarrow> (rVr1 a) \<approx>1 (rVr1 b)"
+ − 41 | a2: "\<lbrakk>t1 \<approx>1 t2; s1 \<approx>1 s2\<rbrakk> \<Longrightarrow> rAp1 t1 s1 \<approx>1 rAp1 t2 s2"
1180
+ − 42 | a3: "(\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 fv_rtrm1 pi ({atom ab}, s))) \<Longrightarrow> rLm1 aa t \<approx>1 rLm1 ab s"
+ − 43 | a4: "t1 \<approx>1 t2 \<Longrightarrow> (\<exists>pi. (((bv1 b1), s1) \<approx>gen alpha1 fv_rtrm1 pi ((bv1 b2), s2))) \<Longrightarrow> rLt1 b1 t1 s1 \<approx>1 rLt1 b2 t2 s2"
1028
+ − 44
1029
+ − 45 lemma alpha1_inj:
1028
+ − 46 "(rVr1 a \<approx>1 rVr1 b) = (a = b)"
+ − 47 "(rAp1 t1 s1 \<approx>1 rAp1 t2 s2) = (t1 \<approx>1 t2 \<and> s1 \<approx>1 s2)"
1180
+ − 48 "(rLm1 aa t \<approx>1 rLm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 fv_rtrm1 pi ({atom ab}, s)))"
+ − 49 "(rLt1 b1 t1 s1 \<approx>1 rLt1 b2 t2 s2) = (t1 \<approx>1 t2 \<and> (\<exists>pi. (((bv1 b1), s1) \<approx>gen alpha1 fv_rtrm1 pi ((bv1 b2), s2))))"
1028
+ − 50 apply -
+ − 51 apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
+ − 52 apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
+ − 53 apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
+ − 54 apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
+ − 55 done
+ − 56
1030
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 57 (* Shouyld we derive it? But bv is given by the user? *)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 58 lemma bv1_eqvt[eqvt]:
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 59 shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)"
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 60 apply (induct x)
1043
+ − 61 apply (simp_all add: empty_eqvt insert_eqvt atom_eqvt)
1030
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 62 done
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 63
1180
+ − 64 lemma fv_rtrm1_eqvt[eqvt]:
+ − 65 shows "(pi\<bullet>fv_rtrm1 t) = fv_rtrm1 (pi\<bullet>t)"
1031
+ − 66 apply (induct t)
1043
+ − 67 apply (simp_all add: insert_eqvt atom_eqvt empty_eqvt union_eqvt Diff_eqvt bv1_eqvt)
1031
+ − 68 done
+ − 69
+ − 70
1028
+ − 71 lemma alpha1_eqvt:
+ − 72 shows "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)"
1031
+ − 73 apply (induct t s rule: alpha1.inducts)
+ − 74 apply (simp_all add:eqvts alpha1_inj)
1033
+ − 75 apply (erule exE)
+ − 76 apply (rule_tac x="pi \<bullet> pia" in exI)
+ − 77 apply (simp add: alpha_gen)
+ − 78 apply(erule conjE)+
+ − 79 apply(rule conjI)
+ − 80 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
1180
+ − 81 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt empty_eqvt fv_rtrm1_eqvt)
1033
+ − 82 apply(rule conjI)
+ − 83 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
1180
+ − 84 apply(simp add: atom_eqvt Diff_eqvt fv_rtrm1_eqvt insert_eqvt empty_eqvt)
1033
+ − 85 apply(simp add: permute_eqvt[symmetric])
+ − 86 apply (erule exE)
+ − 87 apply (rule_tac x="pi \<bullet> pia" in exI)
+ − 88 apply (simp add: alpha_gen)
+ − 89 apply(erule conjE)+
+ − 90 apply(rule conjI)
+ − 91 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
1180
+ − 92 apply(simp add: fv_rtrm1_eqvt Diff_eqvt bv1_eqvt)
1033
+ − 93 apply(rule conjI)
+ − 94 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
1180
+ − 95 apply(simp add: atom_eqvt fv_rtrm1_eqvt Diff_eqvt bv1_eqvt)
1033
+ − 96 apply(simp add: permute_eqvt[symmetric])
+ − 97 done
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 98
957
+ − 99 lemma alpha1_equivp: "equivp alpha1"
+ − 100 sorry
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 101
1028
+ − 102 quotient_type trm1 = rtrm1 / alpha1
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 103 by (rule alpha1_equivp)
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 104
1028
+ − 105 quotient_definition
+ − 106 "Vr1 :: name \<Rightarrow> trm1"
1139
+ − 107 is
1028
+ − 108 "rVr1"
+ − 109
1029
+ − 110 quotient_definition
+ − 111 "Ap1 :: trm1 \<Rightarrow> trm1 \<Rightarrow> trm1"
1139
+ − 112 is
1029
+ − 113 "rAp1"
+ − 114
+ − 115 quotient_definition
+ − 116 "Lm1 :: name \<Rightarrow> trm1 \<Rightarrow> trm1"
1139
+ − 117 is
1029
+ − 118 "rLm1"
+ − 119
+ − 120 quotient_definition
+ − 121 "Lt1 :: bp \<Rightarrow> trm1 \<Rightarrow> trm1 \<Rightarrow> trm1"
1139
+ − 122 is
1029
+ − 123 "rLt1"
+ − 124
+ − 125 quotient_definition
+ − 126 "fv_trm1 :: trm1 \<Rightarrow> atom set"
1139
+ − 127 is
1180
+ − 128 "fv_rtrm1"
1029
+ − 129
+ − 130 lemma alpha_rfv1:
1180
+ − 131 shows "t \<approx>1 s \<Longrightarrow> fv_rtrm1 t = fv_rtrm1 s"
1029
+ − 132 apply(induct rule: alpha1.induct)
+ − 133 apply(simp_all add: alpha_gen.simps)
+ − 134 done
+ − 135
+ − 136 lemma [quot_respect]:
+ − 137 "(op = ===> alpha1) rVr1 rVr1"
+ − 138 "(alpha1 ===> alpha1 ===> alpha1) rAp1 rAp1"
+ − 139 "(op = ===> alpha1 ===> alpha1) rLm1 rLm1"
+ − 140 "(op = ===> alpha1 ===> alpha1 ===> alpha1) rLt1 rLt1"
1181
+ − 141 apply (auto simp add: alpha1_inj)
+ − 142 apply (rule_tac x="0" in exI)
1029
+ − 143 apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen)
1181
+ − 144 apply (rule_tac x="0" in exI)
+ − 145 apply (simp add: alpha_gen fresh_star_def fresh_zero_perm alpha_rfv1)
1029
+ − 146 done
+ − 147
+ − 148 lemma [quot_respect]:
+ − 149 "(op = ===> alpha1 ===> alpha1) permute permute"
1181
+ − 150 by (simp add: alpha1_eqvt)
1029
+ − 151
+ − 152 lemma [quot_respect]:
1180
+ − 153 "(alpha1 ===> op =) fv_rtrm1 fv_rtrm1"
1181
+ − 154 by (simp add: alpha_rfv1)
1029
+ − 155
1073
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 156 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted]
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 157 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted]
1029
+ − 158
+ − 159 instantiation trm1 and bp :: pt
+ − 160 begin
+ − 161
+ − 162 quotient_definition
+ − 163 "permute_trm1 :: perm \<Rightarrow> trm1 \<Rightarrow> trm1"
1139
+ − 164 is
1029
+ − 165 "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"
+ − 166
1083
+ − 167 lemmas permute_trm1[simp] = permute_rtrm1_permute_bp.simps[quot_lifted]
+ − 168
1029
+ − 169 instance
+ − 170 apply default
+ − 171 apply(induct_tac [!] x rule: trm1_bp_inducts(1))
1083
+ − 172 apply(simp_all)
1029
+ − 173 done
+ − 174
+ − 175 end
+ − 176
1180
+ − 177 lemmas fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted]
1029
+ − 178
1180
+ − 179 lemmas fv_trm1_eqvt = fv_rtrm1_eqvt[quot_lifted]
1029
+ − 180
1073
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 181 lemmas alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
1029
+ − 182
1031
+ − 183 lemma lm1_supp_pre:
+ − 184 shows "(supp (atom x, t)) supports (Lm1 x t) "
+ − 185 apply(simp add: supports_def)
+ − 186 apply(fold fresh_def)
+ − 187 apply(simp add: fresh_Pair swap_fresh_fresh)
+ − 188 apply(clarify)
+ − 189 apply(subst swap_at_base_simps(3))
+ − 190 apply(simp_all add: fresh_atom)
+ − 191 done
+ − 192
+ − 193 lemma lt1_supp_pre:
+ − 194 shows "(supp (x, t, s)) supports (Lt1 t x s) "
+ − 195 apply(simp add: supports_def)
+ − 196 apply(fold fresh_def)
+ − 197 apply(simp add: fresh_Pair swap_fresh_fresh)
+ − 198 done
+ − 199
+ − 200 lemma bp_supp: "finite (supp (bp :: bp))"
+ − 201 apply (induct bp)
+ − 202 apply(simp_all add: supp_def)
+ − 203 apply (fold supp_def)
+ − 204 apply (simp add: supp_at_base)
+ − 205 apply(simp add: Collect_imp_eq)
+ − 206 apply(simp add: Collect_neg_eq[symmetric])
+ − 207 apply (fold supp_def)
+ − 208 apply (simp)
+ − 209 done
+ − 210
1030
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 211 instance trm1 :: fs
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 212 apply default
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 213 apply(induct_tac x rule: trm1_bp_inducts(1))
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 214 apply(simp_all)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 215 apply(simp add: supp_def alpha1_INJ eqvts)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 216 apply(simp add: supp_def[symmetric] supp_at_base)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 217 apply(simp only: supp_def alpha1_INJ eqvts permute_trm1)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 218 apply(simp add: Collect_imp_eq Collect_neg_eq)
1031
+ − 219 apply(rule supports_finite)
+ − 220 apply(rule lm1_supp_pre)
+ − 221 apply(simp add: supp_Pair supp_atom)
+ − 222 apply(rule supports_finite)
+ − 223 apply(rule lt1_supp_pre)
+ − 224 apply(simp add: supp_Pair supp_atom bp_supp)
+ − 225 done
1030
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 226
1029
+ − 227 lemma supp_fv:
+ − 228 shows "supp t = fv_trm1 t"
+ − 229 apply(induct t rule: trm1_bp_inducts(1))
1030
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 230 apply(simp_all)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 231 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 232 apply(simp only: supp_at_base[simplified supp_def])
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 233 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 234 apply(simp add: Collect_imp_eq Collect_neg_eq)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 235 apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)")
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 236 apply(simp add: supp_Abs fv_trm1)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 237 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 238 apply(simp add: alpha1_INJ)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 239 apply(simp add: Abs_eq_iff)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 240 apply(simp add: alpha_gen.simps)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 241 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric])
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 242 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)")
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 243 apply(simp add: supp_Abs fv_trm1)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 244 apply(simp (no_asm) add: supp_def)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 245 apply(simp add: alpha1_INJ)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 246 apply(simp add: Abs_eq_iff)
1033
+ − 247 apply(simp add: alpha_gen)
1030
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 248 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 249 apply(simp add: Collect_imp_eq Collect_neg_eq)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 250 done
1029
+ − 251
1032
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 252 lemma trm1_supp:
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 253 "supp (Vr1 x) = {atom x}"
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 254 "supp (Ap1 t1 t2) = supp t1 \<union> supp t2"
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 255 "supp (Lm1 x t) = (supp t) - {atom x}"
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 256 "supp (Lt1 b t s) = supp t \<union> (supp s - bv1 b)"
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 257 by (simp_all only: supp_fv fv_trm1)
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 258
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 259 lemma trm1_induct_strong:
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 260 assumes "\<And>name b. P b (Vr1 name)"
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 261 and "\<And>rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12\<rbrakk> \<Longrightarrow> P b (Ap1 rtrm11 rtrm12)"
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 262 and "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)"
1179
+ − 263 and "\<And>bp rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12; bv1 bp \<sharp>* b\<rbrakk> \<Longrightarrow> P b (Lt1 bp rtrm11 rtrm12)"
1032
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 264 shows "P a rtrma"
1035
+ − 265 sorry
1032
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 266
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 267 section {*** lets with single assignments ***}
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 268
1091
+ − 269 datatype rtrm2 =
+ − 270 rVr2 "name"
+ − 271 | rAp2 "rtrm2" "rtrm2"
1093
+ − 272 | rLm2 "name" "rtrm2" --"bind (name) in (rtrm2)"
+ − 273 | rLt2 "rassign" "rtrm2" --"bind (bv2 rassign) in (rtrm2)"
1091
+ − 274 and rassign =
+ − 275 rAs "name" "rtrm2"
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 276
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 277 (* to be given by the user *)
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 278 primrec
1091
+ − 279 rbv2
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 280 where
1091
+ − 281 "rbv2 (rAs x t) = {atom x}"
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 282
1180
+ − 283 local_setup {* define_raw_fv "Terms.rtrm2"
+ − 284 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv2}, 0)]]],
+ − 285 [[[(NONE, 0)], []]]] *}
+ − 286 print_theorems
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 287
1171
+ − 288 setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *}
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 289
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 290 inductive
1091
+ − 291 alpha2 :: "rtrm2 \<Rightarrow> rtrm2 \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100)
+ − 292 and
+ − 293 alpha2a :: "rassign \<Rightarrow> rassign \<Rightarrow> bool" ("_ \<approx>2a _" [100, 100] 100)
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 294 where
1091
+ − 295 a1: "a = b \<Longrightarrow> (rVr2 a) \<approx>2 (rVr2 b)"
+ − 296 | a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> rAp2 t1 s1 \<approx>2 rAp2 t2 s2"
+ − 297 | a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha2 fv_rtrm2 pi ({atom b}, s))) \<Longrightarrow> rLm2 a t \<approx>2 rLm2 b s"
1092
+ − 298 | a4: "\<lbrakk>\<exists>pi. ((rbv2 bt, t) \<approx>gen alpha2 fv_rtrm2 pi ((rbv2 bs), s));
+ − 299 \<exists>pi. ((rbv2 bt, bt) \<approx>gen alpha2a fv_rassign pi (rbv2 bs, bs))\<rbrakk>
+ − 300 \<Longrightarrow> rLt2 bt t \<approx>2 rLt2 bs s"
+ − 301 | a5: "\<lbrakk>a = b; t \<approx>2 s\<rbrakk> \<Longrightarrow> rAs a t \<approx>2a rAs b s" (* This way rbv2 can be lifted *)
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 302
1091
+ − 303 lemma alpha2_equivp:
+ − 304 "equivp alpha2"
+ − 305 "equivp alpha2a"
957
+ − 306 sorry
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 307
1091
+ − 308 quotient_type
+ − 309 trm2 = rtrm2 / alpha2
+ − 310 and
+ − 311 assign = rassign / alpha2a
+ − 312 by (auto intro: alpha2_equivp)
+ − 313
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 314
1092
+ − 315
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 316 section {*** lets with many assignments ***}
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 317
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 318 datatype trm3 =
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 319 Vr3 "name"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 320 | Ap3 "trm3" "trm3"
1093
+ − 321 | Lm3 "name" "trm3" --"bind (name) in (trm3)"
+ − 322 | Lt3 "assigns" "trm3" --"bind (bv3 assigns) in (trm3)"
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 323 and assigns =
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 324 ANil
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 325 | ACons "name" "trm3" "assigns"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 326
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 327 (* to be given by the user *)
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 328 primrec
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 329 bv3
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 330 where
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 331 "bv3 ANil = {}"
957
+ − 332 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)"
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 333
1180
+ − 334 local_setup {* define_raw_fv "Terms.trm3"
+ − 335 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term bv3}, 0)]]],
+ − 336 [[], [[(NONE, 0)], [], []]]] *}
+ − 337 print_theorems
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 338
1171
+ − 339 setup {* snd o define_raw_perms ["rtrm3", "assigns"] ["Terms.trm3", "Terms.assigns"] *}
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 340
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 341 inductive
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 342 alpha3 :: "trm3 \<Rightarrow> trm3 \<Rightarrow> bool" ("_ \<approx>3 _" [100, 100] 100)
1092
+ − 343 and
+ − 344 alpha3a :: "assigns \<Rightarrow> assigns \<Rightarrow> bool" ("_ \<approx>3a _" [100, 100] 100)
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 345 where
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 346 a1: "a = b \<Longrightarrow> (Vr3 a) \<approx>3 (Vr3 b)"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 347 | a2: "\<lbrakk>t1 \<approx>3 t2; s1 \<approx>3 s2\<rbrakk> \<Longrightarrow> Ap3 t1 s1 \<approx>3 Ap3 t2 s2"
1092
+ − 348 | a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha3 fv_rtrm3 pi ({atom b}, s))) \<Longrightarrow> Lm3 a t \<approx>3 Lm3 b s"
+ − 349 | a4: "\<lbrakk>\<exists>pi. ((bv3 bt, t) \<approx>gen alpha3 fv_trm3 pi ((bv3 bs), s));
+ − 350 \<exists>pi. ((bv3 bt, bt) \<approx>gen alpha3a fv_assign pi (bv3 bs, bs))\<rbrakk>
+ − 351 \<Longrightarrow> Lt3 bt t \<approx>3 Lt3 bs s"
+ − 352 | a5: "ANil \<approx>3a ANil"
+ − 353 | a6: "\<lbrakk>a = b; t \<approx>3 s; tt \<approx>3a st\<rbrakk> \<Longrightarrow> ACons a t tt \<approx>3a ACons b s st"
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 354
1092
+ − 355 lemma alpha3_equivp:
+ − 356 "equivp alpha3"
+ − 357 "equivp alpha3a"
957
+ − 358 sorry
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 359
1092
+ − 360 quotient_type
+ − 361 qtrm3 = trm3 / alpha3
+ − 362 and
+ − 363 qassigns = assigns / alpha3a
+ − 364 by (auto intro: alpha3_equivp)
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 365
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 366
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 367 section {*** lam with indirect list recursion ***}
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 368
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 369 datatype trm4 =
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 370 Vr4 "name"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 371 | Ap4 "trm4" "trm4 list"
1093
+ − 372 | Lm4 "name" "trm4" --"bind (name) in (trm)"
1180
+ − 373 print_theorems
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 374
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 375 thm trm4.recs
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 376
1180
+ − 377 local_setup {* define_raw_fv "Terms.trm4" [
+ − 378 [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]] ] *}
+ − 379 print_theorems
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 380
1171
+ − 381 (* there cannot be a clause for lists, as *)
1092
+ − 382 (* permutations are already defined in Nominal (also functions, options, and so on) *)
1171
+ − 383 setup {* snd o define_raw_perms ["trm4"] ["Terms.trm4"] *}
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 384
963
+ − 385 (* "repairing" of the permute function *)
+ − 386 lemma repaired:
+ − 387 fixes ts::"trm4 list"
+ − 388 shows "permute_trm4_list p ts = p \<bullet> ts"
+ − 389 apply(induct ts)
+ − 390 apply(simp_all)
+ − 391 done
+ − 392
976
+ − 393 thm permute_trm4_permute_trm4_list.simps
963
+ − 394 thm permute_trm4_permute_trm4_list.simps[simplified repaired]
+ − 395
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 396 inductive
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 397 alpha4 :: "trm4 \<Rightarrow> trm4 \<Rightarrow> bool" ("_ \<approx>4 _" [100, 100] 100)
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 398 and alpha4list :: "trm4 list \<Rightarrow> trm4 list \<Rightarrow> bool" ("_ \<approx>4list _" [100, 100] 100)
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 399 where
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 400 a1: "a = b \<Longrightarrow> (Vr4 a) \<approx>4 (Vr4 b)"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 401 | a2: "\<lbrakk>t1 \<approx>4 t2; s1 \<approx>4list s2\<rbrakk> \<Longrightarrow> Ap4 t1 s1 \<approx>4 Ap4 t2 s2"
1092
+ − 402 | a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha4 fv_rtrm4 pi ({atom b}, s))) \<Longrightarrow> Lm4 a t \<approx>4 Lm4 b s"
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 403 | a5: "[] \<approx>4list []"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 404 | a6: "\<lbrakk>t \<approx>4 s; ts \<approx>4list ss\<rbrakk> \<Longrightarrow> (t#ts) \<approx>4list (s#ss)"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 405
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 406 lemma alpha4_equivp: "equivp alpha4" sorry
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 407 lemma alpha4list_equivp: "equivp alpha4list" sorry
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 408
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 409 quotient_type
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 410 qtrm4 = trm4 / alpha4 and
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 411 qtrm4list = "trm4 list" / alpha4list
1042
+ − 412 by (simp_all add: alpha4_equivp alpha4list_equivp)
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 413
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 414
1035
+ − 415 datatype rtrm5 =
+ − 416 rVr5 "name"
+ − 417 | rAp5 "rtrm5" "rtrm5"
1093
+ − 418 | rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)"
1035
+ − 419 and rlts =
+ − 420 rLnil
+ − 421 | rLcons "name" "rtrm5" "rlts"
+ − 422
+ − 423 primrec
1050
+ − 424 rbv5
1035
+ − 425 where
1050
+ − 426 "rbv5 rLnil = {}"
+ − 427 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
1035
+ − 428
1180
+ − 429 local_setup {* define_raw_fv "Terms.rtrm5" [
+ − 430 [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[(NONE, 0)], [], []]] ] *}
+ − 431 print_theorems
1035
+ − 432
1171
+ − 433 setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *}
+ − 434 print_theorems
1035
+ − 435
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 436 inductive
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 437 alpha5 :: "rtrm5 \<Rightarrow> rtrm5 \<Rightarrow> bool" ("_ \<approx>5 _" [100, 100] 100)
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 438 and
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 439 alphalts :: "rlts \<Rightarrow> rlts \<Rightarrow> bool" ("_ \<approx>l _" [100, 100] 100)
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 440 where
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 441 a1: "a = b \<Longrightarrow> (rVr5 a) \<approx>5 (rVr5 b)"
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 442 | a2: "\<lbrakk>t1 \<approx>5 t2; s1 \<approx>5 s2\<rbrakk> \<Longrightarrow> rAp5 t1 s1 \<approx>5 rAp5 t2 s2"
1180
+ − 443 | a3: "\<lbrakk>\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 fv_rtrm5 pi (rbv5 l2, t2));
+ − 444 \<exists>pi. ((rbv5 l1, l1) \<approx>gen alphalts fv_rlts pi (rbv5 l2, l2))\<rbrakk>
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 445 \<Longrightarrow> rLt5 l1 t1 \<approx>5 rLt5 l2 t2"
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 446 | a4: "rLnil \<approx>l rLnil"
1040
+ − 447 | a5: "ls1 \<approx>l ls2 \<Longrightarrow> t1 \<approx>5 t2 \<Longrightarrow> n1 = n2 \<Longrightarrow> rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2"
+ − 448
+ − 449 print_theorems
1035
+ − 450
1040
+ − 451 lemma alpha5_inj:
+ − 452 "((rVr5 a) \<approx>5 (rVr5 b)) = (a = b)"
+ − 453 "(rAp5 t1 s1 \<approx>5 rAp5 t2 s2) = (t1 \<approx>5 t2 \<and> s1 \<approx>5 s2)"
1180
+ − 454 "(rLt5 l1 t1 \<approx>5 rLt5 l2 t2) = ((\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 fv_rtrm5 pi (rbv5 l2, t2))) \<and>
+ − 455 (\<exists>pi. ((rbv5 l1, l1) \<approx>gen alphalts fv_rlts pi (rbv5 l2, l2))))"
1040
+ − 456 "rLnil \<approx>l rLnil"
1057
+ − 457 "(rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2) = (n1 = n2 \<and> ls1 \<approx>l ls2 \<and> t1 \<approx>5 t2)"
1040
+ − 458 apply -
+ − 459 apply (simp_all add: alpha5_alphalts.intros)
+ − 460 apply rule
+ − 461 apply (erule alpha5.cases)
+ − 462 apply (simp_all add: alpha5_alphalts.intros)
+ − 463 apply rule
+ − 464 apply (erule alpha5.cases)
+ − 465 apply (simp_all add: alpha5_alphalts.intros)
+ − 466 apply rule
+ − 467 apply (erule alpha5.cases)
+ − 468 apply (simp_all add: alpha5_alphalts.intros)
+ − 469 apply rule
+ − 470 apply (erule alphalts.cases)
+ − 471 apply (simp_all add: alpha5_alphalts.intros)
+ − 472 done
+ − 473
+ − 474 lemma alpha5_equivps:
+ − 475 shows "equivp alpha5"
+ − 476 and "equivp alphalts"
+ − 477 sorry
+ − 478
+ − 479 quotient_type
+ − 480 trm5 = rtrm5 / alpha5
+ − 481 and
+ − 482 lts = rlts / alphalts
+ − 483 by (auto intro: alpha5_equivps)
+ − 484
1046
+ − 485 quotient_definition
+ − 486 "Vr5 :: name \<Rightarrow> trm5"
1139
+ − 487 is
1046
+ − 488 "rVr5"
+ − 489
+ − 490 quotient_definition
+ − 491 "Ap5 :: trm5 \<Rightarrow> trm5 \<Rightarrow> trm5"
1139
+ − 492 is
1046
+ − 493 "rAp5"
+ − 494
+ − 495 quotient_definition
+ − 496 "Lt5 :: lts \<Rightarrow> trm5 \<Rightarrow> trm5"
1139
+ − 497 is
1046
+ − 498 "rLt5"
+ − 499
+ − 500 quotient_definition
+ − 501 "Lnil :: lts"
1139
+ − 502 is
1046
+ − 503 "rLnil"
+ − 504
+ − 505 quotient_definition
+ − 506 "Lcons :: name \<Rightarrow> trm5 \<Rightarrow> lts \<Rightarrow> lts"
1139
+ − 507 is
1046
+ − 508 "rLcons"
+ − 509
+ − 510 quotient_definition
+ − 511 "fv_trm5 :: trm5 \<Rightarrow> atom set"
1139
+ − 512 is
1180
+ − 513 "fv_rtrm5"
1046
+ − 514
+ − 515 quotient_definition
1050
+ − 516 "fv_lts :: lts \<Rightarrow> atom set"
1139
+ − 517 is
1180
+ − 518 "fv_rlts"
1046
+ − 519
1050
+ − 520 quotient_definition
+ − 521 "bv5 :: lts \<Rightarrow> atom set"
1139
+ − 522 is
1050
+ − 523 "rbv5"
+ − 524
1092
+ − 525 lemma rbv5_eqvt:
+ − 526 "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)"
+ − 527 sorry
+ − 528
1180
+ − 529 lemma fv_rtrm5_eqvt:
+ − 530 "pi \<bullet> (fv_rtrm5 x) = fv_rtrm5 (pi \<bullet> x)"
1092
+ − 531 sorry
+ − 532
1180
+ − 533 lemma fv_rlts_eqvt:
+ − 534 "pi \<bullet> (fv_rlts x) = fv_rlts (pi \<bullet> x)"
1092
+ − 535 sorry
+ − 536
+ − 537 lemma alpha5_eqvt:
+ − 538 "xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)"
+ − 539 "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)"
+ − 540 apply(induct rule: alpha5_alphalts.inducts)
+ − 541 apply (simp_all add: alpha5_inj)
+ − 542 apply (erule exE)+
+ − 543 apply(unfold alpha_gen)
+ − 544 apply (erule conjE)+
+ − 545 apply (rule conjI)
+ − 546 apply (rule_tac x="x \<bullet> pi" in exI)
+ − 547 apply (rule conjI)
+ − 548 apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1])
1180
+ − 549 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt)
1092
+ − 550 apply(rule conjI)
+ − 551 apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1])
1180
+ − 552 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt)
1092
+ − 553 apply (subst permute_eqvt[symmetric])
+ − 554 apply (simp)
+ − 555 apply (rule_tac x="x \<bullet> pia" in exI)
+ − 556 apply (rule conjI)
+ − 557 apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1])
1180
+ − 558 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt)
1092
+ − 559 apply(rule conjI)
+ − 560 apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1])
1180
+ − 561 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt)
1092
+ − 562 apply (subst permute_eqvt[symmetric])
+ − 563 apply (simp)
+ − 564 done
+ − 565
1050
+ − 566 lemma alpha5_rfv:
1180
+ − 567 "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)"
+ − 568 "(l \<approx>l m \<Longrightarrow> fv_rlts l = fv_rlts m)"
1050
+ − 569 apply(induct rule: alpha5_alphalts.inducts)
+ − 570 apply(simp_all add: alpha_gen)
+ − 571 done
+ − 572
1053
+ − 573 lemma bv_list_rsp:
1055
+ − 574 shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"
1092
+ − 575 apply(induct rule: alpha5_alphalts.inducts(2))
+ − 576 apply(simp_all)
+ − 577 done
1053
+ − 578
1092
+ − 579 lemma [quot_respect]:
1180
+ − 580 "(alphalts ===> op =) fv_rlts fv_rlts"
+ − 581 "(alpha5 ===> op =) fv_rtrm5 fv_rtrm5"
1092
+ − 582 "(alphalts ===> op =) rbv5 rbv5"
+ − 583 "(op = ===> alpha5) rVr5 rVr5"
+ − 584 "(alpha5 ===> alpha5 ===> alpha5) rAp5 rAp5"
+ − 585 "(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5"
+ − 586 "(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5"
+ − 587 "(op = ===> alpha5 ===> alphalts ===> alphalts) rLcons rLcons"
+ − 588 "(op = ===> alpha5 ===> alpha5) permute permute"
+ − 589 "(op = ===> alphalts ===> alphalts) permute permute"
+ − 590 apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp)
1181
+ − 591 apply (clarify) apply (rule conjI)
1092
+ − 592 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
+ − 593 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
1181
+ − 594 apply (clarify) apply (rule conjI)
1092
+ − 595 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
+ − 596 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
+ − 597 done
1057
+ − 598
1092
+ − 599 lemma
1053
+ − 600 shows "(alphalts ===> op =) rbv5 rbv5"
+ − 601 by (simp add: bv_list_rsp)
+ − 602
1073
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 603 lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted]
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 604
1050
+ − 605 instantiation trm5 and lts :: pt
+ − 606 begin
+ − 607
+ − 608 quotient_definition
+ − 609 "permute_trm5 :: perm \<Rightarrow> trm5 \<Rightarrow> trm5"
1139
+ − 610 is
1050
+ − 611 "permute :: perm \<Rightarrow> rtrm5 \<Rightarrow> rtrm5"
+ − 612
+ − 613 quotient_definition
+ − 614 "permute_lts :: perm \<Rightarrow> lts \<Rightarrow> lts"
1139
+ − 615 is
1050
+ − 616 "permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts"
+ − 617
+ − 618 lemma trm5_lts_zero:
+ − 619 "0 \<bullet> (x\<Colon>trm5) = x"
+ − 620 "0 \<bullet> (y\<Colon>lts) = y"
1073
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 621 apply(induct x and y rule: trm5_lts_inducts)
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 622 apply(simp_all add: permute_rtrm5_permute_rlts.simps[quot_lifted])
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 623 done
1050
+ − 624
+ − 625 lemma trm5_lts_plus:
+ − 626 "(p + q) \<bullet> (x\<Colon>trm5) = p \<bullet> q \<bullet> x"
+ − 627 "(p + q) \<bullet> (y\<Colon>lts) = p \<bullet> q \<bullet> y"
1073
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 628 apply(induct x and y rule: trm5_lts_inducts)
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 629 apply(simp_all add: permute_rtrm5_permute_rlts.simps[quot_lifted])
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 630 done
1050
+ − 631
+ − 632 instance
+ − 633 apply default
+ − 634 apply (simp_all add: trm5_lts_zero trm5_lts_plus)
+ − 635 done
1040
+ − 636
1035
+ − 637 end
1050
+ − 638
1073
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 639 lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted]
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 640
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 641 lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
1050
+ − 642
1073
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 643 lemmas bv5[simp] = rbv5.simps[quot_lifted]
1050
+ − 644
1180
+ − 645 lemmas fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted]
1050
+ − 646
+ − 647 lemma lets_ok:
+ − 648 "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
+ − 649 apply (subst alpha5_INJ)
1057
+ − 650 apply (rule conjI)
+ − 651 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+ − 652 apply (simp only: alpha_gen)
+ − 653 apply (simp add: permute_trm5_lts fresh_star_def)
1050
+ − 654 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+ − 655 apply (simp only: alpha_gen)
1052
+ − 656 apply (simp add: permute_trm5_lts fresh_star_def)
+ − 657 done
1050
+ − 658
1058
+ − 659 lemma lets_ok2:
+ − 660 "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) =
+ − 661 (Lt5 (Lcons y (Vr5 y) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
+ − 662 apply (subst alpha5_INJ)
+ − 663 apply (rule conjI)
+ − 664 apply (rule_tac x="0 :: perm" in exI)
+ − 665 apply (simp only: alpha_gen)
+ − 666 apply (simp add: permute_trm5_lts fresh_star_def)
+ − 667 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+ − 668 apply (simp only: alpha_gen)
+ − 669 apply (simp add: permute_trm5_lts fresh_star_def)
+ − 670 done
+ − 671
+ − 672
1057
+ − 673 lemma lets_not_ok1:
1056
+ − 674 "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
1057
+ − 675 (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
+ − 676 apply (subst alpha5_INJ(3))
+ − 677 apply(clarify)
1056
+ − 678 apply (simp add: alpha_gen)
+ − 679 apply (simp add: permute_trm5_lts fresh_star_def)
1057
+ − 680 apply (simp add: alpha5_INJ(5))
+ − 681 apply(clarify)
+ − 682 apply (simp add: alpha5_INJ(2))
+ − 683 apply (simp only: alpha5_INJ(1))
1056
+ − 684 done
+ − 685
1058
+ − 686 lemma distinct_helper:
+ − 687 shows "\<not>(rVr5 x \<approx>5 rAp5 y z)"
+ − 688 apply auto
+ − 689 apply (erule alpha5.cases)
+ − 690 apply (simp_all only: rtrm5.distinct)
+ − 691 done
1057
+ − 692
1058
+ − 693 lemma distinct_helper2:
+ − 694 shows "(Vr5 x) \<noteq> (Ap5 y z)"
+ − 695 by (lifting distinct_helper)
1057
+ − 696
1058
+ − 697 lemma lets_nok:
+ − 698 "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
+ − 699 (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
+ − 700 (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
+ − 701 apply (subst alpha5_INJ)
+ − 702 apply (simp only: alpha_gen permute_trm5_lts fresh_star_def)
+ − 703 apply (subst alpha5_INJ(5))
+ − 704 apply (subst alpha5_INJ(5))
+ − 705 apply (simp add: distinct_helper2)
+ − 706 done
1057
+ − 707
1103
+ − 708
1105
+ − 709 (* example with a bn function defined over the type itself *)
1103
+ − 710 datatype rtrm6 =
+ − 711 rVr6 "name"
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 712 | rLm6 "name" "rtrm6"
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 713 | rLt6 "rtrm6" "rtrm6" --"bind (bv6 left) in (right)"
1103
+ − 714
+ − 715 primrec
+ − 716 rbv6
+ − 717 where
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 718 "rbv6 (rVr6 n) = {}"
1117
+ − 719 | "rbv6 (rLm6 n t) = {atom n} \<union> rbv6 t"
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 720 | "rbv6 (rLt6 l r) = rbv6 l \<union> rbv6 r"
1103
+ − 721
1180
+ − 722 local_setup {* define_raw_fv "Terms.rtrm6" [
+ − 723 [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv6}, 0)]]]] *}
+ − 724 print_theorems
1103
+ − 725
1171
+ − 726 setup {* snd o define_raw_perms ["rtrm6"] ["Terms.rtrm6"] *}
+ − 727 print_theorems
1103
+ − 728
+ − 729 inductive
+ − 730 alpha6 :: "rtrm6 \<Rightarrow> rtrm6 \<Rightarrow> bool" ("_ \<approx>6 _" [100, 100] 100)
+ − 731 where
+ − 732 a1: "a = b \<Longrightarrow> (rVr6 a) \<approx>6 (rVr6 b)"
1180
+ − 733 | a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha6 fv_rtrm6 pi ({atom b}, s))) \<Longrightarrow> rLm6 a t \<approx>6 rLm6 b s"
+ − 734 | a3: "(\<exists>pi. (((rbv6 t1), s1) \<approx>gen alpha6 fv_rtrm6 pi ((rbv6 t2), s2))) \<Longrightarrow> rLt6 t1 s1 \<approx>6 rLt6 t2 s2"
1103
+ − 735
+ − 736 lemma alpha6_equivps:
+ − 737 shows "equivp alpha6"
+ − 738 sorry
+ − 739
+ − 740 quotient_type
+ − 741 trm6 = rtrm6 / alpha6
+ − 742 by (auto intro: alpha6_equivps)
+ − 743
+ − 744 quotient_definition
+ − 745 "Vr6 :: name \<Rightarrow> trm6"
1139
+ − 746 is
1103
+ − 747 "rVr6"
+ − 748
+ − 749 quotient_definition
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 750 "Lm6 :: name \<Rightarrow> trm6 \<Rightarrow> trm6"
1139
+ − 751 is
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 752 "rLm6"
1103
+ − 753
+ − 754 quotient_definition
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 755 "Lt6 :: trm6 \<Rightarrow> trm6 \<Rightarrow> trm6"
1139
+ − 756 is
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 757 "rLt6"
1103
+ − 758
+ − 759 quotient_definition
+ − 760 "fv_trm6 :: trm6 \<Rightarrow> atom set"
1139
+ − 761 is
1180
+ − 762 "fv_rtrm6"
1103
+ − 763
+ − 764 quotient_definition
+ − 765 "bv6 :: trm6 \<Rightarrow> atom set"
1139
+ − 766 is
1103
+ − 767 "rbv6"
+ − 768
1106
+ − 769 lemma [quot_respect]:
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 770 "(op = ===> alpha6 ===> alpha6) permute permute"
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 771 apply auto (* will work with eqvt *)
1106
+ − 772 sorry
+ − 773
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 774 (* Definitely not true , see lemma below *)
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 775
1104
+ − 776 lemma [quot_respect]:"(alpha6 ===> op =) rbv6 rbv6"
+ − 777 apply simp apply clarify
+ − 778 apply (erule alpha6.induct)
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 779 oops
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 780
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 781 lemma "(a :: name) \<noteq> b \<Longrightarrow> \<not> (alpha6 ===> op =) rbv6 rbv6"
1104
+ − 782 apply simp
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 783 apply (rule_tac x="rLm6 (a::name) (rVr6 (a :: name))" in exI)
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 784 apply (rule_tac x="rLm6 (b::name) (rVr6 (b :: name))" in exI)
1104
+ − 785 apply simp
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 786 apply (rule a2)
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 787 apply (rule_tac x="(a \<leftrightarrow> b)" in exI)
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 788 apply (simp add: alpha_gen fresh_star_def)
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 789 apply (rule a1)
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 790 apply (rule refl)
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 791 done
1103
+ − 792
1180
+ − 793 lemma [quot_respect]:"(alpha6 ===> op =) fv_rtrm6 fv_rtrm6"
1106
+ − 794 apply simp apply clarify
+ − 795 apply (induct_tac x y rule: alpha6.induct)
+ − 796 apply simp_all
+ − 797 apply (erule exE)
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 798 apply (simp_all add: alpha_gen)
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 799 apply (erule conjE)+
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 800 apply (erule exE)
1106
+ − 801 apply (erule conjE)+
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 802 apply (simp)
1106
+ − 803 oops
1103
+ − 804
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 805
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 806 lemma [quot_respect]: "(op = ===> alpha6) rVr6 rVr6"
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 807 by (simp_all add: a1)
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 808
1103
+ − 809 lemma [quot_respect]:
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 810 "(op = ===> alpha6 ===> alpha6) rLm6 rLm6"
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 811 "(alpha6 ===> alpha6 ===> alpha6) rLt6 rLt6"
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 812 apply simp_all apply (clarify)
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 813 apply (rule a2)
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 814 apply (rule_tac x="0::perm" in exI)
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 815 apply (simp add: alpha_gen)
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 816 (* needs rfv6_rsp *) defer
1103
+ − 817 apply clarify
+ − 818 apply (rule a3)
+ − 819 apply (rule_tac x="0::perm" in exI)
+ − 820 apply (simp add: alpha_gen)
+ − 821 (* needs rbv6_rsp *)
1106
+ − 822 oops
1103
+ − 823
+ − 824 instantiation trm6 :: pt begin
+ − 825
1104
+ − 826 quotient_definition
+ − 827 "permute_trm6 :: perm \<Rightarrow> trm6 \<Rightarrow> trm6"
1139
+ − 828 is
1104
+ − 829 "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"
+ − 830
1103
+ − 831 instance
1106
+ − 832 apply default
1103
+ − 833 sorry
+ − 834 end
+ − 835
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 836 lemma lifted_induct:
1106
+ − 837 "\<lbrakk>x1 = x2; \<And>a b. a = b \<Longrightarrow> P (Vr6 a) (Vr6 b);
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 838 \<And>a t b s.
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 839 \<exists>pi. fv_trm6 t - {atom a} = fv_trm6 s - {atom b} \<and>
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 840 (fv_trm6 t - {atom a}) \<sharp>* pi \<and> pi \<bullet> t = s \<and> P (pi \<bullet> t) s \<Longrightarrow>
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 841 P (Lm6 a t) (Lm6 b s);
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 842 \<And>t1 s1 t2 s2.
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 843 \<exists>pi. fv_trm6 s1 - bv6 t1 = fv_trm6 s2 - bv6 t2 \<and>
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 844 (fv_trm6 s1 - bv6 t1) \<sharp>* pi \<and> pi \<bullet> s1 = s2 \<and> P (pi \<bullet> s1) s2 \<Longrightarrow>
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 845 P (Lt6 t1 s1) (Lt6 t2 s2)\<rbrakk>
1106
+ − 846 \<Longrightarrow> P x1 x2"
+ − 847 unfolding alpha_gen
+ − 848 apply (lifting alpha6.induct[unfolded alpha_gen])
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 849 apply injection
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 850 (* notice unsolvable goals: (alpha6 ===> op =) rbv6 rbv6 *)
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 851 oops
1106
+ − 852
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 853 lemma lifted_inject_a3:
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 854 "\<exists>pi. fv_trm6 s1 - bv6 t1 = fv_trm6 s2 - bv6 t2 \<and>
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 855 (fv_trm6 s1 - bv6 t1) \<sharp>* pi \<and> pi \<bullet> s1 = s2 \<Longrightarrow> Lt6 t1 s1 = Lt6 t2 s2"
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 856 apply(lifting a3[unfolded alpha_gen])
1103
+ − 857 apply injection
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 858 (* notice unsolvable goals: (alpha6 ===> op =) rbv6 rbv6 *)
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 859 oops
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 860
1103
+ − 861
+ − 862
+ − 863
1121
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 864 (* example with a respectful bn function defined over the type itself *)
1131
+ − 865
1121
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 866 datatype rtrm7 =
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 867 rVr7 "name"
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 868 | rLm7 "name" "rtrm7"
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 869 | rLt7 "rtrm7" "rtrm7" --"bind (bv7 left) in (right)"
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 870
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 871 primrec
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 872 rbv7
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 873 where
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 874 "rbv7 (rVr7 n) = {atom n}"
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 875 | "rbv7 (rLm7 n t) = rbv7 t - {atom n}"
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 876 | "rbv7 (rLt7 l r) = rbv7 l \<union> rbv7 r"
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 877
1180
+ − 878 local_setup {* define_raw_fv "Terms.rtrm7" [
+ − 879 [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv7}, 0)]]]] *}
+ − 880 print_theorems
1131
+ − 881
1171
+ − 882 setup {* snd o define_raw_perms ["rtrm7"] ["Terms.rtrm7"] *}
+ − 883 print_theorems
1131
+ − 884
+ − 885 inductive
+ − 886 alpha7 :: "rtrm7 \<Rightarrow> rtrm7 \<Rightarrow> bool" ("_ \<approx>7 _" [100, 100] 100)
+ − 887 where
+ − 888 a1: "a = b \<Longrightarrow> (rVr7 a) \<approx>7 (rVr7 b)"
1180
+ − 889 | a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha7 fv_rtrm7 pi ({atom b}, s))) \<Longrightarrow> rLm7 a t \<approx>7 rLm7 b s"
+ − 890 | a3: "(\<exists>pi. (((rbv7 t1), s1) \<approx>gen alpha7 fv_rtrm7 pi ((rbv7 t2), s2))) \<Longrightarrow> rLt7 t1 s1 \<approx>7 rLt7 t2 s2"
1121
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 891
1180
+ − 892 lemma bvfv7: "rbv7 x = fv_rtrm7 x"
1131
+ − 893 apply induct
+ − 894 apply simp_all
+ − 895 done
1121
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 896
1131
+ − 897 lemma "(x::name) \<noteq> y \<Longrightarrow> \<not> (alpha7 ===> op =) rbv7 rbv7"
+ − 898 apply simp
+ − 899 apply (rule_tac x="rLt7 (rVr7 x) (rVr7 x)" in exI)
+ − 900 apply (rule_tac x="rLt7 (rVr7 y) (rVr7 y)" in exI)
+ − 901 apply simp
+ − 902 apply (rule a3)
+ − 903 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+ − 904 apply (simp_all add: alpha_gen fresh_star_def)
+ − 905 apply (rule a1)
+ − 906 apply (rule refl)
+ − 907 done
1103
+ − 908
1133
+ − 909
+ − 910
+ − 911
+ − 912
1132
+ − 913 datatype rfoo8 =
+ − 914 Foo0 "name"
+ − 915 | Foo1 "rbar8" "rfoo8" --"bind bv(bar) in foo"
+ − 916 and rbar8 =
1135
+ − 917 Bar0 "name"
+ − 918 | Bar1 "name" "name" "rbar8" --"bind second name in b"
1132
+ − 919
+ − 920 primrec
+ − 921 rbv8
+ − 922 where
+ − 923 "rbv8 (Bar0 x) = {}"
+ − 924 | "rbv8 (Bar1 v x b) = {atom v}"
+ − 925
1180
+ − 926 local_setup {* define_raw_fv "Terms.rfoo8" [
+ − 927 [[[]], [[], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
+ − 928 print_theorems
1132
+ − 929
1171
+ − 930 setup {* snd o define_raw_perms ["rfoo8", "rbar8"] ["Terms.rfoo8", "Terms.rbar8"] *}
+ − 931 print_theorems
1132
+ − 932
+ − 933 inductive
+ − 934 alpha8f :: "rfoo8 \<Rightarrow> rfoo8 \<Rightarrow> bool" ("_ \<approx>f _" [100, 100] 100)
+ − 935 and
+ − 936 alpha8b :: "rbar8 \<Rightarrow> rbar8 \<Rightarrow> bool" ("_ \<approx>b _" [100, 100] 100)
+ − 937 where
+ − 938 a1: "a = b \<Longrightarrow> (Foo0 a) \<approx>f (Foo0 b)"
+ − 939 | a2: "a = b \<Longrightarrow> (Bar0 a) \<approx>b (Bar0 b)"
1180
+ − 940 | a3: "b1 \<approx>b b2 \<Longrightarrow> (\<exists>pi. (((rbv8 b1), t1) \<approx>gen alpha8f fv_rfoo8 pi ((rbv8 b2), t2))) \<Longrightarrow> Foo1 b1 t1 \<approx>f Foo1 b2 t2"
+ − 941 | a4: "v1 = v2 \<Longrightarrow> (\<exists>pi. (({atom x1}, t1) \<approx>gen alpha8b fv_rbar8 pi ({atom x2}, t2))) \<Longrightarrow> Bar1 v1 x1 t1 \<approx>b Bar1 v2 x2 t2"
1132
+ − 942
+ − 943 lemma "(alpha8b ===> op =) rbv8 rbv8"
+ − 944 apply simp apply clarify
+ − 945 apply (erule alpha8f_alpha8b.inducts(2))
+ − 946 apply (simp_all)
+ − 947 done
1134
+ − 948
1180
+ − 949 lemma fv_rbar8_rsp_hlp: "x \<approx>b y \<Longrightarrow> fv_rbar8 x = fv_rbar8 y"
1132
+ − 950 apply (erule alpha8f_alpha8b.inducts(2))
1133
+ − 951 apply (simp_all add: alpha_gen)
1132
+ − 952 done
1180
+ − 953 lemma "(alpha8b ===> op =) fv_rbar8 fv_rbar8"
+ − 954 apply simp apply clarify apply (simp add: fv_rbar8_rsp_hlp)
1134
+ − 955 done
1132
+ − 956
1180
+ − 957 lemma "(alpha8f ===> op =) fv_rfoo8 fv_rfoo8"
1134
+ − 958 apply simp apply clarify
+ − 959 apply (erule alpha8f_alpha8b.inducts(1))
1180
+ − 960 apply (simp_all add: alpha_gen fv_rbar8_rsp_hlp)
1133
+ − 961 done
1132
+ − 962
+ − 963
+ − 964
1103
+ − 965
1134
+ − 966
1135
+ − 967
+ − 968 datatype rlam9 =
+ − 969 Var9 "name"
+ − 970 | Lam9 "name" "rlam9" --"bind name in rlam"
+ − 971 and rbla9 =
+ − 972 Bla9 "rlam9" "rlam9" --"bind bv(first) in second"
+ − 973
+ − 974 primrec
+ − 975 rbv9
+ − 976 where
+ − 977 "rbv9 (Var9 x) = {}"
+ − 978 | "rbv9 (Lam9 x b) = {atom x}"
+ − 979
1180
+ − 980 local_setup {* define_raw_fv "Terms.rlam9" [
+ − 981 [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[], [(SOME @{term rbv9}, 0)]]]] *}
+ − 982 print_theorems
1135
+ − 983
1171
+ − 984 setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Terms.rlam9", "Terms.rbla9"] *}
+ − 985 print_theorems
1135
+ − 986
+ − 987 inductive
+ − 988 alpha9l :: "rlam9 \<Rightarrow> rlam9 \<Rightarrow> bool" ("_ \<approx>9l _" [100, 100] 100)
+ − 989 and
+ − 990 alpha9b :: "rbla9 \<Rightarrow> rbla9 \<Rightarrow> bool" ("_ \<approx>9b _" [100, 100] 100)
+ − 991 where
+ − 992 a1: "a = b \<Longrightarrow> (Var9 a) \<approx>9l (Var9 b)"
1180
+ − 993 | a4: "(\<exists>pi. (({atom x1}, t1) \<approx>gen alpha9l fv_rlam9 pi ({atom x2}, t2))) \<Longrightarrow> Lam9 x1 t1 \<approx>9l Lam9 x2 t2"
+ − 994 | a3: "b1 \<approx>9l b2 \<Longrightarrow> (\<exists>pi. (((rbv9 b1), t1) \<approx>gen alpha9l fv_rlam9 pi ((rbv9 b2), t2))) \<Longrightarrow> Bla9 b1 t1 \<approx>9b Bla9 b2 t2"
1135
+ − 995
+ − 996 quotient_type
+ − 997 lam9 = rlam9 / alpha9l and bla9 = rbla9 / alpha9b
+ − 998 sorry
+ − 999
+ − 1000 quotient_definition
+ − 1001 "qVar9 :: name \<Rightarrow> lam9"
1139
+ − 1002 is
1135
+ − 1003 "Var9"
+ − 1004
+ − 1005 quotient_definition
+ − 1006 "qLam :: name \<Rightarrow> lam9 \<Rightarrow> lam9"
1139
+ − 1007 is
1135
+ − 1008 "Lam9"
+ − 1009
+ − 1010 quotient_definition
+ − 1011 "qBla9 :: lam9 \<Rightarrow> lam9 \<Rightarrow> bla9"
1139
+ − 1012 is
1135
+ − 1013 "Bla9"
+ − 1014
+ − 1015 quotient_definition
+ − 1016 "fv_lam9 :: lam9 \<Rightarrow> atom set"
1139
+ − 1017 is
1180
+ − 1018 "fv_rlam9"
1135
+ − 1019
+ − 1020 quotient_definition
+ − 1021 "fv_bla9 :: bla9 \<Rightarrow> atom set"
1139
+ − 1022 is
1180
+ − 1023 "fv_rbla9"
1135
+ − 1024
+ − 1025 quotient_definition
+ − 1026 "bv9 :: lam9 \<Rightarrow> atom set"
1139
+ − 1027 is
1135
+ − 1028 "rbv9"
+ − 1029
+ − 1030 instantiation lam9 and bla9 :: pt
+ − 1031 begin
+ − 1032
+ − 1033 quotient_definition
+ − 1034 "permute_lam9 :: perm \<Rightarrow> lam9 \<Rightarrow> lam9"
1139
+ − 1035 is
1135
+ − 1036 "permute :: perm \<Rightarrow> rlam9 \<Rightarrow> rlam9"
+ − 1037
+ − 1038 quotient_definition
+ − 1039 "permute_bla9 :: perm \<Rightarrow> bla9 \<Rightarrow> bla9"
1139
+ − 1040 is
1135
+ − 1041 "permute :: perm \<Rightarrow> rbla9 \<Rightarrow> rbla9"
+ − 1042
+ − 1043 instance
+ − 1044 sorry
+ − 1045
+ − 1046 end
+ − 1047
+ − 1048 lemma "\<lbrakk>b1 = b2; \<exists>pi. fv_lam9 t1 - bv9 b1 = fv_lam9 t2 - bv9 b2 \<and> (fv_lam9 t1 - bv9 b1) \<sharp>* pi \<and> pi \<bullet> t1 = t2\<rbrakk>
+ − 1049 \<Longrightarrow> qBla9 b1 t1 = qBla9 b2 t2"
+ − 1050 apply (lifting a3[unfolded alpha_gen])
+ − 1051 apply injection
+ − 1052 sorry
+ − 1053
+ − 1054
+ − 1055
+ − 1056
+ − 1057
+ − 1058
+ − 1059
+ − 1060
1048
+ − 1061 text {* type schemes *}
+ − 1062 datatype ty =
+ − 1063 Var "name"
+ − 1064 | Fun "ty" "ty"
+ − 1065
1171
+ − 1066 setup {* snd o define_raw_perms ["ty"] ["Terms.ty"] *}
+ − 1067 print_theorems
1048
+ − 1068
+ − 1069 datatype tyS =
+ − 1070 All "name set" "ty"
1046
+ − 1071
1171
+ − 1072 setup {* snd o define_raw_perms ["tyS"] ["Terms.tyS"] *}
+ − 1073 print_theorems
1040
+ − 1074
1048
+ − 1075 abbreviation
+ − 1076 "atoms xs \<equiv> {atom x| x. x \<in> xs}"
+ − 1077
1180
+ − 1078 local_setup {* define_raw_fv "Terms.ty" [[[[]], [[], []]]] *}
+ − 1079 print_theorems
+ − 1080
+ − 1081 (*
+ − 1082 doesn't work yet
+ − 1083 local_setup {* define_raw_fv "Terms.tyS" [[[[], []]]] *}
+ − 1084 print_theorems
+ − 1085 *)
1048
+ − 1086
+ − 1087 primrec
1180
+ − 1088 fv_tyS
1048
+ − 1089 where
1180
+ − 1090 "fv_tyS (All xs T) = (fv_ty T - atoms xs)"
1048
+ − 1091
+ − 1092 inductive
+ − 1093 alpha_tyS :: "tyS \<Rightarrow> tyS \<Rightarrow> bool" ("_ \<approx>tyS _" [100, 100] 100)
+ − 1094 where
1180
+ − 1095 a1: "\<exists>pi. ((atoms xs1, T1) \<approx>gen (op =) fv_ty pi (atoms xs2, T2))
1048
+ − 1096 \<Longrightarrow> All xs1 T1 \<approx>tyS All xs2 T2"
+ − 1097
+ − 1098 lemma
+ − 1099 shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {b, a} (Fun (Var a) (Var b))"
+ − 1100 apply(rule a1)
+ − 1101 apply(simp add: alpha_gen)
+ − 1102 apply(rule_tac x="0::perm" in exI)
+ − 1103 apply(simp add: fresh_star_def)
+ − 1104 done
+ − 1105
+ − 1106 lemma
+ − 1107 shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var b) (Var a))"
+ − 1108 apply(rule a1)
+ − 1109 apply(simp add: alpha_gen)
+ − 1110 apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
+ − 1111 apply(simp add: fresh_star_def)
+ − 1112 done
+ − 1113
+ − 1114 lemma
+ − 1115 shows "All {a, b, c} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var a) (Var b))"
+ − 1116 apply(rule a1)
+ − 1117 apply(simp add: alpha_gen)
+ − 1118 apply(rule_tac x="0::perm" in exI)
+ − 1119 apply(simp add: fresh_star_def)
+ − 1120 done
+ − 1121
+ − 1122 lemma
+ − 1123 assumes a: "a \<noteq> b"
+ − 1124 shows "\<not>(All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {c} (Fun (Var c) (Var c)))"
+ − 1125 using a
+ − 1126 apply(clarify)
+ − 1127 apply(erule alpha_tyS.cases)
+ − 1128 apply(simp add: alpha_gen)
+ − 1129 apply(erule conjE)+
+ − 1130 apply(erule exE)
+ − 1131 apply(erule conjE)+
+ − 1132 apply(clarify)
+ − 1133 apply(simp)
+ − 1134 apply(simp add: fresh_star_def)
+ − 1135 apply(auto)
+ − 1136 done
1051
+ − 1137
1048
+ − 1138
1035
+ − 1139 end