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 988 a987b5acadc8
parent 986 98375dde48fc
child 989 af02b193a19a
equal deleted inserted replaced
987:542b36e1c390 988:a987b5acadc8 
    53 apply(simp_all)
 
    53 apply(simp_all)
 
    54 done
 
    54 done
 
    55 
    55 
    56 end  
    56 end  
    57 
    57 
    58 inductive
 
    58 fun
 
    59   alpha_abs :: "('a::pt) ABS_raw \<Rightarrow> 'a ABS_raw \<Rightarrow> bool"
 
    59   alpha_abs :: "('a::pt) ABS_raw \<Rightarrow> 'a ABS_raw \<Rightarrow> bool"
 
    60 where
 
    60 where
 
    61   "\<lbrakk>\<exists>pi. (supp x) - as = (supp y) - bs \<and>  ((supp x) - as) \<sharp>* pi \<and> pi \<bullet> x = y\<rbrakk> 
    61   "alpha_abs (Abs_raw as x) (Abs_raw bs y) =
 
    62    \<Longrightarrow> alpha_abs (Abs_raw as x) (Abs_raw bs y)"
 
    62     (\<exists>pi. (supp x) - as = (supp y) - bs \<and>  ((supp x) - as) \<sharp>* pi \<and> pi \<bullet> x = y)" 
    63 
    63 
    64 lemma alpha_reflp:
 
    64 lemma alpha_reflp:
 
    65   shows "alpha_abs ab ab"
 
    65   shows "alpha_abs ab ab"
 
    66 apply(induct ab)
 
    66 apply(induct ab)
 
    67 apply(rule alpha_abs.intros)
 
    67 apply(simp)
 
    68 apply(rule_tac x="0" in exI)
 
    68 apply(rule_tac x="0" in exI)
 
    69 apply(simp add: fresh_star_def fresh_zero_perm)
 
    69 apply(simp add: fresh_star_def fresh_zero_perm)
 
    70 done
 
    70 done
 
    71 
    71 
    72 lemma alpha_symp:
 
    72 lemma alpha_symp:
 
    73   assumes a: "alpha_abs ab1 ab2"
 
    73   assumes a: "alpha_abs ab1 ab2"
 
    74   shows "alpha_abs ab2 ab1"
 
    74   shows "alpha_abs ab2 ab1"
 
    75 using a
 
    75 using a
 
    76 apply(erule_tac alpha_abs.cases)
 
    76 apply(induct rule: alpha_abs.induct)
 
       
    77 apply(simp)
 
    77 apply(clarify)
 
    78 apply(clarify)
 
    78 apply(rule alpha_abs.intros)
 
       
    79 apply(rule_tac x="- pi" in exI)
 
    79 apply(rule_tac x="- pi" in exI)
 
    80 apply(auto)
 
    80 apply(auto)
 
    81 apply(auto simp add: fresh_star_def)
 
    81 apply(auto simp add: fresh_star_def)
 
    82 apply(simp add: fresh_def supp_minus_perm)
 
    82 apply(simp add: fresh_def supp_minus_perm)
 
    83 done
 
    83 done
 
    85 lemma alpha_transp:
 
    85 lemma alpha_transp:
 
    86   assumes a1: "alpha_abs ab1 ab2"
 
    86   assumes a1: "alpha_abs ab1 ab2"
 
    87   and     a2: "alpha_abs ab2 ab3"
 
    87   and     a2: "alpha_abs ab2 ab3"
 
    88   shows "alpha_abs ab1 ab3"
 
    88   shows "alpha_abs ab1 ab3"
 
    89 using a1 a2
 
    89 using a1 a2
 
    90 apply(erule_tac alpha_abs.cases)
 
    90 apply(induct rule: alpha_abs.induct)
 
    91 apply(erule_tac alpha_abs.cases)
 
    91 apply(induct rule: alpha_abs.induct)
 
       
    92 apply(simp)
 
    92 apply(clarify)
 
    93 apply(clarify)
 
    93 apply(rule alpha_abs.intros)
 
       
    94 apply(rule_tac x="pia + pi" in exI)
 
    94 apply(rule_tac x="pia + pi" in exI)
 
    95 apply(simp)
 
    95 apply(simp)
 
    96 apply(auto simp add: fresh_star_def)
 
    96 apply(auto simp add: fresh_star_def)
 
    97 using supp_plus_perm
 
    97 using supp_plus_perm
 
    98 apply(simp add: fresh_def)
 
    98 apply(simp add: fresh_def)
 
   101 
   101 
   102 lemma alpha_eqvt:
 
   102 lemma alpha_eqvt:
 
   103   assumes a: "alpha_abs ab1 ab2"
 
   103   assumes a: "alpha_abs ab1 ab2"
 
   104   shows "alpha_abs (p \<bullet> ab1) (p \<bullet> ab2)"
 
   104   shows "alpha_abs (p \<bullet> ab1) (p \<bullet> ab2)"
 
   105 using a
 
   105 using a
 
   106 apply(erule_tac alpha_abs.cases)
 
   106 apply(induct ab1 ab2 rule: alpha_abs.induct)
 
       
   107 apply(simp)
 
   107 apply(clarify)
 
   108 apply(clarify)
 
   108 apply(simp)
 
       
   109 apply(rule alpha_abs.intros)
 
       
   110 apply(rule_tac x="p \<bullet> pi" in exI)
 
       
   111 apply(rule conjI)
 
   109 apply(rule conjI)
 
   112 apply(simp add: supp_eqvt[symmetric])
 
   110 apply(simp add: supp_eqvt[symmetric])
 
   113 apply(simp add: Diff_eqvt[symmetric])
 
   111 apply(simp add: Diff_eqvt[symmetric])
 
       
   112 apply(rule_tac x="p \<bullet> pi" in exI)
 
   114 apply(rule conjI)
 
   113 apply(rule conjI)
 
   115 apply(simp add: supp_eqvt[symmetric])
 
   114 apply(simp add: supp_eqvt[symmetric])
 
   116 apply(simp add: Diff_eqvt[symmetric])
 
   115 apply(simp add: Diff_eqvt[symmetric])
 
   117 apply(simp only: fresh_star_permute_iff)
 
   116 apply(simp only: fresh_star_permute_iff)
 
   118 apply(simp add: permute_eqvt[symmetric])
 
   117 apply(simp add: permute_eqvt[symmetric])
 
   120 
   119 
   121 lemma test1:
 
   120 lemma test1:
 
   122   assumes a1: "a \<notin> (supp x) - bs"
 
   121   assumes a1: "a \<notin> (supp x) - bs"
 
   123   and     a2: "b \<notin> (supp x) - bs"
 
   122   and     a2: "b \<notin> (supp x) - bs"
 
   124   shows "alpha_abs (Abs_raw bs x) (Abs_raw ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))"
 
   123   shows "alpha_abs (Abs_raw bs x) (Abs_raw ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))"
 
   125 apply(rule alpha_abs.intros)
 
   124 unfolding alpha_abs.simps
 
   126 apply(rule_tac x="(a \<rightleftharpoons> b)" in exI)
 
   125 apply(rule_tac x="(a \<rightleftharpoons> b)" in exI)
 
   127 apply(rule_tac conjI)
 
   126 apply(rule_tac conjI)
 
   128 apply(simp add: supp_eqvt[symmetric])
 
   127 apply(simp add: supp_eqvt[symmetric])
 
   129 apply(simp add: Diff_eqvt[symmetric])
 
   128 apply(simp add: Diff_eqvt[symmetric])
 
   130 using a1 a2
 
   129 using a1 a2
 
   148 
   147 
   149 lemma s_test_lemma:
 
   148 lemma s_test_lemma:
 
   150   assumes a: "alpha_abs x y" 
   149   assumes a: "alpha_abs x y" 
   151   shows "s_test x = s_test y"
 
   150   shows "s_test x = s_test y"
 
   152 using a
 
   151 using a
 
   153 apply(induct)
 
   152 apply(induct rule: alpha_abs.induct)
 
   154 apply(simp)
 
   153 apply(simp)
 
   155 done
 
   154 done
 
   156   
   155   
   157 
   156 
   158 quotient_type 'a ABS = "('a::pt) ABS_raw" / "alpha_abs::('a::pt) ABS_raw \<Rightarrow> 'a ABS_raw \<Rightarrow> bool"
 
   157 quotient_type 'a ABS = "('a::pt) ABS_raw" / "alpha_abs::('a::pt) ABS_raw \<Rightarrow> 'a ABS_raw \<Rightarrow> bool"
 
   166 as
 
   165 as
 
   167    "Abs_raw"
 
   166    "Abs_raw"
 
   168 
   167 
   169 lemma [quot_respect]:
 
   168 lemma [quot_respect]:
 
   170   shows "((op =) ===> (op =) ===> alpha_abs) Abs_raw Abs_raw"
 
   169   shows "((op =) ===> (op =) ===> alpha_abs) Abs_raw Abs_raw"
 
   171 apply(auto)
 
   170 apply(auto simp del: alpha_abs.simps)
 
   172 apply(rule alpha_reflp)
 
   171 apply(rule alpha_reflp)
 
   173 done
 
   172 done
 
   174 
   173 
   175 lemma [quot_respect]:
 
   174 lemma [quot_respect]:
 
   176   shows "((op =) ===> alpha_abs ===> alpha_abs) permute permute"
 
   175   shows "((op =) ===> alpha_abs ===> alpha_abs) permute permute"
 
   308 apply(induct_tac x rule: ABS_induct)
 
   307 apply(induct_tac x rule: ABS_induct)
 
   309 apply(simp add: supp_Abs)
 
   308 apply(simp add: supp_Abs)
 
   310 apply(simp add: finite_supp)
 
   309 apply(simp add: finite_supp)
 
   311 done
 
   310 done
 
   312 
   311 
   313 lemma fresh_abs1:
 
   312 lemma fresh_abs:
 
   314   fixes x::"'a::fs"
 
   313   fixes x::"'a::fs"
 
   315   shows "a \<sharp> Abs bs x = (a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x))"
 
   314   shows "a \<sharp> Abs bs x = (a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x))"
 
   316 apply(simp add: fresh_def)
 
   315 apply(simp add: fresh_def)
 
   317 apply(simp add: supp_Abs)
 
   316 apply(simp add: supp_Abs)
 
   318 apply(auto)
 
   317 apply(auto)
 
   319 done
 
   318 done
 
   320 
   319 
   321 done
 
   320 lemma abs_eq:
 
   322 
   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)"
 
       
   322 apply(lifting alpha_abs.simps(1))
 
       
   323 done
 
       
   324 
       
   325 done
 
       
   326
nominal2