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 1343 693df83172f0
parent 1300 22a084c9316b
child 1345 8d2667ebe26c
equal deleted inserted replaced
1342:2b98012307f7 1343:693df83172f0 
   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 
   146 lemma fv_eq_bv: "fv_bp bp = bv1 bp"
 
   146 lemma fv_eq_bv: "fv_bp bp = bv1 bp"
 
   147 apply(induct bp rule: trm1_bp_inducts(2))
 
   147 apply(induct bp rule: trm1_bp_inducts(2))
 
   148 apply(simp_all)
 
   148 apply(simp_all)
 
   171 apply(induct t and b rule: trm1_bp_inducts)
 
   171 apply(induct t and b rule: trm1_bp_inducts)
 
   172 apply(simp_all)
 
   172 apply(simp_all)
 
   173 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
 
   173 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
 
   174 apply(simp only: supp_at_base[simplified supp_def])
 
   174 apply(simp only: supp_at_base[simplified supp_def])
 
   175 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
 
   175 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
 
   176 apply(simp add: Collect_imp_eq Collect_neg_eq)
 
   176 apply(simp add: Collect_imp_eq Collect_neg_eq Un_commute)
 
   177 apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)")
 
   177 apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)")
 
   178 apply(simp add: supp_Abs fv_trm1)
 
   178 apply(simp add: supp_Abs fv_trm1)
 
   179 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt permute_trm1)
 
   179 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt permute_trm1)
 
   180 apply(simp add: alpha1_INJ)
 
   180 apply(simp add: alpha1_INJ)
 
   181 apply(simp add: Abs_eq_iff)
 
   181 apply(simp add: Abs_eq_iff)
 
   182 apply(simp add: alpha_gen.simps)
 
   182 apply(simp add: alpha_gen.simps)
 
   183 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric])
 
   183 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)")
 
   184 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)
 
   185 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt)
 
   193 apply(simp (no_asm) add: supp_def eqvts)
 
   186 apply(simp (no_asm) add: supp_def eqvts)
 
   194 apply(fold supp_def)
 
   187 apply(fold supp_def)
 
   195 apply(simp add: supp_at_base)
 
   188 apply(simp add: supp_at_base)
 
   196 apply(simp (no_asm) add: supp_def Collect_imp_eq Collect_neg_eq)
 
   189 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])
 
   190 apply(simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric] supp_def[symmetric])
 
   198 done
 
   191 (*apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp (Abs (bv1 bp) (rtrm12)) \<union> supp(rtrm11)*)
 
       
   192 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp (Abs (bv1 bp) (bp, rtrm12)) \<union> supp(rtrm11)")
 
       
   193 apply(simp add: supp_Abs fv_trm1 supp_Pair Un_Diff Un_assoc fv_eq_bv)
 
       
   194 apply(blast) (* Un_commute in a good place *)
 
       
   195 apply(simp (no_asm) only: supp_def permute_trm1)
 
       
   196 apply(simp only: alpha1_INJ)
 
       
   197 apply(simp only: Un_commute)
 
       
   198 apply(simp add: Collect_imp_eq)
 
       
   199 apply(simp add: Collect_neg_eq[symmetric])
 
       
   200 apply(simp only: Abs_eq_iff)
 
       
   201 apply(simp add: alpha_bp_eq)
 
       
   202 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv)
 
       
   203 apply(simp add: alpha_gen fv_eq_bv supp_Pair)
 
       
   204 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv)
 
       
   205 apply(simp add: Collect_imp_eq Collect_neg_eq Collect_disj_eq fresh_star_def helper2)
 
       
   206 sorry
 
   199 
   207 
   200 lemma trm1_supp:
 
   208 lemma trm1_supp:
 
   201   "supp (Vr1 x) = {atom x}"
 
   209   "supp (Vr1 x) = {atom x}"
 
   202   "supp (Ap1 t1 t2) = supp t1 \<union> supp t2"
 
   210   "supp (Ap1 t1 t2) = supp t1 \<union> supp t2"
 
   203   "supp (Lm1 x t) = (supp t) - {atom x}"
 
   211   "supp (Lm1 x t) = (supp t) - {atom x}"
nominal2