isahipster: da2e1698a0d44c6b9c9cb8c257e99f0818227032

     1: theory prop_28
     2: imports Main
     3:         "$HIPSTER_HOME/IsaHipster"
     4: begin
     5:   datatype 'a list = Nil2 | Cons2 "'a" "'a list"
     6:   fun append :: "'a list => 'a list => 'a list" where
     7:   "append (Nil2) y = y"
     8:   | "append (Cons2 z xs) y = Cons2 z (append xs y)"
     9:   fun rev :: "'a list => 'a list" where
    10:   "rev (Nil2) = Nil2"
    11:   | "rev (Cons2 y xs) = append (rev xs) (Cons2 y (Nil2))"
    12:   fun qrevflat :: "('a list) list => 'a list => 'a list" where
    13:   "qrevflat (Nil2) y = y"
    14:   | "qrevflat (Cons2 xs xss) y = qrevflat xss (append (rev xs) y)"
    15:   fun revflat :: "('a list) list => 'a list" where
    16:   "revflat (Nil2) = Nil2"
    17:   | "revflat (Cons2 xs xss) = append (revflat xss) (rev xs)"
    18:   (*hipster append rev qrevflat revflat *)
    19: 
    20: lemma lemma_a [thy_expl]: "append x2 Nil2 = x2"
    21: by (hipster_induct_schemes  append.simps)
    22: 
    23: lemma lemma_aa [thy_expl]: "append (append x2 y2) z2 = append x2 (append y2 z2)"
    24: by (hipster_induct_schemes append.simps)
    25: 
    26: lemma lemma_ab [thy_expl]: "append (rev x4) (rev y4) = rev (append y4 x4)"
    27: by (hipster_induct_schemes rev.simps append.simps)
    28: 
    29: lemma lemma_ac [thy_expl]: "rev (rev x3) = x3"
    30: by (hipster_induct_schemes rev.simps append.simps)
    31: 
    32: hipster qrevflat revflat append rev
    33: lemma lemma_ad [thy_expl]: "append (qrevflat x3 y3) z3 = qrevflat x3 (append y3 z3)"
    34: by (hipster_induct_schemes qrevflat.simps revflat.simps append.simps)
    35: 
    36: lemma lemma_ae [thy_expl]: "qrevflat x3 Nil2 = revflat x3"
    37: by (hipster_induct_schemes qrevflat.simps revflat.simps append.simps rev.simps)
    38: 
    39:   theorem x0 :
    40:     "(revflat x) = (qrevflat x (Nil2))"
    41:     by (hipster_induct_schemes qrevflat.simps revflat.simps append.simps)
    42: 
    43:     by (tactic {* Subgoal.FOCUS_PARAMS (K (Tactic_Data.hard_tac @{context})) @{context} 1 *})
    44: end