src/HOL/Induct/LList.ML
changeset 5996 6b6e0ede3517
parent 5977 9f0c8869cf71
child 7256 0a69baf28961
equal deleted inserted replaced
5995:450cd1f0270b 5996:6b6e0ede3517
   619     "r <= (llist A) Times (llist A) ==> \
   619     "r <= (llist A) Times (llist A) ==> \
   620 \           LListD_Fun (diag A) r <= (llist A) Times (llist A)";
   620 \           LListD_Fun (diag A) r <= (llist A) Times (llist A)";
   621 by (stac llist_unfold 1);
   621 by (stac llist_unfold 1);
   622 by (simp_tac (simpset() addsimps [NIL_def, CONS_def]) 1);
   622 by (simp_tac (simpset() addsimps [NIL_def, CONS_def]) 1);
   623 by (Fast_tac 1);
   623 by (Fast_tac 1);
   624 qed "LListD_Fun_subset_Sigma_llist";
   624 qed "LListD_Fun_subset_Times_llist";
   625 
   625 
   626 Goal "prod_fun Rep_LList Rep_LList `` r <= \
   626 Goal "prod_fun Rep_LList Rep_LList `` r <= \
   627 \    (llist(range Leaf)) Times (llist(range Leaf))";
   627 \    (llist(range Leaf)) Times (llist(range Leaf))";
   628 by (fast_tac (claset() delrules [image_subsetI]
   628 by (fast_tac (claset() delrules [image_subsetI]
   629 		       addIs [Rep_LList RS LListD]) 1);
   629 		       addIs [Rep_LList RS LListD]) 1);
   630 qed "subset_Sigma_llist";
   630 qed "subset_Times_llist";
   631 
   631 
   632 Goal "r <= (llist(range Leaf)) Times (llist(range Leaf)) ==> \
   632 Goal "r <= (llist(range Leaf)) Times (llist(range Leaf)) ==> \
   633 \    prod_fun (Rep_LList o Abs_LList) (Rep_LList o Abs_LList) `` r <= r";
   633 \    prod_fun (Rep_LList o Abs_LList) (Rep_LList o Abs_LList) `` r <= r";
   634 by Safe_tac;
   634 by Safe_tac;
   635 by (etac (subsetD RS SigmaE2) 1);
   635 by (etac (subsetD RS SigmaE2) 1);
   666 by (etac (image_mono RS subset_trans) 1);
   666 by (etac (image_mono RS subset_trans) 1);
   667 by (rtac (image_compose RS subst) 1);
   667 by (rtac (image_compose RS subst) 1);
   668 by (rtac (prod_fun_compose RS subst) 1);
   668 by (rtac (prod_fun_compose RS subst) 1);
   669 by (stac image_Un 1);
   669 by (stac image_Un 1);
   670 by (stac prod_fun_range_eq_diag 1);
   670 by (stac prod_fun_range_eq_diag 1);
   671 by (rtac (LListD_Fun_subset_Sigma_llist RS prod_fun_lemma) 1);
   671 by (rtac (LListD_Fun_subset_Times_llist RS prod_fun_lemma) 1);
   672 by (rtac (subset_Sigma_llist RS Un_least) 1);
   672 by (rtac (subset_Times_llist RS Un_least) 1);
   673 by (rtac diag_subset_Sigma 1);
   673 by (rtac diag_subset_Times 1);
   674 qed "llist_equalityI";
   674 qed "llist_equalityI";
   675 
   675 
   676 (** Rules to prove the 2nd premise of llist_equalityI **)
   676 (** Rules to prove the 2nd premise of llist_equalityI **)
   677 Goalw [llistD_Fun_def,LNil_def] "(LNil,LNil) : llistD_Fun(r)";
   677 Goalw [llistD_Fun_def,LNil_def] "(LNil,LNil) : llistD_Fun(r)";
   678 by (rtac (LListD_Fun_NIL_I RS prod_fun_imageI) 1);
   678 by (rtac (LListD_Fun_NIL_I RS prod_fun_imageI) 1);