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.
Attic/Quot/Examples/FSet3.thy
changeset 1927 6c5e3ac737d9
parent 1921 e41b7046be2c
child 1929 f4e241829b80
equal deleted inserted replaced
1922:94ed05fb090e 1927:6c5e3ac737d9 
     1 theory FSet3
 
     1 theory FSet3
 
     2 imports "../../../Nominal/FSet"
 
     2 imports "../../../Nominal/FSet"
 
     3 begin
 
     3 begin
 
     4 
     4 
     5 (*sledgehammer[overlord,isar_proof,sorts]*)
 
       
     6 
       
     7 notation
 
     5 notation
 
     8   list_eq (infix "\<approx>" 50)
 
     6   list_eq (infix "\<approx>" 50)
 
     9 
     7 
    10 lemma fset_exhaust[case_names fempty finsert, cases type: fset]:
 
     8 lemma fset_exhaust[case_names fempty finsert, cases type: fset]:
 
    11   shows "\<lbrakk>S = {||} \<Longrightarrow> P; \<And>x S'. S = finsert x S' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
 
     9   shows "\<lbrakk>S = {||} \<Longrightarrow> P; \<And>x S'. S = finsert x S' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
 
    12 by (lifting list.exhaust)
 
    10   by (lifting list.exhaust)
 
    13 
    11 
    14 lemma list_rel_find_element:
 
    12 lemma list_rel_find_element:
 
    15   assumes a: "x \<in> set a"
 
    13   assumes a: "x \<in> set a"
 
    16   and b: "list_rel R a b"
 
    14   and b: "list_rel R a b"
 
    17   shows "\<exists>y. (y \<in> set b \<and> R x y)"
 
    15   shows "\<exists>y. (y \<in> set b \<and> R x y)"
 
    46   shows "(P ===> Q) x y"
 
    44   shows "(P ===> Q) x y"
 
    47   using assms by (simp add: fun_rel_def)
 
    45   using assms by (simp add: fun_rel_def)
 
    48 
    46 
    49 lemma [quot_respect]:
 
    47 lemma [quot_respect]:
 
    50   shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"
 
    48   shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"
 
    51 proof (rule fun_relI, (erule pred_compE, erule pred_compE))
 
    49 proof (rule fun_relI, elim pred_compE)
 
    52   fix a b ba bb
 
    50   fix a b ba bb
 
    53   assume a: "list_rel op \<approx> a ba"
 
    51   assume a: "list_rel op \<approx> a ba"
 
    54   assume b: "ba \<approx> bb"
 
    52   assume b: "ba \<approx> bb"
 
    55   assume c: "list_rel op \<approx> bb b"
 
    53   assume c: "list_rel op \<approx> bb b"
 
    56   have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof
 
    54   have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof
 
    77 
    75 
    78 lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
 
    76 lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
 
    79   unfolding list_eq.simps
 
    77   unfolding list_eq.simps
 
    80   by (simp only: set_map set_in_eq)
 
    78   by (simp only: set_map set_in_eq)
 
    81 
    79 
    82 lemma quotient_compose_list_pre:
 
    80 lemma compose_list_refl:
 
    83   "(list_rel op \<approx> OOO op \<approx>) r s =
 
    81   shows "(list_rel op \<approx> OOO op \<approx>) r r"
 
    84   ((list_rel op \<approx> OOO op \<approx>) r r \<and> (list_rel op \<approx> OOO op \<approx>) s s \<and>
 
    82 proof
 
    85   abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"
 
    83   show c: "list_rel op \<approx> r r" by (rule list_rel_refl) (metis equivp_def fset_equivp)
 
    86   apply rule
 
    84   have d: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
 
    87   apply rule
 
    85   show b: "(op \<approx> OO list_rel op \<approx>) r r" by (rule pred_compI) (rule d, rule c)
 
    88   apply rule
 
    86 qed
 
    89   apply (rule list_rel_refl)
 
    87 
    90   apply (metis equivp_def fset_equivp)
 
    88 lemma list_rel_refl:
 
    91   apply rule
 
    89   shows "(list_rel op \<approx>) r r"
 
    92   apply (rule equivp_reflp[OF fset_equivp])
 
    90   by (rule list_rel_refl)(metis equivp_def fset_equivp)
 
    93   apply (rule list_rel_refl)
 
    91 
    94   apply (metis equivp_def fset_equivp)
 
    92 lemma Quotient_fset_list:
 
    95   apply (rule)
 
    93   shows "Quotient (list_rel op \<approx>) (map abs_fset) (map rep_fset)"
 
    96   apply rule
 
    94   by (fact list_quotient[OF Quotient_fset])
 
    97   apply (rule list_rel_refl)
 
       
    98   apply (metis equivp_def fset_equivp)
 
       
    99   apply rule
 
       
   100   apply (rule equivp_reflp[OF fset_equivp])
 
       
   101   apply (rule list_rel_refl)
 
       
   102   apply (metis equivp_def fset_equivp)
 
       
   103   apply (subgoal_tac "map abs_fset r \<approx> map abs_fset s")
 
       
   104   apply (metis Quotient_rel[OF Quotient_fset])
 
       
   105   apply (auto simp only:)[1]
 
       
   106   apply (subgoal_tac "map abs_fset r = map abs_fset b")
 
       
   107   apply (subgoal_tac "map abs_fset s = map abs_fset ba")
 
       
   108   apply (simp only: map_rel_cong)
 
       
   109   apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]])
 
       
   110   apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]])
 
       
   111   apply rule
 
       
   112   apply (rule rep_abs_rsp[of "list_rel op \<approx>" "map abs_fset"])
 
       
   113   apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
 
       
   114   apply (rule list_rel_refl)
 
       
   115   apply (metis equivp_def fset_equivp)
 
       
   116   apply rule
 
       
   117   apply (erule conjE)+
 
       
   118   prefer 2
 
       
   119   apply (rule rep_abs_rsp_left[of "list_rel op \<approx>" "map abs_fset"])
 
       
   120   apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
 
       
   121   apply (rule list_rel_refl)
 
       
   122   apply (metis equivp_def fset_equivp)
 
       
   123   apply (subgoal_tac "map abs_fset r \<approx> map abs_fset s")
 
       
   124   apply (rule map_rel_cong)
 
       
   125   apply (assumption)
 
       
   126   apply (subst Quotient_rel[OF Quotient_fset])
 
       
   127   apply simp
 
       
   128   done
 
       
   129 
    95 
   130 lemma quotient_compose_list[quot_thm]:
 
    96 lemma quotient_compose_list[quot_thm]:
 
   131   shows  "Quotient ((list_rel op \<approx>) OOO (op \<approx>))
 
    97   shows  "Quotient ((list_rel op \<approx>) OOO (op \<approx>))
 
   132     (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
 
    98     (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
 
   133   unfolding Quotient_def comp_def
 
    99   unfolding Quotient_def comp_def
 
   134   apply (rule)+
 
   100 proof (intro conjI allI)
 
   135   apply (simp add: abs_o_rep[OF Quotient_fset] Quotient_abs_rep[OF Quotient_fset] map_id)
 
   101   fix a r s
 
   136   apply (rule)
 
   102   show "abs_fset (map abs_fset (map rep_fset (rep_fset a))) = a"
 
   137   apply (rule)
 
   103     by (simp add: abs_o_rep[OF Quotient_fset] Quotient_abs_rep[OF Quotient_fset] map_id)
 
   138   apply (rule)
 
   104   have b: "list_rel op \<approx> (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
 
   139   apply (rule list_rel_refl)
 
   105     by (rule list_rel_refl)
 
   140   apply (metis equivp_def fset_equivp)
 
   106   have c: "(op \<approx> OO list_rel op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
 
   141   apply (rule)
 
   107     by (rule, rule equivp_reflp[OF fset_equivp]) (rule b)
 
   142   apply (rule equivp_reflp[OF fset_equivp])
 
   108   show "(list_rel op \<approx> OOO op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
 
   143   apply (rule list_rel_refl)
 
   109     by (rule, rule list_rel_refl) (rule c)
 
   144   apply (metis equivp_def fset_equivp)
 
   110   show "(list_rel op \<approx> OOO op \<approx>) r s = ((list_rel op \<approx> OOO op \<approx>) r r \<and>
 
   145   apply rule
 
   111         (list_rel op \<approx> OOO op \<approx>) s s \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"
 
   146   apply rule
 
   112   proof (intro iffI conjI)
 
   147   apply (rule quotient_compose_list_pre)
 
   113     show "(list_rel op \<approx> OOO op \<approx>) r r" by (rule compose_list_refl)
 
   148   done
 
   114     show "(list_rel op \<approx> OOO op \<approx>) s s" by (rule compose_list_refl)
 
       
   115   next
 
       
   116     assume a: "(list_rel op \<approx> OOO op \<approx>) r s"
 
       
   117     then have b: "map abs_fset r \<approx> map abs_fset s" proof (elim pred_compE)
 
       
   118       fix b ba
 
       
   119       assume c: "list_rel op \<approx> r b"
 
       
   120       assume d: "b \<approx> ba"
 
       
   121       assume e: "list_rel op \<approx> ba s"
 
       
   122       have f: "map abs_fset r = map abs_fset b"
 
       
   123         by (metis Quotient_rel[OF Quotient_fset_list] c)
 
       
   124       have g: "map abs_fset s = map abs_fset ba"
 
       
   125         by (metis Quotient_rel[OF Quotient_fset_list] e)
 
       
   126       show "map abs_fset r \<approx> map abs_fset s" using d f g map_rel_cong by simp
 
       
   127     qed
 
       
   128     then show "abs_fset (map abs_fset r) = abs_fset (map abs_fset s)"
 
       
   129       by (metis Quotient_rel[OF Quotient_fset])
 
       
   130   next
 
       
   131     assume a: "(list_rel op \<approx> OOO op \<approx>) r r \<and> (list_rel op \<approx> OOO op \<approx>) s s
 
       
   132       \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s)"
 
       
   133     then have s: "(list_rel op \<approx> OOO op \<approx>) s s" by simp
 
       
   134     have d: "map abs_fset r \<approx> map abs_fset s"
 
       
   135       by (subst Quotient_rel[OF Quotient_fset]) (simp add: a)
 
       
   136     have b: "map rep_fset (map abs_fset r) \<approx> map rep_fset (map abs_fset s)"
 
       
   137       by (rule map_rel_cong[OF d])
 
       
   138     have y: "list_rel op \<approx> (map rep_fset (map abs_fset s)) s"
 
       
   139       by (fact rep_abs_rsp_left[OF Quotient_fset_list, OF list_rel_refl[of s]])
 
       
   140     have c: "(op \<approx> OO list_rel op \<approx>) (map rep_fset (map abs_fset r)) s"
 
       
   141       by (rule pred_compI) (rule b, rule y)
 
       
   142     have z: "list_rel op \<approx> r (map rep_fset (map abs_fset r))"
 
       
   143       by (fact rep_abs_rsp[OF Quotient_fset_list, OF list_rel_refl[of r]])
 
       
   144     then show "(list_rel op \<approx> OOO op \<approx>) r s"
 
       
   145       using a c pred_compI by simp
 
       
   146   qed
 
       
   147 qed
 
   149 
   148 
   150 lemma nil_prs2[quot_preserve]: "(abs_fset \<circ> map f) [] = abs_fset []"
 
   149 lemma nil_prs2[quot_preserve]: "(abs_fset \<circ> map f) [] = abs_fset []"
 
   151   by simp
 
   150   by simp
 
   152 
   151 
   153 lemma fconcat_empty:
 
   152 lemma fconcat_empty:
 
   180 lemma append_prs2[quot_preserve]:
 
   179 lemma append_prs2[quot_preserve]:
 
   181   "((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> abs_fset \<circ> map abs_fset) op @ = funion"
 
   180   "((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> abs_fset \<circ> map abs_fset) op @ = funion"
 
   182   by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset]
 
   181   by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset]
 
   183       abs_o_rep[OF Quotient_fset] map_id sup_fset_def)
 
   182       abs_o_rep[OF Quotient_fset] map_id sup_fset_def)
 
   184 
   183 
       
   184 lemma list_rel_app_l:
 
       
   185   assumes a: "reflp R"
 
       
   186   and b: "list_rel R l r"
 
       
   187   shows "list_rel R (z @ l) (z @ r)"
 
       
   188   by (induct z) (simp_all add: b, metis a reflp_def)
 
       
   189 
       
   190 lemma append_rsp2_pre0:
 
       
   191   assumes a:"list_rel op \<approx> x x'"
 
       
   192   shows "list_rel op \<approx> (x @ z) (x' @ z)"
 
       
   193   using a apply (induct x x' rule: list_induct2')
 
       
   194   apply simp_all
 
       
   195   apply (rule list_rel_refl)
 
       
   196   done
 
       
   197 
       
   198 lemma append_rsp2_pre1:
 
       
   199   assumes a:"list_rel op \<approx> x x'"
 
       
   200   shows "list_rel op \<approx> (z @ x) (z @ x')"
 
       
   201   using a apply (induct x x' arbitrary: z rule: list_induct2')
 
       
   202   apply (rule list_rel_refl)
 
       
   203   apply (simp_all del: list_eq.simps)
 
       
   204   apply (rule list_rel_app_l)
 
       
   205   apply (simp_all add: reflp_def)
 
       
   206   done
 
       
   207 
       
   208 lemma append_rsp2_pre:
 
       
   209   assumes a:"list_rel op \<approx> x x'"
 
       
   210   and     b: "list_rel op \<approx> z z'"
 
       
   211   shows "list_rel op \<approx> (x @ z) (x' @ z')"
 
       
   212   apply (rule list_rel_transp[OF fset_equivp])
 
       
   213   apply (rule append_rsp2_pre0)
 
       
   214   apply (rule a)
 
       
   215   using b apply (induct z z' rule: list_induct2')
 
       
   216   apply (simp_all only: append_Nil2)
 
       
   217   apply (rule list_rel_refl)
 
       
   218   apply simp_all
 
       
   219   apply (rule append_rsp2_pre1)
 
       
   220   apply simp
 
       
   221   done
 
       
   222 
   185 lemma append_rsp2[quot_respect]:
 
   223 lemma append_rsp2[quot_respect]:
 
   186   "(list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx>) op @ op @"
 
   224   "(list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx>) op @ op @"
 
   187   sorry
 
   225 proof (intro fun_relI, elim pred_compE)
 
       
   226   fix x y z w x' z' y' w' :: "'a list list"
 
       
   227   assume a:"list_rel op \<approx> x x'"
 
       
   228   and b:    "x' \<approx> y'"
 
       
   229   and c:    "list_rel op \<approx> y' y"
 
       
   230   assume aa: "list_rel op \<approx> z z'"
 
       
   231   and bb:   "z' \<approx> w'"
 
       
   232   and cc:   "list_rel op \<approx> w' w"
 
       
   233   have a': "list_rel op \<approx> (x @ z) (x' @ z')" using a aa append_rsp2_pre by auto
 
       
   234   have b': "x' @ z' \<approx> y' @ w'" using b bb by simp
 
       
   235   have c': "list_rel op \<approx> (y' @ w') (y @ w)" using c cc append_rsp2_pre by auto
 
       
   236   have d': "(op \<approx> OO list_rel op \<approx>) (x' @ z') (y @ w)"
 
       
   237     by (rule pred_compI) (rule b', rule c')
 
       
   238   show "(list_rel op \<approx> OOO op \<approx>) (x @ z) (y @ w)"
 
       
   239     by (rule pred_compI) (rule a', rule d')
 
       
   240 qed
 
   188 
   241 
   189 lemma "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys"
 
   242 lemma "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys"
 
   190   by (lifting concat_append)
 
   243   by (lifting concat_append)
 
   191 
   244 
   192 (* TBD *)
 
   245 (* TBD *)
 
   193 
       
   194 
       
   195 find_theorems concat
 
       
   196 
   246 
   197 text {* syntax for fset comprehensions (adapted from lists) *}
 
   247 text {* syntax for fset comprehensions (adapted from lists) *}
 
   198 
   248 
   199 nonterminals fsc_qual fsc_quals
 
   249 nonterminals fsc_qual fsc_quals
 
   200 
   250 
   208 
   258 
   209 syntax (xsymbols)
 
   259 syntax (xsymbols)
 
   210 "_fsc_gen" :: "'a \<Rightarrow> 'a fset \<Rightarrow> fsc_qual" ("_ \<leftarrow> _")
 
   260 "_fsc_gen" :: "'a \<Rightarrow> 'a fset \<Rightarrow> fsc_qual" ("_ \<leftarrow> _")
 
   211 syntax (HTML output)
 
   261 syntax (HTML output)
 
   212 "_fsc_gen" :: "'a \<Rightarrow> 'a fset \<Rightarrow> fsc_qual" ("_ \<leftarrow> _")
 
   262 "_fsc_gen" :: "'a \<Rightarrow> 'a fset \<Rightarrow> fsc_qual" ("_ \<leftarrow> _")
 
       
   263 
       
   264 ML {* Syntax.check_term @{context} (Const ("List.append", dummyT) $ @{term "[3::nat,4]"}) *}
 
   213 
   265 
   214 parse_translation (advanced) {*
 
   266 parse_translation (advanced) {*
 
   215 let
 
   267 let
 
   216   val femptyC = Syntax.const @{const_name fempty};
 
   268   val femptyC = Syntax.const @{const_name fempty};
 
   217   val finsertC = Syntax.const @{const_name finsert};
 
   269   val finsertC = Syntax.const @{const_name finsert};
nominal2