src/HOL/Bali/Basis.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45151 2dd44cd8f963
child 51304 0e71a248cacb
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:
12857
a4386cc9b1c3 tuned header;
wenzelm
parents: 12854
diff changeset
     1
(*  Title:      HOL/Bali/Basis.thy
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     2
    Author:     David von Oheimb
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     3
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     4
header {* Definitions extending HOL as logical basis of Bali *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     5
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
     6
theory Basis
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
     7
imports Main "~~/src/HOL/Library/Old_Recdef"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
     8
begin
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     9
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    10
section "misc"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    11
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    12
declare split_if_asm  [split] option.split [split] option.split_asm [split]
24019
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 22781
diff changeset
    13
declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    14
declare if_weak_cong [cong del] option.weak_case_cong [cong del]
18447
da548623916a removed or modified some instances of [iff]
paulson
parents: 17876
diff changeset
    15
declare length_Suc_conv [iff]
da548623916a removed or modified some instances of [iff]
paulson
parents: 17876
diff changeset
    16
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    17
lemma Collect_split_eq: "{p. P (split f p)} = {(a,b). P (f a b)}"
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    18
  by auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    19
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    20
lemma subset_insertD: "A \<subseteq> insert x B \<Longrightarrow> A \<subseteq> B \<and> x \<notin> A \<or> (\<exists>B'. A = insert x B' \<and> B' \<subseteq> B)"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    21
  apply (case_tac "x \<in> A")
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    22
   apply (rule disjI2)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    23
   apply (rule_tac x = "A - {x}" in exI)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    24
   apply fast+
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    25
  done
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    26
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    27
abbreviation nat3 :: nat  ("3") where "3 \<equiv> Suc 2"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    28
abbreviation nat4 :: nat  ("4") where "4 \<equiv> Suc 3"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    29
13867
1fdecd15437f just a few mods to a few thms
nipkow
parents: 13688
diff changeset
    30
(* irrefl_tranclI in Transitive_Closure.thy is more general *)
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    31
lemma irrefl_tranclI': "r\<inverse> \<inter> r\<^sup>+ = {} \<Longrightarrow> \<forall>x. (x, x) \<notin> r\<^sup>+"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    32
  by (blast elim: tranclE dest: trancl_into_rtrancl)
13867
1fdecd15437f just a few mods to a few thms
nipkow
parents: 13688
diff changeset
    33
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    34
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    35
lemma trancl_rtrancl_trancl: "\<lbrakk>(x, y) \<in> r\<^sup>+; (y, z) \<in> r\<^sup>*\<rbrakk> \<Longrightarrow> (x, z) \<in> r\<^sup>+"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    36
  by (auto dest: tranclD rtrancl_trans rtrancl_into_trancl2)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    37
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    38
lemma rtrancl_into_trancl3: "\<lbrakk>(a, b) \<in> r\<^sup>*; a \<noteq> b\<rbrakk> \<Longrightarrow> (a, b) \<in> r\<^sup>+"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    39
  apply (drule rtranclD)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    40
  apply auto
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    41
  done
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    42
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    43
lemma rtrancl_into_rtrancl2: "\<lbrakk>(a, b) \<in>  r; (b, c) \<in> r\<^sup>*\<rbrakk> \<Longrightarrow> (a, c) \<in> r\<^sup>*"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    44
  by (auto intro: rtrancl_trans)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    45
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    46
lemma triangle_lemma:
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    47
  assumes unique: "\<And>a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b = c"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    48
    and ax: "(a,x)\<in>r\<^sup>*" and ay: "(a,y)\<in>r\<^sup>*"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    49
  shows "(x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    50
  using ax ay
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    51
proof (induct rule: converse_rtrancl_induct)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    52
  assume "(x,y)\<in>r\<^sup>*"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    53
  then show ?thesis by blast
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    54
next
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    55
  fix a v
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    56
  assume a_v_r: "(a, v) \<in> r"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    57
    and v_x_rt: "(v, x) \<in> r\<^sup>*"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    58
    and a_y_rt: "(a, y) \<in> r\<^sup>*"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    59
    and hyp: "(v, y) \<in> r\<^sup>* \<Longrightarrow> (x, y) \<in> r\<^sup>* \<or> (y, x) \<in> r\<^sup>*"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    60
  from a_y_rt show "(x, y) \<in> r\<^sup>* \<or> (y, x) \<in> r\<^sup>*"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    61
  proof (cases rule: converse_rtranclE)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    62
    assume "a = y"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    63
    with a_v_r v_x_rt have "(y,x) \<in> r\<^sup>*"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    64
      by (auto intro: rtrancl_trans)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    65
    then show ?thesis by blast
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    66
  next
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    67
    fix w
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    68
    assume a_w_r: "(a, w) \<in> r"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    69
      and w_y_rt: "(w, y) \<in> r\<^sup>*"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    70
    from a_v_r a_w_r unique have "v=w" by auto
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    71
    with w_y_rt hyp show ?thesis by blast
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    72
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    73
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    74
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    75
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    76
lemma rtrancl_cases:
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    77
  assumes "(a,b)\<in>r\<^sup>*"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    78
  obtains (Refl) "a = b"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    79
    | (Trancl) "(a,b)\<in>r\<^sup>+"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    80
  apply (rule rtranclE [OF assms])
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    81
   apply (auto dest: rtrancl_into_trancl1)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    82
  done
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    83
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    84
lemma Ball_weaken: "\<lbrakk>Ball s P; \<And> x. P x\<longrightarrow>Q x\<rbrakk>\<Longrightarrow>Ball s Q"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    85
  by auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    86
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    87
lemma finite_SetCompr2:
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    88
  "finite (Collect P) \<Longrightarrow> \<forall>y. P y \<longrightarrow> finite (range (f y)) \<Longrightarrow>
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    89
    finite {f y x |x y. P y}"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    90
  apply (subgoal_tac "{f y x |x y. P y} = UNION (Collect P) (\<lambda>y. range (f y))")
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    91
   prefer 2 apply fast
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    92
  apply (erule ssubst)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    93
  apply (erule finite_UN_I)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    94
  apply fast
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    95
  done
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    96
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    97
lemma list_all2_trans: "\<forall>a b c. P1 a b \<longrightarrow> P2 b c \<longrightarrow> P3 a c \<Longrightarrow>
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    98
    \<forall>xs2 xs3. list_all2 P1 xs1 xs2 \<longrightarrow> list_all2 P2 xs2 xs3 \<longrightarrow> list_all2 P3 xs1 xs3"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    99
  apply (induct_tac xs1)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   100
   apply simp
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   101
  apply (rule allI)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   102
  apply (induct_tac xs2)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   103
   apply simp
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   104
  apply (rule allI)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   105
  apply (induct_tac xs3)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   106
   apply auto
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   107
  done
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   108
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   109
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   110
section "pairs"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   111
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   112
lemma surjective_pairing5:
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   113
  "p = (fst p, fst (snd p), fst (snd (snd p)), fst (snd (snd (snd p))),
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   114
    snd (snd (snd (snd p))))"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   115
  by auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   116
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   117
lemma fst_splitE [elim!]:
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   118
  assumes "fst s' = x'"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   119
  obtains x s where "s' = (x,s)" and "x = x'"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   120
  using assms by (cases s') auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   121
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   122
lemma fst_in_set_lemma: "(x, y) : set l \<Longrightarrow> x : fst ` set l"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   123
  by (induct l) auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   124
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   125
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   126
section "quantifiers"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   127
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   128
lemma All_Ex_refl_eq2 [simp]: "(\<forall>x. (\<exists>b. x = f b \<and> Q b) \<longrightarrow> P x) = (\<forall>b. Q b \<longrightarrow> P (f b))"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   129
  by auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   130
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   131
lemma ex_ex_miniscope1 [simp]: "(\<exists>w v. P w v \<and> Q v) = (\<exists>v. (\<exists>w. P w v) \<and> Q v)"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   132
  by auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   133
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   134
lemma ex_miniscope2 [simp]: "(\<exists>v. P v \<and> Q \<and> R v) = (Q \<and> (\<exists>v. P v \<and> R v))"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   135
  by auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   136
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   137
lemma ex_reorder31: "(\<exists>z x y. P x y z) = (\<exists>x y z. P x y z)"
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   138
  by auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   139
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   140
lemma All_Ex_refl_eq1 [simp]: "(\<forall>x. (\<exists>b. x = f b) \<longrightarrow> P x) = (\<forall>b. P (f b))"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   141
  by auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   142
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   143
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   144
section "sums"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   145
36176
3fe7e97ccca8 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
wenzelm
parents: 35431
diff changeset
   146
hide_const In0 In1
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   147
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 34915
diff changeset
   148
notation sum_case  (infixr "'(+')"80)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   149
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   150
primrec the_Inl :: "'a + 'b \<Rightarrow> 'a"
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36176
diff changeset
   151
  where "the_Inl (Inl a) = a"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36176
diff changeset
   152
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   153
primrec the_Inr :: "'a + 'b \<Rightarrow> 'b"
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36176
diff changeset
   154
  where "the_Inr (Inr b) = b"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   155
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   156
datatype ('a, 'b, 'c) sum3 = In1 'a | In2 'b | In3 'c
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   157
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   158
primrec the_In1 :: "('a, 'b, 'c) sum3 \<Rightarrow> 'a"
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36176
diff changeset
   159
  where "the_In1 (In1 a) = a"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36176
diff changeset
   160
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   161
primrec the_In2 :: "('a, 'b, 'c) sum3 \<Rightarrow> 'b"
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36176
diff changeset
   162
  where "the_In2 (In2 b) = b"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36176
diff changeset
   163
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   164
primrec the_In3 :: "('a, 'b, 'c) sum3 \<Rightarrow> 'c"
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36176
diff changeset
   165
  where "the_In3 (In3 c) = c"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   166
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   167
abbreviation In1l :: "'al \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   168
  where "In1l e \<equiv> In1 (Inl e)"
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 34915
diff changeset
   169
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   170
abbreviation In1r :: "'ar \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   171
  where "In1r c \<equiv> In1 (Inr c)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   172
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 34915
diff changeset
   173
abbreviation the_In1l :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'al"
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   174
  where "the_In1l \<equiv> the_Inl \<circ> the_In1"
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 34915
diff changeset
   175
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 34915
diff changeset
   176
abbreviation the_In1r :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'ar"
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   177
  where "the_In1r \<equiv> the_Inr \<circ> the_In1"
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13462
diff changeset
   178
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   179
ML {*
27226
5a3e5e46d977 sum3_instantiate: proper context;
wenzelm
parents: 27153
diff changeset
   180
fun sum3_instantiate ctxt thm = map (fn s =>
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   181
  simplify (simpset_of ctxt delsimps [@{thm not_None_eq}])
27239
f2f42f9fa09d pervasive RuleInsts;
wenzelm
parents: 27226
diff changeset
   182
    (read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?x")] thm)) ["1l","2","3","1r"]
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   183
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   184
(* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   185
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   186
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   187
section "quantifiers for option type"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   188
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   189
syntax
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   190
  "_Oall" :: "[pttrn, 'a option, bool] \<Rightarrow> bool"   ("(3! _:_:/ _)" [0,0,10] 10)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   191
  "_Oex"  :: "[pttrn, 'a option, bool] \<Rightarrow> bool"   ("(3? _:_:/ _)" [0,0,10] 10)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   192
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   193
syntax (symbols)
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   194
  "_Oall" :: "[pttrn, 'a option, bool] \<Rightarrow> bool"   ("(3\<forall>_\<in>_:/ _)"  [0,0,10] 10)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   195
  "_Oex"  :: "[pttrn, 'a option, bool] \<Rightarrow> bool"   ("(3\<exists>_\<in>_:/ _)"  [0,0,10] 10)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   196
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   197
translations
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   198
  "\<forall>x\<in>A: P" \<rightleftharpoons> "\<forall>x\<in>CONST Option.set A. P"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   199
  "\<exists>x\<in>A: P" \<rightleftharpoons> "\<exists>x\<in>CONST Option.set A. P"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   200
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   201
19323
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   202
section "Special map update"
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   203
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   204
text{* Deemed too special for theory Map. *}
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   205
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   206
definition chg_map :: "('b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   207
  where "chg_map f a m = (case m a of None \<Rightarrow> m | Some b \<Rightarrow> m(a\<mapsto>f b))"
19323
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   208
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   209
lemma chg_map_new[simp]: "m a = None \<Longrightarrow> chg_map f a m = m"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   210
  unfolding chg_map_def by auto
19323
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   211
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   212
lemma chg_map_upd[simp]: "m a = Some b \<Longrightarrow> chg_map f a m = m(a\<mapsto>f b)"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   213
  unfolding chg_map_def by auto
19323
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   214
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   215
lemma chg_map_other [simp]: "a \<noteq> b \<Longrightarrow> chg_map f a m b = m b"
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   216
  by (auto simp: chg_map_def)
19323
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   217
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   218
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   219
section "unique association lists"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   220
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   221
definition unique :: "('a \<times> 'b) list \<Rightarrow> bool"
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36176
diff changeset
   222
  where "unique = distinct \<circ> map fst"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   223
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   224
lemma uniqueD: "unique l \<Longrightarrow> (x, y) \<in> set l \<Longrightarrow> (x', y') \<in> set l \<Longrightarrow> x = x' \<Longrightarrow> y = y'"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   225
  unfolding unique_def o_def
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   226
  by (induct l) (auto dest: fst_in_set_lemma)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   227
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   228
lemma unique_Nil [simp]: "unique []"
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   229
  by (simp add: unique_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   230
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   231
lemma unique_Cons [simp]: "unique ((x,y)#l) = (unique l \<and> (\<forall>y. (x,y) \<notin> set l))"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   232
  by (auto simp: unique_def dest: fst_in_set_lemma)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   233
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   234
lemma unique_ConsD: "unique (x#xs) \<Longrightarrow> unique xs"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   235
  by (simp add: unique_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   236
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   237
lemma unique_single [simp]: "\<And>p. unique [p]"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   238
  by simp
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   239
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   240
lemma unique_append [rule_format (no_asm)]: "unique l' \<Longrightarrow> unique l \<Longrightarrow>
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   241
    (\<forall>(x,y)\<in>set l. \<forall>(x',y')\<in>set l'. x' \<noteq> x) \<longrightarrow> unique (l @ l')"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   242
  by (induct l) (auto dest: fst_in_set_lemma)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   243
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   244
lemma unique_map_inj: "unique l \<Longrightarrow> inj f \<Longrightarrow> unique (map (\<lambda>(k,x). (f k, g k x)) l)"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   245
  by (induct l) (auto dest: fst_in_set_lemma simp add: inj_eq)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   246
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   247
lemma map_of_SomeI: "unique l \<Longrightarrow> (k, x) : set l \<Longrightarrow> map_of l k = Some x"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   248
  by (induct l) auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   249
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   250
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   251
section "list patterns"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   252
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   253
definition lsplit :: "[['a, 'a list] \<Rightarrow> 'b, 'a list] \<Rightarrow> 'b"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   254
  where "lsplit = (\<lambda>f l. f (hd l) (tl l))"
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36176
diff changeset
   255
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36176
diff changeset
   256
text {* list patterns -- extends pre-defined type "pttrn" used in abstractions *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   257
syntax
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   258
  "_lpttrn" :: "[pttrn, pttrn] \<Rightarrow> pttrn"    ("_#/_" [901,900] 900)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   259
translations
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   260
  "\<lambda>y # x # xs. b" \<rightleftharpoons> "CONST lsplit (\<lambda>y x # xs. b)"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   261
  "\<lambda>x # xs. b" \<rightleftharpoons> "CONST lsplit (\<lambda>x xs. b)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   262
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   263
lemma lsplit [simp]: "lsplit c (x#xs) = c x xs"
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   264
  by (simp add: lsplit_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   265
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   266
lemma lsplit2 [simp]: "lsplit P (x#xs) y z = P x xs y z"
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   267
  by (simp add: lsplit_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   268
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   269
end