Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Term1.thy
changeset 1355 7b0c6d07a24e
parent 1349 6204137160d8
child 1356 094811120a68
equal deleted inserted replaced
1354:367f67311e6f 1355:7b0c6d07a24e 
   136   apply (induct x and b rule: trm1_bp_inducts)
 
   136   apply (induct x and b rule: trm1_bp_inducts)
 
   137   apply(tactic {* ALLGOALS (rtac @{thm supports_finite} THEN' resolve_tac @{thms supports}) *})
 
   137   apply(tactic {* ALLGOALS (rtac @{thm supports_finite} THEN' resolve_tac @{thms supports}) *})
 
   138   apply(simp_all add: supp_atom)
 
   138   apply(simp_all add: supp_atom)
 
   139   done
 
   139   done
 
   140 
   140 
   141 instance trm1 :: fs
 
   141 instance trm1 and bp :: fs
 
   142 apply default
 
   142 apply default
 
   143 apply (rule rtrm1_bp_fs(1))
 
   143 apply (rule rtrm1_bp_fs)+
 
   144 done
 
   144 done
 
   145 
   145 lemma fv_eq_bv_pre: "fv_bp bp = bv1 bp"
 
   146 lemma fv_eq_bv: "fv_bp bp = bv1 bp"
 
       
   147 apply(induct bp rule: trm1_bp_inducts(2))
 
   146 apply(induct bp rule: trm1_bp_inducts(2))
 
   148 apply(simp_all)
 
   147 apply(simp_all)
 
       
   148 done
 
       
   149 
       
   150 lemma fv_eq_bv: "fv_bp = bv1"
 
       
   151 apply(rule ext)
 
       
   152 apply(rule fv_eq_bv_pre)
 
   149 done
 
   153 done
 
   150 
   154 
   151 lemma helper2: "{b. \<forall>pi. pi \<bullet> (a \<rightleftharpoons> b) \<bullet> bp \<noteq> bp} = {}"
 
   155 lemma helper2: "{b. \<forall>pi. pi \<bullet> (a \<rightleftharpoons> b) \<bullet> bp \<noteq> bp} = {}"
 
   152 apply auto
 
   156 apply auto
 
   153 apply (rule_tac x="(x \<rightleftharpoons> a)" in exI)
 
   157 apply (rule_tac x="(x \<rightleftharpoons> a)" in exI)
 
   162 
   166 
   163 lemma alpha_bp_eq: "alpha_bp = (op =)"
 
   167 lemma alpha_bp_eq: "alpha_bp = (op =)"
 
   164 apply (rule ext)+
 
   168 apply (rule ext)+
 
   165 apply (rule alpha_bp_eq_eq)
 
   169 apply (rule alpha_bp_eq_eq)
 
   166 done
 
   170 done
 
       
   171 
       
   172 lemma ex_out: 
       
   173   "(\<exists>x. Z x \<and> Q) = (Q \<and> (\<exists>x. Z x))"
 
       
   174   "(\<exists>x. Q \<and> Z x) = (Q \<and> (\<exists>x. Z x))"
 
       
   175   "(\<exists>x. P x \<and> Q \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))"
 
       
   176   "(\<exists>x. Q \<and> P x \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))"
 
       
   177   "(\<exists>x. Q \<and> P x \<and> Z x \<and> W x) = (Q \<and> (\<exists>x. P x \<and> Z x \<and> W x))"
 
       
   178 apply (blast)+
 
       
   179 done
 
       
   180 
       
   181 lemma "(Abs bs (x, x') = Abs cs (y, y')) = (\<exists>p. (bs, x) \<approx>gen op = supp p (cs, y) \<and> (bs, x') \<approx>gen op = supp p (cs, y'))"
 
       
   182 thm Abs_eq_iff
 
       
   183 apply (simp add: Abs_eq_iff)
 
       
   184 apply (rule arg_cong[of _ _ "Ex"])
 
       
   185 apply (rule ext)
 
       
   186 apply (simp only: alpha_gen)
 
       
   187 apply (simp only: supp_Pair eqvts)
 
       
   188 apply rule
 
       
   189 apply (erule conjE)+
 
       
   190 oops
 
       
   191 
       
   192 lemma "(f (p \<bullet> bp), p \<bullet> bp) \<approx>gen op = f pi (f bp, bp) = False"
 
       
   193 apply (simp add: alpha_gen fresh_star_def)
 
       
   194 oops
 
       
   195 
       
   196 (* TODO: permute_ABS should be in eqvt? *)
 
       
   197 
       
   198 lemma Collect_neg_conj: "{x. \<not>(P x \<and> Q x)} = {x. \<not>(P x)} \<union> {x. \<not>(Q x)}"
 
       
   199 by (simp add: Collect_imp_eq Collect_neg_eq[symmetric])
 
       
   200 
       
   201 lemma "
 
       
   202 {a\<Colon>atom. infinite ({b\<Colon>atom. \<not> (\<exists>pi\<Colon>perm. P pi a b \<and> Q pi a b)})} =
 
       
   203 {a\<Colon>atom. infinite {b\<Colon>atom. \<not> (\<exists>p\<Colon>perm. P p a b)}} \<union>
 
       
   204 {a\<Colon>atom. infinite {b\<Colon>atom. \<not> (\<exists>p\<Colon>perm. Q p a b)}}"
 
       
   205 oops
 
       
   206 
       
   207 lemma inf_or: "(infinite x \<or> infinite y) = infinite (x \<union> y)"
 
       
   208 by (simp add: finite_Un)
 
       
   209 
       
   210 
       
   211 lemma supp_fv_let:
 
       
   212   assumes sa : "fv_bp bp = supp bp"
 
       
   213   shows "\<lbrakk>fv_trm1 rtrm11 = supp rtrm11; fv_trm1 rtrm12 = supp rtrm12\<rbrakk>
 
       
   214        \<Longrightarrow> supp (Lt1 bp rtrm11 rtrm12) = fv_trm1 (Lt1 bp rtrm11 rtrm12)"
 
       
   215 apply(simp only: fv_trm1 fv_eq_bv sa[simplified fv_eq_bv])
 
       
   216 apply(fold supp_Abs)
 
       
   217 apply(simp only: fv_trm1 fv_eq_bv sa[simplified fv_eq_bv,symmetric])
 
       
   218 apply(simp (no_asm) only: supp_def permute_set_eq permute_trm1 alpha1_INJ)
 
       
   219 apply(simp only: ex_out Collect_neg_conj permute_ABS Abs_eq_iff)
 
       
   220 apply(simp only: alpha_bp_eq fv_eq_bv)
 
       
   221 apply(simp only: alpha_gen fv_eq_bv supp_Pair)
 
       
   222 apply(simp only: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv sa[simplified fv_eq_bv,symmetric])
 
       
   223 apply(simp only: Un_left_commute)
 
       
   224 apply simp
 
       
   225 apply(simp add: fresh_star_def) apply(fold fresh_star_def)
 
       
   226 apply(simp add: Collect_imp_eq Collect_neg_eq[symmetric])
 
       
   227 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl)
 
       
   228 apply(simp only: Un_assoc[symmetric])
 
       
   229 apply(simp only: Un_commute)
 
       
   230 apply(simp only: Un_left_commute)
 
       
   231 apply(simp only: Un_assoc[symmetric])
 
       
   232 apply(simp only: Un_commute)
 
       
   233 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl)
 
       
   234 apply(simp only: Collect_disj_eq[symmetric] inf_or)
 
       
   235 sorry
 
   167 
   236 
   168 lemma supp_fv:
 
   237 lemma supp_fv:
 
   169   "supp t = fv_trm1 t"
 
   238   "supp t = fv_trm1 t"
 
   170   "supp b = fv_bp b"
 
   239   "supp b = fv_bp b"
 
   171 apply(induct t and b rule: trm1_bp_inducts)
 
   240 apply(induct t and b rule: trm1_bp_inducts)
 
   172 apply(simp_all)
 
   241 apply(simp_all)
 
   173 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
 
   242 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
 
   174 apply(simp only: supp_at_base[simplified supp_def])
 
   243 apply(simp only: supp_at_base[simplified supp_def])
 
   175 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
 
   244 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
 
   176 apply(simp add: Collect_imp_eq Collect_neg_eq)
 
   245 apply(simp add: Collect_imp_eq Collect_neg_eq Un_commute)
 
   177 apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)")
 
   246 apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)")
 
   178 apply(simp add: supp_Abs fv_trm1)
 
   247 apply(simp add: supp_Abs fv_trm1)
 
   179 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt permute_trm1)
 
   248 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt permute_trm1)
 
   180 apply(simp add: alpha1_INJ)
 
   249 apply(simp add: alpha1_INJ)
 
   181 apply(simp add: Abs_eq_iff)
 
   250 apply(simp add: Abs_eq_iff)
 
   182 apply(simp add: alpha_gen.simps)
 
   251 apply(simp add: alpha_gen.simps)
 
   183 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric])
 
   252 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric])
 
   184 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)")
 
   253 defer
 
   185 apply(simp add: supp_Abs fv_trm1 fv_eq_bv)
 
       
   186 apply(simp (no_asm) add: supp_def permute_trm1)
 
       
   187 apply(simp add: alpha1_INJ alpha_bp_eq)
 
       
   188 apply(simp add: Abs_eq_iff)
 
       
   189 apply(simp add: alpha_gen)
 
       
   190 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv)
 
       
   191 apply(simp add: Collect_imp_eq Collect_neg_eq fresh_star_def helper2)
 
       
   192 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt)
 
   254 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt)
 
   193 apply(simp (no_asm) add: supp_def eqvts)
 
   255 apply(simp (no_asm) add: supp_def eqvts)
 
   194 apply(fold supp_def)
 
   256 apply(fold supp_def)
 
   195 apply(simp add: supp_at_base)
 
   257 apply(simp add: supp_at_base)
 
   196 apply(simp (no_asm) add: supp_def Collect_imp_eq Collect_neg_eq)
 
   258 apply(simp (no_asm) add: supp_def Collect_imp_eq Collect_neg_eq)
 
   197 apply(simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric] supp_def[symmetric])
 
   259 apply(simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric] supp_def[symmetric])
 
   198 done
 
   260 (*apply(rule supp_fv_let) apply(simp_all)*)
 
       
   261 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp (Abs (bv1 bp) (rtrm12)) \<union> supp(rtrm11)")
 
       
   262 (*apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp (Abs (bv1 bp) (bp, rtrm12)) \<union> supp(rtrm11)")*)
 
       
   263 apply(simp add: supp_Abs fv_trm1 supp_Pair Un_Diff Un_assoc fv_eq_bv)
 
       
   264 apply(blast) (* Un_commute in a good place *)
 
       
   265 apply(simp (no_asm) only: supp_def permute_set_eq atom_eqvt permute_trm1)
 
       
   266 apply(simp only: alpha1_INJ permute_ABS permute_prod.simps Abs_eq_iff)
 
       
   267 apply(simp only: ex_out)
 
       
   268 apply(simp only: Un_commute)
 
       
   269 apply(simp only: alpha_bp_eq fv_eq_bv)
 
       
   270 apply(simp only: alpha_gen fv_eq_bv supp_Pair)
 
       
   271 apply(simp only: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv)
 
       
   272 apply(simp only: ex_out)
 
       
   273 apply(simp only: Collect_neg_conj finite_Un Diff_cancel)
 
       
   274 apply(simp)
 
       
   275 apply(simp add: Collect_imp_eq)
 
       
   276 apply(simp add: Collect_neg_eq[symmetric] fresh_star_def)
 
       
   277 apply(fold supp_def)
 
       
   278 sorry
 
   199 
   279 
   200 lemma trm1_supp:
 
   280 lemma trm1_supp:
 
   201   "supp (Vr1 x) = {atom x}"
 
   281   "supp (Vr1 x) = {atom x}"
 
   202   "supp (Ap1 t1 t2) = supp t1 \<union> supp t2"
 
   282   "supp (Ap1 t1 t2) = supp t1 \<union> supp t2"
 
   203   "supp (Lm1 x t) = (supp t) - {atom x}"
 
   283   "supp (Lm1 x t) = (supp t) - {atom x}"
nominal2