src/HOL/Bali/Basis.thy
author schirmer
Thu Oct 31 18:27:10 2002 +0100 (2002-10-31)
changeset 13688 a0b16d42d489
parent 13462 56610e2ba220
child 13867 1fdecd15437f
permissions -rw-r--r--
"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.
wenzelm@12857
     1
(*  Title:      HOL/Bali/Basis.thy
schirmer@12854
     2
    ID:         $Id$
schirmer@12854
     3
    Author:     David von Oheimb
wenzelm@12858
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
schirmer@12854
     5
schirmer@12854
     6
*)
schirmer@12854
     7
header {* Definitions extending HOL as logical basis of Bali *}
schirmer@12854
     8
schirmer@12854
     9
theory Basis = Main:
schirmer@12854
    10
schirmer@12854
    11
ML_setup {*
schirmer@12854
    12
Unify.search_bound := 40;
schirmer@12854
    13
Unify.trace_bound  := 40;
schirmer@12854
    14
*}
schirmer@12854
    15
(*print_depth 100;*)
schirmer@12854
    16
(*Syntax.ambiguity_level := 1;*)
schirmer@12854
    17
schirmer@12854
    18
section "misc"
schirmer@12854
    19
schirmer@12854
    20
declare same_fstI [intro!] (*### TO HOL/Wellfounded_Relations *)
schirmer@12854
    21
schirmer@12854
    22
ML {*
wenzelm@13462
    23
fun cond_simproc name pat pred thm = Simplifier.simproc (Thm.sign_of_thm thm) name [pat]
wenzelm@13462
    24
  (fn _ => fn _ => fn t => if pred t then None else Some (mk_meta_eq thm));
schirmer@12854
    25
*}
schirmer@12854
    26
schirmer@12854
    27
declare split_if_asm  [split] option.split [split] option.split_asm [split]
schirmer@12854
    28
ML {*
schirmer@12854
    29
simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
schirmer@12854
    30
*}
schirmer@12854
    31
declare if_weak_cong [cong del] option.weak_case_cong [cong del]
schirmer@12854
    32
declare length_Suc_conv [iff];
schirmer@12854
    33
schirmer@12854
    34
(*###to be phased out *)
schirmer@12854
    35
ML {*
schirmer@12854
    36
bind_thm ("make_imp", rearrange_prems [1,0] mp)
schirmer@12854
    37
*}
schirmer@12854
    38
schirmer@12854
    39
lemma Collect_split_eq: "{p. P (split f p)} = {(a,b). P (f a b)}"
schirmer@12854
    40
apply auto
schirmer@12854
    41
done
schirmer@12854
    42
schirmer@12854
    43
lemma subset_insertD: 
schirmer@12854
    44
  "A <= insert x B ==> A <= B & x ~: A | (EX B'. A = insert x B' & B' <= B)"
schirmer@12854
    45
apply (case_tac "x:A")
schirmer@12854
    46
apply (rule disjI2)
schirmer@12854
    47
apply (rule_tac x = "A-{x}" in exI)
schirmer@12854
    48
apply fast+
schirmer@12854
    49
done
schirmer@12854
    50
schirmer@12854
    51
syntax
schirmer@12925
    52
  "3" :: nat   ("3") 
schirmer@12854
    53
  "4" :: nat   ("4")
schirmer@12854
    54
translations
schirmer@12854
    55
 "3" == "Suc 2"
schirmer@12854
    56
 "4" == "Suc 3"
schirmer@12854
    57
schirmer@12854
    58
(*unused*)
schirmer@12854
    59
lemma range_bool_domain: "range f = {f True, f False}"
schirmer@12854
    60
apply auto
schirmer@12854
    61
apply (case_tac "xa")
schirmer@12854
    62
apply auto
schirmer@12854
    63
done
schirmer@12854
    64
schirmer@12854
    65
(* context (theory "Transitive_Closure") *)
schirmer@12854
    66
lemma irrefl_tranclI': "r^-1 Int r^+ = {} ==> !x. (x, x) ~: r^+"
schirmer@12854
    67
apply (rule allI)
schirmer@12854
    68
apply (erule irrefl_tranclI)
schirmer@12854
    69
done
schirmer@12854
    70
schirmer@12854
    71
lemma trancl_rtrancl_trancl:
schirmer@12854
    72
"\<lbrakk>(x,y)\<in>r^+; (y,z)\<in>r^*\<rbrakk> \<Longrightarrow> (x,z)\<in>r^+"
schirmer@12854
    73
by (auto dest: tranclD rtrancl_trans rtrancl_into_trancl2)
schirmer@12854
    74
schirmer@12854
    75
lemma rtrancl_into_trancl3:
schirmer@12925
    76
"\<lbrakk>(a,b)\<in>r^*; a\<noteq>b\<rbrakk> \<Longrightarrow> (a,b)\<in>r^+" 
schirmer@12854
    77
apply (drule rtranclD)
schirmer@12854
    78
apply auto
schirmer@12854
    79
done
schirmer@12854
    80
schirmer@12854
    81
lemma rtrancl_into_rtrancl2: 
schirmer@12854
    82
  "\<lbrakk> (a, b) \<in>  r; (b, c) \<in> r^* \<rbrakk> \<Longrightarrow> (a, c) \<in>  r^*"
schirmer@12854
    83
by (auto intro: r_into_rtrancl rtrancl_trans)
schirmer@12854
    84
schirmer@12854
    85
lemma triangle_lemma:
schirmer@12854
    86
 "\<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> 
schirmer@12854
    87
 \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
schirmer@12854
    88
proof -
schirmer@12854
    89
  note converse_rtrancl_induct = converse_rtrancl_induct [consumes 1]
schirmer@12854
    90
  note converse_rtranclE = converse_rtranclE [consumes 1] 
schirmer@12854
    91
  assume unique: "\<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c"
schirmer@12854
    92
  assume "(a,x)\<in>r\<^sup>*" 
schirmer@12854
    93
  then show "(a,y)\<in>r\<^sup>* \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
schirmer@12854
    94
  proof (induct rule: converse_rtrancl_induct)
schirmer@12854
    95
    assume "(x,y)\<in>r\<^sup>*"
schirmer@12854
    96
    then show ?thesis 
schirmer@12854
    97
      by blast
schirmer@12854
    98
  next
schirmer@12854
    99
    fix a v
schirmer@12854
   100
    assume a_v_r: "(a, v) \<in> r" and
schirmer@12854
   101
          v_x_rt: "(v, x) \<in> r\<^sup>*" and
schirmer@12854
   102
          a_y_rt: "(a, y) \<in> r\<^sup>*"  and
schirmer@12854
   103
             hyp: "(v, y) \<in> r\<^sup>* \<Longrightarrow> (x, y) \<in> r\<^sup>* \<or> (y, x) \<in> r\<^sup>*"
schirmer@12854
   104
    from a_y_rt 
schirmer@12854
   105
    show "(x, y) \<in> r\<^sup>* \<or> (y, x) \<in> r\<^sup>*"
schirmer@12854
   106
    proof (cases rule: converse_rtranclE)
schirmer@12854
   107
      assume "a=y"
schirmer@12854
   108
      with a_v_r v_x_rt have "(y,x) \<in> r\<^sup>*"
schirmer@12854
   109
	by (auto intro: r_into_rtrancl rtrancl_trans)
schirmer@12854
   110
      then show ?thesis 
schirmer@12854
   111
	by blast
schirmer@12854
   112
    next
schirmer@12854
   113
      fix w 
schirmer@12854
   114
      assume a_w_r: "(a, w) \<in> r" and
schirmer@12854
   115
            w_y_rt: "(w, y) \<in> r\<^sup>*"
schirmer@12854
   116
      from a_v_r a_w_r unique 
schirmer@12854
   117
      have "v=w" 
schirmer@12854
   118
	by auto
schirmer@12854
   119
      with w_y_rt hyp 
schirmer@12854
   120
      show ?thesis
schirmer@12854
   121
	by blast
schirmer@12854
   122
    qed
schirmer@12854
   123
  qed
schirmer@12854
   124
qed
schirmer@12854
   125
schirmer@12854
   126
schirmer@12854
   127
lemma rtrancl_cases [consumes 1, case_names Refl Trancl]:
schirmer@12854
   128
 "\<lbrakk>(a,b)\<in>r\<^sup>*;  a = b \<Longrightarrow> P; (a,b)\<in>r\<^sup>+ \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
schirmer@12854
   129
apply (erule rtranclE)
schirmer@12854
   130
apply (auto dest: rtrancl_into_trancl1)
schirmer@12854
   131
done
schirmer@12854
   132
schirmer@12854
   133
(* ### To Transitive_Closure *)
schirmer@12854
   134
theorems converse_rtrancl_induct 
schirmer@12854
   135
 = converse_rtrancl_induct [consumes 1,case_names Id Step]
schirmer@12854
   136
schirmer@12854
   137
theorems converse_trancl_induct 
schirmer@12854
   138
         = converse_trancl_induct [consumes 1,case_names Single Step]
schirmer@12854
   139
schirmer@12854
   140
(* context (theory "Set") *)
schirmer@12854
   141
lemma Ball_weaken:"\<lbrakk>Ball s P;\<And> x. P x\<longrightarrow>Q x\<rbrakk>\<Longrightarrow>Ball s Q"
schirmer@12854
   142
by auto
schirmer@12854
   143
schirmer@12854
   144
(* context (theory "Finite") *)
schirmer@12854
   145
lemma finite_SetCompr2: "[| finite (Collect P); !y. P y --> finite (range (f y)) |] ==>  
schirmer@12854
   146
  finite {f y x |x y. P y}"
schirmer@12854
   147
apply (subgoal_tac "{f y x |x y. P y} = UNION (Collect P) (%y. range (f y))")
schirmer@12854
   148
prefer 2 apply  fast
schirmer@12854
   149
apply (erule ssubst)
schirmer@12854
   150
apply (erule finite_UN_I)
schirmer@12854
   151
apply fast
schirmer@12854
   152
done
schirmer@12854
   153
schirmer@12854
   154
schirmer@12854
   155
(* ### TO theory "List" *)
schirmer@12854
   156
lemma list_all2_trans: "\<forall> a b c. P1 a b \<longrightarrow> P2 b c \<longrightarrow> P3 a c \<Longrightarrow>
schirmer@12854
   157
 \<forall>xs2 xs3. list_all2 P1 xs1 xs2 \<longrightarrow> list_all2 P2 xs2 xs3 \<longrightarrow> list_all2 P3 xs1 xs3"
schirmer@12854
   158
apply (induct_tac "xs1")
schirmer@12854
   159
apply simp
schirmer@12854
   160
apply (rule allI)
schirmer@12854
   161
apply (induct_tac "xs2")
schirmer@12854
   162
apply simp
schirmer@12854
   163
apply (rule allI)
schirmer@12854
   164
apply (induct_tac "xs3")
schirmer@12854
   165
apply auto
schirmer@12854
   166
done
schirmer@12854
   167
schirmer@12854
   168
schirmer@12854
   169
section "pairs"
schirmer@12854
   170
schirmer@12854
   171
lemma surjective_pairing5: "p = (fst p, fst (snd p), fst (snd (snd p)), fst (snd (snd (snd p))), 
schirmer@12854
   172
  snd (snd (snd (snd p))))"
schirmer@12854
   173
apply auto
schirmer@12854
   174
done
schirmer@12854
   175
schirmer@12854
   176
lemma fst_splitE [elim!]: 
schirmer@12854
   177
"[| fst s' = x';  !!x s. [| s' = (x,s);  x = x' |] ==> Q |] ==> Q"
schirmer@12854
   178
apply (cut_tac p = "s'" in surjective_pairing)
schirmer@12854
   179
apply auto
schirmer@12854
   180
done
schirmer@12854
   181
schirmer@12854
   182
lemma fst_in_set_lemma [rule_format (no_asm)]: "(x, y) : set l --> x : fst ` set l"
schirmer@12854
   183
apply (induct_tac "l")
schirmer@12854
   184
apply  auto
schirmer@12854
   185
done
schirmer@12854
   186
schirmer@12854
   187
schirmer@12854
   188
section "quantifiers"
schirmer@12854
   189
schirmer@12854
   190
(*###to be phased out *)
schirmer@12854
   191
ML {* 
schirmer@12854
   192
fun noAll_simpset () = simpset() setmksimps 
schirmer@12854
   193
	mksimps (filter (fn (x,_) => x<>"All") mksimps_pairs)
schirmer@12854
   194
*}
schirmer@12854
   195
schirmer@12854
   196
lemma All_Ex_refl_eq2 [simp]: 
schirmer@12854
   197
 "(!x. (? b. x = f b & Q b) \<longrightarrow> P x) = (!b. Q b --> P (f b))"
schirmer@12854
   198
apply auto
schirmer@12854
   199
done
schirmer@12854
   200
schirmer@12854
   201
lemma ex_ex_miniscope1 [simp]:
schirmer@12854
   202
  "(EX w v. P w v & Q v) = (EX v. (EX w. P w v) & Q v)"
schirmer@12854
   203
apply auto
schirmer@12854
   204
done
schirmer@12854
   205
schirmer@12854
   206
lemma ex_miniscope2 [simp]:
schirmer@12854
   207
  "(EX v. P v & Q & R v) = (Q & (EX v. P v & R v))" 
schirmer@12854
   208
apply auto
schirmer@12854
   209
done
schirmer@12854
   210
schirmer@12854
   211
lemma ex_reorder31: "(\<exists>z x y. P x y z) = (\<exists>x y z. P x y z)"
schirmer@12854
   212
apply auto
schirmer@12854
   213
done
schirmer@12854
   214
schirmer@12854
   215
lemma All_Ex_refl_eq1 [simp]: "(!x. (? b. x = f b) --> P x) = (!b. P (f b))"
schirmer@12854
   216
apply auto
schirmer@12854
   217
done
schirmer@12854
   218
schirmer@12854
   219
schirmer@12854
   220
section "sums"
schirmer@12854
   221
schirmer@12854
   222
hide const In0 In1
schirmer@12854
   223
schirmer@12854
   224
syntax
schirmer@12854
   225
  fun_sum :: "('a => 'c) => ('b => 'c) => (('a+'b) => 'c)" (infixr "'(+')"80)
schirmer@12854
   226
translations
schirmer@12854
   227
 "fun_sum" == "sum_case"
schirmer@12854
   228
schirmer@12854
   229
consts    the_Inl  :: "'a + 'b \<Rightarrow> 'a"
schirmer@12854
   230
          the_Inr  :: "'a + 'b \<Rightarrow> 'b"
schirmer@12854
   231
primrec  "the_Inl (Inl a) = a"
schirmer@12854
   232
primrec  "the_Inr (Inr b) = b"
schirmer@12854
   233
schirmer@12854
   234
datatype ('a, 'b, 'c) sum3 = In1 'a | In2 'b | In3 'c
schirmer@12854
   235
schirmer@12854
   236
consts    the_In1  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'a"
schirmer@12854
   237
          the_In2  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'b"
schirmer@12854
   238
          the_In3  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'c"
schirmer@12854
   239
primrec  "the_In1 (In1 a) = a"
schirmer@12854
   240
primrec  "the_In2 (In2 b) = b"
schirmer@12854
   241
primrec  "the_In3 (In3 c) = c"
schirmer@12854
   242
schirmer@12854
   243
syntax
schirmer@12854
   244
	 In1l	:: "'al \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
schirmer@12854
   245
	 In1r	:: "'ar \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
schirmer@12854
   246
translations
schirmer@12854
   247
	"In1l e" == "In1 (Inl e)"
schirmer@12854
   248
	"In1r c" == "In1 (Inr c)"
schirmer@12854
   249
schirmer@13688
   250
syntax the_In1l :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'al"
schirmer@13688
   251
       the_In1r :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'ar"
schirmer@13688
   252
translations
schirmer@13688
   253
   "the_In1l" == "the_Inl \<circ> the_In1"
schirmer@13688
   254
   "the_In1r" == "the_Inr \<circ> the_In1"
schirmer@13688
   255
schirmer@12854
   256
ML {*
schirmer@12854
   257
fun sum3_instantiate thm = map (fn s => simplify(simpset()delsimps[not_None_eq])
schirmer@12854
   258
 (read_instantiate [("t","In"^s^" ?x")] thm)) ["1l","2","3","1r"]
schirmer@12854
   259
*}
schirmer@12854
   260
(* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
schirmer@12854
   261
schirmer@12854
   262
translations
wenzelm@12919
   263
  "option"<= (type) "Datatype.option"
schirmer@12854
   264
  "list"  <= (type) "List.list"
schirmer@12854
   265
  "sum3"  <= (type) "Basis.sum3"
schirmer@12854
   266
schirmer@12854
   267
schirmer@12854
   268
section "quantifiers for option type"
schirmer@12854
   269
schirmer@12854
   270
syntax
schirmer@12854
   271
  Oall :: "[pttrn, 'a option, bool] => bool"   ("(3! _:_:/ _)" [0,0,10] 10)
schirmer@12854
   272
  Oex  :: "[pttrn, 'a option, bool] => bool"   ("(3? _:_:/ _)" [0,0,10] 10)
schirmer@12854
   273
schirmer@12854
   274
syntax (symbols)
schirmer@12854
   275
  Oall :: "[pttrn, 'a option, bool] => bool"   ("(3\<forall>_\<in>_:/ _)"  [0,0,10] 10)
schirmer@12854
   276
  Oex  :: "[pttrn, 'a option, bool] => bool"   ("(3\<exists>_\<in>_:/ _)"  [0,0,10] 10)
schirmer@12854
   277
schirmer@12854
   278
translations
schirmer@12854
   279
  "! x:A: P"    == "! x:o2s A. P"
schirmer@12854
   280
  "? x:A: P"    == "? x:o2s A. P"
schirmer@12854
   281
schirmer@12854
   282
schirmer@12854
   283
section "unique association lists"
schirmer@12854
   284
schirmer@12854
   285
constdefs
schirmer@12854
   286
  unique   :: "('a \<times> 'b) list \<Rightarrow> bool"
wenzelm@12893
   287
 "unique \<equiv> distinct \<circ> map fst"
schirmer@12854
   288
schirmer@12854
   289
lemma uniqueD [rule_format (no_asm)]: 
schirmer@12854
   290
"unique l--> (!x y. (x,y):set l --> (!x' y'. (x',y'):set l --> x=x'-->  y=y'))"
schirmer@12854
   291
apply (unfold unique_def o_def)
schirmer@12854
   292
apply (induct_tac "l")
schirmer@12854
   293
apply  (auto dest: fst_in_set_lemma)
schirmer@12854
   294
done
schirmer@12854
   295
schirmer@12854
   296
lemma unique_Nil [simp]: "unique []"
schirmer@12854
   297
apply (unfold unique_def)
schirmer@12854
   298
apply (simp (no_asm))
schirmer@12854
   299
done
schirmer@12854
   300
schirmer@12854
   301
lemma unique_Cons [simp]: "unique ((x,y)#l) = (unique l & (!y. (x,y) ~: set l))"
schirmer@12854
   302
apply (unfold unique_def)
schirmer@12854
   303
apply  (auto dest: fst_in_set_lemma)
schirmer@12854
   304
done
schirmer@12854
   305
schirmer@12854
   306
lemmas unique_ConsI = conjI [THEN unique_Cons [THEN iffD2], standard]
schirmer@12854
   307
schirmer@12854
   308
lemma unique_single [simp]: "!!p. unique [p]"
schirmer@12854
   309
apply auto
schirmer@12854
   310
done
schirmer@12854
   311
schirmer@12854
   312
lemma unique_ConsD: "unique (x#xs) ==> unique xs"
schirmer@12854
   313
apply (simp add: unique_def)
schirmer@12854
   314
done
schirmer@12854
   315
schirmer@12854
   316
lemma unique_append [rule_format (no_asm)]: "unique l' ==> unique l -->  
schirmer@12854
   317
  (!(x,y):set l. !(x',y'):set l'. x' ~= x) --> unique (l @ l')"
schirmer@12854
   318
apply (induct_tac "l")
schirmer@12854
   319
apply  (auto dest: fst_in_set_lemma)
schirmer@12854
   320
done
schirmer@12854
   321
schirmer@12854
   322
lemma unique_map_inj [rule_format (no_asm)]: "unique l --> inj f --> unique (map (%(k,x). (f k, g k x)) l)"
schirmer@12854
   323
apply (induct_tac "l")
schirmer@12854
   324
apply  (auto dest: fst_in_set_lemma simp add: inj_eq)
schirmer@12854
   325
done
schirmer@12854
   326
schirmer@12854
   327
lemma map_of_SomeI [rule_format (no_asm)]: "unique l --> (k, x) : set l --> map_of l k = Some x"
schirmer@12854
   328
apply (induct_tac "l")
schirmer@12854
   329
apply auto
schirmer@12854
   330
done
schirmer@12854
   331
schirmer@12854
   332
schirmer@12854
   333
section "list patterns"
schirmer@12854
   334
schirmer@12854
   335
consts
schirmer@12854
   336
  lsplit         :: "[['a, 'a list] => 'b, 'a list] => 'b"
schirmer@12854
   337
defs
schirmer@12854
   338
  lsplit_def:    "lsplit == %f l. f (hd l) (tl l)"
schirmer@12854
   339
(*  list patterns -- extends pre-defined type "pttrn" used in abstractions *)
schirmer@12854
   340
syntax
schirmer@12854
   341
  "_lpttrn"    :: "[pttrn,pttrn] => pttrn"     ("_#/_" [901,900] 900)
schirmer@12854
   342
translations
schirmer@12854
   343
  "%y#x#xs. b"  == "lsplit (%y x#xs. b)"
schirmer@12854
   344
  "%x#xs  . b"  == "lsplit (%x xs  . b)"
schirmer@12854
   345
schirmer@12854
   346
lemma lsplit [simp]: "lsplit c (x#xs) = c x xs"
schirmer@12854
   347
apply (unfold lsplit_def)
schirmer@12854
   348
apply (simp (no_asm))
schirmer@12854
   349
done
schirmer@12854
   350
schirmer@12854
   351
lemma lsplit2 [simp]: "lsplit P (x#xs) y z = P x xs y z"
schirmer@12854
   352
apply (unfold lsplit_def)
schirmer@12854
   353
apply simp
schirmer@12854
   354
done 
schirmer@12854
   355
schirmer@12854
   356
schirmer@12854
   357
section "dummy pattern for quantifiers, let, etc."
schirmer@12854
   358
schirmer@12854
   359
syntax
schirmer@12854
   360
  "@dummy_pat"   :: pttrn    ("'_")
schirmer@12854
   361
schirmer@12854
   362
parse_translation {*
schirmer@12854
   363
let fun dummy_pat_tr [] = Free ("_",dummyT)
schirmer@12854
   364
  | dummy_pat_tr ts = raise TERM ("dummy_pat_tr", ts);
schirmer@12854
   365
in [("@dummy_pat", dummy_pat_tr)] 
schirmer@12854
   366
end
schirmer@12854
   367
*}
schirmer@12854
   368
schirmer@12854
   369
end