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.
FSet.thy
changeset 214 a66f81c264aa
parent 213 7610d2bbca48
child 215 89a2ff3f82c7
equal deleted inserted replaced
213:7610d2bbca48 214:a66f81c264aa 
    92 *}*)
 
    92 *}*)
 
    93 
    93 
    94 lemma card1_0:
 
    94 lemma card1_0:
 
    95   fixes a :: "'a list"
 
    95   fixes a :: "'a list"
 
    96   shows "(card1 a = 0) = (a = [])"
 
    96   shows "(card1 a = 0) = (a = [])"
 
    97   apply (induct a)
 
    97   by (induct a) auto
 
    98    apply (simp)
 
       
    99   apply (simp_all)
 
       
   100    apply meson
 
       
   101   apply (simp_all)
 
       
   102   done
 
       
   103 
    98 
   104 lemma not_mem_card1:
 
    99 lemma not_mem_card1:
 
   105   fixes x :: "'a"
 
   100   fixes x :: "'a"
 
   106   fixes xs :: "'a list"
 
   101   fixes xs :: "'a list"
 
   107   shows "~(x memb xs) \<Longrightarrow> card1 (x # xs) = Suc (card1 xs)"
 
   102   shows "~(x memb xs) \<Longrightarrow> card1 (x # xs) = Suc (card1 xs)"
 
   108   by simp
 
   103   by simp
 
   109 
   104 
   110 
       
   111 lemma mem_cons:
 
   105 lemma mem_cons:
 
   112   fixes x :: "'a"
 
   106   fixes x :: "'a"
 
   113   fixes xs :: "'a list"
 
   107   fixes xs :: "'a list"
 
   114   assumes a : "x memb xs"
 
   108   assumes a : "x memb xs"
 
   115   shows "x # xs \<approx> xs"
 
   109   shows "x # xs \<approx> xs"
 
   116   using a
 
   110   using a by (induct xs) (auto intro: list_eq.intros )
 
   117   apply (induct xs)
 
       
   118   apply (auto intro: list_eq.intros)
 
       
   119   done
 
       
   120 
   111 
   121 lemma card1_suc:
 
   112 lemma card1_suc:
 
   122   fixes xs :: "'a list"
 
   113   fixes xs :: "'a list"
 
   123   fixes n :: "nat"
 
   114   fixes n :: "nat"
 
   124   assumes c: "card1 xs = Suc n"
 
   115   assumes c: "card1 xs = Suc n"
 
   175 term map
 
   166 term map
 
   176 term fmap
 
   167 term fmap
 
   177 thm fmap_def
 
   168 thm fmap_def
 
   178 
   169 
   179 
   170 
   180 
   171 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *}
 
   181 
   172 ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *}
 
   182 ML {*
 
   173 
       
   174 (* ML {*
 
   183   val consts = [@{const_name "Nil"}, @{const_name "Cons"},
 
   175   val consts = [@{const_name "Nil"}, @{const_name "Cons"},
 
   184                 @{const_name "membship"}, @{const_name "card1"},
 
   176                 @{const_name "membship"}, @{const_name "card1"},
 
   185                 @{const_name "append"}, @{const_name "fold1"},
 
   177                 @{const_name "append"}, @{const_name "fold1"},
 
   186                 @{const_name "map"}];
 
   178                 @{const_name "map"}];
 
   187 *}
 
   179 *} *)
 
   188 
   180 
   189 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *}
 
       
   190 
       
   191 ML {*
 
       
   192 fun add_lower_defs ctxt defs =
 
       
   193   let
 
       
   194     val defs_pre_sym = map symmetric defs
 
       
   195     val defs_atom = map atomize_thm defs_pre_sym
 
       
   196     val defs_all = flat (map (add_lower_defs_aux ctxt) defs_atom)
 
       
   197   in
 
       
   198     map Thm.varifyT defs_all
 
       
   199   end
 
       
   200 *}
 
       
   201 ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *}
 
   181 ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *}
 
   202 
       
   203 
   182 
   204 lemma memb_rsp:
 
   183 lemma memb_rsp:
 
   205   fixes z
 
   184   fixes z
 
   206   assumes a: "list_eq x y"
 
   185   assumes a: "list_eq x y"
 
   207   shows "(z memb x) = (z memb y)"
 
   186   shows "(z memb x) = (z memb y)"
 
   208   using a by induct auto
 
   187   using a by induct auto
 
   209 
   188 
   210 lemma ho_memb_rsp:
 
   189 lemma ho_memb_rsp:
 
   211   "(op = ===> (op \<approx> ===> op =)) (op memb) (op memb)"
 
   190   "(op = ===> (op \<approx> ===> op =)) (op memb) (op memb)"
 
   212   apply (simp add: FUN_REL.simps)
 
   191   by (simp add: memb_rsp)
 
   213   apply (metis memb_rsp)
 
       
   214   done
 
       
   215 
   192 
   216 lemma card1_rsp:
 
   193 lemma card1_rsp:
 
   217   fixes a b :: "'a list"
 
   194   fixes a b :: "'a list"
 
   218   assumes e: "a \<approx> b"
 
   195   assumes e: "a \<approx> b"
 
   219   shows "card1 a = card1 b"
 
   196   shows "card1 a = card1 b"
 
   220   using e apply induct
 
   197   using e by induct (simp_all add:memb_rsp)
 
   221   apply (simp_all add:memb_rsp)
 
       
   222   done
 
       
   223 
   198 
   224 lemma ho_card1_rsp: "op \<approx> ===> op = card1 card1"
 
   199 lemma ho_card1_rsp: "op \<approx> ===> op = card1 card1"
 
   225   apply (simp add: FUN_REL.simps)
 
   200   by (simp add: card1_rsp)
 
   226   apply (metis card1_rsp)
 
       
   227   done
 
       
   228 
   201 
   229 lemma cons_rsp:
 
   202 lemma cons_rsp:
 
   230   fixes z
 
   203   fixes z
 
   231   assumes a: "xs \<approx> ys"
 
   204   assumes a: "xs \<approx> ys"
 
   232   shows "(z # xs) \<approx> (z # ys)"
 
   205   shows "(z # xs) \<approx> (z # ys)"
 
   233   using a by (rule list_eq.intros(5))
 
   206   using a by (rule list_eq.intros(5))
 
   234 
   207 
   235 lemma ho_cons_rsp:
 
   208 lemma ho_cons_rsp:
 
   236   "op = ===> op \<approx> ===> op \<approx> op # op #"
 
   209   "op = ===> op \<approx> ===> op \<approx> op # op #"
 
   237   apply (simp add: FUN_REL.simps)
 
   210   by (simp add: cons_rsp)
 
   238   apply (metis cons_rsp)
 
       
   239   done
 
       
   240 
   211 
   241 lemma append_rsp_fst:
 
   212 lemma append_rsp_fst:
 
   242   assumes a : "list_eq l1 l2"
 
   213   assumes a : "list_eq l1 l2"
 
   243   shows "list_eq (l1 @ s) (l2 @ s)"
 
   214   shows "(l1 @ s) \<approx> (l2 @ s)"
 
   244   using a
 
   215   using a
 
   245   apply(induct)
 
   216   by (induct) (auto intro: list_eq.intros list_eq_refl)
 
   246   apply(auto intro: list_eq.intros)
 
   217 
   247   apply(rule list_eq_refl)
 
   218 lemma append_end:
 
   248 done
 
   219   shows "(e # l) \<approx> (l @ [e])"
 
   249 
   220   apply (induct l)
 
   250 (* Need stronger induction... *)
 
   221   apply (auto intro: list_eq.intros list_eq_refl)
 
   251 lemma "(a @ b) \<approx> (b @ a)"
 
   222   done
 
   252   apply(induct a)
 
   223 
   253   sorry
 
   224 lemma rev_rsp:
 
       
   225   shows "a \<approx> rev a"
 
       
   226   apply (induct a)
 
       
   227   apply simp
 
       
   228   apply (rule list_eq_refl)
 
       
   229   apply simp_all
 
       
   230   apply (rule list_eq.intros(6))
 
       
   231   prefer 2
 
       
   232   apply (rule append_rsp_fst)
 
       
   233   apply assumption
 
       
   234   apply (rule append_end)
 
       
   235   done
 
       
   236 
       
   237 lemma append_sym_rsp:
 
       
   238   shows "(a @ b) \<approx> (b @ a)"
 
       
   239   apply (rule list_eq.intros(6))
 
       
   240   apply (rule append_rsp_fst)
 
       
   241   apply (rule rev_rsp)
 
       
   242   apply (rule list_eq.intros(6))
 
       
   243   apply (rule rev_rsp)
 
       
   244   apply (simp)
 
       
   245   apply (rule append_rsp_fst)
 
       
   246   apply (rule list_eq.intros(3))
 
       
   247   apply (rule rev_rsp)
 
       
   248   done
 
       
   249 
       
   250 lemma append_rsp:
 
       
   251   assumes a : "list_eq l1 r1"
 
       
   252   assumes b : "list_eq l2 r2 "
 
       
   253   shows "(l1 @ l2) \<approx> (r1 @ r2)"
 
       
   254   apply (rule list_eq.intros(6))
 
       
   255   apply (rule append_rsp_fst)
 
       
   256   using a apply (assumption)
 
       
   257   apply (rule list_eq.intros(6))
 
       
   258   apply (rule append_sym_rsp)
 
       
   259   apply (rule list_eq.intros(6))
 
       
   260   apply (rule append_rsp_fst)
 
       
   261   using b apply (assumption)
 
       
   262   apply (rule append_sym_rsp)
 
       
   263   done
 
   254 
   264 
   255 lemma ho_append_rsp:
 
   265 lemma ho_append_rsp:
 
   256   "op \<approx> ===> op \<approx> ===> op \<approx> op @ op @"
 
   266   "op \<approx> ===> op \<approx> ===> op \<approx> op @ op @"
 
   257 sorry
 
   267   by (simp add: append_rsp)
 
   258 
   268 
   259 lemma map_rsp:
 
   269 lemma map_rsp:
 
   260   assumes a: "a \<approx> b"
 
   270   assumes a: "a \<approx> b"
 
   261   shows "map f a \<approx> map f b"
 
   271   shows "map f a \<approx> map f b"
 
   262   using a
 
   272   using a
nominal2