src/HOL/SPARK/Manual/Complex_Types.thy
author huffman
Sun Apr 01 16:09:58 2012 +0200 (2012-04-01)
changeset 47255 30a1692557b0
parent 45044 2fae15f8984d
child 56798 939e88e79724
permissions -rw-r--r--
removed Nat_Numeral.thy, moving all theorems elsewhere
berghofe@45044
     1
theory Complex_Types
berghofe@45044
     2
imports SPARK
berghofe@45044
     3
begin
berghofe@45044
     4
berghofe@45044
     5
datatype day = Mon | Tue | Wed | Thu | Fri | Sat | Sun
berghofe@45044
     6
berghofe@45044
     7
record two_fields =
berghofe@45044
     8
  Field1 :: "int \<times> day \<Rightarrow> int"
berghofe@45044
     9
  Field2 :: int
berghofe@45044
    10
berghofe@45044
    11
spark_types
berghofe@45044
    12
  complex_types__day = day
berghofe@45044
    13
  complex_types__record_type = two_fields
berghofe@45044
    14
berghofe@45044
    15
definition
berghofe@45044
    16
  initialized3 :: "(int \<times> day \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool" where
berghofe@45044
    17
  "initialized3 A i k = (\<forall>j\<in>{0..<k}. A (i, val j) = 0)"
berghofe@45044
    18
berghofe@45044
    19
definition
berghofe@45044
    20
  initialized2 :: "(int \<times> day \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> bool" where
berghofe@45044
    21
  "initialized2 A i = (\<forall>j\<in>{0..<i}. initialized3 A j 7)"
berghofe@45044
    22
berghofe@45044
    23
definition
berghofe@45044
    24
  initialized :: "(int \<Rightarrow> two_fields) \<Rightarrow> int \<Rightarrow> bool" where
berghofe@45044
    25
  "initialized A i = (\<forall>j\<in>{0..<i}.
berghofe@45044
    26
     initialized2 (Field1 (A j)) 10 \<and> Field2 (A j) = 0)"
berghofe@45044
    27
berghofe@45044
    28
spark_proof_functions
berghofe@45044
    29
  complex_types__initialized = initialized
berghofe@45044
    30
  complex_types__initialized2 = initialized2
berghofe@45044
    31
  complex_types__initialized3 = initialized3
berghofe@45044
    32
berghofe@45044
    33
(*<*)
berghofe@45044
    34
spark_open "complex_types_app/initialize.siv"
berghofe@45044
    35
berghofe@45044
    36
spark_vc procedure_initialize_1
berghofe@45044
    37
  by (simp add: initialized_def)
berghofe@45044
    38
berghofe@45044
    39
spark_vc procedure_initialize_2
berghofe@45044
    40
proof -
berghofe@45044
    41
  from
berghofe@45044
    42
    `initialized a loop__1__i`
berghofe@45044
    43
    `initialized2 (Field1 (a loop__1__i)) 9`
berghofe@45044
    44
    `initialized3 (Field1 (a loop__1__i)) 9 (pos Sun)`
berghofe@45044
    45
  show ?C1
berghofe@45044
    46
    apply (auto simp add: initialized_def initialized2_def initialized3_def)
berghofe@45044
    47
    apply (case_tac "j = 9")
berghofe@45044
    48
    apply auto
berghofe@45044
    49
    apply (case_tac "ja = 6")
berghofe@45044
    50
    apply auto
berghofe@45044
    51
    done
berghofe@45044
    52
  from H5
berghofe@45044
    53
  show ?C2 by simp
berghofe@45044
    54
qed
berghofe@45044
    55
berghofe@45044
    56
spark_vc procedure_initialize_3
berghofe@45044
    57
  by (simp add: initialized2_def)
berghofe@45044
    58
berghofe@45044
    59
spark_vc procedure_initialize_4
berghofe@45044
    60
proof -
berghofe@45044
    61
  from `initialized a loop__1__i`
berghofe@45044
    62
  show ?C1 by (simp add: initialized_def)
berghofe@45044
    63
  from
berghofe@45044
    64
    `initialized2 (Field1 (a loop__1__i)) loop__2__j`
berghofe@45044
    65
    `initialized3 (Field1 (a loop__1__i)) loop__2__j (pos Sun)`
berghofe@45044
    66
  show ?C2
berghofe@45044
    67
    apply (auto simp add: initialized2_def initialized3_def)
berghofe@45044
    68
    apply (case_tac "j = loop__2__j")
berghofe@45044
    69
    apply auto
berghofe@45044
    70
    apply (case_tac "ja = 6")
berghofe@45044
    71
    apply auto
berghofe@45044
    72
    done
berghofe@45044
    73
  from H5
berghofe@45044
    74
  show ?C3 by simp
berghofe@45044
    75
qed
berghofe@45044
    76
berghofe@45044
    77
spark_vc procedure_initialize_5
berghofe@45044
    78
  by (simp add: initialized3_def)
berghofe@45044
    79
berghofe@45044
    80
spark_vc procedure_initialize_6
berghofe@45044
    81
proof -
berghofe@45044
    82
  from `initialized a loop__1__i`
berghofe@45044
    83
  show ?C1 by (simp add: initialized_def)
berghofe@45044
    84
  from `initialized2 (Field1 (a loop__1__i)) loop__2__j`
berghofe@45044
    85
  show ?C2 by (simp add: initialized2_def initialized3_def)
berghofe@45044
    86
  from
berghofe@45044
    87
    `initialized3 (Field1 (a loop__1__i)) loop__2__j (pos loop__3__k)`
berghofe@45044
    88
    `loop__3__k < Sun`
berghofe@45044
    89
    rangeI [of pos loop__3__k]
berghofe@45044
    90
  show ?C3
berghofe@45044
    91
    apply (auto simp add: initialized3_def succ_def less_pos pos_val range_pos)
berghofe@45044
    92
    apply (case_tac "j = pos loop__3__k")
berghofe@45044
    93
    apply (auto simp add: val_pos)
berghofe@45044
    94
    done
berghofe@45044
    95
  from H5
berghofe@45044
    96
  show ?C4 by simp
berghofe@45044
    97
qed
berghofe@45044
    98
berghofe@45044
    99
spark_vc procedure_initialize_9
berghofe@45044
   100
  using
berghofe@45044
   101
    `initialized a 9`
berghofe@45044
   102
    `initialized2 (Field1 (a 9)) 9`
berghofe@45044
   103
    `initialized3 (Field1 (a 9)) 9 (pos Sun)`
berghofe@45044
   104
  apply (auto simp add: initialized_def initialized2_def initialized3_def)
berghofe@45044
   105
  apply (case_tac "j = 9")
berghofe@45044
   106
  apply auto
berghofe@45044
   107
  apply (case_tac "ja = 6")
berghofe@45044
   108
  apply auto
berghofe@45044
   109
  done
berghofe@45044
   110
berghofe@45044
   111
spark_end
berghofe@45044
   112
(*>*)
berghofe@45044
   113
berghofe@45044
   114
end