Structure quoteTheory


Source File Identifier index Theory binding index

signature quoteTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val index_TY_DEF : thm
    val index_case_def : thm
    val index_lt_def : thm
    val index_size_def : thm
    val varmap_TY_DEF : thm
    val varmap_case_def : thm
    val varmap_size_def : thm
  
  (*  Theorems  *)
    val compare_index_equal : thm
    val compare_list_index : thm
    val datatype_index : thm
    val datatype_varmap : thm
    val index_11 : thm
    val index_Axiom : thm
    val index_case_cong : thm
    val index_case_eq : thm
    val index_compare_def : thm
    val index_compare_ind : thm
    val index_distinct : thm
    val index_induction : thm
    val index_nchotomy : thm
    val varmap_11 : thm
    val varmap_Axiom : thm
    val varmap_case_cong : thm
    val varmap_case_eq : thm
    val varmap_distinct : thm
    val varmap_find_def : thm
    val varmap_find_ind : thm
    val varmap_induction : thm
    val varmap_nchotomy : thm
  
  val quote_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [ternaryComparisons] Parent theory of "quote"
   
   [index_TY_DEF]  Definition
      
      ⊢ ∃rep.
          TYPE_DEFINITION
            (λa0.
                 ∀ $var$('index').
                   (∀a0.
                      (∃a. a0 =
                           (λa.
                                ind_type$CONSTR 0 ARB
                                  (ind_type$FCONS a (λn. ind_type$BOTTOM)))
                             a ∧ $var$('index') a) ∨
                      (∃a. a0 =
                           (λa.
                                ind_type$CONSTR (SUC 0) ARB
                                  (ind_type$FCONS a (λn. ind_type$BOTTOM)))
                             a ∧ $var$('index') a) ∨
                      a0 =
                      ind_type$CONSTR (SUC (SUC 0)) ARB
                        (λn. ind_type$BOTTOM) ⇒
                      $var$('index') a0) ⇒
                   $var$('index') a0) rep
   
   [index_case_def]  Definition
      
      ⊢ (∀a f f1 v. index_CASE (Left_idx a) f f1 v = f a) ∧
        (∀a f f1 v. index_CASE (Right_idx a) f f1 v = f1 a) ∧
        ∀f f1 v. index_CASE End_idx f f1 v = v
   
   [index_lt_def]  Definition
      
      ⊢ ∀i1 i2. index_lt i1 i2 ⇔ index_compare i1 i2 = LESS
   
   [index_size_def]  Definition
      
      ⊢ (∀a. index_size (Left_idx a) = 1 + index_size a) ∧
        (∀a. index_size (Right_idx a) = 1 + index_size a) ∧
        index_size End_idx = 0
   
   [varmap_TY_DEF]  Definition
      
      ⊢ ∃rep.
          TYPE_DEFINITION
            (λa0'.
                 ∀ $var$('varmap').
                   (∀a0'.
                      a0' = ind_type$CONSTR 0 ARB (λn. ind_type$BOTTOM) ∨
                      (∃a0 a1 a2.
                         a0' =
                         (λa0 a1 a2.
                              ind_type$CONSTR (SUC 0) a0
                                (ind_type$FCONS a1
                                   (ind_type$FCONS a2 (λn. ind_type$BOTTOM))))
                           a0 a1 a2 ∧ $var$('varmap') a1 ∧
                         $var$('varmap') a2) ⇒
                      $var$('varmap') a0') ⇒
                   $var$('varmap') a0') rep
   
   [varmap_case_def]  Definition
      
      ⊢ (∀v f. varmap_CASE Empty_vm v f = v) ∧
        ∀a0 a1 a2 v f. varmap_CASE (Node_vm a0 a1 a2) v f = f a0 a1 a2
   
   [varmap_size_def]  Definition
      
      ⊢ (∀f. varmap_size f Empty_vm = 0) ∧
        ∀f a0 a1 a2.
          varmap_size f (Node_vm a0 a1 a2) =
          1 + (f a0 + (varmap_size f a1 + varmap_size f a2))
   
   [compare_index_equal]  Theorem
      
      ⊢ ∀i1 i2. index_compare i1 i2 = EQUAL ⇔ i1 = i2
   
   [compare_list_index]  Theorem
      
      ⊢ ∀l1 l2. list_compare index_compare l1 l2 = EQUAL ⇔ l1 = l2
   
   [datatype_index]  Theorem
      
      ⊢ DATATYPE (index Left_idx Right_idx End_idx)
   
   [datatype_varmap]  Theorem
      
      ⊢ DATATYPE (varmap Empty_vm Node_vm)
   
   [index_11]  Theorem
      
      ⊢ (∀a a'. Left_idx a = Left_idx a' ⇔ a = a') ∧
        ∀a a'. Right_idx a = Right_idx a' ⇔ a = a'
   
   [index_Axiom]  Theorem
      
      ⊢ ∀f0 f1 f2. ∃fn.
          (∀a. fn (Left_idx a) = f0 a (fn a)) ∧
          (∀a. fn (Right_idx a) = f1 a (fn a)) ∧ fn End_idx = f2
   
   [index_case_cong]  Theorem
      
      ⊢ ∀M M' f f1 v.
          M = M' ∧ (∀a. M' = Left_idx a ⇒ f a = f' a) ∧
          (∀a. M' = Right_idx a ⇒ f1 a = f1' a) ∧ (M' = End_idx ⇒ v = v') ⇒
          index_CASE M f f1 v = index_CASE M' f' f1' v'
   
   [index_case_eq]  Theorem
      
      ⊢ index_CASE x f f1 v = v' ⇔
        (∃i. x = Left_idx i ∧ f i = v') ∨
        (∃i. x = Right_idx i ∧ f1 i = v') ∨ x = End_idx ∧ v = v'
   
   [index_compare_def]  Theorem
      
      ⊢ index_compare End_idx End_idx = EQUAL ∧
        (∀v10. index_compare End_idx (Left_idx v10) = LESS) ∧
        (∀v11. index_compare End_idx (Right_idx v11) = LESS) ∧
        (∀v2. index_compare (Left_idx v2) End_idx = GREATER) ∧
        (∀v3. index_compare (Right_idx v3) End_idx = GREATER) ∧
        (∀n' m'.
           index_compare (Left_idx n') (Left_idx m') = index_compare n' m') ∧
        (∀n' m'. index_compare (Left_idx n') (Right_idx m') = LESS) ∧
        (∀n' m'.
           index_compare (Right_idx n') (Right_idx m') =
           index_compare n' m') ∧
        ∀n' m'. index_compare (Right_idx n') (Left_idx m') = GREATER
   
   [index_compare_ind]  Theorem
      
      ⊢ ∀P. P End_idx End_idx ∧ (∀v10. P End_idx (Left_idx v10)) ∧
            (∀v11. P End_idx (Right_idx v11)) ∧
            (∀v2. P (Left_idx v2) End_idx) ∧
            (∀v3. P (Right_idx v3) End_idx) ∧
            (∀n' m'. P n' m' ⇒ P (Left_idx n') (Left_idx m')) ∧
            (∀n' m'. P (Left_idx n') (Right_idx m')) ∧
            (∀n' m'. P n' m' ⇒ P (Right_idx n') (Right_idx m')) ∧
            (∀n' m'. P (Right_idx n') (Left_idx m')) ⇒
            ∀v v1. P v v1
   
   [index_distinct]  Theorem
      
      ⊢ (∀a' a. Left_idx a ≠ Right_idx a') ∧ (∀a. Left_idx a ≠ End_idx) ∧
        ∀a. Right_idx a ≠ End_idx
   
   [index_induction]  Theorem
      
      ⊢ ∀P. (∀i. P i ⇒ P (Left_idx i)) ∧ (∀i. P i ⇒ P (Right_idx i)) ∧
            P End_idx ⇒
            ∀i. P i
   
   [index_nchotomy]  Theorem
      
      ⊢ ∀ii. (∃i. ii = Left_idx i) ∨ (∃i. ii = Right_idx i) ∨ ii = End_idx
   
   [varmap_11]  Theorem
      
      ⊢ ∀a0 a1 a2 a0' a1' a2'.
          Node_vm a0 a1 a2 = Node_vm a0' a1' a2' ⇔
          a0 = a0' ∧ a1 = a1' ∧ a2 = a2'
   
   [varmap_Axiom]  Theorem
      
      ⊢ ∀f0 f1. ∃fn.
          fn Empty_vm = f0 ∧
          ∀a0 a1 a2. fn (Node_vm a0 a1 a2) = f1 a0 a1 a2 (fn a1) (fn a2)
   
   [varmap_case_cong]  Theorem
      
      ⊢ ∀M M' v f.
          M = M' ∧ (M' = Empty_vm ⇒ v = v') ∧
          (∀a0 a1 a2. M' = Node_vm a0 a1 a2 ⇒ f a0 a1 a2 = f' a0 a1 a2) ⇒
          varmap_CASE M v f = varmap_CASE M' v' f'
   
   [varmap_case_eq]  Theorem
      
      ⊢ varmap_CASE x v f = v' ⇔
        x = Empty_vm ∧ v = v' ∨
        ∃a v'' v0. x = Node_vm a v'' v0 ∧ f a v'' v0 = v'
   
   [varmap_distinct]  Theorem
      
      ⊢ ∀a2 a1 a0. Empty_vm ≠ Node_vm a0 a1 a2
   
   [varmap_find_def]  Theorem
      
      ⊢ (∀x v2 v1. varmap_find End_idx (Node_vm x v1 v2) = x) ∧
        (∀x v2 v1 i1.
           varmap_find (Right_idx i1) (Node_vm x v1 v2) = varmap_find i1 v2) ∧
        (∀x v2 v1 i1.
           varmap_find (Left_idx i1) (Node_vm x v1 v2) = varmap_find i1 v1) ∧
        ∀i. varmap_find i Empty_vm = @x. T
   
   [varmap_find_ind]  Theorem
      
      ⊢ ∀P. (∀x v1 v2. P End_idx (Node_vm x v1 v2)) ∧
            (∀i1 x v1 v2. P i1 v2 ⇒ P (Right_idx i1) (Node_vm x v1 v2)) ∧
            (∀i1 x v1 v2. P i1 v1 ⇒ P (Left_idx i1) (Node_vm x v1 v2)) ∧
            (∀i. P i Empty_vm) ⇒
            ∀v v1. P v v1
   
   [varmap_induction]  Theorem
      
      ⊢ ∀P. P Empty_vm ∧ (∀v v0. P v ∧ P v0 ⇒ ∀a. P (Node_vm a v v0)) ⇒
            ∀v. P v
   
   [varmap_nchotomy]  Theorem
      
      ⊢ ∀vv. vv = Empty_vm ∨ ∃a v v0. vv = Node_vm a v v0
   
   
*)
end


Source File Identifier index Theory binding index

HOL 4, Kananaskis-14