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.
Quot/Nominal/Abs.thy
changeset 995 ee0619b5adff
parent 989 af02b193a19a
child 1005 9d5d9e7ff71b
equal deleted inserted replaced
990:c25ff084868f 995:ee0619b5adff 
    23 apply(rule_tac ?p1="p" in in_permute_iff[THEN iffD1])
 
    23 apply(rule_tac ?p1="p" in in_permute_iff[THEN iffD1])
 
    24 apply(simp)
 
    24 apply(simp)
 
    25 apply(simp)
 
    25 apply(simp)
 
    26 done
 
    26 done
 
    27 
    27 
    28 datatype 'a ABS_raw = Abs_raw "atom set" "'a::pt"
 
    28 
       
    29 datatype 'a rabst = 
       
    30   RAbst "atom set" "'a::pt"
 
       
    31 
       
    32 fun map_fun 
       
    33 where "map_fun f (RAbst bs x) = RAbst bs (f x)"
 
       
    34 
       
    35 fun map_rel
 
       
    36 where "map_rel R (RAbst bs x) (RAbst cs y) = R x y"
 
       
    37 
       
    38 declare [[map "rabst" = (map_fun, map_rel)]]
 
       
    39 
       
    40 instantiation rabst :: (pt) pt
 
       
    41 begin
 
    29 
    42 
    30 primrec
 
    43 primrec
 
    31   Abs_raw_map
 
    44   permute_rabst
 
    32 where
 
    45 where
 
    33   "Abs_raw_map f (Abs_raw as x) = Abs_raw as (f x)"
 
    46   "p \<bullet> (RAbst bs x) = RAbst (p \<bullet> bs) (p \<bullet> x)"
 
    34 
       
    35 fun
 
       
    36   Abs_raw_rel
 
       
    37 where
 
       
    38   "Abs_raw_rel R (Abs_raw as x) (Abs_raw bs y) = R x y"
 
       
    39 
       
    40 declare [[map "ABS_raw" = (Abs_raw_map, Abs_raw_rel)]]
 
       
    41 
       
    42 instantiation ABS_raw :: (pt) pt
 
       
    43 begin
 
       
    44 
       
    45 primrec
 
       
    46   permute_ABS_raw
 
       
    47 where
 
       
    48   "permute_ABS_raw p (Abs_raw as x) = Abs_raw (p \<bullet> as) (p \<bullet> x)"
 
       
    49 
    47 
    50 instance
 
    48 instance
 
    51 apply(default)
 
    49 apply(default)
 
    52 apply(case_tac [!] x)
 
    50 apply(case_tac [!] x)
 
    53 apply(simp_all)
 
    51 apply(simp_all)
 
    54 done
 
    52 done
 
    55 
    53 
    56 end  
    54 end
 
    57 
    55 
    58 fun
 
    56 fun
 
    59   alpha_abs :: "('a::pt) ABS_raw \<Rightarrow> 'a ABS_raw \<Rightarrow> bool"
 
    57  alpha_gen 
    60 where
 
    58 where
 
    61   "alpha_abs (Abs_raw as x) (Abs_raw bs y) =
 
    59  alpha_gen[simp del]:
 
    62     (\<exists>pi. (supp x) - as = (supp y) - bs \<and>  ((supp x) - as) \<sharp>* pi \<and> pi \<bullet> x = y)" 
    60    "(alpha_gen (bs, x) R f pi (cs, y)) \<longleftrightarrow> (f x - bs = f y - cs) \<and> ((f x - bs) \<sharp>* pi) \<and> (R (pi \<bullet> x) y)"
 
       
    61 
       
    62 notation
 
       
    63   alpha_gen ("_ \<approx>gen _ _ _ _")
 
       
    64 
       
    65 lemma alpha_gen_refl:
 
       
    66   assumes a: "R x x"
 
       
    67   shows "(bs, x) \<approx>gen R f 0 (bs, x)"
 
       
    68   using a by (simp add: alpha_gen fresh_star_def fresh_zero_perm)
 
       
    69 
       
    70 lemma alpha_gen_sym:
 
       
    71   assumes a: "(bs, x) \<approx>gen R f p (cs, y)"
 
       
    72   and     b: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
 
       
    73   shows "(cs, y) \<approx>gen R f (- p) (bs, x)"
 
       
    74   using a b by (simp add: alpha_gen fresh_star_def fresh_def supp_minus_perm)
 
       
    75 
       
    76 lemma alpha_gen_trans:
 
       
    77   assumes a: "(bs, x) \<approx>gen R f p1 (cs, y)"
 
       
    78   and     b: "(cs, y) \<approx>gen R f p2 (ds, z)"
 
       
    79   and     c: "\<lbrakk>R (p1 \<bullet> x) y; R (p2 \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((p2 + p1) \<bullet> x) z"
 
       
    80   shows "(bs, x) \<approx>gen R f (p2 + p1) (ds, z)"
 
       
    81   using a b c using supp_plus_perm
 
       
    82   apply(simp add: alpha_gen fresh_star_def fresh_def)
 
       
    83   apply(blast)
 
       
    84   done
 
       
    85 
       
    86 lemma alpha_gen_eqvt:
 
       
    87   assumes a: "(bs, x) \<approx>gen R f q (cs, y)"
 
       
    88   and     b: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)"
 
       
    89   and     c: "p \<bullet> (f x) = f (p \<bullet> x)"
 
       
    90   and     d: "p \<bullet> (f y) = f (p \<bullet> y)"
 
       
    91   shows "(p \<bullet> bs, p \<bullet> x) \<approx>gen R f (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
 
       
    92   using a b
 
       
    93   apply(simp add: alpha_gen c[symmetric] d[symmetric] Diff_eqvt[symmetric])
 
       
    94   apply(simp add: permute_eqvt[symmetric])
 
       
    95   apply(simp add: fresh_star_permute_iff)
 
       
    96   apply(clarsimp)
 
       
    97   done
 
       
    98 
       
    99 fun
 
       
   100   alpha_rabst :: "('a::pt) rabst \<Rightarrow> 'a rabst \<Rightarrow> bool" ("_ \<approx>raw _") 
       
   101 where
 
       
   102   "(RAbst bs x) \<approx>raw (RAbst cs y) = (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))" 
    63 
   103 
    64 lemma alpha_reflp:
 
   104 lemma alpha_reflp:
 
    65   shows "alpha_abs ab ab"
 
   105   shows "abst \<approx>raw abst"
 
    66 apply(induct ab)
 
   106 apply(induct abst)
 
    67 apply(simp)
 
   107 apply(simp)
 
    68 apply(rule_tac x="0" in exI)
 
   108 apply(rule exI)
 
    69 apply(simp add: fresh_star_def fresh_zero_perm)
 
   109 apply(rule alpha_gen_refl)
 
       
   110 apply(simp)
 
    70 done
 
   111 done
 
    71 
   112 
    72 lemma alpha_symp:
 
   113 lemma alpha_symp:
 
    73   assumes a: "alpha_abs ab1 ab2"
 
   114   assumes a: "abst1 \<approx>raw abst2"
 
    74   shows "alpha_abs ab2 ab1"
 
   115   shows "abst2 \<approx>raw abst1"
 
    75 using a
 
   116 using a
 
    76 apply(induct rule: alpha_abs.induct)
 
   117 apply(induct rule: alpha_rabst.induct)
 
    77 apply(simp)
 
   118 apply(simp)
 
    78 apply(clarify)
 
   119 apply(erule exE)
 
    79 apply(rule_tac x="- pi" in exI)
 
   120 apply(rule exI)
 
    80 apply(auto)
 
   121 apply(rule alpha_gen_sym)
 
    81 apply(auto simp add: fresh_star_def)
 
   122 apply(assumption)
 
    82 apply(simp add: fresh_def supp_minus_perm)
 
   123 apply(clarsimp)
 
    83 done
 
   124 done
 
    84 
   125 
    85 lemma alpha_transp:
 
   126 lemma alpha_transp:
 
    86   assumes a1: "alpha_abs ab1 ab2"
 
   127   assumes a1: "abst1 \<approx>raw abst2"
 
    87   and     a2: "alpha_abs ab2 ab3"
 
   128   and     a2: "abst2 \<approx>raw abst3"
 
    88   shows "alpha_abs ab1 ab3"
 
   129   shows "abst1 \<approx>raw abst3"
 
    89 using a1 a2
 
   130 using a1 a2
 
    90 apply(induct rule: alpha_abs.induct)
 
   131 apply(induct rule: alpha_rabst.induct)
 
    91 apply(induct rule: alpha_abs.induct)
 
   132 apply(induct rule: alpha_rabst.induct)
 
    92 apply(simp)
 
   133 apply(simp)
 
    93 apply(clarify)
 
   134 apply(erule exE)+
 
    94 apply(rule_tac x="pia + pi" in exI)
 
   135 apply(rule exI)
 
    95 apply(simp)
 
   136 apply(rule alpha_gen_trans)
 
    96 apply(auto simp add: fresh_star_def)
 
   137 apply(assumption)
 
    97 using supp_plus_perm
 
   138 apply(assumption)
 
    98 apply(simp add: fresh_def)
 
   139 apply(simp)
 
    99 apply(blast)
 
       
   100 done
 
   140 done
 
   101 
   141 
   102 lemma alpha_eqvt:
 
   142 lemma alpha_eqvt:
 
   103   assumes a: "alpha_abs ab1 ab2"
 
   143   assumes a: "abst1 \<approx>raw abst2"
 
   104   shows "alpha_abs (p \<bullet> ab1) (p \<bullet> ab2)"
 
   144   shows "(p \<bullet> abst1) \<approx>raw(p \<bullet> abst2)"
 
   105 using a
 
   145 using a
 
   106 apply(induct ab1 ab2 rule: alpha_abs.induct)
 
   146 apply(induct abst1 abst2 rule: alpha_rabst.induct)
 
   107 apply(simp)
 
   147 apply(simp)
 
   108 apply(clarify)
 
   148 apply(erule exE)
 
   109 apply(rule conjI)
 
   149 apply(rule exI)
 
   110 apply(simp add: supp_eqvt[symmetric])
 
   150 apply(rule alpha_gen_eqvt)
 
   111 apply(simp add: Diff_eqvt[symmetric])
 
   151 apply(assumption)
 
   112 apply(rule_tac x="p \<bullet> pi" in exI)
 
   152 apply(simp)
 
   113 apply(rule conjI)
 
   153 apply(simp add: supp_eqvt)
 
   114 apply(simp add: supp_eqvt[symmetric])
 
   154 apply(simp add: supp_eqvt)
 
   115 apply(simp add: Diff_eqvt[symmetric])
 
       
   116 apply(simp only: fresh_star_permute_iff)
 
       
   117 apply(simp add: permute_eqvt[symmetric])
 
       
   118 done
 
   155 done
 
   119 
   156 
   120 lemma test1:
 
   157 lemma test1:
 
   121   assumes a1: "a \<notin> (supp x) - bs"
 
   158   assumes a1: "a \<notin> (supp x) - bs"
 
   122   and     a2: "b \<notin> (supp x) - bs"
 
   159   and     a2: "b \<notin> (supp x) - bs"
 
   123   shows "alpha_abs (Abs_raw bs x) (Abs_raw ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))"
 
   160   shows "(RAbst bs x) \<approx>raw (RAbst ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))"
 
   124 unfolding alpha_abs.simps
 
   161 apply(simp)
 
   125 apply(rule_tac x="(a \<rightleftharpoons> b)" in exI)
 
   162 apply(rule_tac x="(a \<rightleftharpoons> b)" in exI)
 
   126 apply(rule_tac conjI)
 
   163 apply(simp add: alpha_gen)
 
   127 apply(simp add: supp_eqvt[symmetric])
 
   164 apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric])
 
   128 apply(simp add: Diff_eqvt[symmetric])
 
   165 apply(simp add: swap_set_fresh[OF a1 a2])
 
   129 using a1 a2
 
       
   130 apply(simp add: swap_set_fresh)
 
       
   131 apply(rule conjI)
 
       
   132 prefer 2
 
       
   133 apply(simp)
 
       
   134 apply(simp add: fresh_star_def)
 
       
   135 apply(simp add: fresh_def)
 
       
   136 apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}")
 
   166 apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}")
 
   137 using a1 a2
 
   167 using a1 a2
 
   138 apply -
 
   168 apply(simp add: fresh_star_def fresh_def)
 
   139 apply(blast)
 
   169 apply(blast)
 
   140 apply(simp add: supp_swap)
 
   170 apply(simp add: supp_swap)
 
   141 done
 
   171 done
 
   142 
   172 
   143 fun
 
   173 fun
 
   144   s_test
 
   174   s_test
 
   145 where
 
   175 where
 
   146   "s_test (Abs_raw bs x) = (supp x) - bs"
 
   176   "s_test (RAbst bs x) = (supp x) - bs"
 
   147 
   177 
   148 lemma s_test_lemma:
 
   178 lemma s_test_lemma:
 
   149   assumes a: "alpha_abs x y" 
   179   assumes a: "x \<approx>raw y" 
   150   shows "s_test x = s_test y"
 
   180   shows "s_test x = s_test y"
 
   151 using a
 
   181 using a
 
   152 apply(induct rule: alpha_abs.induct)
 
   182 apply(induct rule: alpha_rabst.induct)
 
   153 apply(simp)
 
   183 apply(simp add: alpha_gen)
 
   154 done
 
   184 done
 
   155   
   185   
   156 
   186 
   157 quotient_type 'a ABS = "('a::pt) ABS_raw" / "alpha_abs::('a::pt) ABS_raw \<Rightarrow> 'a ABS_raw \<Rightarrow> bool"
 
   187 quotient_type 'a abst = "('a::pt) rabst" / "alpha_rabst::('a::pt) rabst \<Rightarrow> 'a rabst \<Rightarrow> bool"
 
   158   apply(rule equivpI)
 
   188   apply(rule equivpI)
 
   159   unfolding reflp_def symp_def transp_def
 
   189   unfolding reflp_def symp_def transp_def
 
   160   apply(auto intro: alpha_reflp alpha_symp alpha_transp)
 
   190   apply(auto intro: alpha_reflp alpha_symp alpha_transp)
 
   161   done
 
   191   done
 
   162 
   192 
   163 quotient_definition
 
   193 quotient_definition
 
   164    "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a ABS"
 
   194    "Abst::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abst"
 
   165 as
 
   195 as
 
   166    "Abs_raw"
 
   196    "RAbst"
 
   167 
   197 
   168 lemma [quot_respect]:
 
   198 lemma [quot_respect]:
 
   169   shows "((op =) ===> (op =) ===> alpha_abs) Abs_raw Abs_raw"
 
   199   shows "((op =) ===> (op =) ===> alpha_rabst) RAbst RAbst"
 
   170 apply(auto simp del: alpha_abs.simps)
 
   200 apply(simp del: alpha_rabst.simps add: alpha_reflp)
 
   171 apply(rule alpha_reflp)
 
       
   172 done
 
   201 done
 
   173 
   202 
   174 lemma [quot_respect]:
 
   203 lemma [quot_respect]:
 
   175   shows "((op =) ===> alpha_abs ===> alpha_abs) permute permute"
 
   204   shows "((op =) ===> alpha_rabst ===> alpha_rabst) permute permute"
 
   176 apply(auto)
 
       
   177 apply(simp add: alpha_eqvt)
 
   205 apply(simp add: alpha_eqvt)
 
   178 done
 
   206 done
 
   179 
   207 
   180 lemma [quot_respect]:
 
   208 lemma [quot_respect]:
 
   181   shows "(alpha_abs ===> (op =)) s_test s_test"
 
   209   shows "(alpha_rabst ===> (op =)) s_test s_test"
 
   182 apply(simp add: s_test_lemma)
 
   210 apply(simp add: s_test_lemma)
 
   183 done
 
   211 done
 
   184 
   212 
   185 lemma ABS_induct:
 
   213 lemma abst_induct:
 
   186   "\<lbrakk>\<And>as (x::'a::pt). P (Abs as x)\<rbrakk> \<Longrightarrow> P t"
 
   214   "\<lbrakk>\<And>as (x::'a::pt). P (Abst as x)\<rbrakk> \<Longrightarrow> P t"
 
   187 apply(lifting ABS_raw.induct)
 
   215 apply(lifting rabst.induct)
 
   188 done
 
   216 done
 
   189 
   217 
   190 instantiation ABS :: (pt) pt
 
   218 instantiation abst :: (pt) pt
 
   191 begin
 
   219 begin
 
   192 
   220 
   193 quotient_definition
 
   221 quotient_definition
 
   194   "permute_ABS::perm \<Rightarrow> ('a::pt ABS) \<Rightarrow> 'a ABS"
 
   222   "permute_abst::perm \<Rightarrow> ('a::pt abst) \<Rightarrow> 'a abst"
 
   195 as
 
   223 as
 
   196   "permute::perm \<Rightarrow> ('a::pt ABS_raw) \<Rightarrow> 'a ABS_raw"
 
   224   "permute::perm \<Rightarrow> ('a::pt rabst) \<Rightarrow> 'a rabst"
 
   197 
   225 
   198 lemma permute_ABS [simp]:
 
   226 lemma permute_ABS [simp]:
 
   199   fixes x::"'b::pt"  (* ??? has to be 'b \<dots> 'a doe not work *)
 
   227   fixes x::"'a::pt"  (* ??? has to be 'a \<dots> 'b does not work *)
 
   200   shows "(p \<bullet> (Abs as x)) = Abs (p \<bullet> as) (p \<bullet> x)"
 
   228   shows "(p \<bullet> (Abst as x)) = Abst (p \<bullet> as) (p \<bullet> x)"
 
   201 apply(lifting permute_ABS_raw.simps(1))
 
   229 apply(lifting permute_rabst.simps(1))
 
   202 done
 
   230 done
 
   203 
   231 
   204 instance
 
   232 instance
 
   205   apply(default)
 
   233   apply(default)
 
   206   apply(induct_tac [!] x rule: ABS_induct)
 
   234   apply(induct_tac [!] x rule: abst_induct)
 
   207   apply(simp_all)
 
   235   apply(simp_all)
 
   208   done
 
   236   done
 
   209 
   237 
   210 end
 
   238 end
 
   211 
   239 
   212 lemma test1_lifted:
 
   240 lemma test1_lifted:
 
   213   assumes a1: "a \<notin> (supp x) - bs"
 
   241   assumes a1: "a \<notin> (supp x) - bs"
 
   214   and     a2: "b \<notin> (supp x) - bs"
 
   242   and     a2: "b \<notin> (supp x) - bs"
 
   215   shows "(Abs bs x) = (Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))"
 
   243   shows "(Abst bs x) = (Abst ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))"
 
   216 using a1 a2
 
   244 using a1 a2
 
   217 apply(lifting test1)
 
   245 apply(lifting test1)
 
   218 done
 
   246 done
 
   219 
   247 
   220 lemma Abs_supports:
 
   248 lemma Abst_supports:
 
   221   shows "((supp x) - as) supports (Abs as x) "
 
   249   shows "((supp x) - as) supports (Abst as x)"
 
   222 unfolding supports_def
 
   250 unfolding supports_def
 
   223 apply(clarify)
 
   251 apply(clarify)
 
   224 apply(simp (no_asm))
 
   252 apply(simp (no_asm))
 
   225 apply(subst test1_lifted[symmetric])
 
   253 apply(subst test1_lifted[symmetric])
 
   226 apply(simp_all)
 
   254 apply(simp_all)
 
   227 done
 
   255 done
 
   228 
   256 
   229 quotient_definition
 
   257 quotient_definition
 
   230   "s_test_lifted :: ('a::pt) ABS \<Rightarrow> atom \<Rightarrow> bool"
 
   258   "s_test_lifted :: ('a::pt) abst \<Rightarrow> atom \<Rightarrow> bool"
 
   231 as
 
   259 as
 
   232   "s_test::('a::pt) ABS_raw \<Rightarrow> atom \<Rightarrow> bool"
 
   260   "s_test::('a::pt) rabst \<Rightarrow> atom \<Rightarrow> bool"
 
   233 
   261 
   234 lemma s_test_lifted_simp:
 
   262 lemma s_test_lifted_simp:
 
   235   shows "s_test_lifted (Abs bs x) = (supp x) - bs"
 
   263   shows "s_test_lifted (Abst bs x) = (supp x) - bs"
 
   236 apply(lifting s_test.simps(1))
 
   264 apply(lifting s_test.simps(1))
 
   237 done
 
   265 done
 
   238 
   266 
   239 lemma s_test_lifted_eqvt:
 
   267 lemma s_test_lifted_eqvt:
 
   240   shows "(p \<bullet> (s_test_lifted ab)) = s_test_lifted (p \<bullet> ab)"
 
   268   shows "(p \<bullet> (s_test_lifted ab)) = s_test_lifted (p \<bullet> ab)"
 
   241 apply(induct ab rule: ABS_induct)
 
   269 apply(induct ab rule: abst_induct)
 
   242 apply(simp add: s_test_lifted_simp supp_eqvt Diff_eqvt)
 
   270 apply(simp add: s_test_lifted_simp supp_eqvt Diff_eqvt)
 
   243 done
 
   271 done
 
   244 
   272 
   245 lemma fresh_f_empty_supp:
 
   273 lemma fresh_f_empty_supp:
 
   246   assumes a: "\<forall>p. p \<bullet> f = f"
 
   274   assumes a: "\<forall>p. p \<bullet> f = f"
 
   255 apply(auto)
 
   283 apply(auto)
 
   256 done
 
   284 done
 
   257 
   285 
   258 
   286 
   259 lemma s_test_fresh_lemma:
 
   287 lemma s_test_fresh_lemma:
 
   260   shows "(a \<sharp> Abs bs x) \<Longrightarrow> (a \<sharp> s_test_lifted (Abs bs x))"
 
   288   shows "(a \<sharp> Abst bs x) \<Longrightarrow> (a \<sharp> s_test_lifted (Abst bs x))"
 
   261 apply(rule fresh_f_empty_supp)
 
   289 apply(rule fresh_f_empty_supp)
 
   262 apply(rule allI)
 
   290 apply(rule allI)
 
   263 apply(subst permute_fun_def)
 
   291 apply(subst permute_fun_def)
 
   264 apply(simp add: s_test_lifted_eqvt)
 
   292 apply(simp add: s_test_lifted_eqvt)
 
   265 apply(simp)
 
   293 apply(simp)
 
   277   apply(auto simp add: permute_set_eq swap_atom)[1]
 
   305   apply(auto simp add: permute_set_eq swap_atom)[1]
 
   278 done
 
   306 done
 
   279 
   307 
   280 lemma s_test_subset:
 
   308 lemma s_test_subset:
 
   281   fixes x::"'a::fs"
 
   309   fixes x::"'a::fs"
 
   282   shows "((supp x) - as) \<subseteq> (supp (Abs as x))"
 
   310   shows "((supp x) - as) \<subseteq> (supp (Abst as x))"
 
   283 apply(rule subsetI)
 
   311 apply(rule subsetI)
 
   284 apply(rule contrapos_pp)
 
   312 apply(rule contrapos_pp)
 
   285 apply(assumption)
 
   313 apply(assumption)
 
   286 unfolding fresh_def[symmetric]
 
   314 unfolding fresh_def[symmetric]
 
   287 apply(drule_tac s_test_fresh_lemma)
 
   315 apply(drule_tac s_test_fresh_lemma)
 
   290 apply(subgoal_tac "finite (supp x - as)")
 
   318 apply(subgoal_tac "finite (supp x - as)")
 
   291 apply(simp add: supp_finite_set)
 
   319 apply(simp add: supp_finite_set)
 
   292 apply(simp add: finite_supp)
 
   320 apply(simp add: finite_supp)
 
   293 done
 
   321 done
 
   294 
   322 
   295 lemma supp_Abs:
 
   323 lemma supp_Abst:
 
   296   fixes x::"'a::fs"
 
   324   fixes x::"'a::fs"
 
   297   shows "supp (Abs as x) = (supp x) - as"
 
   325   shows "supp (Abst as x) = (supp x) - as"
 
   298 apply(rule subset_antisym)
 
   326 apply(rule subset_antisym)
 
   299 apply(rule supp_is_subset)
 
   327 apply(rule supp_is_subset)
 
   300 apply(rule Abs_supports)
 
   328 apply(rule Abst_supports)
 
   301 apply(simp add: finite_supp)
 
   329 apply(simp add: finite_supp)
 
   302 apply(rule s_test_subset)
 
   330 apply(rule s_test_subset)
 
   303 done
 
   331 done
 
   304 
   332 
   305 instance ABS :: (fs) fs
 
   333 instance abst :: (fs) fs
 
   306 apply(default)
 
   334 apply(default)
 
   307 apply(induct_tac x rule: ABS_induct)
 
   335 apply(induct_tac x rule: abst_induct)
 
   308 apply(simp add: supp_Abs)
 
   336 apply(simp add: supp_Abst)
 
   309 apply(simp add: finite_supp)
 
   337 apply(simp add: finite_supp)
 
   310 done
 
   338 done
 
   311 
   339 
   312 lemma fresh_abs:
 
   340 lemma fresh_abs:
 
   313   fixes x::"'a::fs"
 
   341   fixes x::"'a::fs"
 
   314   shows "a \<sharp> Abs bs x = (a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x))"
 
   342   shows "a \<sharp> Abst bs x = (a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x))"
 
   315 apply(simp add: fresh_def)
 
   343 apply(simp add: fresh_def)
 
   316 apply(simp add: supp_Abs)
 
   344 apply(simp add: supp_Abst)
 
   317 apply(auto)
 
   345 apply(auto)
 
   318 done
 
   346 done
 
   319 
   347 
       
   348 thm alpha_rabst.simps(1)
 
       
   349 
   320 lemma abs_eq:
 
   350 lemma abs_eq:
 
   321   shows "(Abs as x) = (Abs bs y) \<longleftrightarrow> (\<exists>pi. supp x - as = supp y - bs \<and> (supp x - as) \<sharp>* pi \<and> pi \<bullet> x = y)"
 
   351   shows "(Abst bs x) = (Abst cs y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
 
   322 apply(lifting alpha_abs.simps(1))
 
   352 apply(lifting alpha_rabst.simps(1))
 
   323 done
 
   353 done
 
   324 
   354 
   325 end
 
   355 end
 
   326 
   356
nominal2