# Theory Basis

Up to index of Isabelle/HOL/Bali

theory Basis
imports Main
begin

    (*  Title:      HOL/Bali/Basis.thy
        ID:         $Id: Basis.thy,v 1.15 2005/06/17 14:13:06 haftmann Exp $
        Author:     David von Oheimb

    *)
    header {* Definitions extending HOL as logical basis of Bali *}

    theory Basis imports Main begin

    ML {*
    Unify.search_bound := 40;
    Unify.trace_bound  := 40;
    *}
    (*print_depth 100;*)
    (*Syntax.ambiguity_level := 1;*)

    section "misc"

    declare same_fstI [intro!] (*### TO HOL/Wellfounded_Relations *)

    ML {*
    fun cond_simproc name pat pred thm = Simplifier.simproc (Thm.sign_of_thm thm) name [pat]
      (fn _ => fn _ => fn t => if pred t then NONE else SOME (mk_meta_eq thm));
    *}

    declare split_if_asm  [split] option.split [split] option.split_asm [split]
    ML {*
    simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
    *}
    declare if_weak_cong [cong del] option.weak_case_cong [cong del]
    declare length_Suc_conv [iff];

    (*###to be phased out *)
    ML {*
    bind_thm ("make_imp", rearrange_prems [1,0] mp)
    *}

    lemma Collect_split_eq: "{p. P (split f p)} = {(a,b). P (f a b)}"
    apply auto
    done

    lemma subset_insertD:
      "A <= insert x B ==> A <= B & x ~: A | (EX B'. A = insert x B' & B' <= B)"
    apply (case_tac "x:A")
    apply (rule disjI2)
    apply (rule_tac x = "A-{x}" in exI)
    apply fast+
    done

    syntax
      "3" :: nat   ("3")
      "4" :: nat   ("4")
    translations
     "3" == "Suc 2"
     "4" == "Suc 3"

    (*unused*)
    lemma range_bool_domain: "range f = {f True, f False}"
    apply auto
    apply (case_tac "xa")
    apply auto
    done

    (* irrefl_tranclI in Transitive_Closure.thy is more general *)
    lemma irrefl_tranclI': "r^-1 Int r^+ = {} ==> !x. (x, x) ~: r^+"
    by(blast elim: tranclE dest: trancl_into_rtrancl)

    lemma trancl_rtrancl_trancl:
    "[|(x,y)∈r^+; (y,z)∈r^*|] ==> (x,z)∈r^+"
    by (auto dest: tranclD rtrancl_trans rtrancl_into_trancl2)

    lemma rtrancl_into_trancl3:
    "[|(a,b)∈r^*; a≠b|] ==> (a,b)∈r^+"
    apply (drule rtranclD)
    apply auto
    done

    lemma rtrancl_into_rtrancl2:
      "[| (a, b) ∈  r; (b, c) ∈ r^* |] ==> (a, c) ∈  r^*"
    by (auto intro: r_into_rtrancl rtrancl_trans)

    lemma triangle_lemma:
     "[| !! a b c. [|(a,b)∈r; (a,c)∈r|] ==> b=c; (a,x)∈r*; (a,y)∈r*|]
     ==> (x,y)∈r* ∨ (y,x)∈r*"
    proof -
      note converse_rtrancl_induct = converse_rtrancl_induct [consumes 1]
      note converse_rtranclE = converse_rtranclE [consumes 1]
      assume unique: "!! a b c. [|(a,b)∈r; (a,c)∈r|] ==> b=c"
      assume "(a,x)∈r*"
      then show "(a,y)∈r* ==> (x,y)∈r* ∨ (y,x)∈r*"
      proof (induct rule: converse_rtrancl_induct)
        assume "(x,y)∈r*"
        then show ?thesis
          by blast
      next
        fix a v
        assume a_v_r: "(a, v) ∈ r" and
              v_x_rt: "(v, x) ∈ r*" and
              a_y_rt: "(a, y) ∈ r*"  and
                 hyp: "(v, y) ∈ r* ==> (x, y) ∈ r* ∨ (y, x) ∈ r*"
        from a_y_rt
        show "(x, y) ∈ r* ∨ (y, x) ∈ r*"
        proof (cases rule: converse_rtranclE)
          assume "a=y"
          with a_v_r v_x_rt have "(y,x) ∈ r*"
            by (auto intro: r_into_rtrancl rtrancl_trans)
          then show ?thesis
            by blast
        next
          fix w
          assume a_w_r: "(a, w) ∈ r" and
                w_y_rt: "(w, y) ∈ r*"
          from a_v_r a_w_r unique
          have "v=w"
            by auto
          with w_y_rt hyp
          show ?thesis
            by blast
        qed
      qed
    qed

    lemma rtrancl_cases [consumes 1, case_names Refl Trancl]:
     "[|(a,b)∈r*;  a = b ==> P; (a,b)∈r+ ==> P|] ==> P"
    apply (erule rtranclE)
    apply (auto dest: rtrancl_into_trancl1)
    done

    (* ### To Transitive_Closure *)
    theorems converse_rtrancl_induct
     = converse_rtrancl_induct [consumes 1,case_names Id Step]

    theorems converse_trancl_induct
             = converse_trancl_induct [consumes 1,case_names Single Step]

    (* context (theory "Set") *)
    lemma Ball_weaken:"[|Ball s P;!! x. P x-->Q x|]==>Ball s Q"
    by auto

    (* context (theory "Finite") *)
    lemma finite_SetCompr2: "[| finite (Collect P); !y. P y --> finite (range (f y)) |] ==>
      finite {f y x |x y. P y}"
    apply (subgoal_tac "{f y x |x y. P y} = UNION (Collect P) (%y. range (f y))")
    prefer 2 apply  fast
    apply (erule ssubst)
    apply (erule finite_UN_I)
    apply fast
    done

    (* ### TO theory "List" *)
    lemma list_all2_trans: "∀ a b c. P1 a b --> P2 b c --> P3 a c ==>
     ∀xs2 xs3. list_all2 P1 xs1 xs2 --> list_all2 P2 xs2 xs3 --> list_all2 P3 xs1 xs3"
    apply (induct_tac "xs1")
    apply simp
    apply (rule allI)
    apply (induct_tac "xs2")
    apply simp
    apply (rule allI)
    apply (induct_tac "xs3")
    apply auto
    done

    section "pairs"

    lemma surjective_pairing5: "p = (fst p, fst (snd p), fst (snd (snd p)), fst (snd (snd (snd p))),
      snd (snd (snd (snd p))))"
    apply auto
    done

    lemma fst_splitE [elim!]:
    "[| fst s' = x';  !!x s. [| s' = (x,s);  x = x' |] ==> Q |] ==> Q"
    apply (cut_tac p = "s'" in surjective_pairing)
    apply auto
    done

    lemma fst_in_set_lemma [rule_format (no_asm)]: "(x, y) : set l --> x : fst ` set l"
    apply (induct_tac "l")
    apply  auto
    done

    section "quantifiers"

    (*###to be phased out *)
    ML {*
    fun noAll_simpset () = simpset() setmksimps
            mksimps (List.filter (fn (x,_) => x<>"All") mksimps_pairs)
    *}

    lemma All_Ex_refl_eq2 [simp]:
     "(!x. (? b. x = f b & Q b) --> P x) = (!b. Q b --> P (f b))"
    apply auto
    done

    lemma ex_ex_miniscope1 [simp]:
      "(EX w v. P w v & Q v) = (EX v. (EX w. P w v) & Q v)"
    apply auto
    done

    lemma ex_miniscope2 [simp]:
      "(EX v. P v & Q & R v) = (Q & (EX v. P v & R v))"
    apply auto
    done

    lemma ex_reorder31: "(∃z x y. P x y z) = (∃x y z. P x y z)"
    apply auto
    done

    lemma All_Ex_refl_eq1 [simp]: "(!x. (? b. x = f b) --> P x) = (!b. P (f b))"
    apply auto
    done

    section "sums"

    hide const In0 In1

    syntax
      fun_sum :: "('a => 'c) => ('b => 'c) => (('a+'b) => 'c)" (infixr "'(+')"80)
    translations
     "fun_sum" == "sum_case"

    consts    the_Inl  :: "'a + 'b => 'a"
              the_Inr  :: "'a + 'b => 'b"
    primrec  "the_Inl (Inl a) = a"
    primrec  "the_Inr (Inr b) = b"

    datatype ('a, 'b, 'c) sum3 = In1 'a | In2 'b | In3 'c

    consts    the_In1  :: "('a, 'b, 'c) sum3 => 'a"
              the_In2  :: "('a, 'b, 'c) sum3 => 'b"
              the_In3  :: "('a, 'b, 'c) sum3 => 'c"
    primrec  "the_In1 (In1 a) = a"
    primrec  "the_In2 (In2 b) = b"
    primrec  "the_In3 (In3 c) = c"

    syntax
             In1l   :: "'al => ('al + 'ar, 'b, 'c) sum3"
             In1r   :: "'ar => ('al + 'ar, 'b, 'c) sum3"
    translations
            "In1l e" == "In1 (Inl e)"
            "In1r c" == "In1 (Inr c)"

    syntax the_In1l :: "('al + 'ar, 'b, 'c) sum3 => 'al"
           the_In1r :: "('al + 'ar, 'b, 'c) sum3 => 'ar"
    translations
       "the_In1l" == "the_Inl o the_In1"
       "the_In1r" == "the_Inr o the_In1"

    ML {*
    fun sum3_instantiate thm = map (fn s => simplify(simpset()delsimps[not_None_eq])
     (read_instantiate [("t","In"^s^" ?x")] thm)) ["1l","2","3","1r"]
    *}
    (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)

    translations
      "option"<= (type) "Datatype.option"
      "list"  <= (type) "List.list"
      "sum3"  <= (type) "Basis.sum3"

    section "quantifiers for option type"

    syntax
      Oall :: "[pttrn, 'a option, bool] => bool"   ("(3! _:_:/ _)" [0,0,10] 10)
      Oex  :: "[pttrn, 'a option, bool] => bool"   ("(3? _:_:/ _)" [0,0,10] 10)

    syntax (symbols)
      Oall :: "[pttrn, 'a option, bool] => bool"   ("(3∀_∈_:/ _)"  [0,0,10] 10)
      Oex  :: "[pttrn, 'a option, bool] => bool"   ("(3∃_∈_:/ _)"  [0,0,10] 10)

    translations
      "! x:A: P"    == "! x:o2s A. P"
      "? x:A: P"    == "? x:o2s A. P"

    section "unique association lists"

    constdefs
      unique   :: "('a × 'b) list => bool"
     "unique ≡ distinct o map fst"

    lemma uniqueD [rule_format (no_asm)]:
    "unique l--> (!x y. (x,y):set l --> (!x' y'. (x',y'):set l --> x=x'-->  y=y'))"
    apply (unfold unique_def o_def)
    apply (induct_tac "l")
    apply  (auto dest: fst_in_set_lemma)
    done

    lemma unique_Nil [simp]: "unique []"
    apply (unfold unique_def)
    apply (simp (no_asm))
    done

    lemma unique_Cons [simp]: "unique ((x,y)#l) = (unique l & (!y. (x,y) ~: set l))"
    apply (unfold unique_def)
    apply  (auto dest: fst_in_set_lemma)
    done

    lemmas unique_ConsI = conjI [THEN unique_Cons [THEN iffD2], standard]

    lemma unique_single [simp]: "!!p. unique [p]"
    apply auto
    done

    lemma unique_ConsD: "unique (x#xs) ==> unique xs"
    apply (simp add: unique_def)
    done

    lemma unique_append [rule_format (no_asm)]: "unique l' ==> unique l -->
      (!(x,y):set l. !(x',y'):set l'. x' ~= x) --> unique (l @ l')"
    apply (induct_tac "l")
    apply  (auto dest: fst_in_set_lemma)
    done

    lemma unique_map_inj [rule_format (no_asm)]: "unique l --> inj f --> unique (map (%(k,x). (f k, g k x)) l)"
    apply (induct_tac "l")
    apply  (auto dest: fst_in_set_lemma simp add: inj_eq)
    done

    lemma map_of_SomeI [rule_format (no_asm)]: "unique l --> (k, x) : set l --> map_of l k = Some x"
    apply (induct_tac "l")
    apply auto
    done

    section "list patterns"

    consts
      lsplit         :: "[['a, 'a list] => 'b, 'a list] => 'b"
    defs
      lsplit_def:    "lsplit == %f l. f (hd l) (tl l)"
    (*  list patterns -- extends pre-defined type "pttrn" used in abstractions *)
    syntax
      "_lpttrn"    :: "[pttrn,pttrn] => pttrn"     ("_#/_" [901,900] 900)
    translations
      "%y#x#xs. b"  == "lsplit (%y x#xs. b)"
      "%x#xs  . b"  == "lsplit (%x xs  . b)"

    lemma lsplit [simp]: "lsplit c (x#xs) = c x xs"
    apply (unfold lsplit_def)
    apply (simp (no_asm))
    done

    lemma lsplit2 [simp]: "lsplit P (x#xs) y z = P x xs y z"
    apply (unfold lsplit_def)
    apply simp
    done

    section "dummy pattern for quantifiers, let, etc."

    syntax
      "@dummy_pat"   :: pttrn    ("'_")

    parse_translation {*
    let fun dummy_pat_tr [] = Free ("_",dummyT)
      | dummy_pat_tr ts = raise TERM ("dummy_pat_tr", ts);
    in [("@dummy_pat", dummy_pat_tr)]
    end
    *}

    end

## misc

theorem make_imp:

      [| P; P --> Q |] ==> Q

lemma Collect_split_eq:

      {p. P (split f p)} = {(a, b). P (f a b)}

lemma subset_insertD:

      A ⊆ insert x B ==> A ⊆ B ∧ x ∉ A ∨ (∃B'. A = insert x B' ∧ B' ⊆ B)

lemma range_bool_domain:

      range f = {f True, f False}

lemma irrefl_tranclI':

      r^-1 ∩ r+ = {} ==> ∀x. (x, x) ∉ r+

lemma trancl_rtrancl_trancl:

      [| (x, y) ∈ r+; (y, z) ∈ r* |] ==> (x, z) ∈ r+

lemma rtrancl_into_trancl3:

      [| (a, b) ∈ r*; a ≠ b |] ==> (a, b) ∈ r+

lemma rtrancl_into_rtrancl2:

      [| (a, b) ∈ r; (b, c) ∈ r* |] ==> (a, c) ∈ r*

lemma triangle_lemma:

      [| !!a b c. [| (a, b) ∈ r; (a, c) ∈ r |] ==> b = c; (a, x) ∈ r*; (a, y) ∈ r* |]
      ==> (x, y) ∈ r* ∨ (y, x) ∈ r*

lemma rtrancl_cases:

      [| (a, b) ∈ r*; a = b ==> P; (a, b) ∈ r+ ==> P |] ==> P

theorems converse_rtrancl_induct:

      [| (a, b) ∈ r*; P b; !!y z. [| (y, z) ∈ r; (z, b) ∈ r*; P z |] ==> P y |]
      ==> P a

theorems converse_rtrancl_induct:

      [| (a, b) ∈ r*; P b; !!y z. [| (y, z) ∈ r; (z, b) ∈ r*; P z |] ==> P y |]
      ==> P a

theorems converse_trancl_induct:

      [| (a, b) ∈ r+; !!y. (y, b) ∈ r ==> P y;
         !!y z. [| (y, z) ∈ r; (z, b) ∈ r+; P z |] ==> P y |]
      ==> P a

theorems converse_trancl_induct:

      [| (a, b) ∈ r+; !!y. (y, b) ∈ r ==> P y;
         !!y z. [| (y, z) ∈ r; (z, b) ∈ r+; P z |] ==> P y |]
      ==> P a

lemma Ball_weaken:

      [| Ball s P; !!x. P x --> Q x |] ==> Ball s Q

lemma finite_SetCompr2:

      [| finite (Collect P); ∀y. P y --> finite (range (f y)) |]
      ==> finite {f y x |x y. P y}

lemma list_all2_trans:

      ∀a b c. P1.0 a b --> P2.0 b c --> P3.0 a c
      ==> ∀xs2 xs3.
             list_all2 P1.0 xs1.0 xs2 -->
             list_all2 P2.0 xs2 xs3 --> list_all2 P3.0 xs1.0 xs3

## pairs

lemma surjective_pairing5:

      p = (fst p, fst (snd p), fst (snd (snd p)), fst (snd (snd (snd p))),
           snd (snd (snd (snd p))))

lemma fst_splitE:

      [| fst s' = x'; !!x s. [| s' = (x, s); x = x' |] ==> Q |] ==> Q

lemma fst_in_set_lemma:

      (x, y) ∈ set l ==> x ∈ fst ` set l

## quantifiers

lemma All_Ex_refl_eq2:

      (∀x. (∃b. x = f b ∧ Q b) --> P x) = (∀b. Q b --> P (f b))

lemma ex_ex_miniscope1:

      (∃w v. P w v ∧ Q v) = (∃v. (∃w. P w v) ∧ Q v)

lemma ex_miniscope2:

      (∃v. P v ∧ Q ∧ R v) = (Q ∧ (∃v. P v ∧ R v))

lemma ex_reorder31:

      (∃z x y. P x y z) = (∃x y z. P x y z)

lemma All_Ex_refl_eq1:

      (∀x. (∃b. x = f b) --> P x) = (∀b. P (f b))

## sums

## quantifiers for option type

## unique association lists

lemma uniqueD:

      [| unique l; (x, y) ∈ set l; (x', y') ∈ set l; x = x' |] ==> y = y'

lemma unique_Nil:

      unique []

lemma unique_Cons:

      unique ((x, y) # l) = (unique l ∧ (∀y. (x, y) ∉ set l))

lemmas unique_ConsI:

      [| unique l; ∀y. (x, y) ∉ set l |] ==> unique ((x, y) # l)

lemmas unique_ConsI:

      [| unique l; ∀y. (x, y) ∉ set l |] ==> unique ((x, y) # l)

lemma unique_single:

      unique [p]

lemma unique_ConsD:

      unique (x # xs) ==> unique xs

lemma unique_append:

      [| unique l'; unique l; ∀(x, y)∈set l. ∀(x', y')∈set l'. x' ≠ x |]
      ==> unique (l @ l')

lemma unique_map_inj:

      [| unique l; inj f |] ==> unique (map (%(k, x). (f k, g k x)) l)

lemma map_of_SomeI:

      [| unique l; (k, x) ∈ set l |] ==> map_of l k = Some x

## list patterns

lemma lsplit:

      lsplit c (x # xs) = c x xs

lemma lsplit2:

      lsplit P (x # xs) y z = P x xs y z

## dummy pattern for quantifiers, let, etc.