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 1007 b4f956137114
parent 1006 ef34da709a0b
child 1014 272ea46a1766
equal deleted inserted replaced
1006:ef34da709a0b 1007:b4f956137114 
     1 theory Abs
 
     1 theory Abs
 
     2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" 
     2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "../QuotProd"
 
     3 begin
 
     3 begin
 
     4 
     4 
     5 (* lemmas that should be in Nominal \<dots>\<dots>must be cleaned *)
 
     5 (* lemmas that should be in Nominal \<dots>\<dots>must be cleaned *)
 
     6 lemma in_permute_iff:
 
     6 lemma in_permute_iff:
 
     7   shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"
 
     7   shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"
 
    71   apply(simp add: fresh_star_permute_iff)
 
    71   apply(simp add: fresh_star_permute_iff)
 
    72   apply(clarsimp)
 
    72   apply(clarsimp)
 
    73   done
 
    73   done
 
    74 
    74 
    75 fun
 
    75 fun
 
    76   alpha_abst 
    76   alpha_abs 
    77 where
 
    77 where
 
    78   "alpha_abst (bs, x) (cs, y) = (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))"
 
    78   "alpha_abs (bs, x) (cs, y) = (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))"
 
    79 
    79 
    80 notation
 
    80 notation
 
    81   alpha_abst ("_ \<approx>abst _")
 
    81   alpha_abs ("_ \<approx>abs _")
 
    82 
    82 
    83 lemma test1:
 
    83 lemma test1:
 
    84   assumes a1: "a \<notin> (supp x) - bs"
 
    84   assumes a1: "a \<notin> (supp x) - bs"
 
    85   and     a2: "b \<notin> (supp x) - bs"
 
    85   and     a2: "b \<notin> (supp x) - bs"
 
    86   shows "(bs, x) \<approx>abst ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)"
 
    86   shows "(bs, x) \<approx>abs ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)"
 
    87 apply(simp)
 
    87 apply(simp)
 
    88 apply(rule_tac x="(a \<rightleftharpoons> b)" in exI)
 
    88 apply(rule_tac x="(a \<rightleftharpoons> b)" in exI)
 
    89 apply(simp add: alpha_gen)
 
    89 apply(simp add: alpha_gen)
 
    90 apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric])
 
    90 apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric])
 
    91 apply(simp add: swap_set_fresh[OF a1 a2])
 
    91 apply(simp add: swap_set_fresh[OF a1 a2])
 
   100   s_test
 
   100   s_test
 
   101 where
 
   101 where
 
   102   "s_test (bs, x) = (supp x) - bs"
 
   102   "s_test (bs, x) = (supp x) - bs"
 
   103 
   103 
   104 lemma s_test_lemma:
 
   104 lemma s_test_lemma:
 
   105   assumes a: "x \<approx>abst y" 
   105   assumes a: "x \<approx>abs y" 
   106   shows "s_test x = s_test y"
 
   106   shows "s_test x = s_test y"
 
   107 using a
 
   107 using a
 
   108 apply(induct rule: alpha_abst.induct)
 
   108 apply(induct rule: alpha_abs.induct)
 
   109 apply(simp add: alpha_gen)
 
   109 apply(simp add: alpha_gen)
 
   110 done
 
   110 done
 
   111   
   111   
   112 quotient_type 'a abst = "(atom set \<times> 'a::pt)" / "alpha_abst"
 
   112 quotient_type 'a abs = "(atom set \<times> 'a::pt)" / "alpha_abs"
 
   113   apply(rule equivpI)
 
   113   apply(rule equivpI)
 
   114   unfolding reflp_def symp_def transp_def
 
   114   unfolding reflp_def symp_def transp_def
 
   115   apply(simp_all)
 
   115   apply(simp_all)
 
   116   apply(clarify)
 
   116   apply(clarify)
 
   117   apply(rule exI)
 
   117   apply(rule exI)
 
   129   apply(assumption)
 
   129   apply(assumption)
 
   130   apply(simp)
 
   130   apply(simp)
 
   131   done
 
   131   done
 
   132 
   132 
   133 quotient_definition
 
   133 quotient_definition
 
   134    "Abst::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abst"
 
   134    "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs"
 
   135 as
 
   135 as
 
   136    "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
 
   136    "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
 
   137 
   137 
   138 lemma [quot_respect]:
 
   138 lemma [quot_respect]:
 
   139   shows "((op =) ===> (op =) ===> alpha_abst) Pair Pair"
 
   139   shows "((op =) ===> (op =) ===> alpha_abs) Pair Pair"
 
   140 apply(clarsimp)
 
   140 apply(clarsimp)
 
   141 apply(rule exI)
 
   141 apply(rule exI)
 
   142 apply(rule alpha_gen_refl)
 
   142 apply(rule alpha_gen_refl)
 
   143 apply(simp)
 
   143 apply(simp)
 
   144 done
 
   144 done
 
   145 
   145 
   146 lemma [quot_respect]:
 
   146 lemma [quot_respect]:
 
   147   shows "((op =) ===> alpha_abst ===> alpha_abst) permute permute"
 
   147   shows "((op =) ===> alpha_abs ===> alpha_abs) permute permute"
 
   148 apply(clarsimp)
 
   148 apply(clarsimp)
 
   149 apply(rule exI)
 
   149 apply(rule exI)
 
   150 apply(rule alpha_gen_eqvt)
 
   150 apply(rule alpha_gen_eqvt)
 
   151 apply(assumption)
 
   151 apply(assumption)
 
   152 apply(simp_all add: supp_eqvt)
 
   152 apply(simp_all add: supp_eqvt)
 
   153 done
 
   153 done
 
   154 
   154 
   155 lemma [quot_respect]:
 
   155 lemma [quot_respect]:
 
   156   shows "(alpha_abst ===> (op =)) s_test s_test"
 
   156   shows "(alpha_abs ===> (op =)) s_test s_test"
 
   157 apply(simp add: s_test_lemma)
 
   157 apply(simp add: s_test_lemma)
 
   158 done
 
   158 done
 
   159 
   159 
   160 lemma abst_induct:
 
   160 lemma abs_induct:
 
   161   "\<lbrakk>\<And>as (x::'a::pt). P (Abst as x)\<rbrakk> \<Longrightarrow> P t"
 
   161   "\<lbrakk>\<And>as (x::'a::pt). P (Abs as x)\<rbrakk> \<Longrightarrow> P t"
 
   162 apply(lifting prod.induct[where 'a="atom set" and 'b="'a"])
 
   162 apply(lifting prod.induct[where 'a="atom set" and 'b="'a"])
 
   163 done
 
   163 done
 
   164 
   164 
   165 instantiation abst :: (pt) pt
 
   165 instantiation abs :: (pt) pt
 
   166 begin
 
   166 begin
 
   167 
   167 
   168 quotient_definition
 
   168 quotient_definition
 
   169   "permute_abst::perm \<Rightarrow> ('a::pt abst) \<Rightarrow> 'a abst"
 
   169   "permute_abs::perm \<Rightarrow> ('a::pt abs) \<Rightarrow> 'a abs"
 
   170 as
 
   170 as
 
   171   "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
 
   171   "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
 
   172 
   172 
   173 lemma permute_ABS [simp]:
 
   173 lemma permute_ABS [simp]:
 
   174   fixes x::"'a::pt"  (* ??? has to be 'a \<dots> 'b does not work *)
 
   174   fixes x::"'a::pt"  (* ??? has to be 'a \<dots> 'b does not work *)
 
   175   shows "(p \<bullet> (Abst as x)) = Abst (p \<bullet> as) (p \<bullet> x)"
 
   175   shows "(p \<bullet> (Abs as x)) = Abs (p \<bullet> as) (p \<bullet> x)"
 
   176 apply(lifting permute_prod.simps(1)[where 'a="atom set" and 'b="'a"])
 
   176 apply(lifting permute_prod.simps(1)[where 'a="atom set" and 'b="'a"])
 
   177 done
 
   177 done
 
   178 
   178 
   179 instance
 
   179 instance
 
   180   apply(default)
 
   180   apply(default)
 
   181   apply(induct_tac [!] x rule: abst_induct)
 
   181   apply(induct_tac [!] x rule: abs_induct)
 
   182   apply(simp_all)
 
   182   apply(simp_all)
 
   183   done
 
   183   done
 
   184 
   184 
   185 end
 
   185 end
 
   186 
   186 
   187 lemma test1_lifted:
 
   187 lemma test1_lifted:
 
   188   assumes a1: "a \<notin> (supp x) - bs"
 
   188   assumes a1: "a \<notin> (supp x) - bs"
 
   189   and     a2: "b \<notin> (supp x) - bs"
 
   189   and     a2: "b \<notin> (supp x) - bs"
 
   190   shows "(Abst bs x) = (Abst ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))"
 
   190   shows "(Abs bs x) = (Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))"
 
   191 using a1 a2
 
   191 using a1 a2
 
   192 apply(lifting test1)
 
   192 apply(lifting test1)
 
   193 done
 
   193 done
 
   194 
   194 
   195 lemma Abst_supports:
 
   195 lemma Abs_supports:
 
   196   shows "((supp x) - as) supports (Abst as x)"
 
   196   shows "((supp x) - as) supports (Abs as x)"
 
   197 unfolding supports_def
 
   197 unfolding supports_def
 
   198 apply(clarify)
 
   198 apply(clarify)
 
   199 apply(simp (no_asm))
 
   199 apply(simp (no_asm))
 
   200 apply(subst test1_lifted[symmetric])
 
   200 apply(subst test1_lifted[symmetric])
 
   201 apply(simp_all)
 
   201 apply(simp_all)
 
   202 done
 
   202 done
 
   203 
   203 
   204 quotient_definition
 
   204 quotient_definition
 
   205   "s_test_lifted :: ('a::pt) abst \<Rightarrow> atom \<Rightarrow> bool"
 
   205   "s_test_lifted :: ('a::pt) abs \<Rightarrow> atom \<Rightarrow> bool"
 
   206 as
 
   206 as
 
   207   "s_test"
 
   207   "s_test"
 
   208 
   208 
   209 lemma s_test_lifted_simp:
 
   209 lemma s_test_lifted_simp:
 
   210   shows "s_test_lifted (Abst bs x) = (supp x) - bs"
 
   210   shows "s_test_lifted (Abs bs x) = (supp x) - bs"
 
   211 apply(lifting s_test.simps(1))
 
   211 apply(lifting s_test.simps(1))
 
   212 done
 
   212 done
 
   213 
   213 
   214 lemma s_test_lifted_eqvt:
 
   214 lemma s_test_lifted_eqvt:
 
   215   shows "(p \<bullet> (s_test_lifted ab)) = s_test_lifted (p \<bullet> ab)"
 
   215   shows "(p \<bullet> (s_test_lifted ab)) = s_test_lifted (p \<bullet> ab)"
 
   216 apply(induct ab rule: abst_induct)
 
   216 apply(induct ab rule: abs_induct)
 
   217 apply(simp add: s_test_lifted_simp supp_eqvt Diff_eqvt)
 
   217 apply(simp add: s_test_lifted_simp supp_eqvt Diff_eqvt)
 
   218 done
 
   218 done
 
   219 
   219 
   220 lemma fresh_f_empty_supp:
 
   220 lemma fresh_f_empty_supp:
 
   221   assumes a: "\<forall>p. p \<bullet> f = f"
 
   221   assumes a: "\<forall>p. p \<bullet> f = f"
 
   230 apply(auto)
 
   230 apply(auto)
 
   231 done
 
   231 done
 
   232 
   232 
   233 
   233 
   234 lemma s_test_fresh_lemma:
 
   234 lemma s_test_fresh_lemma:
 
   235   shows "(a \<sharp> Abst bs x) \<Longrightarrow> (a \<sharp> s_test_lifted (Abst bs x))"
 
   235   shows "(a \<sharp> Abs bs x) \<Longrightarrow> (a \<sharp> s_test_lifted (Abs bs x))"
 
   236 apply(rule fresh_f_empty_supp)
 
   236 apply(rule fresh_f_empty_supp)
 
   237 apply(rule allI)
 
   237 apply(rule allI)
 
   238 apply(subst permute_fun_def)
 
   238 apply(subst permute_fun_def)
 
   239 apply(simp add: s_test_lifted_eqvt)
 
   239 apply(simp add: s_test_lifted_eqvt)
 
   240 apply(simp)
 
   240 apply(simp)
 
   253   apply(auto simp add: permute_set_eq swap_atom)[1]
 
   253   apply(auto simp add: permute_set_eq swap_atom)[1]
 
   254 done
 
   254 done
 
   255 
   255 
   256 lemma s_test_subset:
 
   256 lemma s_test_subset:
 
   257   fixes x::"'a::fs"
 
   257   fixes x::"'a::fs"
 
   258   shows "((supp x) - as) \<subseteq> (supp (Abst as x))"
 
   258   shows "((supp x) - as) \<subseteq> (supp (Abs as x))"
 
   259 apply(rule subsetI)
 
   259 apply(rule subsetI)
 
   260 apply(rule contrapos_pp)
 
   260 apply(rule contrapos_pp)
 
   261 apply(assumption)
 
   261 apply(assumption)
 
   262 unfolding fresh_def[symmetric]
 
   262 unfolding fresh_def[symmetric]
 
   263 thm s_test_fresh_lemma
 
   263 thm s_test_fresh_lemma
 
   267 apply(subgoal_tac "finite (supp x - as)")
 
   267 apply(subgoal_tac "finite (supp x - as)")
 
   268 apply(simp add: supp_finite_set)
 
   268 apply(simp add: supp_finite_set)
 
   269 apply(simp add: finite_supp)
 
   269 apply(simp add: finite_supp)
 
   270 done
 
   270 done
 
   271 
   271 
   272 lemma supp_Abst:
 
   272 lemma supp_Abs:
 
   273   fixes x::"'a::fs"
 
   273   fixes x::"'a::fs"
 
   274   shows "supp (Abst as x) = (supp x) - as"
 
   274   shows "supp (Abs as x) = (supp x) - as"
 
   275 apply(rule subset_antisym)
 
   275 apply(rule subset_antisym)
 
   276 apply(rule supp_is_subset)
 
   276 apply(rule supp_is_subset)
 
   277 apply(rule Abst_supports)
 
   277 apply(rule Abs_supports)
 
   278 apply(simp add: finite_supp)
 
   278 apply(simp add: finite_supp)
 
   279 apply(rule s_test_subset)
 
   279 apply(rule s_test_subset)
 
   280 done
 
   280 done
 
   281 
   281 
   282 instance abst :: (fs) fs
 
   282 instance abs :: (fs) fs
 
   283 apply(default)
 
   283 apply(default)
 
   284 apply(induct_tac x rule: abst_induct)
 
   284 apply(induct_tac x rule: abs_induct)
 
   285 apply(simp add: supp_Abst)
 
   285 apply(simp add: supp_Abs)
 
   286 apply(simp add: finite_supp)
 
   286 apply(simp add: finite_supp)
 
   287 done
 
   287 done
 
   288 
   288 
   289 lemma fresh_abs:
 
   289 lemma fresh_abs:
 
   290   fixes x::"'a::fs"
 
   290   fixes x::"'a::fs"
 
   291   shows "a \<sharp> Abst bs x = (a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x))"
 
   291   shows "a \<sharp> Abs bs x = (a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x))"
 
   292 apply(simp add: fresh_def)
 
   292 apply(simp add: fresh_def)
 
   293 apply(simp add: supp_Abst)
 
   293 apply(simp add: supp_Abs)
 
   294 apply(auto)
 
   294 apply(auto)
 
   295 done
 
   295 done
 
   296 
   296 
   297 lemma abs_eq:
 
   297 lemma abs_eq:
 
   298   shows "(Abst bs x) = (Abst cs y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
 
   298   shows "(Abs bs x) = (Abs cs y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
 
   299 apply(lifting alpha_abst.simps(1))
 
   299 apply(lifting alpha_abs.simps(1))
 
   300 done
 
   300 done
 
   301 
   301 
   302 end
 
   302 end
 
   303 
   303
nominal2