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/Examples/FSet3.thy
changeset 722 d5fce1ead432
parent 716 1e08743b6997
child 724 d705d7ae2410
equal deleted inserted replaced
718:7b74d77a61aa 722:d5fce1ead432 
     1 theory FSet3
 
     1 theory FSet3
 
     2 imports "../QuotMain" List
 
     2 imports "../QuotMain" List
 
     3 begin
 
     3 begin
 
     4 
     4 
     5 definition
 
     5 fun
 
     6   list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
 
     6   list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
 
     7 where
 
     7 where
 
     8   "list_eq x y = (\<forall>e. e mem x = e mem y)"
 
     8   "list_eq xs ys = (\<forall>e. (e \<in> set xs) = (e \<in> set ys))"
 
     9 
       
    10 lemma list_eq_reflp:
 
       
    11   shows "xs \<approx> xs"
 
       
    12   by (metis list_eq_def)
 
       
    13 
     9 
    14 lemma list_eq_equivp:
 
    10 lemma list_eq_equivp:
 
    15   shows "equivp list_eq"
 
    11   shows "equivp list_eq"
 
    16   unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
 
    12 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
 
    17   apply (auto intro: list_eq_def)
 
    13 by auto
 
    18   apply (metis list_eq_def)
 
       
    19   apply (metis list_eq_def)
 
       
    20   sorry
 
       
    21 
    14 
    22 quotient fset = "'a list" / "list_eq"
 
    15 quotient fset = "'a list" / "list_eq"
 
    23   by (rule list_eq_equivp)
 
    16   by (rule list_eq_equivp)
 
    24 
    17 
    25 lemma not_nil_equiv_cons: "\<not>[] \<approx> a # A" sorry
 
    18 lemma not_nil_equiv_cons: 
    26 
    19   "\<not>[] \<approx> a # A" 
    27 (* The 2 lemmas below are different from the ones in QuotList *)
 
    20 by auto
 
       
    21 
    28 lemma nil_rsp[quot_respect]:
 
    22 lemma nil_rsp[quot_respect]:
 
    29   shows "[] \<approx> []"
 
    23   shows "[] \<approx> []"
 
    30 by (rule list_eq_reflp)
 
    24   by simp
 
    31 
    25 
    32 lemma cons_rsp[quot_respect]: (* Better then the one from QuotList *)
 
    26 lemma cons_rsp[quot_respect]: 
    33   " (op = ===> op \<approx> ===> op \<approx>) op # op #"
 
    27   shows "(op = ===> op \<approx> ===> op \<approx>) op # op #"
 
    34   sorry
 
    28   by simp
 
    35 
    29 
       
    30 (*
 
    36 lemma mem_rsp[quot_respect]:
 
    31 lemma mem_rsp[quot_respect]:
 
    37   "(op = ===> op \<approx> ===> op =) (op mem) (op mem)"
 
    32   "(op = ===> op \<approx> ===> op =) (op mem) (op mem)"
 
    38   sorry
 
    33 *)
 
    39 
    34 
    40 lemma no_mem_nil: "(\<forall>a. \<not>(a mem A)) = (A = [])"
 
    35 
    41 sorry
 
    36 lemma no_mem_nil: 
    42 
    37   "(\<forall>a. \<not>(a \<in> set A)) = (A = [])"
 
    43 lemma none_mem_nil: "(\<forall>a. \<not>(a mem A)) = (A \<approx> [])"
 
    38 by (induct A) (auto)
 
    44 sorry
 
    39 
    45 
    40 lemma none_mem_nil: 
    46 lemma mem_cons: "a mem A \<Longrightarrow> a # A \<approx> A"
 
    41   "(\<forall>a. \<not>(a \<in> set A)) = (A \<approx> [])"
 
    47 sorry
 
    42 by simp
 
    48 
    43 
    49 lemma cons_left_comm: "x # y # A \<approx> y # x # A"
 
    44 lemma mem_cons: 
    50 sorry
 
    45   "a \<in> set A \<Longrightarrow> a # A \<approx> A"
 
    51 
    46 by auto
 
    52 lemma cons_left_idem: "x # x # A \<approx> x # A"
 
    47 
    53 sorry
 
    48 lemma cons_left_comm: 
       
    49   "x #y # A \<approx> y # x # A"
 
       
    50 by auto
 
       
    51 
       
    52 lemma cons_left_idem: 
       
    53   "x # x # A \<approx> x # A"
 
       
    54 by auto
 
    54 
    55 
    55 lemma finite_set_raw_strong_cases:
 
    56 lemma finite_set_raw_strong_cases:
 
    56   "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a mem Y) \<and> (X \<approx> a # Y)))"
 
    57   "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a mem Y) \<and> (X \<approx> a # Y)))"
 
    57   apply (induct X)
 
    58   apply (induct X)
 
    58   apply (simp)
 
    59   apply (auto)
 
    59   sorry
 
    60   sorry
 
    60 
    61 
    61 primrec
 
    62 fun
 
    62   delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"
 
    63   delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"
 
    63 where
 
    64 where
 
    64   "delete_raw [] x = []"
 
    65   "delete_raw [] x = []"
 
    65 | "delete_raw (a # A) x = (if (a = x) then delete_raw A x else a # (delete_raw A x))"
 
    66 | "delete_raw (a # A) x = (if (a = x) then delete_raw A x else a # (delete_raw A x))"
 
    66 
    67 
       
    68 (* definitely FALSE
 
    67 lemma mem_delete_raw:
 
    69 lemma mem_delete_raw:
 
    68   "x mem (delete_raw A a) = x mem A \<and> \<not>(x = a)"
 
    70   "x mem (delete_raw A a) = x mem A \<and> \<not>(x = a)"
 
    69 sorry
 
    71 apply(induct A arbitrary: x a)
 
       
    72 apply(auto)
 
       
    73 sorry
 
       
    74 *)
 
    70 
    75 
    71 lemma mem_delete_raw_ident:
 
    76 lemma mem_delete_raw_ident:
 
    72   "\<not>(MEM a (A delete_raw a))"
 
    77   "\<not>(a \<in> set (delete_raw A a))"
 
    73 sorry
 
    78 by (induct A) (auto)
 
    74 
    79 
    75 lemma not_mem_delete_raw_ident:
 
    80 lemma not_mem_delete_raw_ident:
 
    76   "\<not>(b mem A) \<Longrightarrow> (delete_raw A b = A)"
 
    81   "b \<notin> set A \<Longrightarrow> (delete_raw A b = A)"
 
    77 sorry
 
    82 by (induct A) (auto)
 
    78 
    83 
    79 lemma delete_raw_RSP:
 
    84 lemma delete_raw_RSP:
 
    80   "A \<approx> B \<Longrightarrow> delete_raw A a \<approx> delete_raw B a"
 
    85   "A \<approx> B \<Longrightarrow> delete_raw A a \<approx> delete_raw B a"
 
       
    86 apply(induct A arbitrary: B a)
 
       
    87 apply(auto)
 
    81 sorry
 
    88 sorry
 
    82 
    89 
    83 lemma cons_delete_raw:
 
    90 lemma cons_delete_raw:
 
    84   "a # (delete_raw A a) \<approx> (if a mem A then A else (a # A))"
 
    91   "a # (delete_raw A a) \<approx> (if a mem A then A else (a # A))"
 
    85 sorry
 
    92 sorry
 
   113   fixes n :: "nat"
 
   120   fixes n :: "nat"
 
   114   assumes c: "card_raw xs = Suc n"
 
   121   assumes c: "card_raw xs = Suc n"
 
   115   shows "\<exists>a ys. \<not>(a mem ys) \<and> xs \<approx> (a # ys)"
 
   122   shows "\<exists>a ys. \<not>(a mem ys) \<and> xs \<approx> (a # ys)"
 
   116   using c
 
   123   using c
 
   117 apply(induct xs)
 
   124 apply(induct xs)
 
       
   125 (*apply(metis mem_delete_raw)
 
   118 apply(metis mem_delete_raw)
 
   126 apply(metis mem_delete_raw)
 
   119 apply(metis mem_delete_raw)
 
   127 done*)
 
   120 done
 
   128 sorry
 
       
   129 
   121 
   130 
   122 lemma mem_card_raw_not_0:
 
   131 lemma mem_card_raw_not_0:
 
   123   "a mem A \<Longrightarrow> \<not>(card_raw A = 0)"
 
   132   "a mem A \<Longrightarrow> \<not>(card_raw A = 0)"
 
   124 sorry
 
   133 sorry
 
   125 
   134 
   172   "rsp_fold f \<Longrightarrow> h mem B \<Longrightarrow> fold_raw f z B = f h (fold_raw f z (delete_raw B h))"
 
   181   "rsp_fold f \<Longrightarrow> h mem B \<Longrightarrow> fold_raw f z B = f h (fold_raw f z (delete_raw B h))"
 
   173 sorry
 
   182 sorry
 
   174 
   183 
   175 lemma fold_rsp[quot_respect]:
 
   184 lemma fold_rsp[quot_respect]:
 
   176   "(op = ===> op = ===> op \<approx> ===> op =) fold_raw fold_raw"
 
   185   "(op = ===> op = ===> op \<approx> ===> op =) fold_raw fold_raw"
 
   177   apply (auto)
 
   186 apply(auto)
 
   178   apply (case_tac "rsp_fold x")
 
       
   179 sorry
 
   187 sorry
 
   180 
   188 
   181 lemma append_rsp[quot_respect]:
 
   189 lemma append_rsp[quot_respect]:
 
   182   "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
 
   190   "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
 
   183   sorry
 
   191 by auto
 
   184 
   192 
   185 primrec
 
   193 primrec
 
   186   inter_raw
 
   194   inter_raw
 
   187 where
 
   195 where
 
   188   "inter_raw [] B = []"
 
   196   "inter_raw [] B = []"
 
   197 sorry
 
   205 sorry
 
   198 
   206 
   199 
   207 
   200 (* LIFTING DEFS *)
 
   208 (* LIFTING DEFS *)
 
   201 
   209 
   202 quotient_def
 
   210 
   203   "Empty :: 'a fset" as "[]::'a list"
 
   211 section {* Constants on the Quotient Type *} 
   204 
   212 
   205 quotient_def
 
   213 quotient_def
 
   206   "Insert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" as "op #"
 
   214   "fempty :: 'a fset" 
   207 
   215   as "[]::'a list"
 
   208 quotient_def
 
   216 
   209   "In :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" as "op mem"
 
   217 quotient_def
 
   210 
   218   "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" 
   211 quotient_def
 
   219   as "op #"
 
   212   "Card :: 'a fset \<Rightarrow> nat" as "card_raw"
 
   220 
   213 
   221 quotient_def
 
   214 quotient_def
 
   222   "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<in>f _" [50, 51] 50)
 
   215   "Delete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" as "delete_raw"
 
   223   as "\<lambda>x X. x \<in> set X"
 
   216 
   224 
   217 quotient_def
 
   225 abbreviation
 
   218   "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" as "op @"
 
   226   fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<notin>f _" [50, 51] 50)
 
   219 
   227 where
 
   220 quotient_def
 
   228   "a \<notin>f S \<equiv> \<not>(a \<in>f S)"
 
   221   "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" as "inter_raw"
 
   229 
   222 
   230 quotient_def
 
   223 quotient_def
 
   231   "fcard :: 'a fset \<Rightarrow> nat" 
   224   "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" as "fold_raw"
 
   232   as "card_raw"
 
   225 
   233 
   226 quotient_def
 
   234 quotient_def
 
   227   "fset_to_set :: 'a fset \<Rightarrow> 'a set" as "set"
 
   235   "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" 
   228 
   236   as "delete_raw"
 
   229 
   237 
   230 (* LIFTING THMS *)
 
   238 quotient_def
 
       
   239   "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<in>f _" [50, 51] 50)
 
       
   240   as "op @"
 
       
   241 
       
   242 quotient_def
 
       
   243   "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70)
 
       
   244   as "inter_raw"
 
       
   245 
       
   246 quotient_def
 
       
   247   "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" 
       
   248   as "fold_raw"
 
       
   249 
       
   250 quotient_def
 
       
   251   "fset_to_set :: 'a fset \<Rightarrow> 'a set" 
       
   252   as "set"
 
       
   253 
       
   254 
       
   255 section {* Lifted Theorems *}
 
   231 
   256 
   232 thm list.cases (* ??? *)
 
   257 thm list.cases (* ??? *)
 
   233 
   258 
   234 thm cons_left_comm
 
   259 thm cons_left_comm
 
   235 lemma "Insert a (Insert b x) = Insert b (Insert a x)"
 
   260 lemma "finsert a (finsert b S) = finsert b (finsert a S)"
 
   236 by (lifting cons_left_comm)
 
   261 by (lifting cons_left_comm)
 
   237 
   262 
   238 thm cons_left_idem
 
   263 thm cons_left_idem
 
   239 lemma "Insert a (Insert a x) = Insert a x"
 
   264 lemma "finsert a (finsert a S) = finsert a S"
 
   240 by (lifting cons_left_idem)
 
   265 by (lifting cons_left_idem)
 
   241 
   266 
   242 (* thm MEM:
 
   267 (* thm MEM:
 
   243   MEM x [] = F
 
   268   MEM x [] = F
 
   244   MEM x (h::t) = (x=h) \/ MEM x t *)
 
   269   MEM x (h::t) = (x=h) \/ MEM x t *)
 
   246 thm mem_cons
 
   271 thm mem_cons
 
   247 thm finite_set_raw_strong_cases
 
   272 thm finite_set_raw_strong_cases
 
   248 thm card_raw.simps
 
   273 thm card_raw.simps
 
   249 thm not_mem_card_raw
 
   274 thm not_mem_card_raw
 
   250 thm card_raw_suc
 
   275 thm card_raw_suc
 
   251 lemma "Card x = Suc n \<Longrightarrow> (\<exists>a b. \<not> In a b & x = Insert a b)"
 
   276 
   252 by (lifting card_raw_suc)
 
   277 lemma "fcard X = Suc n \<Longrightarrow> (\<exists>a S. a \<notin>f S & X = finsert a S)"
 
       
   278 (*by (lifting card_raw_suc)*)
 
       
   279 sorry
 
   253 
   280 
   254 thm card_raw_cons_gt_0
 
   281 thm card_raw_cons_gt_0
 
   255 thm mem_card_raw_not_0
 
   282 thm mem_card_raw_not_0
 
   256 thm not_nil_equiv_cons
 
   283 thm not_nil_equiv_cons
 
   257 thm delete_raw.simps
 
   284 thm delete_raw.simps
 
   258 thm mem_delete_raw
 
   285 (*thm mem_delete_raw*)
 
   259 thm card_raw_delete_raw
 
   286 thm card_raw_delete_raw
 
   260 thm cons_delete_raw
 
   287 thm cons_delete_raw
 
   261 thm mem_cons_delete_raw
 
   288 thm mem_cons_delete_raw
 
   262 thm finite_set_raw_delete_raw_cases
 
   289 thm finite_set_raw_delete_raw_cases
 
   263 thm append.simps
 
   290 thm append.simps
 
   266 thm mem_inter_raw
 
   293 thm mem_inter_raw
 
   267 thm fold_raw.simps
 
   294 thm fold_raw.simps
 
   268 thm list2set_thm
 
   295 thm list2set_thm
 
   269 thm list_eq_def
 
   296 thm list_eq_def
 
   270 thm list.induct
 
   297 thm list.induct
 
   271 lemma "\<lbrakk>P Empty; \<And>a x. P x \<Longrightarrow> P (Insert a x)\<rbrakk> \<Longrightarrow> P l"
 
   298 lemma "\<lbrakk>P fempty; \<And>a x. P x \<Longrightarrow> P (finsert a x)\<rbrakk> \<Longrightarrow> P l"
 
   272 by (lifting list.induct)
 
   299 by (lifting list.induct)
 
   273 
   300 
   274 (* We also have map and some properties of it in FSet *)
 
   301 (* We also have map and some properties of it in FSet *)
 
   275 (* and the following which still lifts ok *)
 
   302 (* and the following which still lifts ok *)
 
   276 lemma "funion (funion x xa) xb = funion x (funion xa xb)"
 
   303 lemma "funion (funion x xa) xb = funion x (funion xa xb)"
 
   285 lemma list_case_rsp[quot_respect]:
 
   312 lemma list_case_rsp[quot_respect]:
 
   286   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
 
   313   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
 
   287   apply (auto)
 
   314   apply (auto)
 
   288   sorry
 
   315   sorry
 
   289 
   316 
   290 lemma "fset_case (f1::'t) f2 (Insert a xa) = f2 a xa"
 
   317 lemma "fset_case (f1::'t) f2 (finsert a xa) = f2 a xa"
 
   291 apply (lifting list.cases(2))
 
   318 apply (lifting list.cases(2))
 
   292 done
 
   319 done
 
   293 
   320 
   294 
   321 
   295 end
 
   322 end
nominal2