src/HOL/Bali/Basis.thy
author wenzelm
Thu, 18 Apr 2013 17:07:01 +0200
changeset 51717 9e7d1c139569
parent 51304 0e71a248cacb
child 52037 837211662fb8
permissions -rw-r--r--
simplifier uses proper Proof.context instead of historic type simpset;
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
51304
0e71a248cacb marginalized historic strip_tac;
wenzelm
parents: 45151
diff changeset
    12
ML {* fun strip_tac i = REPEAT (resolve_tac [impI, allI] i) *}
0e71a248cacb marginalized historic strip_tac;
wenzelm
parents: 45151
diff changeset
    13
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    14
declare split_if_asm  [split] option.split [split] option.split_asm [split]
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51304
diff changeset
    15
setup {* map_theory_simpset (fn ctxt => ctxt addloop' ("split_all_tac", split_all_tac)) *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    16
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
    17
declare length_Suc_conv [iff]
da548623916a removed or modified some instances of [iff]
paulson
parents: 17876
diff changeset
    18
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    19
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
    20
  by auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    21
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    22
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
    23
  apply (case_tac "x \<in> A")
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    24
   apply (rule disjI2)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    25
   apply (rule_tac x = "A - {x}" in exI)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    26
   apply fast+
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    27
  done
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    28
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    29
abbreviation nat3 :: nat  ("3") where "3 \<equiv> Suc 2"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    30
abbreviation nat4 :: nat  ("4") where "4 \<equiv> Suc 3"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    31
13867
1fdecd15437f just a few mods to a few thms
nipkow
parents: 13688
diff changeset
    32
(* irrefl_tranclI in Transitive_Closure.thy is more general *)
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    33
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
    34
  by (blast elim: tranclE dest: trancl_into_rtrancl)
13867
1fdecd15437f just a few mods to a few thms
nipkow
parents: 13688
diff changeset
    35
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    36
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    37
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
    38
  by (auto dest: tranclD rtrancl_trans rtrancl_into_trancl2)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    39
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    40
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
    41
  apply (drule rtranclD)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    42
  apply auto
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    43
  done
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    44
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    45
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
    46
  by (auto intro: rtrancl_trans)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    47
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    48
lemma triangle_lemma:
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    49
  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
    50
    and ax: "(a,x)\<in>r\<^sup>*" and ay: "(a,y)\<in>r\<^sup>*"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    51
  shows "(x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    52
  using ax ay
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    53
proof (induct rule: converse_rtrancl_induct)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    54
  assume "(x,y)\<in>r\<^sup>*"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    55
  then show ?thesis by blast
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    56
next
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    57
  fix a v
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    58
  assume a_v_r: "(a, v) \<in> r"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    59
    and v_x_rt: "(v, x) \<in> r\<^sup>*"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    60
    and a_y_rt: "(a, y) \<in> r\<^sup>*"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    61
    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
    62
  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
    63
  proof (cases rule: converse_rtranclE)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    64
    assume "a = y"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    65
    with a_v_r v_x_rt have "(y,x) \<in> r\<^sup>*"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    66
      by (auto intro: rtrancl_trans)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    67
    then show ?thesis by blast
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    68
  next
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    69
    fix w
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    70
    assume a_w_r: "(a, w) \<in> r"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    71
      and w_y_rt: "(w, y) \<in> r\<^sup>*"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    72
    from a_v_r a_w_r unique have "v=w" by auto
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    73
    with w_y_rt hyp show ?thesis by blast
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    74
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    75
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    76
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    77
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    78
lemma rtrancl_cases:
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    79
  assumes "(a,b)\<in>r\<^sup>*"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    80
  obtains (Refl) "a = b"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    81
    | (Trancl) "(a,b)\<in>r\<^sup>+"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    82
  apply (rule rtranclE [OF assms])
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    83
   apply (auto dest: rtrancl_into_trancl1)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    84
  done
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    85
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    86
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
    87
  by auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    88
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    89
lemma finite_SetCompr2:
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    90
  "finite (Collect P) \<Longrightarrow> \<forall>y. P y \<longrightarrow> finite (range (f y)) \<Longrightarrow>
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    91
    finite {f y x |x y. P y}"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    92
  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
    93
   prefer 2 apply fast
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    94
  apply (erule ssubst)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    95
  apply (erule finite_UN_I)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    96
  apply fast
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    97
  done
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    98
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
    99
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
   100
    \<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
   101
  apply (induct_tac xs1)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   102
   apply simp
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   103
  apply (rule allI)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   104
  apply (induct_tac xs2)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   105
   apply simp
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   106
  apply (rule allI)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   107
  apply (induct_tac xs3)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   108
   apply auto
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   109
  done
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   110
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   111
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   112
section "pairs"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   113
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   114
lemma surjective_pairing5:
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   115
  "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
   116
    snd (snd (snd (snd p))))"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   117
  by auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   118
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   119
lemma fst_splitE [elim!]:
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   120
  assumes "fst s' = x'"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   121
  obtains x s where "s' = (x,s)" and "x = x'"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   122
  using assms by (cases s') auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   123
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   124
lemma fst_in_set_lemma: "(x, y) : set l \<Longrightarrow> x : fst ` set l"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   125
  by (induct l) auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   126
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   127
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   128
section "quantifiers"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   129
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   130
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
   131
  by auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   132
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   133
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
   134
  by auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   135
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   136
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
   137
  by auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   138
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   139
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
   140
  by auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   141
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   142
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
   143
  by auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   144
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   145
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   146
section "sums"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   147
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
   148
hide_const In0 In1
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   149
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 34915
diff changeset
   150
notation sum_case  (infixr "'(+')"80)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   151
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   152
primrec the_Inl :: "'a + 'b \<Rightarrow> 'a"
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36176
diff changeset
   153
  where "the_Inl (Inl a) = a"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36176
diff changeset
   154
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   155
primrec the_Inr :: "'a + 'b \<Rightarrow> 'b"
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36176
diff changeset
   156
  where "the_Inr (Inr b) = b"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   157
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   158
datatype ('a, 'b, 'c) sum3 = In1 'a | In2 'b | In3 'c
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   159
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   160
primrec the_In1 :: "('a, 'b, 'c) sum3 \<Rightarrow> 'a"
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36176
diff changeset
   161
  where "the_In1 (In1 a) = a"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36176
diff changeset
   162
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   163
primrec the_In2 :: "('a, 'b, 'c) sum3 \<Rightarrow> 'b"
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36176
diff changeset
   164
  where "the_In2 (In2 b) = b"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36176
diff changeset
   165
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   166
primrec the_In3 :: "('a, 'b, 'c) sum3 \<Rightarrow> 'c"
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36176
diff changeset
   167
  where "the_In3 (In3 c) = c"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   168
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   169
abbreviation In1l :: "'al \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   170
  where "In1l e \<equiv> In1 (Inl e)"
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 34915
diff changeset
   171
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   172
abbreviation In1r :: "'ar \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   173
  where "In1r c \<equiv> In1 (Inr c)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   174
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 34915
diff changeset
   175
abbreviation the_In1l :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'al"
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   176
  where "the_In1l \<equiv> the_Inl \<circ> the_In1"
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 34915
diff changeset
   177
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 34915
diff changeset
   178
abbreviation the_In1r :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'ar"
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   179
  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
   180
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   181
ML {*
27226
5a3e5e46d977 sum3_instantiate: proper context;
wenzelm
parents: 27153
diff changeset
   182
fun sum3_instantiate ctxt thm = map (fn s =>
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51304
diff changeset
   183
  simplify (ctxt delsimps [@{thm not_None_eq}])
27239
f2f42f9fa09d pervasive RuleInsts;
wenzelm
parents: 27226
diff changeset
   184
    (read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?x")] thm)) ["1l","2","3","1r"]
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   185
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   186
(* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   187
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   188
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   189
section "quantifiers for option type"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   190
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   191
syntax
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   192
  "_Oall" :: "[pttrn, 'a option, bool] \<Rightarrow> bool"   ("(3! _:_:/ _)" [0,0,10] 10)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   193
  "_Oex"  :: "[pttrn, 'a option, bool] \<Rightarrow> bool"   ("(3? _:_:/ _)" [0,0,10] 10)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   194
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   195
syntax (symbols)
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   196
  "_Oall" :: "[pttrn, 'a option, bool] \<Rightarrow> bool"   ("(3\<forall>_\<in>_:/ _)"  [0,0,10] 10)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   197
  "_Oex"  :: "[pttrn, 'a option, bool] \<Rightarrow> bool"   ("(3\<exists>_\<in>_:/ _)"  [0,0,10] 10)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   198
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   199
translations
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   200
  "\<forall>x\<in>A: P" \<rightleftharpoons> "\<forall>x\<in>CONST Option.set A. P"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   201
  "\<exists>x\<in>A: P" \<rightleftharpoons> "\<exists>x\<in>CONST Option.set A. P"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   202
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   203
19323
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   204
section "Special map update"
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   205
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   206
text{* Deemed too special for theory Map. *}
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   207
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   208
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
   209
  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
   210
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   211
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
   212
  unfolding chg_map_def by auto
19323
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   213
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   214
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
   215
  unfolding chg_map_def by auto
19323
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   216
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   217
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
   218
  by (auto simp: chg_map_def)
19323
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   219
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   220
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   221
section "unique association lists"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   222
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   223
definition unique :: "('a \<times> 'b) list \<Rightarrow> bool"
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36176
diff changeset
   224
  where "unique = distinct \<circ> map fst"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   225
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   226
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
   227
  unfolding unique_def o_def
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   228
  by (induct l) (auto dest: fst_in_set_lemma)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   229
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   230
lemma unique_Nil [simp]: "unique []"
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   231
  by (simp add: unique_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   232
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   233
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
   234
  by (auto simp: unique_def dest: fst_in_set_lemma)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   235
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   236
lemma unique_ConsD: "unique (x#xs) \<Longrightarrow> unique xs"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   237
  by (simp add: unique_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   238
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   239
lemma unique_single [simp]: "\<And>p. unique [p]"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   240
  by simp
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   241
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   242
lemma unique_append [rule_format (no_asm)]: "unique l' \<Longrightarrow> unique l \<Longrightarrow>
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   243
    (\<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
   244
  by (induct l) (auto dest: fst_in_set_lemma)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   245
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   246
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
   247
  by (induct l) (auto dest: fst_in_set_lemma simp add: inj_eq)
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   248
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   249
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
   250
  by (induct l) auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   251
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   252
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   253
section "list patterns"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   254
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   255
definition lsplit :: "[['a, 'a list] \<Rightarrow> 'b, 'a list] \<Rightarrow> 'b"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   256
  where "lsplit = (\<lambda>f l. f (hd l) (tl l))"
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36176
diff changeset
   257
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36176
diff changeset
   258
text {* list patterns -- extends pre-defined type "pttrn" used in abstractions *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   259
syntax
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   260
  "_lpttrn" :: "[pttrn, pttrn] \<Rightarrow> pttrn"    ("_#/_" [901,900] 900)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   261
translations
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   262
  "\<lambda>y # x # xs. b" \<rightleftharpoons> "CONST lsplit (\<lambda>y x # xs. b)"
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   263
  "\<lambda>x # xs. b" \<rightleftharpoons> "CONST lsplit (\<lambda>x xs. b)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   264
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   265
lemma lsplit [simp]: "lsplit c (x#xs) = c x xs"
45151
2dd44cd8f963 misc tuning and modernization;
wenzelm
parents: 44013
diff changeset
   266
  by (simp add: lsplit_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   267
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   268
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
   269
  by (simp add: lsplit_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   270
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   271
end