src/HOL/HOLCF/Library/Int_Discrete.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 42151 4da4fc77664b
child 58880 0baae4311a9f
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:
42151
4da4fc77664b tuned headers;
wenzelm
parents: 41292
diff changeset
     1
(*  Title:      HOL/HOLCF/Library/Int_Discrete.thy
41112
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
     2
    Author:     Brian Huffman
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
     3
*)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
     4
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
     5
header {* Discrete cpo instance for integers *}
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
     6
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
     7
theory Int_Discrete
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
     8
imports HOLCF
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
     9
begin
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    10
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    11
text {* Discrete cpo instance for @{typ int}. *}
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    12
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    13
instantiation int :: discrete_cpo
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    14
begin
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    15
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    16
definition below_int_def:
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    17
  "(x::int) \<sqsubseteq> y \<longleftrightarrow> x = y"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    18
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    19
instance proof
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    20
qed (rule below_int_def)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    21
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    22
end
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    23
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    24
text {*
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    25
  TODO: implement a command to automate discrete predomain instances.
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    26
*}
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    27
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    28
instantiation int :: predomain
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    29
begin
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    30
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    31
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41112
diff changeset
    32
  "(liftemb :: int u \<rightarrow> udom u) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
41112
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    33
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    34
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41112
diff changeset
    35
  "(liftprj :: udom u \<rightarrow> int u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
41112
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    36
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    37
definition
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    38
  "liftdefl \<equiv> (\<lambda>(t::int itself). LIFTDEFL(int discr))"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    39
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    40
instance proof
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41112
diff changeset
    41
  show "ep_pair liftemb (liftprj :: udom u \<rightarrow> int u)"
41112
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    42
    unfolding liftemb_int_def liftprj_int_def
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    43
    apply (rule ep_pair_comp)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    44
    apply (rule ep_pair_u_map)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    45
    apply (simp add: ep_pair.intro)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    46
    apply (rule predomain_ep)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    47
    done
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41112
diff changeset
    48
  show "cast\<cdot>LIFTDEFL(int) = liftemb oo (liftprj :: udom u \<rightarrow> int u)"
41112
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    49
    unfolding liftemb_int_def liftprj_int_def liftdefl_int_def
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    50
    apply (simp add: cast_liftdefl cfcomp1 u_map_map)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    51
    apply (simp add: ID_def [symmetric] u_map_ID)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    52
    done
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    53
qed
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    54
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    55
end
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    56
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    57
end