nominal2: comparison Nominal/Abs.thy

equal deleted inserted replaced

-:e8cf0520c820
+:7b3dd407f6b3
 unfolding Diff_eqvt[symmetric]
 apply(erule_tac [!] exE)
 apply(rule_tac [!] x="p \<bullet> pa" in exI)
 by (auto simp add: fresh_star_permute_iff permute_eqvt[symmetric])
-fun
-aux_set
-where
-"aux_set (bs, x) = (supp x) - bs"
-fun
-aux_list
-where
-"aux_list (cs, x) = (supp x) - (set cs)"
-lemma aux_abs_lemma:
-assumes a: "(bs, x) \<approx>abs (cs, y)"
-shows "aux_set (bs, x) = aux_set (cs, y)"
-using a
-by (induct rule: alpha_abs.induct)
-(simp add: alphas_abs alphas)
-lemma aux_abs_res_lemma:
-assumes a: "(bs, x) \<approx>abs_res (cs, y)"
-shows "aux_set (bs, x) = aux_set (cs, y)"
-using a
-by (induct rule: alpha_abs_res.induct)
-(simp add: alphas_abs alphas)
-lemma aux_abs_list_lemma:
-assumes a: "(bs, x) \<approx>abs_lst (cs, y)"
-shows "aux_list (bs, x) = aux_list (cs, y)"
-using a
-by (induct rule: alpha_abs_lst.induct)
-(simp add: alphas_abs alphas)
 quotient_type
 'a abs_gen = "(atom set \<times> 'a::pt)" / "alpha_abs"
 and 'b abs_res = "(atom set \<times> 'b::pt)" / "alpha_abs_res"
 and 'c abs_lst = "(atom list \<times> 'c::pt)" / "alpha_abs_lst"
 apply(rule_tac [!] equivpI)
 and   "(op= ===> alpha_abs_res ===> alpha_abs_res) permute permute"
 and   "(op= ===> alpha_abs_lst ===> alpha_abs_lst) permute permute"
 unfolding fun_rel_def
 by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)
-lemma [quot_respect]:
+lemma abs_exhausts:
-shows "(alpha_abs ===> op=) aux_set aux_set"
+shows "(\<And>as (x::'a::pt). y1 = Abs as x \<Longrightarrow> P1) \<Longrightarrow> P1"
-and   "(alpha_abs_res ===> op=) aux_set aux_set"
+and   "(\<And>as (x::'a::pt). y2 = Abs_res as x \<Longrightarrow> P2) \<Longrightarrow> P2"
-and   "(alpha_abs_lst ===> op=) aux_list aux_list"
+and   "(\<And>as (x::'a::pt). y3 = Abs_lst as x \<Longrightarrow> P3) \<Longrightarrow> P3"
-unfolding fun_rel_def
+by (lifting prod.exhaust[where 'a="atom set" and 'b="'a"]
-apply(rule_tac [!] allI)
+prod.exhaust[where 'a="atom set" and 'b="'a"]
-apply(rule_tac [!] allI)
+prod.exhaust[where 'a="atom list" and 'b="'a"])
-apply(case_tac [!] x, case_tac [!] y)
-apply(rule_tac [!] impI)
-by (simp_all only: aux_abs_lemma aux_abs_res_lemma aux_abs_list_lemma)
-lemma abs_inducts:
-shows "(\<And>as (x::'a::pt). P1 (Abs as x)) \<Longrightarrow> P1 x1"
-and   "(\<And>as (x::'a::pt). P2 (Abs_res as x)) \<Longrightarrow> P2 x2"
-and   "(\<And>as (x::'a::pt). P3 (Abs_lst as x)) \<Longrightarrow> P3 x3"
-by (lifting prod.induct[where 'a="atom set" and 'b="'a"]
-prod.induct[where 'a="atom set" and 'b="'a"]
-prod.induct[where 'a="atom list" and 'b="'a"])
 lemma abs_eq_iff:
 shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (cs, y)"
 and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (bs, x) \<approx>abs_res (cs, y)"
 and   "Abs_lst ds x = Abs_lst hs y \<longleftrightarrow> (ds, x) \<approx>abs_lst (hs, y)"
 shows "(p \<bullet> (Abs as x)) = Abs (p \<bullet> as) (p \<bullet> x)"
 by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])
 instance
 apply(default)
-apply(induct_tac [!] x rule: abs_inducts(1))
+apply(case_tac [!] x rule: abs_exhausts(1))
 apply(simp_all)
 done
 end
 shows "(p \<bullet> (Abs_res as x)) = Abs_res (p \<bullet> as) (p \<bullet> x)"
 by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])
 instance
 apply(default)
-apply(induct_tac [!] x rule: abs_inducts(2))
+apply(case_tac [!] x rule: abs_exhausts(2))
 apply(simp_all)
 done
 end
 shows "(p \<bullet> (Abs_lst as x)) = Abs_lst (p \<bullet> as) (p \<bullet> x)"
 by (lifting permute_prod.simps[where 'a="atom list" and 'b="'a"])
 instance
 apply(default)
-apply(induct_tac [!] x rule: abs_inducts(3))
+apply(case_tac [!] x rule: abs_exhausts(3))
 apply(simp_all)
 done
 end
 and   "((supp x) - (set bs)) supports (Abs_lst bs x)"
 unfolding supports_def
 unfolding permute_abs
 by (simp_all add: abs_swap1[symmetric] abs_swap2[symmetric])
-quotient_definition
+function
-"supp_gen :: ('a::pt) abs_gen \<Rightarrow> atom set"
+supp_gen  :: "('a::pt) abs_gen \<Rightarrow> atom set"
-is
+where
-"aux_set"
+"supp_gen (Abs as x) = supp x - as"
+apply(case_tac x rule: abs_exhausts(1))
-quotient_definition
+apply(simp)
-"supp_res :: ('a::pt) abs_res \<Rightarrow> atom set"
+apply(simp add: abs_eq_iff alphas_abs alphas)
-is
+done
-"aux_set"
+termination supp_gen
-quotient_definition
+by (auto intro!: local.termination)
-"supp_lst :: ('a::pt) abs_lst \<Rightarrow> atom set"
-is
+function
-"aux_list"
+supp_res :: "('a::pt) abs_res \<Rightarrow> atom set"
+where
-lemma aux_supps:
+"supp_res (Abs_res as x) = supp x - as"
-shows "supp_gen (Abs bs x) = (supp x) - bs"
+apply(case_tac x rule: abs_exhausts(2))
-and   "supp_res (Abs_res bs x) = (supp x) - bs"
+apply(simp)
-and   "supp_lst (Abs_lst cs x) = (supp x) - (set cs)"
+apply(simp add: abs_eq_iff alphas_abs alphas)
-by (lifting aux_set.simps aux_set.simps aux_list.simps)
+done
-lemma aux_supp_eqvt[eqvt]:
+termination supp_res
+by (auto intro!: local.termination)
+function
+supp_lst :: "('a::pt) abs_lst \<Rightarrow> atom set"
+where
+"supp_lst (Abs_lst cs x) = (supp x) - (set cs)"
+apply(case_tac x rule: abs_exhausts(3))
+apply(simp)
+apply(simp add: abs_eq_iff alphas_abs alphas)
+done
+termination supp_lst
+by (auto intro!: local.termination)
+lemma [eqvt]:
 shows "(p \<bullet> supp_gen x) = supp_gen (p \<bullet> x)"
 and   "(p \<bullet> supp_res y) = supp_res (p \<bullet> y)"
 and   "(p \<bullet> supp_lst z) = supp_lst (p \<bullet> z)"
-apply(induct_tac x rule: abs_inducts(1))
+apply(case_tac x rule: abs_exhausts(1))
-apply(simp add: aux_supps supp_eqvt Diff_eqvt)
+apply(simp add: supp_eqvt Diff_eqvt)
-apply(induct_tac y rule: abs_inducts(2))
+apply(case_tac y rule: abs_exhausts(2))
-apply(simp add: aux_supps supp_eqvt Diff_eqvt)
+apply(simp add: supp_eqvt Diff_eqvt)
-apply(induct_tac z rule: abs_inducts(3))
+apply(case_tac z rule: abs_exhausts(3))
-apply(simp add: aux_supps supp_eqvt Diff_eqvt set_eqvt)
+apply(simp add: supp_eqvt Diff_eqvt set_eqvt)
 done
 lemma aux_fresh:
 shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_gen (Abs bs x)"
 and   "a \<sharp> Abs_res bs x \<Longrightarrow> a \<sharp> supp_res (Abs_res bs x)"
 assumes a: "finite (supp x)"
 shows "(supp x) - as \<subseteq> supp (Abs as x)"
 and   "(supp x) - as \<subseteq> supp (Abs_res as x)"
 and   "(supp x) - (set bs) \<subseteq> supp (Abs_lst bs x)"
 unfolding supp_conv_fresh
-apply(auto dest!: aux_fresh simp add: aux_supps)
+apply(auto dest!: aux_fresh)
 apply(simp_all add: fresh_def supp_finite_atom_set a)
 done
 lemma supp_abs_subset2:
 assumes a: "finite (supp x)"
 apply(simp_all add: finite_supp)
 done
 instance abs_gen :: (fs) fs
 apply(default)
-apply(induct_tac x rule: abs_inducts(1))
+apply(case_tac x rule: abs_exhausts(1))
 apply(simp add: supp_abs finite_supp)
 done
 instance abs_res :: (fs) fs
 apply(default)
-apply(induct_tac x rule: abs_inducts(2))
+apply(case_tac x rule: abs_exhausts(2))
 apply(simp add: supp_abs finite_supp)
 done
 instance abs_lst :: (fs) fs
 apply(default)
-apply(induct_tac x rule: abs_inducts(3))
+apply(case_tac x rule: abs_exhausts(3))
 apply(simp add: supp_abs finite_supp)
 done
 lemma abs_fresh_iff:
 fixes x::"'a::fs"
 and   "a \<sharp> Abs_res bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
 and   "a \<sharp> Abs_lst cs x \<longleftrightarrow> a \<in> (set cs) \<or> (a \<notin> (set cs) \<and> a \<sharp> x)"
 unfolding fresh_def
 unfolding supp_abs
 by auto
 section {* BELOW is stuff that may or may not be needed *}
 (* support of concrete atom sets *)

changeset 1686	7b3dd407f6b3
parent 1673	e8cf0520c820
child 1688	0b2535a72fd0