src/HOL/Induct/LList.ML
changeset 5278 a903b66822e2
parent 5184 9b8547a9496a
child 5788 e3a98a7c0634
     1.1 --- a/src/HOL/Induct/LList.ML	Thu Aug 06 15:47:26 1998 +0200
     1.2 +++ b/src/HOL/Induct/LList.ML	Thu Aug 06 15:48:13 1998 +0200
     1.3 @@ -103,8 +103,7 @@
     1.4  qed "LList_corec_subset2";
     1.5  
     1.6  (*the recursion equation for LList_corec -- NOT SUITABLE FOR REWRITING!*)
     1.7 -Goal
     1.8 -    "LList_corec a f = sum_case (%u. NIL) \
     1.9 +Goal "LList_corec a f = sum_case (%u. NIL) \
    1.10  \                           (split(%z w. CONS z (LList_corec w f))) (f a)";
    1.11  by (REPEAT (resolve_tac [equalityI, LList_corec_subset1, 
    1.12                           LList_corec_subset2] 1));
    1.13 @@ -129,8 +128,7 @@
    1.14  qed "LList_corec_type";
    1.15  
    1.16  (*Lemma for the proof of llist_corec*)
    1.17 -Goal
    1.18 -   "LList_corec a (%z. sum_case Inl (split(%v w. Inr((Leaf(v),w)))) (f z)) : \
    1.19 +Goal "LList_corec a (%z. sum_case Inl (split(%v w. Inr((Leaf(v),w)))) (f z)) : \
    1.20  \   llist(range Leaf)";
    1.21  by (res_inst_tac [("X", "range(%x. LList_corec x ?g)")] llist_coinduct 1);
    1.22  by (rtac rangeI 1);
    1.23 @@ -235,8 +233,7 @@
    1.24                           diag_subset_LListD] 1));
    1.25  qed "LListD_eq_diag";
    1.26  
    1.27 -Goal 
    1.28 -    "M: llist(A) ==> (M,M) : LListD_Fun (diag A) (X Un diag(llist(A)))";
    1.29 +Goal "M: llist(A) ==> (M,M) : LListD_Fun (diag A) (X Un diag(llist(A)))";
    1.30  by (rtac (LListD_eq_diag RS subst) 1);
    1.31  by (rtac LListD_Fun_LListD_I 1);
    1.32  by (asm_simp_tac (simpset() addsimps [LListD_eq_diag, diagI]) 1);
    1.33 @@ -246,8 +243,7 @@
    1.34  (** To show two LLists are equal, exhibit a bisimulation! 
    1.35        [also admits true equality]
    1.36     Replace "A" by some particular set, like {x.True}??? *)
    1.37 -Goal 
    1.38 -    "[| (M,N) : r;  r <= LListD_Fun (diag A) (r Un diag(llist(A))) \
    1.39 +Goal "[| (M,N) : r;  r <= LListD_Fun (diag A) (r Un diag(llist(A))) \
    1.40  \         |] ==>  M=N";
    1.41  by (rtac (LListD_subset_diag RS subsetD RS diagE) 1);
    1.42  by (etac LListD_coinduct 1);
    1.43 @@ -538,8 +534,7 @@
    1.44  (** Alternative type-checking proofs for Lappend **)
    1.45  
    1.46  (*weak co-induction: bisimulation and case analysis on both variables*)
    1.47 -Goal
    1.48 -    "[| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
    1.49 +Goal "[| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
    1.50  by (res_inst_tac
    1.51      [("X", "UN u:llist(A). UN v: llist(A). {Lappend u v}")] llist_coinduct 1);
    1.52  by (Fast_tac 1);
    1.53 @@ -551,8 +546,7 @@
    1.54  qed "Lappend_type";
    1.55  
    1.56  (*strong co-induction: bisimulation and case analysis on one variable*)
    1.57 -Goal
    1.58 -    "[| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
    1.59 +Goal "[| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
    1.60  by (res_inst_tac [("X", "(%u. Lappend u N)``llist(A)")] llist_coinduct 1);
    1.61  by (etac imageI 1);
    1.62  by (rtac image_subsetI 1);
    1.63 @@ -627,8 +621,7 @@
    1.64  by (Fast_tac 1);
    1.65  qed "LListD_Fun_subset_Sigma_llist";
    1.66  
    1.67 -Goal
    1.68 -    "prod_fun Rep_llist Rep_llist `` r <= \
    1.69 +Goal "prod_fun Rep_llist Rep_llist `` r <= \
    1.70  \    (llist(range Leaf)) Times (llist(range Leaf))";
    1.71  by (fast_tac (claset() delrules [image_subsetI]
    1.72  		       addIs [Rep_llist]) 1);
    1.73 @@ -643,8 +636,7 @@
    1.74  by (asm_simp_tac (simpset() addsimps [Abs_llist_inverse]) 1);
    1.75  qed "prod_fun_lemma";
    1.76  
    1.77 -Goal
    1.78 -    "prod_fun Rep_llist  Rep_llist `` range(%x. (x, x)) = \
    1.79 +Goal "prod_fun Rep_llist  Rep_llist `` range(%x. (x, x)) = \
    1.80  \    diag(llist(range Leaf))";
    1.81  by (rtac equalityI 1);
    1.82  by (fast_tac (claset() addIs [Rep_llist]) 1);
    1.83 @@ -779,8 +771,7 @@
    1.84  
    1.85  (** Two lemmas about natrec n x (%m.g), which is essentially (g^n)(x) **)
    1.86  
    1.87 -Goal
    1.88 -    "nat_rec (LCons b l) (%m. lmap(f)) n =      \
    1.89 +Goal "nat_rec (LCons b l) (%m. lmap(f)) n =      \
    1.90  \    LCons (nat_rec b (%m. f) n) (nat_rec l (%m. lmap(f)) n)";
    1.91  by (induct_tac "n" 1);
    1.92  by (ALLGOALS Asm_simp_tac);