src/HOL/Bali/Basis.thy
changeset 12854 00d4a435777f
child 12857 a4386cc9b1c3
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Bali/Basis.thy	Mon Jan 28 17:00:19 2002 +0100
     1.3 @@ -0,0 +1,370 @@
     1.4 +(*  Title:      isabelle/Bali/Basis.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     David von Oheimb
     1.7 +    Copyright   1997 Technische Universitaet Muenchen
     1.8 +
     1.9 +*)
    1.10 +header {* Definitions extending HOL as logical basis of Bali *}
    1.11 +
    1.12 +theory Basis = Main:
    1.13 +
    1.14 +ML_setup {*
    1.15 +Unify.search_bound := 40;
    1.16 +Unify.trace_bound  := 40;
    1.17 +
    1.18 +quick_and_dirty:=true;
    1.19 +
    1.20 +Pretty.setmargin 77;
    1.21 +goals_limit:=2;
    1.22 +*}
    1.23 +(*print_depth 100;*)
    1.24 +(*Syntax.ambiguity_level := 1;*)
    1.25 +
    1.26 +section "misc"
    1.27 +
    1.28 +declare same_fstI [intro!] (*### TO HOL/Wellfounded_Relations *)
    1.29 +
    1.30 +(* ###TO HOL/???.ML?? *)
    1.31 +ML {*
    1.32 +fun make_simproc name pat pred thm = Simplifier.mk_simproc name
    1.33 +   [Thm.read_cterm (Thm.sign_of_thm thm) (pat, HOLogic.typeT)] 
    1.34 +   (K (K (fn s => if pred s then None else Some (standard (mk_meta_eq thm)))))
    1.35 +*}
    1.36 +
    1.37 +declare split_if_asm  [split] option.split [split] option.split_asm [split]
    1.38 +ML {*
    1.39 +simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
    1.40 +*}
    1.41 +declare if_weak_cong [cong del] option.weak_case_cong [cong del]
    1.42 +declare length_Suc_conv [iff];
    1.43 +
    1.44 +(*###to be phased out *)
    1.45 +ML {*
    1.46 +bind_thm ("make_imp", rearrange_prems [1,0] mp)
    1.47 +*}
    1.48 +
    1.49 +lemma Collect_split_eq: "{p. P (split f p)} = {(a,b). P (f a b)}"
    1.50 +apply auto
    1.51 +done
    1.52 +
    1.53 +lemma subset_insertD: 
    1.54 +  "A <= insert x B ==> A <= B & x ~: A | (EX B'. A = insert x B' & B' <= B)"
    1.55 +apply (case_tac "x:A")
    1.56 +apply (rule disjI2)
    1.57 +apply (rule_tac x = "A-{x}" in exI)
    1.58 +apply fast+
    1.59 +done
    1.60 +
    1.61 +syntax
    1.62 +  "3" :: nat   ("3")
    1.63 +  "4" :: nat   ("4")
    1.64 +translations
    1.65 + "3" == "Suc 2"
    1.66 + "4" == "Suc 3"
    1.67 +
    1.68 +(*unused*)
    1.69 +lemma range_bool_domain: "range f = {f True, f False}"
    1.70 +apply auto
    1.71 +apply (case_tac "xa")
    1.72 +apply auto
    1.73 +done
    1.74 +
    1.75 +(* context (theory "Transitive_Closure") *)
    1.76 +lemma irrefl_tranclI': "r^-1 Int r^+ = {} ==> !x. (x, x) ~: r^+"
    1.77 +apply (rule allI)
    1.78 +apply (erule irrefl_tranclI)
    1.79 +done
    1.80 +
    1.81 +lemma trancl_rtrancl_trancl:
    1.82 +"\<lbrakk>(x,y)\<in>r^+; (y,z)\<in>r^*\<rbrakk> \<Longrightarrow> (x,z)\<in>r^+"
    1.83 +by (auto dest: tranclD rtrancl_trans rtrancl_into_trancl2)
    1.84 +
    1.85 +lemma rtrancl_into_trancl3:
    1.86 +"\<lbrakk>(a,b)\<in>r^*; a\<noteq>b\<rbrakk> \<Longrightarrow> (a,b)\<in>r^+"
    1.87 +apply (drule rtranclD)
    1.88 +apply auto
    1.89 +done
    1.90 +
    1.91 +lemma rtrancl_into_rtrancl2: 
    1.92 +  "\<lbrakk> (a, b) \<in>  r; (b, c) \<in> r^* \<rbrakk> \<Longrightarrow> (a, c) \<in>  r^*"
    1.93 +by (auto intro: r_into_rtrancl rtrancl_trans)
    1.94 +
    1.95 +lemma triangle_lemma:
    1.96 + "\<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> 
    1.97 + \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
    1.98 +proof -
    1.99 +  note converse_rtrancl_induct = converse_rtrancl_induct [consumes 1]
   1.100 +  note converse_rtranclE = converse_rtranclE [consumes 1] 
   1.101 +  assume unique: "\<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c"
   1.102 +  assume "(a,x)\<in>r\<^sup>*" 
   1.103 +  then show "(a,y)\<in>r\<^sup>* \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
   1.104 +  proof (induct rule: converse_rtrancl_induct)
   1.105 +    assume "(x,y)\<in>r\<^sup>*"
   1.106 +    then show ?thesis 
   1.107 +      by blast
   1.108 +  next
   1.109 +    fix a v
   1.110 +    assume a_v_r: "(a, v) \<in> r" and
   1.111 +          v_x_rt: "(v, x) \<in> r\<^sup>*" and
   1.112 +          a_y_rt: "(a, y) \<in> r\<^sup>*"  and
   1.113 +             hyp: "(v, y) \<in> r\<^sup>* \<Longrightarrow> (x, y) \<in> r\<^sup>* \<or> (y, x) \<in> r\<^sup>*"
   1.114 +    from a_y_rt 
   1.115 +    show "(x, y) \<in> r\<^sup>* \<or> (y, x) \<in> r\<^sup>*"
   1.116 +    proof (cases rule: converse_rtranclE)
   1.117 +      assume "a=y"
   1.118 +      with a_v_r v_x_rt have "(y,x) \<in> r\<^sup>*"
   1.119 +	by (auto intro: r_into_rtrancl rtrancl_trans)
   1.120 +      then show ?thesis 
   1.121 +	by blast
   1.122 +    next
   1.123 +      fix w 
   1.124 +      assume a_w_r: "(a, w) \<in> r" and
   1.125 +            w_y_rt: "(w, y) \<in> r\<^sup>*"
   1.126 +      from a_v_r a_w_r unique 
   1.127 +      have "v=w" 
   1.128 +	by auto
   1.129 +      with w_y_rt hyp 
   1.130 +      show ?thesis
   1.131 +	by blast
   1.132 +    qed
   1.133 +  qed
   1.134 +qed
   1.135 +
   1.136 +
   1.137 +lemma rtrancl_cases [consumes 1, case_names Refl Trancl]:
   1.138 + "\<lbrakk>(a,b)\<in>r\<^sup>*;  a = b \<Longrightarrow> P; (a,b)\<in>r\<^sup>+ \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   1.139 +apply (erule rtranclE)
   1.140 +apply (auto dest: rtrancl_into_trancl1)
   1.141 +done
   1.142 +
   1.143 +(* ### To Transitive_Closure *)
   1.144 +theorems converse_rtrancl_induct 
   1.145 + = converse_rtrancl_induct [consumes 1,case_names Id Step]
   1.146 +
   1.147 +theorems converse_trancl_induct 
   1.148 +         = converse_trancl_induct [consumes 1,case_names Single Step]
   1.149 +
   1.150 +(* context (theory "Set") *)
   1.151 +lemma Ball_weaken:"\<lbrakk>Ball s P;\<And> x. P x\<longrightarrow>Q x\<rbrakk>\<Longrightarrow>Ball s Q"
   1.152 +by auto
   1.153 +
   1.154 +(* context (theory "Finite") *)
   1.155 +lemma finite_SetCompr2: "[| finite (Collect P); !y. P y --> finite (range (f y)) |] ==>  
   1.156 +  finite {f y x |x y. P y}"
   1.157 +apply (subgoal_tac "{f y x |x y. P y} = UNION (Collect P) (%y. range (f y))")
   1.158 +prefer 2 apply  fast
   1.159 +apply (erule ssubst)
   1.160 +apply (erule finite_UN_I)
   1.161 +apply fast
   1.162 +done
   1.163 +
   1.164 +
   1.165 +(* ### TO theory "List" *)
   1.166 +lemma list_all2_trans: "\<forall> a b c. P1 a b \<longrightarrow> P2 b c \<longrightarrow> P3 a c \<Longrightarrow>
   1.167 + \<forall>xs2 xs3. list_all2 P1 xs1 xs2 \<longrightarrow> list_all2 P2 xs2 xs3 \<longrightarrow> list_all2 P3 xs1 xs3"
   1.168 +apply (induct_tac "xs1")
   1.169 +apply simp
   1.170 +apply (rule allI)
   1.171 +apply (induct_tac "xs2")
   1.172 +apply simp
   1.173 +apply (rule allI)
   1.174 +apply (induct_tac "xs3")
   1.175 +apply auto
   1.176 +done
   1.177 +
   1.178 +
   1.179 +section "pairs"
   1.180 +
   1.181 +lemma surjective_pairing5: "p = (fst p, fst (snd p), fst (snd (snd p)), fst (snd (snd (snd p))), 
   1.182 +  snd (snd (snd (snd p))))"
   1.183 +apply auto
   1.184 +done
   1.185 +
   1.186 +lemma fst_splitE [elim!]: 
   1.187 +"[| fst s' = x';  !!x s. [| s' = (x,s);  x = x' |] ==> Q |] ==> Q"
   1.188 +apply (cut_tac p = "s'" in surjective_pairing)
   1.189 +apply auto
   1.190 +done
   1.191 +
   1.192 +lemma fst_in_set_lemma [rule_format (no_asm)]: "(x, y) : set l --> x : fst ` set l"
   1.193 +apply (induct_tac "l")
   1.194 +apply  auto
   1.195 +done
   1.196 +
   1.197 +
   1.198 +section "quantifiers"
   1.199 +
   1.200 +(*###to be phased out *)
   1.201 +ML {* 
   1.202 +fun noAll_simpset () = simpset() setmksimps 
   1.203 +	mksimps (filter (fn (x,_) => x<>"All") mksimps_pairs)
   1.204 +*}
   1.205 +
   1.206 +lemma All_Ex_refl_eq2 [simp]: 
   1.207 + "(!x. (? b. x = f b & Q b) \<longrightarrow> P x) = (!b. Q b --> P (f b))"
   1.208 +apply auto
   1.209 +done
   1.210 +
   1.211 +lemma ex_ex_miniscope1 [simp]:
   1.212 +  "(EX w v. P w v & Q v) = (EX v. (EX w. P w v) & Q v)"
   1.213 +apply auto
   1.214 +done
   1.215 +
   1.216 +lemma ex_miniscope2 [simp]:
   1.217 +  "(EX v. P v & Q & R v) = (Q & (EX v. P v & R v))" 
   1.218 +apply auto
   1.219 +done
   1.220 +
   1.221 +lemma ex_reorder31: "(\<exists>z x y. P x y z) = (\<exists>x y z. P x y z)"
   1.222 +apply auto
   1.223 +done
   1.224 +
   1.225 +lemma All_Ex_refl_eq1 [simp]: "(!x. (? b. x = f b) --> P x) = (!b. P (f b))"
   1.226 +apply auto
   1.227 +done
   1.228 +
   1.229 +
   1.230 +section "sums"
   1.231 +
   1.232 +hide const In0 In1
   1.233 +
   1.234 +syntax
   1.235 +  fun_sum :: "('a => 'c) => ('b => 'c) => (('a+'b) => 'c)" (infixr "'(+')"80)
   1.236 +translations
   1.237 + "fun_sum" == "sum_case"
   1.238 +
   1.239 +consts    the_Inl  :: "'a + 'b \<Rightarrow> 'a"
   1.240 +          the_Inr  :: "'a + 'b \<Rightarrow> 'b"
   1.241 +primrec  "the_Inl (Inl a) = a"
   1.242 +primrec  "the_Inr (Inr b) = b"
   1.243 +
   1.244 +datatype ('a, 'b, 'c) sum3 = In1 'a | In2 'b | In3 'c
   1.245 +
   1.246 +consts    the_In1  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'a"
   1.247 +          the_In2  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'b"
   1.248 +          the_In3  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'c"
   1.249 +primrec  "the_In1 (In1 a) = a"
   1.250 +primrec  "the_In2 (In2 b) = b"
   1.251 +primrec  "the_In3 (In3 c) = c"
   1.252 +
   1.253 +syntax
   1.254 +	 In1l	:: "'al \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
   1.255 +	 In1r	:: "'ar \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
   1.256 +translations
   1.257 +	"In1l e" == "In1 (Inl e)"
   1.258 +	"In1r c" == "In1 (Inr c)"
   1.259 +
   1.260 +ML {*
   1.261 +fun sum3_instantiate thm = map (fn s => simplify(simpset()delsimps[not_None_eq])
   1.262 + (read_instantiate [("t","In"^s^" ?x")] thm)) ["1l","2","3","1r"]
   1.263 +*}
   1.264 +(* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
   1.265 +
   1.266 +translations
   1.267 +  "option"<= (type) "Option.option"
   1.268 +  "list"  <= (type) "List.list"
   1.269 +  "sum3"  <= (type) "Basis.sum3"
   1.270 +
   1.271 +
   1.272 +section "quantifiers for option type"
   1.273 +
   1.274 +syntax
   1.275 +  Oall :: "[pttrn, 'a option, bool] => bool"   ("(3! _:_:/ _)" [0,0,10] 10)
   1.276 +  Oex  :: "[pttrn, 'a option, bool] => bool"   ("(3? _:_:/ _)" [0,0,10] 10)
   1.277 +
   1.278 +syntax (symbols)
   1.279 +  Oall :: "[pttrn, 'a option, bool] => bool"   ("(3\<forall>_\<in>_:/ _)"  [0,0,10] 10)
   1.280 +  Oex  :: "[pttrn, 'a option, bool] => bool"   ("(3\<exists>_\<in>_:/ _)"  [0,0,10] 10)
   1.281 +
   1.282 +translations
   1.283 +  "! x:A: P"    == "! x:o2s A. P"
   1.284 +  "? x:A: P"    == "? x:o2s A. P"
   1.285 +
   1.286 +
   1.287 +section "unique association lists"
   1.288 +
   1.289 +constdefs
   1.290 +  unique   :: "('a \<times> 'b) list \<Rightarrow> bool"
   1.291 + "unique \<equiv> nodups \<circ> map fst"
   1.292 +
   1.293 +lemma uniqueD [rule_format (no_asm)]: 
   1.294 +"unique l--> (!x y. (x,y):set l --> (!x' y'. (x',y'):set l --> x=x'-->  y=y'))"
   1.295 +apply (unfold unique_def o_def)
   1.296 +apply (induct_tac "l")
   1.297 +apply  (auto dest: fst_in_set_lemma)
   1.298 +done
   1.299 +
   1.300 +lemma unique_Nil [simp]: "unique []"
   1.301 +apply (unfold unique_def)
   1.302 +apply (simp (no_asm))
   1.303 +done
   1.304 +
   1.305 +lemma unique_Cons [simp]: "unique ((x,y)#l) = (unique l & (!y. (x,y) ~: set l))"
   1.306 +apply (unfold unique_def)
   1.307 +apply  (auto dest: fst_in_set_lemma)
   1.308 +done
   1.309 +
   1.310 +lemmas unique_ConsI = conjI [THEN unique_Cons [THEN iffD2], standard]
   1.311 +
   1.312 +lemma unique_single [simp]: "!!p. unique [p]"
   1.313 +apply auto
   1.314 +done
   1.315 +
   1.316 +lemma unique_ConsD: "unique (x#xs) ==> unique xs"
   1.317 +apply (simp add: unique_def)
   1.318 +done
   1.319 +
   1.320 +lemma unique_append [rule_format (no_asm)]: "unique l' ==> unique l -->  
   1.321 +  (!(x,y):set l. !(x',y'):set l'. x' ~= x) --> unique (l @ l')"
   1.322 +apply (induct_tac "l")
   1.323 +apply  (auto dest: fst_in_set_lemma)
   1.324 +done
   1.325 +
   1.326 +lemma unique_map_inj [rule_format (no_asm)]: "unique l --> inj f --> unique (map (%(k,x). (f k, g k x)) l)"
   1.327 +apply (induct_tac "l")
   1.328 +apply  (auto dest: fst_in_set_lemma simp add: inj_eq)
   1.329 +done
   1.330 +
   1.331 +lemma map_of_SomeI [rule_format (no_asm)]: "unique l --> (k, x) : set l --> map_of l k = Some x"
   1.332 +apply (induct_tac "l")
   1.333 +apply auto
   1.334 +done
   1.335 +
   1.336 +
   1.337 +section "list patterns"
   1.338 +
   1.339 +consts
   1.340 +  lsplit         :: "[['a, 'a list] => 'b, 'a list] => 'b"
   1.341 +defs
   1.342 +  lsplit_def:    "lsplit == %f l. f (hd l) (tl l)"
   1.343 +(*  list patterns -- extends pre-defined type "pttrn" used in abstractions *)
   1.344 +syntax
   1.345 +  "_lpttrn"    :: "[pttrn,pttrn] => pttrn"     ("_#/_" [901,900] 900)
   1.346 +translations
   1.347 +  "%y#x#xs. b"  == "lsplit (%y x#xs. b)"
   1.348 +  "%x#xs  . b"  == "lsplit (%x xs  . b)"
   1.349 +
   1.350 +lemma lsplit [simp]: "lsplit c (x#xs) = c x xs"
   1.351 +apply (unfold lsplit_def)
   1.352 +apply (simp (no_asm))
   1.353 +done
   1.354 +
   1.355 +lemma lsplit2 [simp]: "lsplit P (x#xs) y z = P x xs y z"
   1.356 +apply (unfold lsplit_def)
   1.357 +apply simp
   1.358 +done 
   1.359 +
   1.360 +
   1.361 +section "dummy pattern for quantifiers, let, etc."
   1.362 +
   1.363 +syntax
   1.364 +  "@dummy_pat"   :: pttrn    ("'_")
   1.365 +
   1.366 +parse_translation {*
   1.367 +let fun dummy_pat_tr [] = Free ("_",dummyT)
   1.368 +  | dummy_pat_tr ts = raise TERM ("dummy_pat_tr", ts);
   1.369 +in [("@dummy_pat", dummy_pat_tr)] 
   1.370 +end
   1.371 +*}
   1.372 +
   1.373 +end