half-ported Imperative HOL to new datatypes
authorblanchet
Tue Sep 09 20:51:36 2014 +0200 (2014-09-09)
changeset 582570662f35534fe
parent 58256 08c0f0d4b9f4
child 58258 b66034025548
half-ported Imperative HOL to new datatypes
src/HOL/Imperative_HOL/Heap.thy
src/HOL/Imperative_HOL/ex/Linked_Lists.thy
src/HOL/Library/RBT_Impl.thy
     1.1 --- a/src/HOL/Imperative_HOL/Heap.thy	Tue Sep 09 20:51:36 2014 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap.thy	Tue Sep 09 20:51:36 2014 +0200
     1.3 @@ -53,8 +53,11 @@
     1.4  definition empty :: heap where
     1.5    "empty = \<lparr>arrays = (\<lambda>_ _. []), refs = (\<lambda>_ _. 0), lim = 0\<rparr>"
     1.6  
     1.7 -datatype_new 'a array = Array addr
     1.8 -datatype_new 'a ref = Ref addr -- "note the phantom type 'a "
     1.9 +datatype_new 'a array = Array addr -- "note the phantom type 'a"
    1.10 +datatype_compat array
    1.11 +
    1.12 +datatype_new 'a ref = Ref addr -- "note the phantom type 'a"
    1.13 +datatype_compat ref
    1.14  
    1.15  primrec addr_of_array :: "'a array \<Rightarrow> addr" where
    1.16    "addr_of_array (Array x) = x"
     2.1 --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Tue Sep 09 20:51:36 2014 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Tue Sep 09 20:51:36 2014 +0200
     2.3 @@ -11,7 +11,7 @@
     2.4  section {* Definition of Linked Lists *}
     2.5  
     2.6  setup {* Sign.add_const_constraint (@{const_name Ref}, SOME @{typ "nat \<Rightarrow> 'a\<Colon>type ref"}) *}
     2.7 -datatype_new 'a node = Empty | Node 'a "('a node) ref"
     2.8 +datatype 'a node = Empty | Node 'a "'a node ref"
     2.9  
    2.10  primrec
    2.11    node_encode :: "'a\<Colon>countable node \<Rightarrow> nat"
     3.1 --- a/src/HOL/Library/RBT_Impl.thy	Tue Sep 09 20:51:36 2014 +0200
     3.2 +++ b/src/HOL/Library/RBT_Impl.thy	Tue Sep 09 20:51:36 2014 +0200
     3.3 @@ -1056,7 +1056,7 @@
     3.4  theorem (in linorder) rbt_lookup_map: "rbt_lookup (map f t) x = map_option (f x) (rbt_lookup t x)"
     3.5    apply(induct t)
     3.6    apply auto
     3.7 -  apply(subgoal_tac "x = a")
     3.8 +  apply(rename_tac a b c, subgoal_tac "x = a")
     3.9    apply auto
    3.10    done
    3.11   (* FIXME: simproc "antisym less" does not work for linorder context, only for linorder type class
    3.12 @@ -1749,7 +1749,7 @@
    3.13  hide_type (open) compare
    3.14  hide_const (open)
    3.15    compare_height skip_black skip_red LT GT EQ case_compare rec_compare
    3.16 -  Abs_compare Rep_compare rep_set_compare
    3.17 +  Abs_compare Rep_compare
    3.18  hide_fact (open)
    3.19    Abs_compare_cases Abs_compare_induct Abs_compare_inject Abs_compare_inverse
    3.20    Rep_compare Rep_compare_cases Rep_compare_induct Rep_compare_inject Rep_compare_inverse