Nominal/FSet.thy
author Christian Urban <urbanc@in.tum.de>
Fri, 15 Oct 2010 16:01:03 +0100
changeset 2537 d73fa7a3e04b
parent 2536 98e84b56543f
child 2538 c9deccd12476
permissions -rw-r--r--
renamed fminus_raw to diff_list
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2084
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
     1
(*  Title:      HOL/Quotient_Examples/FSet.thy
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
     2
    Author:     Cezary Kaliszyk, TU Munich
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
     3
    Author:     Christian Urban, TU Munich
1823
91ba55dba5e0 added header and more tuning
Christian Urban <urbanc@in.tum.de>
parents: 1822
diff changeset
     4
2533
767161329839 further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2532
diff changeset
     5
    Type of finite sets.
1823
91ba55dba5e0 added header and more tuning
Christian Urban <urbanc@in.tum.de>
parents: 1822
diff changeset
     6
*)
2084
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
     7
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     8
theory FSet
2528
9bde8a508594 Partially merging changes from Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2525
diff changeset
     9
imports Quotient_List
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    10
begin
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    11
2533
767161329839 further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2532
diff changeset
    12
text {* Definiton of the list equivalence relation *}
1909
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
    13
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    14
fun
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    15
  list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    16
where
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
    17
  "list_eq xs ys = (set xs = set ys)"
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    18
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    19
lemma list_eq_equivp:
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    20
  shows "equivp list_eq"
1909
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
    21
  unfolding equivp_reflp_symp_transp
1889
6c5b5ec53a0b sub_list definition and respects
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1888
diff changeset
    22
  unfolding reflp_def symp_def transp_def
6c5b5ec53a0b sub_list definition and respects
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1888
diff changeset
    23
  by auto
6c5b5ec53a0b sub_list definition and respects
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1888
diff changeset
    24
2533
767161329839 further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2532
diff changeset
    25
text {* Fset type *}
767161329839 further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2532
diff changeset
    26
1909
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
    27
quotient_type
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
    28
  'a fset = "'a list" / "list_eq"
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
    29
  by (rule list_eq_equivp)
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
    30
2533
767161329839 further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2532
diff changeset
    31
text {* 
767161329839 further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2532
diff changeset
    32
  Definitions of membership, sublist, cardinality,
767161329839 further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2532
diff changeset
    33
  intersection etc over lists
2372
Christian Urban <urbanc@in.tum.de>
parents: 2371
diff changeset
    34
*}
1909
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
    35
1889
6c5b5ec53a0b sub_list definition and respects
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1888
diff changeset
    36
definition
6c5b5ec53a0b sub_list definition and respects
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1888
diff changeset
    37
  memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
6c5b5ec53a0b sub_list definition and respects
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1888
diff changeset
    38
where
6c5b5ec53a0b sub_list definition and respects
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1888
diff changeset
    39
  "memb x xs \<equiv> x \<in> set xs"
6c5b5ec53a0b sub_list definition and respects
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1888
diff changeset
    40
6c5b5ec53a0b sub_list definition and respects
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1888
diff changeset
    41
definition
6c5b5ec53a0b sub_list definition and respects
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1888
diff changeset
    42
  sub_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
6c5b5ec53a0b sub_list definition and respects
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1888
diff changeset
    43
where
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
    44
  "sub_list xs ys \<equiv> set xs \<subseteq> set ys"
1889
6c5b5ec53a0b sub_list definition and respects
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1888
diff changeset
    45
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
    46
definition
2536
98e84b56543f renamed fcard_raw to card_list
Christian Urban <urbanc@in.tum.de>
parents: 2534
diff changeset
    47
  card_list :: "'a list \<Rightarrow> nat"
1909
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
    48
where
2536
98e84b56543f renamed fcard_raw to card_list
Christian Urban <urbanc@in.tum.de>
parents: 2534
diff changeset
    49
  "card_list xs = card (set xs)"
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    50
1909
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
    51
primrec
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
    52
  finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
    53
where
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
    54
  "finter_raw [] ys = []"
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
    55
| "finter_raw (x # xs) ys =
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
    56
    (if x \<in> set ys then x # (finter_raw xs ys) else finter_raw xs ys)"
2084
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
    57
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
    58
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
    59
definition
2537
d73fa7a3e04b renamed fminus_raw to diff_list
Christian Urban <urbanc@in.tum.de>
parents: 2536
diff changeset
    60
  diff_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
2084
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
    61
where
2537
d73fa7a3e04b renamed fminus_raw to diff_list
Christian Urban <urbanc@in.tum.de>
parents: 2536
diff changeset
    62
  "diff_list xs ys \<equiv> [x \<leftarrow> xs. x\<notin>set ys]"
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
    63
1909
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
    64
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
    65
definition
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
    66
  rsp_fold
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
    67
where
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
    68
  "rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))"
1893
464dd13efff6 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1892
diff changeset
    69
1909
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
    70
primrec
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
    71
  ffold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
    72
where
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
    73
  "ffold_raw f z [] = z"
2084
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
    74
| "ffold_raw f z (a # xs) =
1909
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
    75
     (if (rsp_fold f) then
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
    76
       if a \<in> set xs then ffold_raw f z xs
2084
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
    77
       else f a (ffold_raw f z xs)
1909
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
    78
     else z)"
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
    79
2533
767161329839 further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2532
diff changeset
    80
767161329839 further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2532
diff changeset
    81
767161329839 further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2532
diff changeset
    82
lemma set_finter_raw[simp]:
767161329839 further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2532
diff changeset
    83
  shows "set (finter_raw xs ys) = set xs \<inter> set ys"
767161329839 further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2532
diff changeset
    84
  by (induct xs) (auto simp add: memb_def)
767161329839 further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2532
diff changeset
    85
2537
d73fa7a3e04b renamed fminus_raw to diff_list
Christian Urban <urbanc@in.tum.de>
parents: 2536
diff changeset
    86
lemma set_diff_list[simp]: 
d73fa7a3e04b renamed fminus_raw to diff_list
Christian Urban <urbanc@in.tum.de>
parents: 2536
diff changeset
    87
  shows "set (diff_list xs ys) = (set xs - set ys)"
d73fa7a3e04b renamed fminus_raw to diff_list
Christian Urban <urbanc@in.tum.de>
parents: 2536
diff changeset
    88
  by (auto simp add: diff_list_def)
2533
767161329839 further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2532
diff changeset
    89
767161329839 further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2532
diff changeset
    90
767161329839 further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2532
diff changeset
    91
section {* Quotient composition lemmas *}
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
    92
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
    93
lemma list_all2_refl1:
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
    94
  shows "(list_all2 op \<approx>) r r"
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
    95
  by (rule list_all2_refl) (metis equivp_def fset_equivp)
1938
3641d055b260 Further cleaning of proofs in FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1936
diff changeset
    96
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
    97
lemma compose_list_refl:
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
    98
  shows "(list_all2 op \<approx> OOO op \<approx>) r r"
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
    99
proof
2084
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   100
  have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   101
  show "list_all2 op \<approx> r r" by (rule list_all2_refl1)
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   102
  with * show "(op \<approx> OO list_all2 op \<approx>) r r" ..
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   103
qed
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   104
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   105
lemma Quotient_fset_list:
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   106
  shows "Quotient (list_all2 op \<approx>) (map abs_fset) (map rep_fset)"
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   107
  by (fact list_quotient[OF Quotient_fset])
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   108
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   109
lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   110
  unfolding list_eq.simps
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   111
  by (simp only: set_map)
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   112
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   113
lemma quotient_compose_list[quot_thm]:
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   114
  shows  "Quotient ((list_all2 op \<approx>) OOO (op \<approx>))
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   115
    (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   116
  unfolding Quotient_def comp_def
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   117
proof (intro conjI allI)
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   118
  fix a r s
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   119
  show "abs_fset (map abs_fset (map rep_fset (rep_fset a))) = a"
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   120
    by (simp add: abs_o_rep[OF Quotient_fset] Quotient_abs_rep[OF Quotient_fset] map_id)
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   121
  have b: "list_all2 op \<approx> (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   122
    by (rule list_all2_refl1)
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   123
  have c: "(op \<approx> OO list_all2 op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   124
    by (rule, rule equivp_reflp[OF fset_equivp]) (rule b)
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   125
  show "(list_all2 op \<approx> OOO op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   126
    by (rule, rule list_all2_refl1) (rule c)
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   127
  show "(list_all2 op \<approx> OOO op \<approx>) r s = ((list_all2 op \<approx> OOO op \<approx>) r r \<and>
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   128
        (list_all2 op \<approx> OOO op \<approx>) s s \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   129
  proof (intro iffI conjI)
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   130
    show "(list_all2 op \<approx> OOO op \<approx>) r r" by (rule compose_list_refl)
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   131
    show "(list_all2 op \<approx> OOO op \<approx>) s s" by (rule compose_list_refl)
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   132
  next
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   133
    assume a: "(list_all2 op \<approx> OOO op \<approx>) r s"
2084
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   134
    then have b: "map abs_fset r \<approx> map abs_fset s"
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   135
    proof (elim pred_compE)
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   136
      fix b ba
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   137
      assume c: "list_all2 op \<approx> r b"
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   138
      assume d: "b \<approx> ba"
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   139
      assume e: "list_all2 op \<approx> ba s"
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   140
      have f: "map abs_fset r = map abs_fset b"
1938
3641d055b260 Further cleaning of proofs in FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1936
diff changeset
   141
        using Quotient_rel[OF Quotient_fset_list] c by blast
3641d055b260 Further cleaning of proofs in FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1936
diff changeset
   142
      have "map abs_fset ba = map abs_fset s"
3641d055b260 Further cleaning of proofs in FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1936
diff changeset
   143
        using Quotient_rel[OF Quotient_fset_list] e by blast
3641d055b260 Further cleaning of proofs in FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1936
diff changeset
   144
      then have g: "map abs_fset s = map abs_fset ba" by simp
3641d055b260 Further cleaning of proofs in FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1936
diff changeset
   145
      then show "map abs_fset r \<approx> map abs_fset s" using d f map_rel_cong by simp
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   146
    qed
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   147
    then show "abs_fset (map abs_fset r) = abs_fset (map abs_fset s)"
1938
3641d055b260 Further cleaning of proofs in FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1936
diff changeset
   148
      using Quotient_rel[OF Quotient_fset] by blast
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   149
  next
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   150
    assume a: "(list_all2 op \<approx> OOO op \<approx>) r r \<and> (list_all2 op \<approx> OOO op \<approx>) s s
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   151
      \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s)"
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   152
    then have s: "(list_all2 op \<approx> OOO op \<approx>) s s" by simp
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   153
    have d: "map abs_fset r \<approx> map abs_fset s"
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   154
      by (subst Quotient_rel[OF Quotient_fset]) (simp add: a)
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   155
    have b: "map rep_fset (map abs_fset r) \<approx> map rep_fset (map abs_fset s)"
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   156
      by (rule map_rel_cong[OF d])
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   157
    have y: "list_all2 op \<approx> (map rep_fset (map abs_fset s)) s"
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   158
      by (fact rep_abs_rsp_left[OF Quotient_fset_list, OF list_all2_refl1[of s]])
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   159
    have c: "(op \<approx> OO list_all2 op \<approx>) (map rep_fset (map abs_fset r)) s"
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   160
      by (rule pred_compI) (rule b, rule y)
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   161
    have z: "list_all2 op \<approx> r (map rep_fset (map abs_fset r))"
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   162
      by (fact rep_abs_rsp[OF Quotient_fset_list, OF list_all2_refl1[of r]])
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   163
    then show "(list_all2 op \<approx> OOO op \<approx>) r s"
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   164
      using a c pred_compI by simp
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   165
  qed
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   166
qed
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   167
2525
c848f93807b9 deleted some unused lemmas
Christian Urban <urbanc@in.tum.de>
parents: 2524
diff changeset
   168
2532
Christian Urban <urbanc@in.tum.de>
parents: 2531
diff changeset
   169
text {* Respectfulness *}
1893
464dd13efff6 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1892
diff changeset
   170
2187
f9cc69b432ff Name some respectfullness
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2084
diff changeset
   171
lemma append_rsp[quot_respect]:
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   172
  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) append append"
2533
767161329839 further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2532
diff changeset
   173
  by simp
1895
91d67240c9c1 FSet is a semi-lattice
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1893
diff changeset
   174
2525
c848f93807b9 deleted some unused lemmas
Christian Urban <urbanc@in.tum.de>
parents: 2524
diff changeset
   175
lemma sub_list_rsp[quot_respect]:
1909
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   176
  shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   177
  by (auto simp add: sub_list_def)
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   178
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   179
lemma memb_rsp[quot_respect]:
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   180
  shows "(op = ===> op \<approx> ===> op =) memb memb"
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   181
  by (auto simp add: memb_def)
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   182
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   183
lemma nil_rsp[quot_respect]:
2525
c848f93807b9 deleted some unused lemmas
Christian Urban <urbanc@in.tum.de>
parents: 2524
diff changeset
   184
  shows "(op \<approx>) Nil Nil"
1909
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   185
  by simp
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   186
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   187
lemma cons_rsp[quot_respect]:
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   188
  shows "(op = ===> op \<approx> ===> op \<approx>) Cons Cons"
1909
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   189
  by simp
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   190
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   191
lemma map_rsp[quot_respect]:
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   192
  shows "(op = ===> op \<approx> ===> op \<approx>) map map"
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   193
  by auto
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   194
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   195
lemma set_rsp[quot_respect]:
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   196
  "(op \<approx> ===> op =) set set"
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   197
  by auto
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   198
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   199
lemma list_equiv_rsp[quot_respect]:
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   200
  shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   201
  by auto
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   202
2525
c848f93807b9 deleted some unused lemmas
Christian Urban <urbanc@in.tum.de>
parents: 2524
diff changeset
   203
lemma finter_raw_rsp[quot_respect]:
c848f93807b9 deleted some unused lemmas
Christian Urban <urbanc@in.tum.de>
parents: 2524
diff changeset
   204
  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) finter_raw finter_raw"
c848f93807b9 deleted some unused lemmas
Christian Urban <urbanc@in.tum.de>
parents: 2524
diff changeset
   205
  by simp
c848f93807b9 deleted some unused lemmas
Christian Urban <urbanc@in.tum.de>
parents: 2524
diff changeset
   206
c848f93807b9 deleted some unused lemmas
Christian Urban <urbanc@in.tum.de>
parents: 2524
diff changeset
   207
lemma removeAll_rsp[quot_respect]:
c848f93807b9 deleted some unused lemmas
Christian Urban <urbanc@in.tum.de>
parents: 2524
diff changeset
   208
  shows "(op = ===> op \<approx> ===> op \<approx>) removeAll removeAll"
c848f93807b9 deleted some unused lemmas
Christian Urban <urbanc@in.tum.de>
parents: 2524
diff changeset
   209
  by simp
c848f93807b9 deleted some unused lemmas
Christian Urban <urbanc@in.tum.de>
parents: 2524
diff changeset
   210
2537
d73fa7a3e04b renamed fminus_raw to diff_list
Christian Urban <urbanc@in.tum.de>
parents: 2536
diff changeset
   211
lemma diff_list_rsp[quot_respect]:
d73fa7a3e04b renamed fminus_raw to diff_list
Christian Urban <urbanc@in.tum.de>
parents: 2536
diff changeset
   212
  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) diff_list diff_list"
2525
c848f93807b9 deleted some unused lemmas
Christian Urban <urbanc@in.tum.de>
parents: 2524
diff changeset
   213
  by simp
c848f93807b9 deleted some unused lemmas
Christian Urban <urbanc@in.tum.de>
parents: 2524
diff changeset
   214
2536
98e84b56543f renamed fcard_raw to card_list
Christian Urban <urbanc@in.tum.de>
parents: 2534
diff changeset
   215
lemma card_list_rsp[quot_respect]:
98e84b56543f renamed fcard_raw to card_list
Christian Urban <urbanc@in.tum.de>
parents: 2534
diff changeset
   216
  shows "(op \<approx> ===> op =) card_list card_list"
98e84b56543f renamed fcard_raw to card_list
Christian Urban <urbanc@in.tum.de>
parents: 2534
diff changeset
   217
  by (simp add: card_list_def)
2525
c848f93807b9 deleted some unused lemmas
Christian Urban <urbanc@in.tum.de>
parents: 2524
diff changeset
   218
c848f93807b9 deleted some unused lemmas
Christian Urban <urbanc@in.tum.de>
parents: 2524
diff changeset
   219
c848f93807b9 deleted some unused lemmas
Christian Urban <urbanc@in.tum.de>
parents: 2524
diff changeset
   220
1909
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   221
lemma memb_commute_ffold_raw:
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   222
  "rsp_fold f \<Longrightarrow> h \<in> set b \<Longrightarrow> ffold_raw f z b = f h (ffold_raw f z (removeAll h b))"
1909
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   223
  apply (induct b)
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   224
  apply (auto simp add: rsp_fold_def)
1909
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   225
  done
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   226
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   227
lemma ffold_raw_rsp_pre:
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   228
  "set a = set b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b"
1909
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   229
  apply (induct a arbitrary: b)
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   230
  apply (simp)
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   231
  apply (simp (no_asm_use))
1909
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   232
  apply (rule conjI)
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   233
  apply (rule_tac [!] impI)
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   234
  apply (rule_tac [!] conjI)
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   235
  apply (rule_tac [!] impI)
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   236
  apply (metis insert_absorb)
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   237
  apply (metis List.insert_def List.set.simps(2) List.set_insert ffold_raw.simps(2))
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   238
  apply (metis Diff_insert_absorb insertI1 memb_commute_ffold_raw set_removeAll)
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   239
  apply(drule_tac x="removeAll a1 b" in meta_spec)
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   240
  apply(auto)
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   241
  apply(drule meta_mp)
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   242
  apply(blast)
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   243
  by (metis List.set.simps(2) emptyE ffold_raw.simps(2) in_listsp_conv_set listsp.simps mem_def)
1909
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   244
2525
c848f93807b9 deleted some unused lemmas
Christian Urban <urbanc@in.tum.de>
parents: 2524
diff changeset
   245
lemma ffold_raw_rsp[quot_respect]:
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   246
  shows "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw"
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   247
  unfolding fun_rel_def
2529
775d0bfd99fd Synchronizing FSet further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2528
diff changeset
   248
  by(auto intro: ffold_raw_rsp_pre)
1909
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   249
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   250
lemma concat_rsp_pre:
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   251
  assumes a: "list_all2 op \<approx> x x'"
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   252
  and     b: "x' \<approx> y'"
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   253
  and     c: "list_all2 op \<approx> y' y"
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   254
  and     d: "\<exists>x\<in>set x. xa \<in> set x"
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   255
  shows "\<exists>x\<in>set y. xa \<in> set x"
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   256
proof -
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   257
  obtain xb where e: "xb \<in> set x" and f: "xa \<in> set xb" using d by auto
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   258
  have "\<exists>y. y \<in> set x' \<and> xb \<approx> y" by (rule list_all2_find_element[OF e a])
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   259
  then obtain ya where h: "ya \<in> set x'" and i: "xb \<approx> ya" by auto
2084
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   260
  have "ya \<in> set y'" using b h by simp
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   261
  then have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" using c by (rule list_all2_find_element)
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   262
  then show ?thesis using f i by auto
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   263
qed
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   264
2187
f9cc69b432ff Name some respectfullness
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2084
diff changeset
   265
lemma concat_rsp[quot_respect]:
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   266
  shows "(list_all2 op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   267
proof (rule fun_relI, elim pred_compE)
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   268
  fix a b ba bb
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   269
  assume a: "list_all2 op \<approx> a ba"
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   270
  assume b: "ba \<approx> bb"
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   271
  assume c: "list_all2 op \<approx> bb b"
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   272
  have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" 
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   273
  proof
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   274
    fix x
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   275
    show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" 
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   276
    proof
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   277
      assume d: "\<exists>xa\<in>set a. x \<in> set xa"
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   278
      show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d])
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   279
    next
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   280
      assume e: "\<exists>xa\<in>set b. x \<in> set xa"
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   281
      have a': "list_all2 op \<approx> ba a" by (rule list_all2_symp[OF list_eq_equivp, OF a])
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   282
      have b': "bb \<approx> ba" by (rule equivp_symp[OF list_eq_equivp, OF b])
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   283
      have c': "list_all2 op \<approx> b bb" by (rule list_all2_symp[OF list_eq_equivp, OF c])
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   284
      show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e])
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   285
    qed
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   286
  qed
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   287
  then show "concat a \<approx> concat b" by auto
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   288
qed
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   289
2084
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   290
lemma [quot_respect]:
2532
Christian Urban <urbanc@in.tum.de>
parents: 2531
diff changeset
   291
  shows "(op = ===> op \<approx> ===> op \<approx>) filter filter"
2084
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   292
  by auto
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   293
1905
dbc9e88c44da fsets are distributive lattices.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1895
diff changeset
   294
2528
9bde8a508594 Partially merging changes from Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2525
diff changeset
   295
instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}"
1893
464dd13efff6 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1892
diff changeset
   296
begin
464dd13efff6 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1892
diff changeset
   297
464dd13efff6 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1892
diff changeset
   298
quotient_definition
464dd13efff6 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1892
diff changeset
   299
  "bot :: 'a fset" is "[] :: 'a list"
464dd13efff6 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1892
diff changeset
   300
464dd13efff6 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1892
diff changeset
   301
abbreviation
464dd13efff6 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1892
diff changeset
   302
  fempty  ("{||}")
464dd13efff6 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1892
diff changeset
   303
where
464dd13efff6 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1892
diff changeset
   304
  "{||} \<equiv> bot :: 'a fset"
464dd13efff6 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1892
diff changeset
   305
464dd13efff6 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1892
diff changeset
   306
quotient_definition
464dd13efff6 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1892
diff changeset
   307
  "less_eq_fset \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> bool)"
464dd13efff6 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1892
diff changeset
   308
is
464dd13efff6 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1892
diff changeset
   309
  "sub_list \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> bool)"
464dd13efff6 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1892
diff changeset
   310
464dd13efff6 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1892
diff changeset
   311
abbreviation
464dd13efff6 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1892
diff changeset
   312
  f_subset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subseteq>|" 50)
464dd13efff6 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1892
diff changeset
   313
where
464dd13efff6 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1892
diff changeset
   314
  "xs |\<subseteq>| ys \<equiv> xs \<le> ys"
464dd13efff6 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1892
diff changeset
   315
464dd13efff6 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1892
diff changeset
   316
definition
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   317
  less_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool"
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   318
where  
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   319
  "xs < ys \<equiv> xs \<le> ys \<and> xs \<noteq> (ys::'a fset)"
1893
464dd13efff6 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1892
diff changeset
   320
464dd13efff6 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1892
diff changeset
   321
abbreviation
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   322
  fsubset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subset>|" 50)
1893
464dd13efff6 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1892
diff changeset
   323
where
464dd13efff6 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1892
diff changeset
   324
  "xs |\<subset>| ys \<equiv> xs < ys"
464dd13efff6 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1892
diff changeset
   325
1895
91d67240c9c1 FSet is a semi-lattice
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1893
diff changeset
   326
quotient_definition
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   327
  "sup :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
1895
91d67240c9c1 FSet is a semi-lattice
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1893
diff changeset
   328
is
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   329
  "append :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
1895
91d67240c9c1 FSet is a semi-lattice
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1893
diff changeset
   330
91d67240c9c1 FSet is a semi-lattice
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1893
diff changeset
   331
abbreviation
2084
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   332
  funion (infixl "|\<union>|" 65)
1895
91d67240c9c1 FSet is a semi-lattice
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1893
diff changeset
   333
where
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   334
  "xs |\<union>| ys \<equiv> sup xs (ys::'a fset)"
1895
91d67240c9c1 FSet is a semi-lattice
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1893
diff changeset
   335
1905
dbc9e88c44da fsets are distributive lattices.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1895
diff changeset
   336
quotient_definition
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   337
  "inf :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
1905
dbc9e88c44da fsets are distributive lattices.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1895
diff changeset
   338
is
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   339
  "finter_raw :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
1905
dbc9e88c44da fsets are distributive lattices.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1895
diff changeset
   340
dbc9e88c44da fsets are distributive lattices.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1895
diff changeset
   341
abbreviation
dbc9e88c44da fsets are distributive lattices.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1895
diff changeset
   342
  finter (infixl "|\<inter>|" 65)
dbc9e88c44da fsets are distributive lattices.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1895
diff changeset
   343
where
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   344
  "xs |\<inter>| ys \<equiv> inf xs (ys::'a fset)"
1905
dbc9e88c44da fsets are distributive lattices.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1895
diff changeset
   345
2084
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   346
quotient_definition
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   347
  "minus :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
2084
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   348
is
2537
d73fa7a3e04b renamed fminus_raw to diff_list
Christian Urban <urbanc@in.tum.de>
parents: 2536
diff changeset
   349
  "diff_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
2084
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   350
2533
767161329839 further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2532
diff changeset
   351
lemma append_finter_raw_distrib:
767161329839 further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2532
diff changeset
   352
  "x @ (finter_raw y z) \<approx> finter_raw (x @ y) (x @ z)"
767161329839 further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2532
diff changeset
   353
  apply (induct x)
767161329839 further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2532
diff changeset
   354
  apply (auto)
767161329839 further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2532
diff changeset
   355
  done
767161329839 further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2532
diff changeset
   356
1895
91d67240c9c1 FSet is a semi-lattice
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1893
diff changeset
   357
instance
91d67240c9c1 FSet is a semi-lattice
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1893
diff changeset
   358
proof
1905
dbc9e88c44da fsets are distributive lattices.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1895
diff changeset
   359
  fix x y z :: "'a fset"
2528
9bde8a508594 Partially merging changes from Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2525
diff changeset
   360
  show "x |\<subset>| y \<longleftrightarrow> x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x"
2530
3b8741ecfda3 FSet synchronizing
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2529
diff changeset
   361
    unfolding less_fset_def 
3b8741ecfda3 FSet synchronizing
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2529
diff changeset
   362
    by (descending) (auto simp add: sub_list_def)
2528
9bde8a508594 Partially merging changes from Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2525
diff changeset
   363
  show "x |\<subseteq>| x"  by (descending) (simp add: sub_list_def)
9bde8a508594 Partially merging changes from Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2525
diff changeset
   364
  show "{||} |\<subseteq>| x" by (descending) (simp add: sub_list_def)
9bde8a508594 Partially merging changes from Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2525
diff changeset
   365
  show "x |\<subseteq>| x |\<union>| y" by (descending) (simp add: sub_list_def)
9bde8a508594 Partially merging changes from Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2525
diff changeset
   366
  show "y |\<subseteq>| x |\<union>| y" by (descending) (simp add: sub_list_def)
9bde8a508594 Partially merging changes from Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2525
diff changeset
   367
  show "x |\<inter>| y |\<subseteq>| x"
9bde8a508594 Partially merging changes from Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2525
diff changeset
   368
    by (descending) (simp add: sub_list_def memb_def[symmetric])
9bde8a508594 Partially merging changes from Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2525
diff changeset
   369
  show "x |\<inter>| y |\<subseteq>| y" 
9bde8a508594 Partially merging changes from Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2525
diff changeset
   370
    by (descending) (simp add: sub_list_def memb_def[symmetric])
9bde8a508594 Partially merging changes from Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2525
diff changeset
   371
  show "x |\<union>| (y |\<inter>| z) = x |\<union>| y |\<inter>| (x |\<union>| z)" 
2533
767161329839 further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2532
diff changeset
   372
    by (descending) (rule append_finter_raw_distrib)
1905
dbc9e88c44da fsets are distributive lattices.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1895
diff changeset
   373
next
dbc9e88c44da fsets are distributive lattices.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1895
diff changeset
   374
  fix x y z :: "'a fset"
dbc9e88c44da fsets are distributive lattices.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1895
diff changeset
   375
  assume a: "x |\<subseteq>| y"
dbc9e88c44da fsets are distributive lattices.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1895
diff changeset
   376
  assume b: "y |\<subseteq>| z"
2528
9bde8a508594 Partially merging changes from Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2525
diff changeset
   377
  show "x |\<subseteq>| z" using a b 
9bde8a508594 Partially merging changes from Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2525
diff changeset
   378
    by (descending) (simp add: sub_list_def)
1895
91d67240c9c1 FSet is a semi-lattice
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1893
diff changeset
   379
next
91d67240c9c1 FSet is a semi-lattice
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1893
diff changeset
   380
  fix x y :: "'a fset"
91d67240c9c1 FSet is a semi-lattice
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1893
diff changeset
   381
  assume a: "x |\<subseteq>| y"
91d67240c9c1 FSet is a semi-lattice
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1893
diff changeset
   382
  assume b: "y |\<subseteq>| x"
2528
9bde8a508594 Partially merging changes from Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2525
diff changeset
   383
  show "x = y" using a b 
9bde8a508594 Partially merging changes from Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2525
diff changeset
   384
    by (descending) (unfold sub_list_def list_eq.simps, blast)
1895
91d67240c9c1 FSet is a semi-lattice
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1893
diff changeset
   385
next
91d67240c9c1 FSet is a semi-lattice
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1893
diff changeset
   386
  fix x y z :: "'a fset"
91d67240c9c1 FSet is a semi-lattice
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1893
diff changeset
   387
  assume a: "y |\<subseteq>| x"
91d67240c9c1 FSet is a semi-lattice
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1893
diff changeset
   388
  assume b: "z |\<subseteq>| x"
2528
9bde8a508594 Partially merging changes from Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2525
diff changeset
   389
  show "y |\<union>| z |\<subseteq>| x" using a b 
9bde8a508594 Partially merging changes from Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2525
diff changeset
   390
    by (descending) (simp add: sub_list_def)
1905
dbc9e88c44da fsets are distributive lattices.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1895
diff changeset
   391
next
dbc9e88c44da fsets are distributive lattices.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1895
diff changeset
   392
  fix x y z :: "'a fset"
dbc9e88c44da fsets are distributive lattices.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1895
diff changeset
   393
  assume a: "x |\<subseteq>| y"
dbc9e88c44da fsets are distributive lattices.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1895
diff changeset
   394
  assume b: "x |\<subseteq>| z"
2528
9bde8a508594 Partially merging changes from Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2525
diff changeset
   395
  show "x |\<subseteq>| y |\<inter>| z" using a b 
9bde8a508594 Partially merging changes from Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2525
diff changeset
   396
    by (descending) (simp add: sub_list_def memb_def[symmetric])
1895
91d67240c9c1 FSet is a semi-lattice
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1893
diff changeset
   397
qed
1905
dbc9e88c44da fsets are distributive lattices.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1895
diff changeset
   398
1893
464dd13efff6 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1892
diff changeset
   399
end
464dd13efff6 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1892
diff changeset
   400
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   401
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   402
section {* Definitions for fsets *}
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   403
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   404
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   405
quotient_definition
1893
464dd13efff6 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1892
diff changeset
   406
  "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   407
  is "Cons"
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   408
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   409
syntax
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   410
  "@Finset"     :: "args => 'a fset"  ("{|(_)|}")
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   411
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   412
translations
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   413
  "{|x, xs|}" == "CONST finsert x {|xs|}"
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   414
  "{|x|}"     == "CONST finsert x {||}"
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   415
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   416
quotient_definition
1938
3641d055b260 Further cleaning of proofs in FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1936
diff changeset
   417
  fin (infix "|\<in>|" 50)
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   418
where
1816
56cebe7f8e24 some small tunings (incompleted work in Lambda.thy)
Christian Urban <urbanc@in.tum.de>
parents: 1682
diff changeset
   419
  "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" is "memb"
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   420
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   421
abbreviation
1938
3641d055b260 Further cleaning of proofs in FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1936
diff changeset
   422
  fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50)
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   423
where
1860
d3fe17786640 some tuning of proofs
Christian Urban <urbanc@in.tum.de>
parents: 1826
diff changeset
   424
  "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   425
2084
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   426
section {* Other constants on the Quotient Type *}
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   427
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   428
quotient_definition
2084
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   429
  "fcard :: 'a fset \<Rightarrow> nat"
2536
98e84b56543f renamed fcard_raw to card_list
Christian Urban <urbanc@in.tum.de>
parents: 2534
diff changeset
   430
  is card_list
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   431
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   432
quotient_definition
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   433
  "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   434
  is map
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   435
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   436
quotient_definition
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   437
  "fdelete :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   438
  is removeAll
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   439
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   440
quotient_definition
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   441
  "fset :: 'a fset \<Rightarrow> 'a set"
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   442
  is "set"
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   443
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   444
quotient_definition
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   445
  "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   446
  is ffold_raw
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   447
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   448
quotient_definition
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   449
  "fconcat :: ('a fset) fset \<Rightarrow> 'a fset"
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   450
  is concat
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   451
2084
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   452
quotient_definition
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   453
  "ffilter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   454
  is filter
2084
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   455
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   456
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   457
subsection {* Compositional Respectfulness and Preservation *}
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   458
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   459
lemma [quot_respect]: "(list_all2 op \<approx> OOO op \<approx>) [] []"
1938
3641d055b260 Further cleaning of proofs in FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1936
diff changeset
   460
  by (fact compose_list_refl)
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   461
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   462
lemma [quot_preserve]: "(abs_fset \<circ> map f) [] = abs_fset []"
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   463
  by simp
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   464
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   465
lemma [quot_respect]:
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   466
  shows "(op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) Cons Cons"
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   467
  apply auto
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   468
  apply (rule_tac b="x # b" in pred_compI)
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   469
  apply auto
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   470
  apply (rule_tac b="x # ba" in pred_compI)
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   471
  apply auto
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   472
  done
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   473
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   474
lemma [quot_preserve]:
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   475
  "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = finsert"
2479
a9b6a00b1ba0 updated to Isabelle Sept 16
Christian Urban <urbanc@in.tum.de>
parents: 2378
diff changeset
   476
  by (simp add: fun_eq_iff Quotient_abs_rep[OF Quotient_fset]
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   477
      abs_o_rep[OF Quotient_fset] map_id finsert_def)
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   478
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   479
lemma [quot_preserve]:
1938
3641d055b260 Further cleaning of proofs in FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1936
diff changeset
   480
  "((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op @ = funion"
2479
a9b6a00b1ba0 updated to Isabelle Sept 16
Christian Urban <urbanc@in.tum.de>
parents: 2378
diff changeset
   481
  by (simp add: fun_eq_iff Quotient_abs_rep[OF Quotient_fset]
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   482
      abs_o_rep[OF Quotient_fset] map_id sup_fset_def)
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   483
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   484
lemma list_all2_app_l:
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   485
  assumes a: "reflp R"
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   486
  and b: "list_all2 R l r"
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   487
  shows "list_all2 R (z @ l) (z @ r)"
1938
3641d055b260 Further cleaning of proofs in FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1936
diff changeset
   488
  by (induct z) (simp_all add: b rev_iffD1[OF a meta_eq_to_obj_eq[OF reflp_def]])
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   489
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   490
lemma append_rsp2_pre0:
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   491
  assumes a:"list_all2 op \<approx> x x'"
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   492
  shows "list_all2 op \<approx> (x @ z) (x' @ z)"
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   493
  using a apply (induct x x' rule: list_induct2')
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   494
  by simp_all (rule list_all2_refl1)
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   495
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   496
lemma append_rsp2_pre1:
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   497
  assumes a:"list_all2 op \<approx> x x'"
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   498
  shows "list_all2 op \<approx> (z @ x) (z @ x')"
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   499
  using a apply (induct x x' arbitrary: z rule: list_induct2')
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   500
  apply (rule list_all2_refl1)
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   501
  apply (simp_all del: list_eq.simps)
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   502
  apply (rule list_all2_app_l)
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   503
  apply (simp_all add: reflp_def)
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   504
  done
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   505
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   506
lemma append_rsp2_pre:
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   507
  assumes a:"list_all2 op \<approx> x x'"
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   508
  and     b: "list_all2 op \<approx> z z'"
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   509
  shows "list_all2 op \<approx> (x @ z) (x' @ z')"
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   510
  apply (rule list_all2_transp[OF fset_equivp])
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   511
  apply (rule append_rsp2_pre0)
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   512
  apply (rule a)
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   513
  using b apply (induct z z' rule: list_induct2')
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   514
  apply (simp_all only: append_Nil2)
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   515
  apply (rule list_all2_refl1)
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   516
  apply simp_all
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   517
  apply (rule append_rsp2_pre1)
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   518
  apply simp
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   519
  done
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   520
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   521
lemma [quot_respect]:
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   522
  "(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) op @ op @"
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   523
proof (intro fun_relI, elim pred_compE)
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   524
  fix x y z w x' z' y' w' :: "'a list list"
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   525
  assume a:"list_all2 op \<approx> x x'"
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   526
  and b:    "x' \<approx> y'"
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   527
  and c:    "list_all2 op \<approx> y' y"
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   528
  assume aa: "list_all2 op \<approx> z z'"
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   529
  and bb:   "z' \<approx> w'"
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   530
  and cc:   "list_all2 op \<approx> w' w"
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   531
  have a': "list_all2 op \<approx> (x @ z) (x' @ z')" using a aa append_rsp2_pre by auto
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   532
  have b': "x' @ z' \<approx> y' @ w'" using b bb by simp
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   533
  have c': "list_all2 op \<approx> (y' @ w') (y @ w)" using c cc append_rsp2_pre by auto
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   534
  have d': "(op \<approx> OO list_all2 op \<approx>) (x' @ z') (y @ w)"
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   535
    by (rule pred_compI) (rule b', rule c')
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
   536
  show "(list_all2 op \<approx> OOO op \<approx>) (x @ z) (y @ w)"
1935
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   537
    by (rule pred_compI) (rule a', rule d')
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   538
qed
266abc3ee228 Moved working Fset3 properties to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1927
diff changeset
   539
1878
c22947214948 2 more lifted lemmas needed for second representation
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1860
diff changeset
   540
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   541
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   542
section {* Cases *}
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   543
1819
63dd459dbc0d Much more in FSet (currently non-working)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1817
diff changeset
   544
63dd459dbc0d Much more in FSet (currently non-working)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1817
diff changeset
   545
lemma fset_raw_strong_cases:
2084
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   546
  obtains "xs = []"
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   547
    | x ys where "\<not> memb x ys" and "xs \<approx> x # ys"
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   548
proof (induct xs arbitrary: x ys)
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   549
  case Nil
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   550
  then show thesis by simp
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   551
next
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   552
  case (Cons a xs)
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   553
  have a: "\<lbrakk>xs = [] \<Longrightarrow> thesis; \<And>x ys. \<lbrakk>\<not> memb x ys; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis" by fact
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   554
  have b: "\<And>x' ys'. \<lbrakk>\<not> memb x' ys'; a # xs \<approx> x' # ys'\<rbrakk> \<Longrightarrow> thesis" by fact
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   555
  have c: "xs = [] \<Longrightarrow> thesis" using b unfolding memb_def
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   556
    by (metis in_set_conv_nth less_zeroE list.size(3) list_eq.simps member_set)
2084
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   557
  have "\<And>x ys. \<lbrakk>\<not> memb x ys; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis"
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   558
  proof -
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   559
    fix x :: 'a
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   560
    fix ys :: "'a list"
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   561
    assume d:"\<not> memb x ys"
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   562
    assume e:"xs \<approx> x # ys"
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   563
    show thesis
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   564
    proof (cases "x = a")
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   565
      assume h: "x = a"
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   566
      then have f: "\<not> memb a ys" using d by simp
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   567
      have g: "a # xs \<approx> a # ys" using e h by auto
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   568
      show thesis using b f g by simp
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   569
    next
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   570
      assume h: "x \<noteq> a"
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   571
      then have f: "\<not> memb x (a # ys)" using d unfolding memb_def by auto
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   572
      have g: "a # xs \<approx> x # (a # ys)" using e h by auto
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   573
      show thesis using b f g by simp
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   574
    qed
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   575
  qed
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   576
  then show thesis using a c by blast
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   577
qed
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   578
1533
5f5e99a11f66 A few more theorems in FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1518
diff changeset
   579
1888
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   580
text {* alternate formulation with a different decomposition principle
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   581
  and a proof of equivalence *}
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   582
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   583
inductive
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   584
  list_eq2
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   585
where
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   586
  "list_eq2 (a # b # xs) (b # a # xs)"
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   587
| "list_eq2 [] []"
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   588
| "list_eq2 xs ys \<Longrightarrow> list_eq2 ys xs"
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   589
| "list_eq2 (a # a # xs) (a # xs)"
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   590
| "list_eq2 xs ys \<Longrightarrow> list_eq2 (a # xs) (a # ys)"
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   591
| "\<lbrakk>list_eq2 xs1 xs2; list_eq2 xs2 xs3\<rbrakk> \<Longrightarrow> list_eq2 xs1 xs3"
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   592
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   593
lemma list_eq2_refl:
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   594
  shows "list_eq2 xs xs"
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   595
  by (induct xs) (auto intro: list_eq2.intros)
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   596
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   597
lemma cons_delete_list_eq2:
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   598
  shows "list_eq2 (a # (removeAll a A)) (if memb a A then A else a # A)"
1888
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   599
  apply (induct A)
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   600
  apply (simp add: memb_def list_eq2_refl)
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   601
  apply (case_tac "memb a (aa # A)")
2533
767161329839 further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2532
diff changeset
   602
  apply (simp_all only: memb_def)
1888
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   603
  apply (case_tac [!] "a = aa")
1909
9972dc5bd7ad Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1907
diff changeset
   604
  apply (simp_all)
1888
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   605
  apply (case_tac "memb a A")
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   606
  apply (auto simp add: memb_def)[2]
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   607
  apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6))
1895
91d67240c9c1 FSet is a semi-lattice
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1893
diff changeset
   608
  apply (metis list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6))
2525
c848f93807b9 deleted some unused lemmas
Christian Urban <urbanc@in.tum.de>
parents: 2524
diff changeset
   609
  apply (auto simp add: list_eq2_refl memb_def)
1888
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   610
  done
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   611
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   612
lemma memb_delete_list_eq2:
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   613
  assumes a: "memb e r"
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   614
  shows "list_eq2 (e # removeAll e r) r"
1888
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   615
  using a cons_delete_list_eq2[of e r]
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   616
  by simp
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   617
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   618
lemma list_eq2_equiv:
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   619
  "(l \<approx> r) \<longleftrightarrow> (list_eq2 l r)"
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   620
proof
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   621
  show "list_eq2 l r \<Longrightarrow> l \<approx> r" by (induct rule: list_eq2.induct) auto
1938
3641d055b260 Further cleaning of proofs in FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1936
diff changeset
   622
next
3641d055b260 Further cleaning of proofs in FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1936
diff changeset
   623
  {
3641d055b260 Further cleaning of proofs in FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1936
diff changeset
   624
    fix n
2536
98e84b56543f renamed fcard_raw to card_list
Christian Urban <urbanc@in.tum.de>
parents: 2534
diff changeset
   625
    assume a: "card_list l = n" and b: "l \<approx> r"
1938
3641d055b260 Further cleaning of proofs in FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1936
diff changeset
   626
    have "list_eq2 l r"
3641d055b260 Further cleaning of proofs in FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1936
diff changeset
   627
      using a b
3641d055b260 Further cleaning of proofs in FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1936
diff changeset
   628
    proof (induct n arbitrary: l r)
3641d055b260 Further cleaning of proofs in FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1936
diff changeset
   629
      case 0
2536
98e84b56543f renamed fcard_raw to card_list
Christian Urban <urbanc@in.tum.de>
parents: 2534
diff changeset
   630
      have "card_list l = 0" by fact
98e84b56543f renamed fcard_raw to card_list
Christian Urban <urbanc@in.tum.de>
parents: 2534
diff changeset
   631
      then have "\<forall>x. \<not> memb x l" unfolding card_list_def memb_def by auto
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   632
      then have z: "l = []" unfolding memb_def by auto
1938
3641d055b260 Further cleaning of proofs in FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1936
diff changeset
   633
      then have "r = []" using `l \<approx> r` by simp
3641d055b260 Further cleaning of proofs in FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1936
diff changeset
   634
      then show ?case using z list_eq2_refl by simp
3641d055b260 Further cleaning of proofs in FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1936
diff changeset
   635
    next
3641d055b260 Further cleaning of proofs in FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1936
diff changeset
   636
      case (Suc m)
3641d055b260 Further cleaning of proofs in FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1936
diff changeset
   637
      have b: "l \<approx> r" by fact
2536
98e84b56543f renamed fcard_raw to card_list
Christian Urban <urbanc@in.tum.de>
parents: 2534
diff changeset
   638
      have d: "card_list l = Suc m" by fact
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   639
      then have "\<exists>a. memb a l" 
2536
98e84b56543f renamed fcard_raw to card_list
Christian Urban <urbanc@in.tum.de>
parents: 2534
diff changeset
   640
	apply(simp add: card_list_def memb_def)
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   641
	apply(drule card_eq_SucD)
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   642
	apply(blast)
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   643
	done
1938
3641d055b260 Further cleaning of proofs in FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1936
diff changeset
   644
      then obtain a where e: "memb a l" by auto
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   645
      then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b 
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   646
	unfolding memb_def by auto
2536
98e84b56543f renamed fcard_raw to card_list
Christian Urban <urbanc@in.tum.de>
parents: 2534
diff changeset
   647
      have f: "card_list (removeAll a l) = m" using e d by (simp add: card_list_def memb_def)
2525
c848f93807b9 deleted some unused lemmas
Christian Urban <urbanc@in.tum.de>
parents: 2524
diff changeset
   648
      have g: "removeAll a l \<approx> removeAll a r" using removeAll_rsp b by simp
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   649
      have "list_eq2 (removeAll a l) (removeAll a r)" by (rule Suc.hyps[OF f g])
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   650
      then have h: "list_eq2 (a # removeAll a l) (a # removeAll a r)" by (rule list_eq2.intros(5))
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   651
      have i: "list_eq2 l (a # removeAll a l)"
1938
3641d055b260 Further cleaning of proofs in FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1936
diff changeset
   652
        by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]])
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   653
      have "list_eq2 l (a # removeAll a r)" by (rule list_eq2.intros(6)[OF i h])
1938
3641d055b260 Further cleaning of proofs in FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1936
diff changeset
   654
      then show ?case using list_eq2.intros(6)[OF _ memb_delete_list_eq2[OF e']] by simp
3641d055b260 Further cleaning of proofs in FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1936
diff changeset
   655
    qed
3641d055b260 Further cleaning of proofs in FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1936
diff changeset
   656
    }
3641d055b260 Further cleaning of proofs in FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1936
diff changeset
   657
  then show "l \<approx> r \<Longrightarrow> list_eq2 l r" by blast
1888
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   658
qed
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
   659
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   660
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   661
section {* Lifted theorems *}
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   662
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   663
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   664
subsection {* fin *}
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   665
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   666
lemma not_fin_fnil: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   667
  shows "x |\<notin>| {||}"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   668
  by (descending) (simp add: memb_def)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   669
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   670
lemma fin_set: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   671
  shows "x |\<in>| S \<longleftrightarrow> x \<in> fset S"
2529
775d0bfd99fd Synchronizing FSet further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2528
diff changeset
   672
  by (descending) (simp add: memb_def)
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   673
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   674
lemma fnotin_set: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   675
  shows "x |\<notin>| S \<longleftrightarrow> x \<notin> fset S"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   676
  by (descending) (simp add: memb_def)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   677
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   678
lemma fset_eq_iff:
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   679
  shows "S = T \<longleftrightarrow> (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   680
  by (descending) (auto simp add: memb_def)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   681
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   682
lemma none_fin_fempty:
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   683
  shows "(\<forall>x. x |\<notin>| S) \<longleftrightarrow> S = {||}"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   684
  by (descending) (simp add: memb_def)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   685
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   686
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   687
subsection {* finsert *}
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   688
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   689
lemma fin_finsert_iff[simp]:
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   690
  shows "x |\<in>| finsert y S \<longleftrightarrow> x = y \<or> x |\<in>| S"
2528
9bde8a508594 Partially merging changes from Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2525
diff changeset
   691
  by (descending) (simp add: memb_def)
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   692
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   693
lemma
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   694
  shows finsertI1: "x |\<in>| finsert x S"
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   695
  and   finsertI2: "x |\<in>| S \<Longrightarrow> x |\<in>| finsert y S"
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   696
  by (descending, simp add: memb_def)+
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   697
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   698
lemma finsert_absorb[simp]:
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   699
  shows "x |\<in>| S \<Longrightarrow> finsert x S = S"
2528
9bde8a508594 Partially merging changes from Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2525
diff changeset
   700
  by (descending) (auto simp add: memb_def)
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   701
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   702
lemma fempty_not_finsert[simp]:
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   703
  shows "{||} \<noteq> finsert x S"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   704
  and   "finsert x S \<noteq> {||}"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   705
  by (descending, simp)+
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   706
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   707
lemma finsert_left_comm:
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   708
  shows "finsert x (finsert y S) = finsert y (finsert x S)"
2528
9bde8a508594 Partially merging changes from Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2525
diff changeset
   709
  by (descending) (auto)
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   710
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   711
lemma finsert_left_idem:
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   712
  shows "finsert x (finsert x S) = finsert x S"
2528
9bde8a508594 Partially merging changes from Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2525
diff changeset
   713
  by (descending) (auto)
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   714
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   715
lemma fsingleton_eq[simp]:
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   716
  shows "{|x|} = {|y|} \<longleftrightarrow> x = y"
2528
9bde8a508594 Partially merging changes from Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2525
diff changeset
   717
  by (descending) (auto)
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   718
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   719
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   720
(* FIXME: is this in any case a useful lemma *)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   721
lemma fin_mdef:
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   722
  shows "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = finsert x (F - {|x|})"
2537
d73fa7a3e04b renamed fminus_raw to diff_list
Christian Urban <urbanc@in.tum.de>
parents: 2536
diff changeset
   723
  by (descending) (auto simp add: memb_def diff_list_def)
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   724
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   725
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   726
subsection {* fset *}
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   727
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   728
lemma fset_simps[simp]:
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   729
  "fset {||} = ({} :: 'a set)"
2533
767161329839 further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2532
diff changeset
   730
  "fset (finsert (x :: 'a) S) = insert x (fset S)"
1819
63dd459dbc0d Much more in FSet (currently non-working)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1817
diff changeset
   731
  by (lifting set.simps)
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   732
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   733
lemma finite_fset [simp]: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   734
  shows "finite (fset S)"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   735
  by (descending) (simp)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   736
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   737
lemma fset_cong:
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   738
  shows "fset S = fset T \<longleftrightarrow> S = T"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   739
  by (descending) (simp)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   740
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   741
lemma ffilter_set [simp]: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   742
  shows "fset (ffilter P xs) = P \<inter> fset xs"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   743
  by (descending) (auto simp add: mem_def)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   744
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   745
lemma fdelete_set [simp]: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   746
  shows "fset (fdelete x xs) = fset xs - {x}"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   747
  by (descending) (simp)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   748
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   749
lemma finter_set [simp]: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   750
  shows "fset (xs |\<inter>| ys) = fset xs \<inter> fset ys"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   751
  by (lifting set_finter_raw)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   752
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   753
lemma funion_set [simp]: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   754
  shows "fset (xs |\<union>| ys) = fset xs \<union> fset ys"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   755
  by (lifting set_append)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   756
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   757
lemma fminus_set [simp]: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   758
  shows "fset (xs - ys) = fset xs - fset ys"
2537
d73fa7a3e04b renamed fminus_raw to diff_list
Christian Urban <urbanc@in.tum.de>
parents: 2536
diff changeset
   759
  by (lifting set_diff_list)
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   760
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   761
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   762
subsection {* funion *}
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   763
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   764
lemmas [simp] =
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   765
  sup_bot_left[where 'a="'a fset", standard]
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   766
  sup_bot_right[where 'a="'a fset", standard]
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   767
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   768
lemma funion_finsert[simp]:
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   769
  shows "finsert x S |\<union>| T = finsert x (S |\<union>| T)"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   770
  by (lifting append.simps(2))
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   771
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   772
lemma singleton_funion_left:
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   773
  shows "{|a|} |\<union>| S = finsert a S"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   774
  by simp
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   775
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   776
lemma singleton_funion_right:
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   777
  shows "S |\<union>| {|a|} = finsert a S"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   778
  by (subst sup.commute) simp
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   779
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   780
lemma fin_funion:
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   781
  shows "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   782
  by (descending) (simp add: memb_def)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   783
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   784
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   785
subsection {* fminus *}
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   786
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   787
lemma fminus_fin: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   788
  shows "x |\<in>| (xs - ys) \<longleftrightarrow> x |\<in>| xs \<and> x |\<notin>| ys"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   789
  by (descending) (simp add: memb_def)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   790
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   791
lemma fminus_red: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   792
  shows "finsert x xs - ys = (if x |\<in>| ys then xs - ys else finsert x (xs - ys))"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   793
  by (descending) (auto simp add: memb_def)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   794
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   795
lemma fminus_red_fin[simp]: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   796
  shows "x |\<in>| ys \<Longrightarrow> finsert x xs - ys = xs - ys"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   797
  by (simp add: fminus_red)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   798
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   799
lemma fminus_red_fnotin[simp]: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   800
  shows "x |\<notin>| ys \<Longrightarrow> finsert x xs - ys = finsert x (xs - ys)"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   801
  by (simp add: fminus_red)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   802
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   803
lemma fin_fminus_fnotin: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   804
  shows "x |\<in>| F - S \<Longrightarrow> x |\<notin>| S"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   805
  unfolding fin_set fminus_set
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   806
  by blast
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   807
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   808
lemma fin_fnotin_fminus: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   809
  shows "x |\<in>| S \<Longrightarrow> x |\<notin>| F - S"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   810
  unfolding fin_set fminus_set
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   811
  by blast
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   812
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   813
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   814
section {* fdelete *}
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   815
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   816
lemma fin_fdelete:
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   817
  shows "x |\<in>| fdelete y S \<longleftrightarrow> x |\<in>| S \<and> x \<noteq> y"
2533
767161329839 further cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2532
diff changeset
   818
  by (descending) (simp add: memb_def)
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   819
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   820
lemma fnotin_fdelete:
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   821
  shows "x |\<notin>| fdelete x S"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   822
  by (descending) (simp add: memb_def)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   823
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   824
lemma fnotin_fdelete_ident:
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   825
  shows "x |\<notin>| S \<Longrightarrow> fdelete x S = S"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   826
  by (descending) (simp add: memb_def)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   827
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   828
lemma fset_fdelete_cases:
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   829
  shows "S = {||} \<or> (\<exists>x. x |\<in>| S \<and> S = finsert x (fdelete x S))"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   830
  by (descending) (auto simp add: memb_def insert_absorb)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   831
  
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   832
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   833
section {* finter *}
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   834
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   835
lemma finter_empty_l:
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   836
  shows "{||} |\<inter>| S = {||}"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   837
  by simp
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   838
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   839
lemma finter_empty_r:
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   840
  shows "S |\<inter>| {||} = {||}"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   841
  by simp
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   842
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   843
lemma finter_finsert:
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   844
  shows "finsert x S |\<inter>| T = (if x |\<in>| T then finsert x (S |\<inter>| T) else S |\<inter>| T)"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   845
  by (descending) (simp add: memb_def)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   846
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   847
lemma fin_finter:
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   848
  shows "x |\<in>| (S |\<inter>| T) \<longleftrightarrow> x |\<in>| S \<and> x |\<in>| T"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   849
  by (descending) (simp add: memb_def)
1533
5f5e99a11f66 A few more theorems in FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1518
diff changeset
   850
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   851
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   852
subsection {* fsubset *}
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   853
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   854
lemma fsubseteq_set: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   855
  shows "xs |\<subseteq>| ys \<longleftrightarrow> fset xs \<subseteq> fset ys"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   856
  by (descending) (simp add: sub_list_def)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   857
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   858
lemma fsubset_set: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   859
  shows "xs |\<subset>| ys \<longleftrightarrow> fset xs \<subset> fset ys"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   860
  unfolding less_fset_def 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   861
  by (descending) (auto simp add: sub_list_def)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   862
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   863
lemma fsubseteq_finsert:
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   864
  shows "(finsert x xs) |\<subseteq>| ys \<longleftrightarrow> x |\<in>| ys \<and> xs |\<subseteq>| ys"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   865
  by (descending) (simp add: sub_list_def memb_def)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   866
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   867
lemma fsubset_fin: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   868
  shows "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   869
  by (descending) (auto simp add: sub_list_def memb_def)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   870
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   871
(* FIXME: no type ord *)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   872
(*
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   873
lemma fsubset_finsert:
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   874
  shows "(finsert x xs) |\<subset>| ys \<longleftrightarrow> x |\<in>| ys \<and> xs |\<subset>| ys"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   875
  by (descending) (simp add: sub_list_def memb_def)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   876
*)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   877
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   878
lemma fsubseteq_fempty:
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   879
  shows "xs |\<subseteq>| {||} \<longleftrightarrow> xs = {||}"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   880
  by (descending) (simp add: sub_list_def)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   881
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   882
(* also problem with ord *)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   883
lemma not_fsubset_fnil: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   884
  shows "\<not> xs |\<subset>| {||}"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   885
  by (metis fset_simps(1) fsubset_set not_psubset_empty)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   886
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   887
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   888
section {* fmap *}
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   889
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   890
lemma fmap_simps [simp]:
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   891
   shows "fmap f {||} = {||}"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   892
  and   "fmap f (finsert x S) = finsert (f x) (fmap f S)"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   893
  by (descending, simp)+
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   894
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   895
lemma fmap_set_image [simp]:
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   896
  shows "fset (fmap f S) = f ` (fset S)"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   897
  by (descending) (simp)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   898
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   899
lemma inj_fmap_eq_iff:
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   900
  shows "inj f \<Longrightarrow> fmap f S = fmap f T \<longleftrightarrow> S = T"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   901
  by (descending) (metis inj_vimage_image_eq list_eq.simps set_map)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   902
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   903
lemma fmap_funion: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   904
  shows "fmap f (S |\<union>| T) = fmap f S |\<union>| fmap f T"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   905
  by (descending) (simp)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   906
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   907
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   908
subsection {* fcard *}
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   909
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   910
lemma fcard_set: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   911
  shows "fcard xs = card (fset xs)"
2536
98e84b56543f renamed fcard_raw to card_list
Christian Urban <urbanc@in.tum.de>
parents: 2534
diff changeset
   912
  by (lifting card_list_def)
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   913
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   914
lemma fcard_finsert_if [simp]:
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   915
  shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))"
2536
98e84b56543f renamed fcard_raw to card_list
Christian Urban <urbanc@in.tum.de>
parents: 2534
diff changeset
   916
  by (descending) (auto simp add: card_list_def memb_def insert_absorb)
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   917
2530
3b8741ecfda3 FSet synchronizing
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2529
diff changeset
   918
lemma fcard_0[simp]:
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   919
  shows "fcard S = 0 \<longleftrightarrow> S = {||}"
2536
98e84b56543f renamed fcard_raw to card_list
Christian Urban <urbanc@in.tum.de>
parents: 2534
diff changeset
   920
  by (descending) (simp add: card_list_def)
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   921
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   922
lemma fcard_fempty[simp]:
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   923
  shows "fcard {||} = 0"
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   924
  by (simp add: fcard_0)
1813
69fff336dd18 Porting lemmas from Quotient package FSet to new FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1682
diff changeset
   925
1821
Christian Urban <urbanc@in.tum.de>
parents: 1820
diff changeset
   926
lemma fcard_1:
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   927
  shows "fcard S = 1 \<longleftrightarrow> (\<exists>x. S = {|x|})"
2536
98e84b56543f renamed fcard_raw to card_list
Christian Urban <urbanc@in.tum.de>
parents: 2534
diff changeset
   928
  by (descending) (auto simp add: card_list_def card_Suc_eq)
1819
63dd459dbc0d Much more in FSet (currently non-working)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1817
diff changeset
   929
2084
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   930
lemma fcard_gt_0:
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   931
  shows "x \<in> fset S \<Longrightarrow> 0 < fcard S"
2536
98e84b56543f renamed fcard_raw to card_list
Christian Urban <urbanc@in.tum.de>
parents: 2534
diff changeset
   932
  by (descending) (auto simp add: card_list_def card_gt_0_iff)
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   933
  
2084
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
   934
lemma fcard_not_fin:
2531
8054f4988672 FSet: stronger fact in Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2530
diff changeset
   935
  shows "(x |\<notin>| S) = (fcard (finsert x S) = Suc (fcard S))"
2536
98e84b56543f renamed fcard_raw to card_list
Christian Urban <urbanc@in.tum.de>
parents: 2534
diff changeset
   936
  by (descending) (auto simp add: memb_def card_list_def insert_absorb)
1813
69fff336dd18 Porting lemmas from Quotient package FSet to new FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1682
diff changeset
   937
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   938
lemma fcard_suc: 
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   939
  shows "fcard S = Suc n \<Longrightarrow> \<exists>x T. x |\<notin>| T \<and> S = finsert x T \<and> fcard T = n"
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   940
  apply(descending)
2536
98e84b56543f renamed fcard_raw to card_list
Christian Urban <urbanc@in.tum.de>
parents: 2534
diff changeset
   941
  apply(auto simp add: card_list_def memb_def)
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   942
  apply(drule card_eq_SucD)
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   943
  apply(auto)
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   944
  apply(rule_tac x="b" in exI)
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   945
  apply(rule_tac x="removeAll b S" in exI)
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   946
  apply(auto)
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   947
  done
1813
69fff336dd18 Porting lemmas from Quotient package FSet to new FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1682
diff changeset
   948
1819
63dd459dbc0d Much more in FSet (currently non-working)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1817
diff changeset
   949
lemma fcard_delete:
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   950
  shows "fcard (fdelete y S) = (if y |\<in>| S then fcard S - 1 else fcard S)"
2536
98e84b56543f renamed fcard_raw to card_list
Christian Urban <urbanc@in.tum.de>
parents: 2534
diff changeset
   951
  by (descending) (simp add: card_list_def memb_def)
1819
63dd459dbc0d Much more in FSet (currently non-working)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1817
diff changeset
   952
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   953
lemma fcard_suc_memb: 
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   954
  shows "fcard A = Suc n \<Longrightarrow> \<exists>a. a |\<in>| A"
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   955
  apply(descending)
2536
98e84b56543f renamed fcard_raw to card_list
Christian Urban <urbanc@in.tum.de>
parents: 2534
diff changeset
   956
  apply(simp add: card_list_def memb_def)
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   957
  apply(drule card_eq_SucD)
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   958
  apply(auto)
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   959
  done
1878
c22947214948 2 more lifted lemmas needed for second representation
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1860
diff changeset
   960
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   961
lemma fin_fcard_not_0: 
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   962
  shows "a |\<in>| A \<Longrightarrow> fcard A \<noteq> 0"
2536
98e84b56543f renamed fcard_raw to card_list
Christian Urban <urbanc@in.tum.de>
parents: 2534
diff changeset
   963
  by (descending) (auto simp add: card_list_def memb_def)
1878
c22947214948 2 more lifted lemmas needed for second representation
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1860
diff changeset
   964
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   965
lemma fcard_mono: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   966
  shows "xs |\<subseteq>| ys \<Longrightarrow> fcard xs \<le> fcard ys"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   967
  unfolding fcard_set fsubseteq_set
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   968
  by (simp add: card_mono[OF finite_fset])
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   969
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   970
lemma fcard_fsubset_eq: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   971
  shows "xs |\<subseteq>| ys \<Longrightarrow> fcard ys \<le> fcard xs \<Longrightarrow> xs = ys"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   972
  unfolding fcard_set fsubseteq_set
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   973
  by (auto dest: card_seteq[OF finite_fset] simp add: fset_cong)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   974
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   975
lemma psubset_fcard_mono: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   976
  shows "xs |\<subset>| ys \<Longrightarrow> fcard xs < fcard ys"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   977
  unfolding fcard_set fsubset_set
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   978
  by (rule psubset_card_mono[OF finite_fset])
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   979
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   980
lemma fcard_funion_finter: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   981
  shows "fcard xs + fcard ys = fcard (xs |\<union>| ys) + fcard (xs |\<inter>| ys)"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   982
  unfolding fcard_set funion_set finter_set
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   983
  by (rule card_Un_Int[OF finite_fset finite_fset])
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   984
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   985
lemma fcard_funion_disjoint: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   986
  shows "xs |\<inter>| ys = {||} \<Longrightarrow> fcard (xs |\<union>| ys) = fcard xs + fcard ys"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   987
  unfolding fcard_set funion_set 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   988
  apply (rule card_Un_disjoint[OF finite_fset finite_fset])
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   989
  by (metis finter_set fset_simps(1))
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   990
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   991
lemma fcard_delete1_less: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   992
  shows "x |\<in>| xs \<Longrightarrow> fcard (fdelete x xs) < fcard xs"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   993
  unfolding fcard_set fin_set fdelete_set 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   994
  by (rule card_Diff1_less[OF finite_fset])
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   995
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   996
lemma fcard_delete2_less: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   997
  shows "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> fcard (fdelete y (fdelete x xs)) < fcard xs"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   998
  unfolding fcard_set fdelete_set fin_set
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
   999
  by (rule card_Diff2_less[OF finite_fset])
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1000
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1001
lemma fcard_delete1_le: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1002
  shows "fcard (fdelete x xs) \<le> fcard xs"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1003
  unfolding fdelete_set fcard_set
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1004
  by (rule card_Diff1_le[OF finite_fset])
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1005
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1006
lemma fcard_psubset: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1007
  shows "ys |\<subseteq>| xs \<Longrightarrow> fcard ys < fcard xs \<Longrightarrow> ys |\<subset>| xs"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1008
  unfolding fcard_set fsubseteq_set fsubset_set
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1009
  by (rule card_psubset[OF finite_fset])
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1010
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1011
lemma fcard_fmap_le: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1012
  shows "fcard (fmap f xs) \<le> fcard xs"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1013
  unfolding fcard_set fmap_set_image
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1014
  by (rule card_image_le[OF finite_fset])
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1015
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1016
lemma fcard_fminus_finsert[simp]:
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1017
  assumes "a |\<in>| A" and "a |\<notin>| B"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1018
  shows "fcard (A - finsert a B) = fcard (A - B) - 1"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1019
  using assms 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1020
  unfolding fin_set fcard_set fminus_set
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1021
  by (simp add: card_Diff_insert[OF finite_fset])
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1022
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1023
lemma fcard_fminus_fsubset:
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1024
  assumes "B |\<subseteq>| A"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1025
  shows "fcard (A - B) = fcard A - fcard B"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1026
  using assms 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1027
  unfolding fsubseteq_set fcard_set fminus_set
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1028
  by (rule card_Diff_subset[OF finite_fset])
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
  1029
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1030
lemma fcard_fminus_subset_finter:
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1031
  shows "fcard (A - B) = fcard A - fcard (A |\<inter>| B)"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1032
  unfolding finter_set fcard_set fminus_set
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1033
  by (rule card_Diff_subset_Int) (simp)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1034
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1035
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1036
section {* fconcat *}
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1037
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1038
lemma fconcat_fempty:
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1039
  shows "fconcat {||} = {||}"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1040
  by (lifting concat.simps(1))
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1041
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1042
lemma fconcat_finsert:
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1043
  shows "fconcat (finsert x S) = x |\<union>| fconcat S"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1044
  by (lifting concat.simps(2))
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1045
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1046
lemma fconcat_finter:
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1047
  shows "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1048
  by (lifting concat_append)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1049
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1050
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1051
section {* ffilter *}
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1052
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1053
lemma subseteq_filter: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1054
  shows "ffilter P xs <= ffilter Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1055
  by  (descending) (auto simp add: memb_def sub_list_def)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1056
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1057
lemma eq_ffilter: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1058
  shows "(ffilter P xs = ffilter Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1059
  by (descending) (auto simp add: memb_def)
1887
7abd8c1d9f4b Some new lemmas
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1886
diff changeset
  1060
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1061
lemma subset_ffilter:
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1062
  shows "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> ffilter P xs < ffilter Q xs"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1063
  unfolding less_fset_def by (auto simp add: subseteq_filter eq_ffilter)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1064
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1065
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1066
subsection {* ffold *}
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1067
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1068
lemma ffold_nil: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1069
  shows "ffold f z {||} = z"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1070
  by (descending) (simp)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1071
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1072
lemma ffold_finsert: "ffold f z (finsert a A) =
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1073
  (if rsp_fold f then if a |\<in>| A then ffold f z A else f a (ffold f z A) else z)"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1074
  by (descending) (simp add: memb_def)
1887
7abd8c1d9f4b Some new lemmas
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1886
diff changeset
  1075
2534
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1076
lemma fin_commute_ffold:
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1077
  "\<lbrakk>rsp_fold f; h |\<in>| b\<rbrakk> \<Longrightarrow> ffold f z b = f h (ffold f z (fdelete h b))"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1078
  by (descending) (simp add: memb_def memb_commute_ffold_raw)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1079
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1080
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1081
subsection {* Choice in fsets *}
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1082
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1083
lemma fset_choice: 
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1084
  assumes a: "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>y. P x y)"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1085
  shows "\<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)"
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1086
  using a
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1087
  apply(descending)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1088
  using finite_set_choice
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1089
  by (auto simp add: memb_def Ball_def)
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1090
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1091
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1092
(* FIXME: is that in any way useful *)  
f99578469d08 Further reorganisation and cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2533
diff changeset
  1093
1887
7abd8c1d9f4b Some new lemmas
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1886
diff changeset
  1094
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
  1095
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
  1096
section {* Induction and Cases rules for fsets *}
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
  1097
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
  1098
lemma fset_strong_cases:
2084
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
  1099
  obtains "xs = {||}"
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
  1100
    | x ys where "x |\<notin>| ys" and "xs = finsert x ys"
1819
63dd459dbc0d Much more in FSet (currently non-working)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1817
diff changeset
  1101
  by (lifting fset_raw_strong_cases)
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
  1102
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
  1103
lemma fset_exhaust[case_names fempty finsert, cases type: fset]:
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
  1104
  shows "\<lbrakk>S = {||} \<Longrightarrow> P; \<And>x S'. S = finsert x S' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
  1105
  by (lifting list.exhaust)
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
  1106
1533
5f5e99a11f66 A few more theorems in FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1518
diff changeset
  1107
lemma fset_induct_weak[case_names fempty finsert]:
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
  1108
  shows "\<lbrakk>P {||}; \<And>x S. P S \<Longrightarrow> P (finsert x S)\<rbrakk> \<Longrightarrow> P S"
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
  1109
  by (lifting list.induct)
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
  1110
1533
5f5e99a11f66 A few more theorems in FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1518
diff changeset
  1111
lemma fset_induct[case_names fempty finsert, induct type: fset]:
2084
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
  1112
  assumes prem1: "P {||}"
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
  1113
  and     prem2: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (finsert x S)"
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
  1114
  shows "P S"
1533
5f5e99a11f66 A few more theorems in FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1518
diff changeset
  1115
proof(induct S rule: fset_induct_weak)
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
  1116
  case fempty
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
  1117
  show "P {||}" by (rule prem1)
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
  1118
next
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
  1119
  case (finsert x S)
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
  1120
  have asm: "P S" by fact
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
  1121
  show "P (finsert x S)"
1938
3641d055b260 Further cleaning of proofs in FSet
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1936
diff changeset
  1122
    by (cases "x |\<in>| S") (simp_all add: asm prem2)
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
  1123
qed
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
  1124
1533
5f5e99a11f66 A few more theorems in FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1518
diff changeset
  1125
lemma fset_induct2:
5f5e99a11f66 A few more theorems in FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1518
diff changeset
  1126
  "P {||} {||} \<Longrightarrow>
5f5e99a11f66 A few more theorems in FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1518
diff changeset
  1127
  (\<And>x xs. x |\<notin>| xs \<Longrightarrow> P (finsert x xs) {||}) \<Longrightarrow>
5f5e99a11f66 A few more theorems in FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1518
diff changeset
  1128
  (\<And>y ys. y |\<notin>| ys \<Longrightarrow> P {||} (finsert y ys)) \<Longrightarrow>
5f5e99a11f66 A few more theorems in FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1518
diff changeset
  1129
  (\<And>x xs y ys. \<lbrakk>P xs ys; x |\<notin>| xs; y |\<notin>| ys\<rbrakk> \<Longrightarrow> P (finsert x xs) (finsert y ys)) \<Longrightarrow>
5f5e99a11f66 A few more theorems in FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1518
diff changeset
  1130
  P xsa ysa"
5f5e99a11f66 A few more theorems in FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1518
diff changeset
  1131
  apply (induct xsa arbitrary: ysa)
5f5e99a11f66 A few more theorems in FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1518
diff changeset
  1132
  apply (induct_tac x rule: fset_induct)
5f5e99a11f66 A few more theorems in FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1518
diff changeset
  1133
  apply simp_all
5f5e99a11f66 A few more theorems in FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1518
diff changeset
  1134
  apply (induct_tac xa rule: fset_induct)
5f5e99a11f66 A few more theorems in FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1518
diff changeset
  1135
  apply simp_all
5f5e99a11f66 A few more theorems in FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1518
diff changeset
  1136
  done
1518
212629c90971 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
  1137
2084
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
  1138
lemma fset_fcard_induct:
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
  1139
  assumes a: "P {||}"
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
  1140
  and     b: "\<And>xs ys. Suc (fcard xs) = (fcard ys) \<Longrightarrow> P xs \<Longrightarrow> P ys"
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
  1141
  shows "P zs"
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
  1142
proof (induct zs)
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
  1143
  show "P {||}" by (rule a)
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
  1144
next
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
  1145
  fix x :: 'a and zs :: "'a fset"
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
  1146
  assume h: "P zs"
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
  1147
  assume "x |\<notin>| zs"
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
  1148
  then have H1: "Suc (fcard zs) = fcard (finsert x zs)" using fcard_suc by auto
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
  1149
  then show "P (finsert x zs)" using b h by simp
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
  1150
qed
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
  1151
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
  1152
1888
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
  1153
(* We cannot write it as "assumes .. shows" since Isabelle changes
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
  1154
   the quantifiers to schematic variables and reintroduces them in
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
  1155
   a different order *)
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
  1156
lemma fset_eq_cases:
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
  1157
 "\<lbrakk>a1 = a2;
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
  1158
   \<And>a b xs. \<lbrakk>a1 = finsert a (finsert b xs); a2 = finsert b (finsert a xs)\<rbrakk> \<Longrightarrow> P;
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
  1159
   \<lbrakk>a1 = {||}; a2 = {||}\<rbrakk> \<Longrightarrow> P; \<And>xs ys. \<lbrakk>a1 = ys; a2 = xs; xs = ys\<rbrakk> \<Longrightarrow> P;
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
  1160
   \<And>a xs. \<lbrakk>a1 = finsert a (finsert a xs); a2 = finsert a xs\<rbrakk> \<Longrightarrow> P;
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
  1161
   \<And>xs ys a. \<lbrakk>a1 = finsert a xs; a2 = finsert a ys; xs = ys\<rbrakk> \<Longrightarrow> P;
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
  1162
   \<And>xs1 xs2 xs3. \<lbrakk>a1 = xs1; a2 = xs3; xs1 = xs2; xs2 = xs3\<rbrakk> \<Longrightarrow> P\<rbrakk>
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
  1163
  \<Longrightarrow> P"
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
  1164
  by (lifting list_eq2.cases[simplified list_eq2_equiv[symmetric]])
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
  1165
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
  1166
lemma fset_eq_induct:
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
  1167
  assumes "x1 = x2"
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
  1168
  and "\<And>a b xs. P (finsert a (finsert b xs)) (finsert b (finsert a xs))"
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
  1169
  and "P {||} {||}"
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
  1170
  and "\<And>xs ys. \<lbrakk>xs = ys; P xs ys\<rbrakk> \<Longrightarrow> P ys xs"
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
  1171
  and "\<And>a xs. P (finsert a (finsert a xs)) (finsert a xs)"
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
  1172
  and "\<And>xs ys a. \<lbrakk>xs = ys; P xs ys\<rbrakk> \<Longrightarrow> P (finsert a xs) (finsert a ys)"
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
  1173
  and "\<And>xs1 xs2 xs3. \<lbrakk>xs1 = xs2; P xs1 xs2; xs2 = xs3; P xs2 xs3\<rbrakk> \<Longrightarrow> P xs1 xs3"
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
  1174
  shows "P x1 x2"
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
  1175
  using assms
59f41804b3f8 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1887
diff changeset
  1176
  by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]])
1820
de28a91eaca3 Working FSet with additional lemmas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1819
diff changeset
  1177
2524
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
  1178
2084
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
  1179
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
  1180
section {* lemmas transferred from Finite_Set theory *}
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
  1181
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
  1182
text {* finiteness for finite sets holds *}
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
  1183
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
  1184
72b777cc5479 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1952
diff changeset
  1185
2234
8035515bbbc6 something about the quotient ype definitions
Christian Urban <urbanc@in.tum.de>
parents: 2222
diff changeset
  1186
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
  1187
lemma list_all2_refl:
2266
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1188
  assumes q: "equivp R"
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
  1189
  shows "(list_all2 R) r r"
2378
2f13fe48c877 updated to new Isabelle; made FSet more "quiet"
Christian Urban <urbanc@in.tum.de>
parents: 2372
diff changeset
  1190
  by (rule list_all2_refl) (metis equivp_def q)
2266
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1191
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1192
lemma compose_list_refl2:
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1193
  assumes q: "equivp R"
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
  1194
  shows "(list_all2 R OOO op \<approx>) r r"
2266
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1195
proof
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1196
  have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
  1197
  show "list_all2 R r r" by (rule list_all2_refl[OF q])
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
  1198
  with * show "(op \<approx> OO list_all2 R) r r" ..
2266
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1199
qed
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1200
2285
965ee8f08d4c eliminated a quot_thm flag
Christian Urban <urbanc@in.tum.de>
parents: 2278
diff changeset
  1201
lemma quotient_compose_list_g:
2266
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1202
  assumes q: "Quotient R Abs Rep"
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1203
  and     e: "equivp R"
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
  1204
  shows  "Quotient ((list_all2 R) OOO (op \<approx>))
2266
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1205
    (abs_fset \<circ> (map Abs)) ((map Rep) \<circ> rep_fset)"
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1206
  unfolding Quotient_def comp_def
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1207
proof (intro conjI allI)
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1208
  fix a r s
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1209
  show "abs_fset (map Abs (map Rep (rep_fset a))) = a"
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1210
    by (simp add: abs_o_rep[OF q] Quotient_abs_rep[OF Quotient_fset] map_id)
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
  1211
  have b: "list_all2 R (map Rep (rep_fset a)) (map Rep (rep_fset a))"
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
  1212
    by (rule list_all2_refl[OF e])
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
  1213
  have c: "(op \<approx> OO list_all2 R) (map Rep (rep_fset a)) (map Rep (rep_fset a))"
2266
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1214
    by (rule, rule equivp_reflp[OF fset_equivp]) (rule b)
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
  1215
  show "(list_all2 R OOO op \<approx>) (map Rep (rep_fset a)) (map Rep (rep_fset a))"
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
  1216
    by (rule, rule list_all2_refl[OF e]) (rule c)
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
  1217
  show "(list_all2 R OOO op \<approx>) r s = ((list_all2 R OOO op \<approx>) r r \<and>
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
  1218
        (list_all2 R OOO op \<approx>) s s \<and> abs_fset (map Abs r) = abs_fset (map Abs s))"
2266
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1219
  proof (intro iffI conjI)
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
  1220
    show "(list_all2 R OOO op \<approx>) r r" by (rule compose_list_refl2[OF e])
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
  1221
    show "(list_all2 R OOO op \<approx>) s s" by (rule compose_list_refl2[OF e])
2266
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1222
  next
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
  1223
    assume a: "(list_all2 R OOO op \<approx>) r s"
2266
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1224
    then have b: "map Abs r \<approx> map Abs s"
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1225
    proof (elim pred_compE)
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1226
      fix b ba
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
  1227
      assume c: "list_all2 R r b"
2266
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1228
      assume d: "b \<approx> ba"
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
  1229
      assume e: "list_all2 R ba s"
2266
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1230
      have f: "map Abs r = map Abs b"
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1231
        using Quotient_rel[OF list_quotient[OF q]] c by blast
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1232
      have "map Abs ba = map Abs s"
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1233
        using Quotient_rel[OF list_quotient[OF q]] e by blast
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1234
      then have g: "map Abs s = map Abs ba" by simp
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1235
      then show "map Abs r \<approx> map Abs s" using d f map_rel_cong by simp
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1236
    qed
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1237
    then show "abs_fset (map Abs r) = abs_fset (map Abs s)"
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1238
      using Quotient_rel[OF Quotient_fset] by blast
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1239
  next
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
  1240
    assume a: "(list_all2 R OOO op \<approx>) r r \<and> (list_all2 R OOO op \<approx>) s s
2266
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1241
      \<and> abs_fset (map Abs r) = abs_fset (map Abs s)"
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
  1242
    then have s: "(list_all2 R OOO op \<approx>) s s" by simp
2266
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1243
    have d: "map Abs r \<approx> map Abs s"
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1244
      by (subst Quotient_rel[OF Quotient_fset]) (simp add: a)
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1245
    have b: "map Rep (map Abs r) \<approx> map Rep (map Abs s)"
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1246
      by (rule map_rel_cong[OF d])
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
  1247
    have y: "list_all2 R (map Rep (map Abs s)) s"
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
  1248
      by (fact rep_abs_rsp_left[OF list_quotient[OF q], OF list_all2_refl[OF e, of s]])
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
  1249
    have c: "(op \<approx> OO list_all2 R) (map Rep (map Abs r)) s"
2266
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1250
      by (rule pred_compI) (rule b, rule y)
2326
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
  1251
    have z: "list_all2 R r (map Rep (map Abs r))"
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
  1252
      by (fact rep_abs_rsp[OF list_quotient[OF q], OF list_all2_refl[OF e, of r]])
b51532dd5689 Changes for PER and list_all2 committed to Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2278
diff changeset
  1253
    then show "(list_all2 R OOO op \<approx>) r s"
2266
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1254
      using a c pred_compI by simp
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1255
  qed
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1256
qed
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1257
2528
9bde8a508594 Partially merging changes from Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2525
diff changeset
  1258
9bde8a508594 Partially merging changes from Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2525
diff changeset
  1259
ML {*
9bde8a508594 Partially merging changes from Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2525
diff changeset
  1260
fun dest_fsetT (Type (@{type_name fset}, [T])) = T
9bde8a508594 Partially merging changes from Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2525
diff changeset
  1261
  | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
9bde8a508594 Partially merging changes from Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2525
diff changeset
  1262
*}
9bde8a508594 Partially merging changes from Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2525
diff changeset
  1263
2266
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1264
no_notation
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1265
  list_eq (infix "\<approx>" 50)
dcffc2f132c9 Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2250
diff changeset
  1266
2234
8035515bbbc6 something about the quotient ype definitions
Christian Urban <urbanc@in.tum.de>
parents: 2222
diff changeset
  1267
end