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