import Sublist rather than PrefixOrder to avoid unnecessary class instantiation
authortraytel
Tue Nov 13 12:06:43 2012 +0100 (2012-11-13)
changeset 50058bb1fadeba35e
parent 50057 57209cfbf16b
child 50059 a292751fb345
import Sublist rather than PrefixOrder to avoid unnecessary class instantiation
src/HOL/BNF/BNF_GFP.thy
src/HOL/BNF/Tools/bnf_gfp.ML
src/HOL/BNF/Tools/bnf_gfp_tactics.ML
src/HOL/BNF/Tools/bnf_gfp_util.ML
     1.1 --- a/src/HOL/BNF/BNF_GFP.thy	Tue Nov 13 09:08:32 2012 +0100
     1.2 +++ b/src/HOL/BNF/BNF_GFP.thy	Tue Nov 13 12:06:43 2012 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  header {* Greatest Fixed Point Operation on Bounded Natural Functors *}
     1.5  
     1.6  theory BNF_GFP
     1.7 -imports BNF_FP Equiv_Relations_More "~~/src/HOL/Library/Prefix_Order"
     1.8 +imports BNF_FP Equiv_Relations_More "~~/src/HOL/Library/Sublist"
     1.9  keywords
    1.10    "codata" :: thy_decl
    1.11  begin
    1.12 @@ -163,9 +163,9 @@
    1.13  (*Extended Sublist*)
    1.14  
    1.15  definition prefCl where
    1.16 -  "prefCl Kl = (\<forall> kl1 kl2. kl1 \<le> kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl)"
    1.17 +  "prefCl Kl = (\<forall> kl1 kl2. prefixeq kl1 kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl)"
    1.18  definition PrefCl where
    1.19 -  "PrefCl A n = (\<forall>kl kl'. kl \<in> A n \<and> kl' \<le> kl \<longrightarrow> (\<exists>m\<le>n. kl' \<in> A m))"
    1.20 +  "PrefCl A n = (\<forall>kl kl'. kl \<in> A n \<and> prefixeq kl' kl \<longrightarrow> (\<exists>m\<le>n. kl' \<in> A m))"
    1.21  
    1.22  lemma prefCl_UN:
    1.23    "\<lbrakk>\<And>n. PrefCl A n\<rbrakk> \<Longrightarrow> prefCl (\<Union>n. A n)"
    1.24 @@ -185,9 +185,9 @@
    1.25  unfolding prefCl_def Shift_def
    1.26  proof safe
    1.27    fix kl1 kl2
    1.28 -  assume "\<forall>kl1 kl2. kl1 \<le> kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl"
    1.29 -    "kl1 \<le> kl2" "k # kl2 \<in> Kl"
    1.30 -  thus "k # kl1 \<in> Kl" using Cons_prefix_Cons[of k kl1 k kl2] by blast
    1.31 +  assume "\<forall>kl1 kl2. prefixeq kl1 kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl"
    1.32 +    "prefixeq kl1 kl2" "k # kl2 \<in> Kl"
    1.33 +  thus "k # kl1 \<in> Kl" using Cons_prefixeq_Cons[of k kl1 k kl2] by blast
    1.34  qed
    1.35  
    1.36  lemma not_in_Shift: "kl \<notin> Shift Kl x \<Longrightarrow> x # kl \<notin> Kl"
    1.37 @@ -196,7 +196,7 @@
    1.38  lemma prefCl_Succ: "\<lbrakk>prefCl Kl; k # kl \<in> Kl\<rbrakk> \<Longrightarrow> k \<in> Succ Kl []"
    1.39  unfolding Succ_def proof
    1.40    assume "prefCl Kl" "k # kl \<in> Kl"
    1.41 -  moreover have "k # [] \<le> k # kl" by auto
    1.42 +  moreover have "prefixeq (k # []) (k # kl)" by auto
    1.43    ultimately have "k # [] \<in> Kl" unfolding prefCl_def by blast
    1.44    thus "[] @ [k] \<in> Kl" by simp
    1.45  qed
     2.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Tue Nov 13 09:08:32 2012 +0100
     2.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Tue Nov 13 12:06:43 2012 +0100
     2.3 @@ -1610,7 +1610,7 @@
     2.4      val prefCl_Lev_thms =
     2.5        let
     2.6          fun mk_conjunct i z = HOLogic.mk_imp
     2.7 -          (HOLogic.mk_conj (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z), mk_subset kl_copy kl),
     2.8 +          (HOLogic.mk_conj (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z), mk_prefixeq kl_copy kl),
     2.9            HOLogic.mk_mem (kl_copy, mk_Lev ss (mk_size kl_copy) i $ z));
    2.10          val goal = list_all_free (kl :: kl_copy :: zs)
    2.11            (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs));
     3.1 --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Tue Nov 13 09:08:32 2012 +0100
     3.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Tue Nov 13 12:06:43 2012 +0100
     3.3 @@ -658,7 +658,7 @@
     3.4        REPEAT_DETERM o rtac allI,
     3.5        CONJ_WRAP' (fn Lev_0 =>
     3.6          EVERY' [rtac impI, etac conjE, dtac (Lev_0 RS equalityD1 RS set_mp),
     3.7 -          etac @{thm singletonE}, hyp_subst_tac, dtac @{thm prefix_Nil[THEN subst, of "%x. x"]},
     3.8 +          etac @{thm singletonE}, hyp_subst_tac, dtac @{thm prefixeq_Nil[THEN subst, of "%x. x"]},
     3.9            hyp_subst_tac, rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
    3.10            rtac Lev_0, rtac @{thm singletonI}]) Lev_0s,
    3.11        REPEAT_DETERM o rtac allI,
    3.12 @@ -666,7 +666,7 @@
    3.13          EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS set_mp),
    3.14            CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
    3.15              (fn i => EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
    3.16 -              dtac @{thm prefix_Cons[THEN subst, of "%x. x"]}, etac disjE, hyp_subst_tac,
    3.17 +              dtac @{thm prefixeq_Cons[THEN subst, of "%x. x"]}, etac disjE, hyp_subst_tac,
    3.18                rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
    3.19                rtac Lev_0, rtac @{thm singletonI},
    3.20                REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac,
    3.21 @@ -857,7 +857,7 @@
    3.22          rtac conjI,
    3.23            rtac @{thm prefCl_UN}, rtac ssubst, rtac @{thm PrefCl_def}, REPEAT_DETERM o rtac allI,
    3.24            rtac impI, etac conjE, rtac exI, rtac conjI, rtac @{thm ord_le_eq_trans},
    3.25 -          etac @{thm prefix_length_le}, etac length_Lev, rtac prefCl_Lev, etac conjI, atac,
    3.26 +          etac @{thm prefixeq_length_le}, etac length_Lev, rtac prefCl_Lev, etac conjI, atac,
    3.27          rtac conjI,
    3.28            rtac ballI, etac @{thm UN_E}, rtac conjI,
    3.29            if n = 1 then K all_tac else rtac (mk_sumEN n),
     4.1 --- a/src/HOL/BNF/Tools/bnf_gfp_util.ML	Tue Nov 13 09:08:32 2012 +0100
     4.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_util.ML	Tue Nov 13 12:06:43 2012 +0100
     4.3 @@ -25,6 +25,7 @@
     4.4    val mk_nat_rec: term -> term -> term
     4.5    val mk_pickWP: term -> term -> term -> term -> term -> term
     4.6    val mk_prefCl: term -> term
     4.7 +  val mk_prefixeq: term -> term -> term
     4.8    val mk_proj: term -> term
     4.9    val mk_quotient: term -> term -> term
    4.10    val mk_shift: term -> term -> term
    4.11 @@ -93,6 +94,9 @@
    4.12  fun mk_prefCl A =
    4.13    Const (@{const_name prefCl}, fastype_of A --> HOLogic.boolT) $ A;
    4.14  
    4.15 +fun mk_prefixeq xs ys =
    4.16 +  Const (@{const_name prefixeq}, fastype_of xs --> fastype_of ys --> HOLogic.boolT) $ xs $ ys;
    4.17 +
    4.18  fun mk_clists r =
    4.19    let val T = fastype_of r;
    4.20    in Const (@{const_name clists}, T --> mk_relT (`I (HOLogic.listT (fst (dest_relT T))))) $ r end;