src/HOL/Quotient_Examples/Lift_DList.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 47361 87c0eaf04bad
child 49834 b27bbb021df1
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
     1
(*  Title:      HOL/Quotient_Examples/Lift_DList.thy
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
     2
    Author:     Ondrej Kuncar
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
     3
*)
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
     4
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
     5
theory Lift_DList
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
     6
imports Main "~~/src/HOL/Library/Quotient_List"
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
     7
begin
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
     8
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
     9
subsection {* The type of distinct lists *}
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    10
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    11
typedef (open) 'a dlist = "{xs::'a list. distinct xs}"
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    12
  morphisms list_of_dlist Abs_dlist
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    13
proof
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    14
  show "[] \<in> {xs. distinct xs}" by simp
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    15
qed
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    16
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    17
setup_lifting type_definition_dlist
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    18
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    19
text {* Fundamental operations: *}
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    20
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    21
lift_definition empty :: "'a dlist" is "[]"
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    22
by simp
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    23
  
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    24
lift_definition insert :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" is List.insert
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    25
by simp
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    26
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    27
lift_definition remove :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" is List.remove1
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    28
by simp
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    29
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    30
lift_definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b dlist" is "\<lambda>f. remdups o List.map f"
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    31
by simp
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    32
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    33
lift_definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" is List.filter
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    34
by simp
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    35
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    36
text {* Derived operations: *}
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    37
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    38
lift_definition null :: "'a dlist \<Rightarrow> bool" is List.null
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    39
by simp
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    40
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    41
lift_definition member :: "'a dlist \<Rightarrow> 'a \<Rightarrow> bool" is List.member
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    42
by simp
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    43
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    44
lift_definition length :: "'a dlist \<Rightarrow> nat" is List.length
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    45
by simp
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    46
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    47
lift_definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" is List.fold
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    48
by simp
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    49
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    50
lift_definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" is List.foldr
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    51
by simp
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    52
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    53
lift_definition concat :: "'a dlist dlist \<Rightarrow> 'a dlist" is "remdups o List.concat"
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    54
proof -
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    55
  {
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    56
    fix x y
47361
87c0eaf04bad support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents: 47308
diff changeset
    57
    have "list_all2 cr_dlist x y \<Longrightarrow> x = List.map list_of_dlist y"
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    58
      unfolding list_all2_def cr_dlist_def by (induction x y rule: list_induct2') auto
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    59
  }
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    60
  note cr = this
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    61
  fix x :: "'a list list" and y :: "'a list list"
47361
87c0eaf04bad support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents: 47308
diff changeset
    62
  assume "(list_all2 cr_dlist OO Lifting.invariant distinct OO (list_all2 cr_dlist)\<inverse>\<inverse>) x y"
87c0eaf04bad support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents: 47308
diff changeset
    63
  then have "x = y" by (auto dest: cr simp add: Lifting.invariant_def)
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    64
  then show "?thesis x y" unfolding Lifting.invariant_def by auto
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    65
qed
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    66
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    67
text {* We can export code: *}
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    68
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    69
export_code empty insert remove map filter null member length fold foldr concat in SML
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    70
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    71
end