src/HOL/Bali/Basis.thy
author wenzelm
Wed, 10 Feb 2010 00:45:16 +0100
changeset 35067 af4c18c30593
parent 34915 7894c7dab132
child 35355 613e133966ea
child 35416 d8d7d1b785af
permissions -rw-r--r--
modernized syntax translations, using mostly abbreviation/notation; minor tuning;
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
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 16121
diff changeset
     6
theory Basis imports Main begin
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     7
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     8
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     9
section "misc"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    10
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    11
declare same_fstI [intro!] (*### TO HOL/Wellfounded_Relations *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    12
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    13
declare split_if_asm  [split] option.split [split] option.split_asm [split]
24019
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 22781
diff changeset
    14
declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    15
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
    16
declare length_Suc_conv [iff]
da548623916a removed or modified some instances of [iff]
paulson
parents: 17876
diff changeset
    17
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    18
lemma Collect_split_eq: "{p. P (split f p)} = {(a,b). P (f a b)}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    19
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    20
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    21
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    22
lemma subset_insertD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    23
  "A <= insert x B ==> A <= B & x ~: A | (EX B'. A = insert x B' & B' <= B)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    24
apply (case_tac "x:A")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    25
apply (rule disjI2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    26
apply (rule_tac x = "A-{x}" in exI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    27
apply fast+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    28
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    29
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 34915
diff changeset
    30
abbreviation nat3 :: nat  ("3") where "3 == Suc 2"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 34915
diff changeset
    31
abbreviation nat4 :: nat  ("4") where "4 == Suc 3"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    32
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    33
(*unused*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    34
lemma range_bool_domain: "range f = {f True, f False}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    35
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    36
apply (case_tac "xa")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    37
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    38
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    39
13867
1fdecd15437f just a few mods to a few thms
nipkow
parents: 13688
diff changeset
    40
(* irrefl_tranclI in Transitive_Closure.thy is more general *)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    41
lemma irrefl_tranclI': "r^-1 Int r^+ = {} ==> !x. (x, x) ~: r^+"
13867
1fdecd15437f just a few mods to a few thms
nipkow
parents: 13688
diff changeset
    42
by(blast elim: tranclE dest: trancl_into_rtrancl)
1fdecd15437f just a few mods to a few thms
nipkow
parents: 13688
diff changeset
    43
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    44
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    45
lemma trancl_rtrancl_trancl:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    46
"\<lbrakk>(x,y)\<in>r^+; (y,z)\<in>r^*\<rbrakk> \<Longrightarrow> (x,z)\<in>r^+"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    47
by (auto dest: tranclD rtrancl_trans rtrancl_into_trancl2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    48
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    49
lemma rtrancl_into_trancl3:
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
    50
"\<lbrakk>(a,b)\<in>r^*; a\<noteq>b\<rbrakk> \<Longrightarrow> (a,b)\<in>r^+" 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    51
apply (drule rtranclD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    52
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    53
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    54
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    55
lemma rtrancl_into_rtrancl2: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    56
  "\<lbrakk> (a, b) \<in>  r; (b, c) \<in> r^* \<rbrakk> \<Longrightarrow> (a, c) \<in>  r^*"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    57
by (auto intro: r_into_rtrancl rtrancl_trans)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    58
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    59
lemma triangle_lemma:
32376
66b4946d9483 reverted accidential corruption of superscripts introduced in a508148f7c25
krauss
parents: 32367
diff changeset
    60
 "\<lbrakk> \<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c; (a,x)\<in>r\<^sup>*; (a,y)\<in>r\<^sup>*\<rbrakk> 
66b4946d9483 reverted accidential corruption of superscripts introduced in a508148f7c25
krauss
parents: 32367
diff changeset
    61
 \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    62
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    63
  assume unique: "\<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c"
32376
66b4946d9483 reverted accidential corruption of superscripts introduced in a508148f7c25
krauss
parents: 32367
diff changeset
    64
  assume "(a,x)\<in>r\<^sup>*" 
66b4946d9483 reverted accidential corruption of superscripts introduced in a508148f7c25
krauss
parents: 32367
diff changeset
    65
  then show "(a,y)\<in>r\<^sup>* \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    66
  proof (induct rule: converse_rtrancl_induct)
32376
66b4946d9483 reverted accidential corruption of superscripts introduced in a508148f7c25
krauss
parents: 32367
diff changeset
    67
    assume "(x,y)\<in>r\<^sup>*"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    68
    then show ?thesis 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    69
      by blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    70
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    71
    fix a v
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    72
    assume a_v_r: "(a, v) \<in> r" and
32376
66b4946d9483 reverted accidential corruption of superscripts introduced in a508148f7c25
krauss
parents: 32367
diff changeset
    73
          v_x_rt: "(v, x) \<in> r\<^sup>*" and
66b4946d9483 reverted accidential corruption of superscripts introduced in a508148f7c25
krauss
parents: 32367
diff changeset
    74
          a_y_rt: "(a, y) \<in> r\<^sup>*"  and
66b4946d9483 reverted accidential corruption of superscripts introduced in a508148f7c25
krauss
parents: 32367
diff changeset
    75
             hyp: "(v, y) \<in> r\<^sup>* \<Longrightarrow> (x, y) \<in> r\<^sup>* \<or> (y, x) \<in> r\<^sup>*"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    76
    from a_y_rt 
32376
66b4946d9483 reverted accidential corruption of superscripts introduced in a508148f7c25
krauss
parents: 32367
diff changeset
    77
    show "(x, y) \<in> r\<^sup>* \<or> (y, x) \<in> r\<^sup>*"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    78
    proof (cases rule: converse_rtranclE)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    79
      assume "a=y"
32376
66b4946d9483 reverted accidential corruption of superscripts introduced in a508148f7c25
krauss
parents: 32367
diff changeset
    80
      with a_v_r v_x_rt have "(y,x) \<in> r\<^sup>*"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32376
diff changeset
    81
        by (auto intro: r_into_rtrancl rtrancl_trans)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    82
      then show ?thesis 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32376
diff changeset
    83
        by blast
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    84
    next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    85
      fix w 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    86
      assume a_w_r: "(a, w) \<in> r" and
32376
66b4946d9483 reverted accidential corruption of superscripts introduced in a508148f7c25
krauss
parents: 32367
diff changeset
    87
            w_y_rt: "(w, y) \<in> r\<^sup>*"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    88
      from a_v_r a_w_r unique 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    89
      have "v=w" 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32376
diff changeset
    90
        by auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    91
      with w_y_rt hyp 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    92
      show ?thesis
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32376
diff changeset
    93
        by blast
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    94
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    95
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    96
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    97
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    98
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    99
lemma rtrancl_cases [consumes 1, case_names Refl Trancl]:
32376
66b4946d9483 reverted accidential corruption of superscripts introduced in a508148f7c25
krauss
parents: 32367
diff changeset
   100
 "\<lbrakk>(a,b)\<in>r\<^sup>*;  a = b \<Longrightarrow> P; (a,b)\<in>r\<^sup>+ \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   101
apply (erule rtranclE)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   102
apply (auto dest: rtrancl_into_trancl1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   103
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   104
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   105
(* context (theory "Set") *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   106
lemma Ball_weaken:"\<lbrakk>Ball s P;\<And> x. P x\<longrightarrow>Q x\<rbrakk>\<Longrightarrow>Ball s Q"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   107
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   108
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   109
(* context (theory "Finite") *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   110
lemma finite_SetCompr2: "[| finite (Collect P); !y. P y --> finite (range (f y)) |] ==>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   111
  finite {f y x |x y. P y}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   112
apply (subgoal_tac "{f y x |x y. P y} = UNION (Collect P) (%y. range (f y))")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   113
prefer 2 apply  fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   114
apply (erule ssubst)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   115
apply (erule finite_UN_I)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   116
apply fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   117
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   118
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   119
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   120
(* ### TO theory "List" *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   121
lemma list_all2_trans: "\<forall> a b c. P1 a b \<longrightarrow> P2 b c \<longrightarrow> P3 a c \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   122
 \<forall>xs2 xs3. list_all2 P1 xs1 xs2 \<longrightarrow> list_all2 P2 xs2 xs3 \<longrightarrow> list_all2 P3 xs1 xs3"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   123
apply (induct_tac "xs1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   124
apply simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   125
apply (rule allI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   126
apply (induct_tac "xs2")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   127
apply simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   128
apply (rule allI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   129
apply (induct_tac "xs3")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   130
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   131
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   132
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   133
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   134
section "pairs"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   135
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   136
lemma surjective_pairing5: "p = (fst p, fst (snd p), fst (snd (snd p)), fst (snd (snd (snd p))), 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   137
  snd (snd (snd (snd p))))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   138
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   139
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   140
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   141
lemma fst_splitE [elim!]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   142
"[| fst s' = x';  !!x s. [| s' = (x,s);  x = x' |] ==> Q |] ==> Q"
26349
7f5a2f6d9119 tuned proof
haftmann
parents: 24194
diff changeset
   143
by (cases s') auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   144
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   145
lemma fst_in_set_lemma [rule_format (no_asm)]: "(x, y) : set l --> x : fst ` set l"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   146
apply (induct_tac "l")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   147
apply  auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   148
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   149
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   150
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   151
section "quantifiers"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   152
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   153
lemma All_Ex_refl_eq2 [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   154
 "(!x. (? b. x = f b & Q b) \<longrightarrow> P x) = (!b. Q b --> P (f b))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   155
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   156
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   157
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   158
lemma ex_ex_miniscope1 [simp]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   159
  "(EX w v. P w v & Q v) = (EX v. (EX w. P w v) & Q v)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   160
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   161
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   162
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   163
lemma ex_miniscope2 [simp]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   164
  "(EX v. P v & Q & R v) = (Q & (EX v. P v & R v))" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   165
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   166
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   167
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   168
lemma ex_reorder31: "(\<exists>z x y. P x y z) = (\<exists>x y z. P x y z)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   169
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   170
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   171
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   172
lemma All_Ex_refl_eq1 [simp]: "(!x. (? b. x = f b) --> P x) = (!b. P (f b))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   173
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   174
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   175
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   176
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   177
section "sums"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   178
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   179
hide const In0 In1
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   180
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 34915
diff changeset
   181
notation sum_case  (infixr "'(+')"80)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   182
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   183
consts    the_Inl  :: "'a + 'b \<Rightarrow> 'a"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   184
          the_Inr  :: "'a + 'b \<Rightarrow> 'b"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   185
primrec  "the_Inl (Inl a) = a"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   186
primrec  "the_Inr (Inr b) = b"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   187
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   188
datatype ('a, 'b, 'c) sum3 = In1 'a | In2 'b | In3 'c
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   189
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   190
consts    the_In1  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'a"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   191
          the_In2  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'b"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   192
          the_In3  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   193
primrec  "the_In1 (In1 a) = a"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   194
primrec  "the_In2 (In2 b) = b"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   195
primrec  "the_In3 (In3 c) = c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   196
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 34915
diff changeset
   197
abbreviation In1l   :: "'al \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 34915
diff changeset
   198
      where "In1l e == In1 (Inl e)"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 34915
diff changeset
   199
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 34915
diff changeset
   200
abbreviation In1r   :: "'ar \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 34915
diff changeset
   201
      where "In1r c == In1 (Inr c)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   202
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 34915
diff changeset
   203
abbreviation the_In1l :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'al"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 34915
diff changeset
   204
      where "the_In1l == the_Inl \<circ> the_In1"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 34915
diff changeset
   205
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 34915
diff changeset
   206
abbreviation the_In1r :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'ar"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 34915
diff changeset
   207
      where "the_In1r == 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
   208
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   209
ML {*
27226
5a3e5e46d977 sum3_instantiate: proper context;
wenzelm
parents: 27153
diff changeset
   210
fun sum3_instantiate ctxt thm = map (fn s =>
32149
ef59550a55d3 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
wenzelm
parents: 30235
diff changeset
   211
  simplify (simpset_of ctxt delsimps[@{thm not_None_eq}])
27239
f2f42f9fa09d pervasive RuleInsts;
wenzelm
parents: 27226
diff changeset
   212
    (read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?x")] thm)) ["1l","2","3","1r"]
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   213
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   214
(* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   215
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   216
translations
33965
f57c11db4ad4 Inl and Inr now with authentic syntax
haftmann
parents: 32960
diff changeset
   217
  "option"<= (type) "Option.option"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   218
  "list"  <= (type) "List.list"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   219
  "sum3"  <= (type) "Basis.sum3"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   220
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   221
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   222
section "quantifiers for option type"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   223
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   224
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   225
  Oall :: "[pttrn, 'a option, bool] => bool"   ("(3! _:_:/ _)" [0,0,10] 10)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   226
  Oex  :: "[pttrn, 'a option, bool] => bool"   ("(3? _:_:/ _)" [0,0,10] 10)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   227
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   228
syntax (symbols)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   229
  Oall :: "[pttrn, 'a option, bool] => bool"   ("(3\<forall>_\<in>_:/ _)"  [0,0,10] 10)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   230
  Oex  :: "[pttrn, 'a option, bool] => bool"   ("(3\<exists>_\<in>_:/ _)"  [0,0,10] 10)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   231
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   232
translations
30235
58d147683393 Made Option a separate theory and renamed option_map to Option.map
nipkow
parents: 27239
diff changeset
   233
  "! x:A: P"    == "! x:CONST Option.set A. P"
58d147683393 Made Option a separate theory and renamed option_map to Option.map
nipkow
parents: 27239
diff changeset
   234
  "? x:A: P"    == "? x:CONST Option.set A. P"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   235
19323
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   236
section "Special map update"
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   237
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   238
text{* Deemed too special for theory Map. *}
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   239
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   240
constdefs
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   241
  chg_map :: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   242
 "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   243
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   244
lemma chg_map_new[simp]: "m a = None   ==> chg_map f a m = m"
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   245
by (unfold chg_map_def, auto)
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   246
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   247
lemma chg_map_upd[simp]: "m a = Some b ==> chg_map f a m = m(a|->f b)"
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   248
by (unfold chg_map_def, auto)
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   249
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   250
lemma chg_map_other [simp]: "a \<noteq> b \<Longrightarrow> chg_map f a m b = m b"
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   251
by (auto simp: chg_map_def split add: option.split)
ec5cd5b1804c Converted translations to abbbreviations.
nipkow
parents: 18576
diff changeset
   252
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   253
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   254
section "unique association lists"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   255
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   256
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   257
  unique   :: "('a \<times> 'b) list \<Rightarrow> bool"
12893
cbb4dc5e6478 replaced nodups by distinct;
wenzelm
parents: 12859
diff changeset
   258
 "unique \<equiv> distinct \<circ> map fst"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   259
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   260
lemma uniqueD [rule_format (no_asm)]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   261
"unique l--> (!x y. (x,y):set l --> (!x' y'. (x',y'):set l --> x=x'-->  y=y'))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   262
apply (unfold unique_def o_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   263
apply (induct_tac "l")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   264
apply  (auto dest: fst_in_set_lemma)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   265
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   266
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   267
lemma unique_Nil [simp]: "unique []"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   268
apply (unfold unique_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   269
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   270
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   271
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   272
lemma unique_Cons [simp]: "unique ((x,y)#l) = (unique l & (!y. (x,y) ~: set l))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   273
apply (unfold unique_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   274
apply  (auto dest: fst_in_set_lemma)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   275
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   276
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   277
lemmas unique_ConsI = conjI [THEN unique_Cons [THEN iffD2], standard]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   278
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   279
lemma unique_single [simp]: "!!p. unique [p]"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   280
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   281
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   282
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   283
lemma unique_ConsD: "unique (x#xs) ==> unique xs"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   284
apply (simp add: unique_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   285
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   286
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   287
lemma unique_append [rule_format (no_asm)]: "unique l' ==> unique l -->  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   288
  (!(x,y):set l. !(x',y'):set l'. x' ~= x) --> unique (l @ l')"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   289
apply (induct_tac "l")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   290
apply  (auto dest: fst_in_set_lemma)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   291
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   292
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   293
lemma unique_map_inj [rule_format (no_asm)]: "unique l --> inj f --> unique (map (%(k,x). (f k, g k x)) l)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   294
apply (induct_tac "l")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   295
apply  (auto dest: fst_in_set_lemma simp add: inj_eq)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   296
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   297
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   298
lemma map_of_SomeI [rule_format (no_asm)]: "unique l --> (k, x) : set l --> map_of l k = Some x"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   299
apply (induct_tac "l")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   300
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   301
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   302
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   303
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   304
section "list patterns"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   305
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   306
consts
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   307
  lsplit         :: "[['a, 'a list] => 'b, 'a list] => 'b"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   308
defs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   309
  lsplit_def:    "lsplit == %f l. f (hd l) (tl l)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   310
(*  list patterns -- extends pre-defined type "pttrn" used in abstractions *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   311
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   312
  "_lpttrn"    :: "[pttrn,pttrn] => pttrn"     ("_#/_" [901,900] 900)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   313
translations
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 34915
diff changeset
   314
  "%y#x#xs. b"  == "CONST lsplit (%y x#xs. b)"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 34915
diff changeset
   315
  "%x#xs  . b"  == "CONST lsplit (%x xs  . b)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   316
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   317
lemma lsplit [simp]: "lsplit c (x#xs) = c x xs"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   318
apply (unfold lsplit_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   319
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   320
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   321
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   322
lemma lsplit2 [simp]: "lsplit P (x#xs) y z = P x xs y z"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   323
apply (unfold lsplit_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   324
apply simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   325
done 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   326
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   327
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   328
end