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 732 33cd648df179
parent 729 8d5408322de5
child 734 ac2ed047988d
equal deleted inserted replaced
731:e16523f01908 732:33cd648df179 
    32   "(op = ===> op \<approx> ===> op =) (op mem) (op mem)"
 
    32   "(op = ===> op \<approx> ===> op =) (op mem) (op mem)"
 
    33 *)
 
    33 *)
 
    34 
    34 
    35 
    35 
    36 lemma no_mem_nil: 
    36 lemma no_mem_nil: 
    37   "(\<forall>a. \<not>(a \<in> set A)) = (A = [])"
 
    37   "(\<forall>a. a \<notin> set A) = (A = [])"
 
    38 by (induct A) (auto)
 
    38 by (induct A) (auto)
 
    39 
    39 
    40 lemma none_mem_nil: 
    40 lemma none_mem_nil: 
    41   "(\<forall>a. \<not>(a \<in> set A)) = (A \<approx> [])"
 
    41   "(\<forall>a. a \<notin> set A) = (A \<approx> [])"
 
    42 by simp
 
    42 by simp
 
    43 
    43 
    44 lemma mem_cons: 
    44 lemma mem_cons: 
    45   "a \<in> set A \<Longrightarrow> a # A \<approx> A"
 
    45   "a \<in> set A \<Longrightarrow> a # A \<approx> A"
 
    46 by auto
 
    46 by auto
 
    52 lemma cons_left_idem: 
    52 lemma cons_left_idem: 
    53   "x # x # A \<approx> x # A"
 
    53   "x # x # A \<approx> x # A"
 
    54 by auto
 
    54 by auto
 
    55 
    55 
    56 lemma finite_set_raw_strong_cases:
 
    56 lemma finite_set_raw_strong_cases:
 
    57   "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a mem Y) \<and> (X \<approx> a # Y)))"
 
    57   "(X = []) \<or> (\<exists>a Y. ((a \<notin> set Y) \<and> (X \<approx> a # Y)))"
 
    58   apply (induct X)
 
    58   apply (induct X)
 
       
    59   apply (simp)
 
       
    60   apply (rule disjI2)
 
       
    61   apply (erule disjE)
 
       
    62   apply (rule_tac x="a" in exI)
 
       
    63   apply (rule_tac x="[]" in exI)
 
       
    64   apply (simp)
 
       
    65   apply (erule exE)+
 
       
    66   apply (case_tac "a = aa")
 
       
    67   apply (rule_tac x="a" in exI)
 
       
    68   apply (rule_tac x="Y" in exI)
 
       
    69   apply (simp)
 
       
    70   apply (rule_tac x="aa" in exI)
 
       
    71   apply (rule_tac x="a # Y" in exI)
 
    59   apply (auto)
 
    72   apply (auto)
 
    60   sorry
 
    73   done
 
    61 
    74 
    62 fun
 
    75 fun
 
    63   delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"
 
    76   delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"
 
    64 where
 
    77 where
 
    65   "delete_raw [] x = []"
 
    78   "delete_raw [] x = []"
 
    66 | "delete_raw (a # A) x = (if (a = x) then delete_raw A x else a # (delete_raw A x))"
 
    79 | "delete_raw (a # A) x = (if (a = x) then delete_raw A x else a # (delete_raw A x))"
 
    67 
    80 
    68 (* definitely FALSE
 
       
    69 lemma mem_delete_raw:
 
    81 lemma mem_delete_raw:
 
    70   "x mem (delete_raw A a) = x mem A \<and> \<not>(x = a)"
 
    82   "x \<in> set (delete_raw A a) = (x \<in> set A \<and> \<not>(x = a))"
 
    71 apply(induct A arbitrary: x a)
 
    83   by (induct A arbitrary: x a) (auto)
 
    72 apply(auto)
 
       
    73 sorry
 
       
    74 *)
 
       
    75 
    84 
    76 lemma mem_delete_raw_ident:
 
    85 lemma mem_delete_raw_ident:
 
    77   "\<not>(a \<in> set (delete_raw A a))"
 
    86   "\<not>(a \<in> set (delete_raw A a))"
 
    78 by (induct A) (auto)
 
    87 by (induct A) (auto)
 
    79 
    88 
    86 apply(induct A arbitrary: B a)
 
    95 apply(induct A arbitrary: B a)
 
    87 apply(auto)
 
    96 apply(auto)
 
    88 sorry
 
    97 sorry
 
    89 
    98 
    90 lemma cons_delete_raw:
 
    99 lemma cons_delete_raw:
 
    91   "a # (delete_raw A a) \<approx> (if a mem A then A else (a # A))"
 
   100   "a # (delete_raw A a) \<approx> (if a \<in> set A then A else (a # A))"
 
    92 sorry
 
   101 sorry
 
    93 
   102 
    94 lemma mem_cons_delete_raw:
 
   103 lemma mem_cons_delete_raw:
 
    95     "a mem A \<Longrightarrow> a # (delete_raw A a) \<approx> A"
 
   104     "a \<in> set A \<Longrightarrow> a # (delete_raw A a) \<approx> A"
 
    96 sorry
 
       
    97 
       
    98 lemma finite_set_raw_delete_raw_cases1:
 
       
    99     "X = [] \<or> (\<exists>a. X \<approx> a # delete_raw X a)"
 
       
   100 sorry
 
   105 sorry
 
   101 
   106 
   102 lemma finite_set_raw_delete_raw_cases:
 
   107 lemma finite_set_raw_delete_raw_cases:
 
   103     "X = [] \<or> (\<exists>a. a mem X \<and> X \<approx> a # delete_raw X a)"
 
   108     "X = [] \<or> (\<exists>a. a mem X \<and> X \<approx> a # delete_raw X a)"
 
   104 sorry
 
   109   by (induct X) (auto)
 
   105 
   110 
   106 fun
 
   111 fun
 
   107   card_raw :: "'a list \<Rightarrow> nat"
 
   112   card_raw :: "'a list \<Rightarrow> nat"
 
   108 where
 
   113 where
 
   109   card_raw_nil: "card_raw [] = 0"
 
   114   card_raw_nil: "card_raw [] = 0"
 
   110 | card_raw_cons: "card_raw (x # xs) = (if x mem xs then card_raw xs else Suc (card_raw xs))"
 
   115 | card_raw_cons: "card_raw (x # xs) = (if x \<in> set xs then card_raw xs else Suc (card_raw xs))"
 
   111 
   116 
   112 lemma not_mem_card_raw:
 
   117 lemma not_mem_card_raw:
 
   113   fixes x :: "'a"
 
   118   fixes x :: "'a"
 
   114   fixes xs :: "'a list"
 
   119   fixes xs :: "'a list"
 
   115   shows "(\<not>(x mem xs)) = (card_raw (x # xs) = Suc (card_raw xs))"
 
   120   shows "(\<not>(x mem xs)) = (card_raw (x # xs) = Suc (card_raw xs))"
 
   116   sorry
 
   121   sorry
 
   117 
   122 
   118 lemma card_raw_suc:
 
   123 lemma card_raw_suc:
 
   119   fixes xs :: "'a list"
 
       
   120   fixes n :: "nat"
 
       
   121   assumes c: "card_raw xs = Suc n"
 
   124   assumes c: "card_raw xs = Suc n"
 
   122   shows "\<exists>a ys. \<not>(a mem ys) \<and> xs \<approx> (a # ys)"
 
   125   shows "\<exists>a ys. (a \<notin> set ys) \<and> xs \<approx> (a # ys)"
 
   123   using c
 
   126   using c apply(induct xs)
 
   124 apply(induct xs)
 
   127   apply(simp)
 
   125 (*apply(metis mem_delete_raw)
 
   128   sorry
 
   126 apply(metis mem_delete_raw)
 
   129 
   127 done*)
 
   130 lemma mem_card_raw_gt_0:
 
   128 sorry
 
   131   "a \<in> set A \<Longrightarrow> 0 < card_raw A"
 
   129 
   132   by (induct A) (auto)
 
   130 
       
   131 lemma mem_card_raw_not_0:
 
       
   132   "a mem A \<Longrightarrow> \<not>(card_raw A = 0)"
 
       
   133 sorry
 
       
   134 
   133 
   135 lemma card_raw_cons_gt_0:
 
   134 lemma card_raw_cons_gt_0:
 
   136   "0 < card_raw (a # A)"
 
   135   "0 < card_raw (a # A)"
 
   137 sorry
 
   136   by (induct A) (auto)
 
   138 
   137 
   139 lemma card_raw_delete_raw:
 
   138 lemma card_raw_delete_raw:
 
   140   "card_raw (delete_raw A a) = (if a mem A then card_raw A - 1 else card_raw A)"
 
   139   "card_raw (delete_raw A a) = (if a \<in> set A then card_raw A - 1 else card_raw A)"
 
   141 sorry
 
   140 sorry
 
   142 
   141 
   143 lemma card_raw_rsp_aux:
 
   142 lemma card_raw_rsp_aux:
 
   144   assumes e: "a \<approx> b"
 
   143   assumes e: "a \<approx> b"
 
   145   shows "card_raw a = card_raw b"
 
   144   shows "card_raw a = card_raw b"
 
   149   "(op \<approx> ===> op =) card_raw card_raw"
 
   148   "(op \<approx> ===> op =) card_raw card_raw"
 
   150   by (simp add: card_raw_rsp_aux)
 
   149   by (simp add: card_raw_rsp_aux)
 
   151 
   150 
   152 lemma card_raw_0:
 
   151 lemma card_raw_0:
 
   153   "(card_raw A = 0) = (A = [])"
 
   152   "(card_raw A = 0) = (A = [])"
 
   154 sorry
 
   153   by (induct A) (auto)
 
   155 
   154 
   156 lemma list2set_thm:
 
   155 lemma list2set_thm:
 
   157   shows "set [] = {}"
 
   156   shows "set [] = {}"
 
   158   and "set (h # t) = insert h (set t)"
 
   157   and "set (h # t) = insert h (set t)"
 
   159 sorry
 
   158   by (auto)
 
   160 
   159 
   161 lemma list2set_RSP:
 
   160 lemma list2set_RSP:
 
   162   "A \<approx> B \<Longrightarrow> set A = set B"
 
   161   "A \<approx> B \<Longrightarrow> set A = set B"
 
   163 sorry
 
   162   by auto
 
   164 
   163 
   165 definition
 
   164 definition
 
   166   rsp_fold
 
   165   rsp_fold
 
   167 where
 
   166 where
 
   168   "rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))"
 
   167   "rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))"
 
   234 quotient_def
 
   233 quotient_def
 
   235   "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" 
   234   "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" 
   236   as "delete_raw"
 
   235   as "delete_raw"
 
   237 
   236 
   238 quotient_def
 
   237 quotient_def
 
   239   "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<in>f _" [50, 51] 50)
 
   238   "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<union>f _" [50, 51] 50)
 
   240   as "op @"
 
   239   as "op @"
 
   241 
   240 
   242 quotient_def
 
   241 quotient_def
 
   243   "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70)
 
   242   "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70)
 
   244   as "inter_raw"
 
   243   as "inter_raw"
 
   266 
   265 
   267 (* thm MEM:
 
   266 (* thm MEM:
 
   268   MEM x [] = F
 
   267   MEM x [] = F
 
   269   MEM x (h::t) = (x=h) \/ MEM x t *)
 
   268   MEM x (h::t) = (x=h) \/ MEM x t *)
 
   270 thm none_mem_nil
 
   269 thm none_mem_nil
 
       
   270 (*lemma "(\<forall>a. a \<notin>f A) = (A = fempty)"*)
 
       
   271 
   271 thm mem_cons
 
   272 thm mem_cons
 
   272 thm finite_set_raw_strong_cases
 
   273 thm finite_set_raw_strong_cases
 
   273 thm card_raw.simps
 
   274 thm card_raw.simps
 
   274 thm not_mem_card_raw
 
   275 thm not_mem_card_raw
 
   275 thm card_raw_suc
 
   276 thm card_raw_suc
nominal2