merged
authorhaftmann
Fri Sep 25 09:50:31 2009 +0200 (2009-09-25)
changeset 3270504ce6bb14d85
parent 32682 304a47739407
parent 32704 6f0a56d255f4
child 32706 b68f3afdc137
merged
src/HOL/Finite_Set.thy
src/HOL/Library/Executable_Set.thy
src/HOL/Predicate.thy
     1.1 --- a/NEWS	Thu Sep 24 19:14:18 2009 +0200
     1.2 +++ b/NEWS	Fri Sep 25 09:50:31 2009 +0200
     1.3 @@ -94,13 +94,18 @@
     1.4    - mere abbreviations:
     1.5      Set.empty               (for bot)
     1.6      Set.UNIV                (for top)
     1.7 +    Set.inter               (for inf)
     1.8 +    Set.union               (for sup)
     1.9      Complete_Lattice.Inter  (for Inf)
    1.10      Complete_Lattice.Union  (for Sup)
    1.11      Complete_Lattice.INTER  (for INFI)
    1.12      Complete_Lattice.UNION  (for SUPR)
    1.13    - object-logic definitions as far as appropriate
    1.14  
    1.15 -  INCOMPATIBILITY.
    1.16 +INCOMPATIBILITY.  Care is required when theorems Int_subset_iff or
    1.17 +Un_subset_iff are explicitly deleted as default simp rules;  then
    1.18 +also their lattice counterparts le_inf_iff and le_sup_iff have to be
    1.19 +deleted to achieve the desired effect.
    1.20  
    1.21  * Rules inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no
    1.22  simp rules by default any longer.  The same applies to
     2.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Thu Sep 24 19:14:18 2009 +0200
     2.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Fri Sep 25 09:50:31 2009 +0200
     2.3 @@ -212,7 +212,7 @@
     2.4    apply (induct set: finite)
     2.5     apply simp
     2.6    apply (simp add: foldD_insert foldD_commute Int_insert_left insert_absorb
     2.7 -    Int_mono2 Un_subset_iff)
     2.8 +    Int_mono2)
     2.9    done
    2.10  
    2.11  lemma (in LCD) foldD_nest_Un_disjoint:
    2.12 @@ -274,14 +274,14 @@
    2.13    apply (simp add: AC insert_absorb Int_insert_left
    2.14      LCD.foldD_insert [OF LCD.intro [of D]]
    2.15      LCD.foldD_closed [OF LCD.intro [of D]]
    2.16 -    Int_mono2 Un_subset_iff)
    2.17 +    Int_mono2)
    2.18    done
    2.19  
    2.20  lemma (in ACeD) foldD_Un_disjoint:
    2.21    "[| finite A; finite B; A Int B = {}; A \<subseteq> D; B \<subseteq> D |] ==>
    2.22      foldD D f e (A Un B) = foldD D f e A \<cdot> foldD D f e B"
    2.23    by (simp add: foldD_Un_Int
    2.24 -    left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff)
    2.25 +    left_commute LCD.foldD_closed [OF LCD.intro [of D]])
    2.26  
    2.27  
    2.28  subsubsection {* Products over Finite Sets *}
    2.29 @@ -377,7 +377,7 @@
    2.30    from insert have A: "g \<in> A -> carrier G" by fast
    2.31    from insert A a show ?case
    2.32      by (simp add: m_ac Int_insert_left insert_absorb finprod_closed
    2.33 -          Int_mono2 Un_subset_iff) 
    2.34 +          Int_mono2) 
    2.35  qed
    2.36  
    2.37  lemma finprod_Un_disjoint:
     3.1 --- a/src/HOL/Auth/Guard/Extensions.thy	Thu Sep 24 19:14:18 2009 +0200
     3.2 +++ b/src/HOL/Auth/Guard/Extensions.thy	Fri Sep 25 09:50:31 2009 +0200
     3.3 @@ -11,7 +11,9 @@
     3.4  
     3.5  header {*Extensions to Standard Theories*}
     3.6  
     3.7 -theory Extensions imports "../Event" begin
     3.8 +theory Extensions
     3.9 +imports "../Event"
    3.10 +begin
    3.11  
    3.12  subsection{*Extensions to Theory @{text Set}*}
    3.13  
    3.14 @@ -173,7 +175,7 @@
    3.15  subsubsection{*lemmas on analz*}
    3.16  
    3.17  lemma analz_UnI1 [intro]: "X:analz G ==> X:analz (G Un H)"
    3.18 -by (subgoal_tac "G <= G Un H", auto dest: analz_mono)
    3.19 +  by (subgoal_tac "G <= G Un H") (blast dest: analz_mono)+
    3.20  
    3.21  lemma analz_sub: "[| X:analz G; G <= H |] ==> X:analz H"
    3.22  by (auto dest: analz_mono)
     4.1 --- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Thu Sep 24 19:14:18 2009 +0200
     4.2 +++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Fri Sep 25 09:50:31 2009 +0200
     4.3 @@ -1747,7 +1747,7 @@
     4.4        have "assigns (In1l e2) \<subseteq> dom (locals (store s2))"
     4.5  	by (simp add: need_second_arg_def)
     4.6        with s2
     4.7 -      show ?thesis using False by (simp add: Un_subset_iff)
     4.8 +      show ?thesis using False by simp
     4.9      qed
    4.10    next
    4.11      case Super thus ?case by simp
     5.1 --- a/src/HOL/Bali/TypeSafe.thy	Thu Sep 24 19:14:18 2009 +0200
     5.2 +++ b/src/HOL/Bali/TypeSafe.thy	Fri Sep 25 09:50:31 2009 +0200
     5.3 @@ -2953,7 +2953,7 @@
     5.4  	  by simp
     5.5  	from da_e1 s0_s1 True obtain E1' where
     5.6  	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e1\<guillemotright> E1'"
     5.7 -	  by - (rule da_weakenE, auto iff del: Un_subset_iff)
     5.8 +	  by - (rule da_weakenE, auto iff del: Un_subset_iff le_sup_iff)
     5.9  	with conf_s1 wt_e1
    5.10  	obtain 
    5.11  	  "s2\<Colon>\<preceq>(G, L)"
    5.12 @@ -2972,7 +2972,7 @@
    5.13  	  by simp
    5.14  	from da_e2 s0_s1 False obtain E2' where
    5.15  	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e2\<guillemotright> E2'"
    5.16 -	  by - (rule da_weakenE, auto iff del: Un_subset_iff)
    5.17 +	  by - (rule da_weakenE, auto iff del: Un_subset_iff le_sup_iff)
    5.18  	with conf_s1 wt_e2
    5.19  	obtain 
    5.20  	  "s2\<Colon>\<preceq>(G, L)"
     6.1 --- a/src/HOL/Finite_Set.thy	Thu Sep 24 19:14:18 2009 +0200
     6.2 +++ b/src/HOL/Finite_Set.thy	Fri Sep 25 09:50:31 2009 +0200
     6.3 @@ -1565,9 +1565,7 @@
     6.4    apply (rule finite_subset)
     6.5    prefer 2
     6.6    apply assumption
     6.7 -  apply auto
     6.8 -  apply (rule setsum_cong)
     6.9 -  apply auto
    6.10 +  apply (auto simp add: sup_absorb2)
    6.11  done
    6.12  
    6.13  lemma setsum_right_distrib: 
     7.1 --- a/src/HOL/Hoare_Parallel/Gar_Coll.thy	Thu Sep 24 19:14:18 2009 +0200
     7.2 +++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy	Fri Sep 25 09:50:31 2009 +0200
     7.3 @@ -253,7 +253,7 @@
     7.4      \<and> ( \<acute>obc < Blacks \<acute>M \<or> \<acute>Safe)}."
     7.5  apply (unfold Propagate_Black_def  PBInv_def Auxk_def collector_defs)
     7.6  apply annhoare
     7.7 -apply(simp_all add:Graph6 Graph7 Graph8 Graph12)
     7.8 +apply(simp_all add: Graph6 Graph7 Graph8 Graph12)
     7.9         apply force
    7.10        apply force
    7.11       apply force
    7.12 @@ -297,8 +297,6 @@
    7.13  apply(erule subset_psubset_trans)
    7.14  apply(erule Graph11)
    7.15  apply fast
    7.16 ---{* 3 subgoals left *}
    7.17 -apply force
    7.18  --{* 2 subgoals left *}
    7.19  apply clarify
    7.20  apply(simp add:Proper_Edges_def Graph6 Graph7 Graph8 Graph12)
     8.1 --- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Thu Sep 24 19:14:18 2009 +0200
     8.2 +++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Fri Sep 25 09:50:31 2009 +0200
     8.3 @@ -276,8 +276,6 @@
     8.4    apply(force)
     8.5   apply(force)
     8.6  apply(rule disjI2, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
     8.7 ---{* 3 subgoals left *}
     8.8 -apply force
     8.9  --{* 2 subgoals left *}
    8.10  apply clarify
    8.11  apply(conjI_tac)
    8.12 @@ -1235,9 +1233,9 @@
    8.13  apply(unfold mul_modules mul_collector_defs mul_mutator_defs)
    8.14  apply(tactic  {* TRYALL (interfree_aux_tac) *})
    8.15  --{* 76 subgoals left *}
    8.16 -apply (clarify,simp add: nth_list_update)+
    8.17 +apply (clarsimp simp add: nth_list_update)+
    8.18  --{* 56 subgoals left *}
    8.19 -apply(clarify,simp add:Mul_AppendInv_def Append_to_free0 nth_list_update)+
    8.20 +apply (clarsimp simp add: Mul_AppendInv_def Append_to_free0 nth_list_update)+
    8.21  done
    8.22  
    8.23  subsubsection {* The Multi-Mutator Garbage Collection Algorithm *}
     9.1 --- a/src/HOL/Hoare_Parallel/RG_Hoare.thy	Thu Sep 24 19:14:18 2009 +0200
     9.2 +++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy	Fri Sep 25 09:50:31 2009 +0200
     9.3 @@ -4,8 +4,8 @@
     9.4  
     9.5  subsection {* Proof System for Component Programs *}
     9.6  
     9.7 -declare Un_subset_iff [iff del]
     9.8 -declare Cons_eq_map_conv[iff]
     9.9 +declare Un_subset_iff [simp del] le_sup_iff [simp del]
    9.10 +declare Cons_eq_map_conv [iff]
    9.11  
    9.12  constdefs
    9.13    stable :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool"  
    10.1 --- a/src/HOL/Inductive.thy	Thu Sep 24 19:14:18 2009 +0200
    10.2 +++ b/src/HOL/Inductive.thy	Fri Sep 25 09:50:31 2009 +0200
    10.3 @@ -83,7 +83,7 @@
    10.4        and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)"
    10.5    shows "P(a)"
    10.6    by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp])
    10.7 -    (auto simp: inf_set_eq intro: indhyp)
    10.8 +    (auto simp: intro: indhyp)
    10.9  
   10.10  lemma lfp_ordinal_induct:
   10.11    fixes f :: "'a\<Colon>complete_lattice \<Rightarrow> 'a"
   10.12 @@ -184,7 +184,7 @@
   10.13  
   10.14  text{*strong version, thanks to Coen and Frost*}
   10.15  lemma coinduct_set: "[| mono(f);  a: X;  X \<subseteq> f(X Un gfp(f)) |] ==> a : gfp(f)"
   10.16 -by (blast intro: weak_coinduct [OF _ coinduct_lemma, simplified sup_set_eq])
   10.17 +by (blast intro: weak_coinduct [OF _ coinduct_lemma])
   10.18  
   10.19  lemma coinduct: "[| mono(f); X \<le> f (sup X (gfp f)) |] ==> X \<le> gfp(f)"
   10.20    apply (rule order_trans)
    11.1 --- a/src/HOL/Library/Euclidean_Space.thy	Thu Sep 24 19:14:18 2009 +0200
    11.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Fri Sep 25 09:50:31 2009 +0200
    11.3 @@ -3649,10 +3649,7 @@
    11.4      from setsum_restrict_set[OF fS, of "\<lambda>v. u v *s v" S', symmetric] SS'
    11.5      have "setsum (\<lambda>v. ?u v *s v) S = setsum (\<lambda>v. u v *s v) S'"
    11.6        unfolding cond_value_iff cond_application_beta
    11.7 -      apply (simp add: cond_value_iff cong del: if_weak_cong)
    11.8 -      apply (rule setsum_cong)
    11.9 -      apply auto
   11.10 -      done
   11.11 +      by (simp add: cond_value_iff inf_absorb2 cong del: if_weak_cong)
   11.12      hence "setsum (\<lambda>v. ?u v *s v) S = y" by (metis u)
   11.13      hence "y \<in> ?rhs" by auto}
   11.14    moreover
    12.1 --- a/src/HOL/Library/Executable_Set.thy	Thu Sep 24 19:14:18 2009 +0200
    12.2 +++ b/src/HOL/Library/Executable_Set.thy	Fri Sep 25 09:50:31 2009 +0200
    12.3 @@ -12,6 +12,21 @@
    12.4  
    12.5  declare member [code] 
    12.6  
    12.7 +definition empty :: "'a set" where
    12.8 +  "empty = {}"
    12.9 +
   12.10 +declare empty_def [symmetric, code_unfold]
   12.11 +
   12.12 +definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
   12.13 +  "inter = op \<inter>"
   12.14 +
   12.15 +declare inter_def [symmetric, code_unfold]
   12.16 +
   12.17 +definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
   12.18 +  "union = op \<union>"
   12.19 +
   12.20 +declare union_def [symmetric, code_unfold]
   12.21 +
   12.22  definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   12.23    "subset = op \<le>"
   12.24  
   12.25 @@ -66,7 +81,7 @@
   12.26    Set ("\<module>Set")
   12.27  
   12.28  consts_code
   12.29 -  "Set.empty"         ("{*Fset.empty*}")
   12.30 +  "empty"             ("{*Fset.empty*}")
   12.31    "List_Set.is_empty" ("{*Fset.is_empty*}")
   12.32    "Set.insert"        ("{*Fset.insert*}")
   12.33    "List_Set.remove"   ("{*Fset.remove*}")
   12.34 @@ -74,14 +89,14 @@
   12.35    "List_Set.project"  ("{*Fset.filter*}")
   12.36    "Ball"              ("{*flip Fset.forall*}")
   12.37    "Bex"               ("{*flip Fset.exists*}")
   12.38 -  "op \<union>"              ("{*Fset.union*}")
   12.39 -  "op \<inter>"              ("{*Fset.inter*}")
   12.40 +  "union"             ("{*Fset.union*}")
   12.41 +  "inter"             ("{*Fset.inter*}")
   12.42    "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip Fset.subtract*}")
   12.43    "Union"             ("{*Fset.Union*}")
   12.44    "Inter"             ("{*Fset.Inter*}")
   12.45    card                ("{*Fset.card*}")
   12.46    fold                ("{*foldl o flip*}")
   12.47  
   12.48 -hide (open) const subset eq_set Inter Union flip
   12.49 +hide (open) const empty inter union subset eq_set Inter Union flip
   12.50  
   12.51  end
   12.52 \ No newline at end of file
    13.1 --- a/src/HOL/Library/Topology_Euclidean_Space.thy	Thu Sep 24 19:14:18 2009 +0200
    13.2 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Fri Sep 25 09:50:31 2009 +0200
    13.3 @@ -99,11 +99,9 @@
    13.4  
    13.5  lemma Diff_Diff_Int: "A - (A - B) = A \<inter> B" by blast
    13.6  lemma openin_closedin_eq: "openin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> closedin U (topspace U - S)"
    13.7 -  apply (auto simp add: closedin_def)
    13.8 +  apply (auto simp add: closedin_def Diff_Diff_Int inf_absorb2)
    13.9    apply (metis openin_subset subset_eq)
   13.10 -  apply (auto simp add: Diff_Diff_Int)
   13.11 -  apply (subgoal_tac "topspace U \<inter> S = S")
   13.12 -  by auto
   13.13 +  done
   13.14  
   13.15  lemma openin_closedin:  "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U - S))"
   13.16    by (simp add: openin_closedin_eq)
    14.1 --- a/src/HOL/MetisExamples/Message.thy	Thu Sep 24 19:14:18 2009 +0200
    14.2 +++ b/src/HOL/MetisExamples/Message.thy	Fri Sep 25 09:50:31 2009 +0200
    14.3 @@ -1,5 +1,4 @@
    14.4  (*  Title:      HOL/MetisTest/Message.thy
    14.5 -    ID:         $Id$
    14.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    14.7  
    14.8  Testing the metis method
    14.9 @@ -711,17 +710,17 @@
   14.10  proof (neg_clausify)
   14.11  assume 0: "analz (synth H) \<noteq> analz H \<union> synth H"
   14.12  have 1: "\<And>X1 X3. sup (analz (sup X3 X1)) (synth X3) = analz (sup (synth X3) X1)"
   14.13 -  by (metis analz_synth_Un sup_set_eq sup_set_eq sup_set_eq)
   14.14 +  by (metis analz_synth_Un)
   14.15  have 2: "sup (analz H) (synth H) \<noteq> analz (synth H)"
   14.16 -  by (metis 0 sup_set_eq)
   14.17 +  by (metis 0)
   14.18  have 3: "\<And>X1 X3. sup (synth X3) (analz (sup X3 X1)) = analz (sup (synth X3) X1)"
   14.19 -  by (metis 1 Un_commute sup_set_eq sup_set_eq)
   14.20 +  by (metis 1 Un_commute)
   14.21  have 4: "\<And>X3. sup (synth X3) (analz X3) = analz (sup (synth X3) {})"
   14.22 -  by (metis 3 Un_empty_right sup_set_eq)
   14.23 +  by (metis 3 Un_empty_right)
   14.24  have 5: "\<And>X3. sup (synth X3) (analz X3) = analz (synth X3)"
   14.25 -  by (metis 4 Un_empty_right sup_set_eq)
   14.26 +  by (metis 4 Un_empty_right)
   14.27  have 6: "\<And>X3. sup (analz X3) (synth X3) = analz (synth X3)"
   14.28 -  by (metis 5 Un_commute sup_set_eq sup_set_eq)
   14.29 +  by (metis 5 Un_commute)
   14.30  show "False"
   14.31    by (metis 2 6)
   14.32  qed
    15.1 --- a/src/HOL/MetisExamples/set.thy	Thu Sep 24 19:14:18 2009 +0200
    15.2 +++ b/src/HOL/MetisExamples/set.thy	Fri Sep 25 09:50:31 2009 +0200
    15.3 @@ -1,5 +1,4 @@
    15.4  (*  Title:      HOL/MetisExamples/set.thy
    15.5 -    ID:         $Id$
    15.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    15.7  
    15.8  Testing the metis method
    15.9 @@ -36,23 +35,23 @@
   15.10  assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
   15.11  assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
   15.12  have 6: "sup Y Z = X \<or> Y \<subseteq> X"
   15.13 -  by (metis 0 sup_set_eq)
   15.14 +  by (metis 0)
   15.15  have 7: "sup Y Z = X \<or> Z \<subseteq> X"
   15.16 -  by (metis 1 sup_set_eq)
   15.17 +  by (metis 1)
   15.18  have 8: "\<And>X3. sup Y Z = X \<or> X \<subseteq> X3 \<or> \<not> Y \<subseteq> X3 \<or> \<not> Z \<subseteq> X3"
   15.19 -  by (metis 5 sup_set_eq)
   15.20 +  by (metis 5)
   15.21  have 9: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
   15.22 -  by (metis 2 sup_set_eq)
   15.23 +  by (metis 2)
   15.24  have 10: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
   15.25 -  by (metis 3 sup_set_eq)
   15.26 +  by (metis 3)
   15.27  have 11: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
   15.28 -  by (metis 4 sup_set_eq)
   15.29 +  by (metis 4)
   15.30  have 12: "Z \<subseteq> X"
   15.31 -  by (metis Un_upper2 sup_set_eq 7)
   15.32 +  by (metis Un_upper2 7)
   15.33  have 13: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
   15.34 -  by (metis 8 Un_upper2 sup_set_eq)
   15.35 +  by (metis 8 Un_upper2)
   15.36  have 14: "Y \<subseteq> X"
   15.37 -  by (metis Un_upper1 sup_set_eq 6)
   15.38 +  by (metis Un_upper1 6)
   15.39  have 15: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
   15.40    by (metis 10 12)
   15.41  have 16: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
   15.42 @@ -66,17 +65,17 @@
   15.43  have 20: "Y \<subseteq> x \<or> sup Y Z \<noteq> X"
   15.44    by (metis 16 14)
   15.45  have 21: "sup Y Z = X \<or> X \<subseteq> sup Y Z"
   15.46 -  by (metis 13 Un_upper1 sup_set_eq)
   15.47 +  by (metis 13 Un_upper1)
   15.48  have 22: "sup Y Z = X \<or> \<not> sup Y Z \<subseteq> X"
   15.49    by (metis equalityI 21)
   15.50  have 23: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
   15.51 -  by (metis 22 Un_least sup_set_eq)
   15.52 +  by (metis 22 Un_least)
   15.53  have 24: "sup Y Z = X \<or> \<not> Y \<subseteq> X"
   15.54    by (metis 23 12)
   15.55  have 25: "sup Y Z = X"
   15.56    by (metis 24 14)
   15.57  have 26: "\<And>X3. X \<subseteq> X3 \<or> \<not> Z \<subseteq> X3 \<or> \<not> Y \<subseteq> X3"
   15.58 -  by (metis Un_least sup_set_eq 25)
   15.59 +  by (metis Un_least 25)
   15.60  have 27: "Y \<subseteq> x"
   15.61    by (metis 20 25)
   15.62  have 28: "Z \<subseteq> x"
   15.63 @@ -105,31 +104,31 @@
   15.64  assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
   15.65  assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
   15.66  have 6: "sup Y Z = X \<or> Y \<subseteq> X"
   15.67 -  by (metis 0 sup_set_eq)
   15.68 +  by (metis 0)
   15.69  have 7: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
   15.70 -  by (metis 2 sup_set_eq)
   15.71 +  by (metis 2)
   15.72  have 8: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
   15.73 -  by (metis 4 sup_set_eq)
   15.74 +  by (metis 4)
   15.75  have 9: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
   15.76 -  by (metis 5 sup_set_eq Un_upper2 sup_set_eq)
   15.77 +  by (metis 5 Un_upper2)
   15.78  have 10: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
   15.79 -  by (metis 3 sup_set_eq Un_upper2 sup_set_eq sup_set_eq)
   15.80 +  by (metis 3 Un_upper2)
   15.81  have 11: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X"
   15.82 -  by (metis 8 Un_upper2 sup_set_eq sup_set_eq)
   15.83 +  by (metis 8 Un_upper2)
   15.84  have 12: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
   15.85 -  by (metis 10 Un_upper1 sup_set_eq)
   15.86 +  by (metis 10 Un_upper1)
   15.87  have 13: "sup Y Z = X \<or> X \<subseteq> sup Y Z"
   15.88 -  by (metis 9 Un_upper1 sup_set_eq)
   15.89 +  by (metis 9 Un_upper1)
   15.90  have 14: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
   15.91 -  by (metis equalityI 13 Un_least sup_set_eq)
   15.92 +  by (metis equalityI 13 Un_least)
   15.93  have 15: "sup Y Z = X"
   15.94 -  by (metis 14 sup_set_eq 1 sup_set_eq sup_set_eq 6)
   15.95 +  by (metis 14 1 6)
   15.96  have 16: "Y \<subseteq> x"
   15.97 -  by (metis 7 Un_upper2 sup_set_eq sup_set_eq Un_upper1 sup_set_eq 15)
   15.98 +  by (metis 7 Un_upper2 Un_upper1 15)
   15.99  have 17: "\<not> X \<subseteq> x"
  15.100 -  by (metis 11 Un_upper1 sup_set_eq 15)
  15.101 +  by (metis 11 Un_upper1 15)
  15.102  have 18: "X \<subseteq> x"
  15.103 -  by (metis Un_least sup_set_eq 15 12 15 16)
  15.104 +  by (metis Un_least 15 12 15 16)
  15.105  show "False"
  15.106    by (metis 18 17)
  15.107  qed
  15.108 @@ -148,23 +147,23 @@
  15.109  assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
  15.110  assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
  15.111  have 6: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
  15.112 -  by (metis 3 sup_set_eq)
  15.113 +  by (metis 3)
  15.114  have 7: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
  15.115 -  by (metis 5 sup_set_eq Un_upper2 sup_set_eq)
  15.116 +  by (metis 5 Un_upper2)
  15.117  have 8: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
  15.118 -  by (metis 2 sup_set_eq Un_upper2 sup_set_eq sup_set_eq)
  15.119 +  by (metis 2 Un_upper2)
  15.120  have 9: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
  15.121 -  by (metis 6 Un_upper2 sup_set_eq sup_set_eq Un_upper1 sup_set_eq sup_set_eq)
  15.122 +  by (metis 6 Un_upper2 Un_upper1)
  15.123  have 10: "sup Y Z = X \<or> \<not> sup Y Z \<subseteq> X"
  15.124 -  by (metis equalityI 7 Un_upper1 sup_set_eq)
  15.125 +  by (metis equalityI 7 Un_upper1)
  15.126  have 11: "sup Y Z = X"
  15.127 -  by (metis 10 Un_least sup_set_eq sup_set_eq 1 sup_set_eq sup_set_eq 0 sup_set_eq)
  15.128 +  by (metis 10 Un_least 1 0)
  15.129  have 12: "Z \<subseteq> x"
  15.130    by (metis 9 11)
  15.131  have 13: "X \<subseteq> x"
  15.132 -  by (metis Un_least sup_set_eq 11 12 8 Un_upper1 sup_set_eq sup_set_eq 11)
  15.133 +  by (metis Un_least 11 12 8 Un_upper1 11)
  15.134  show "False"
  15.135 -  by (metis 13 4 sup_set_eq Un_upper2 sup_set_eq sup_set_eq Un_upper1 sup_set_eq sup_set_eq 11)
  15.136 +  by (metis 13 4 Un_upper2 Un_upper1 11)
  15.137  qed
  15.138  
  15.139  (*Example included in TPHOLs paper*)
  15.140 @@ -183,19 +182,19 @@
  15.141  assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
  15.142  assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
  15.143  have 6: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
  15.144 -  by (metis 4 sup_set_eq)
  15.145 +  by (metis 4)
  15.146  have 7: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
  15.147 -  by (metis 3 sup_set_eq Un_upper2 sup_set_eq sup_set_eq)
  15.148 +  by (metis 3 Un_upper2)
  15.149  have 8: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
  15.150 -  by (metis 7 Un_upper1 sup_set_eq sup_set_eq)
  15.151 +  by (metis 7 Un_upper1)
  15.152  have 9: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
  15.153 -  by (metis equalityI 5 sup_set_eq Un_upper2 sup_set_eq Un_upper1 sup_set_eq Un_least sup_set_eq)
  15.154 +  by (metis equalityI 5 Un_upper2 Un_upper1 Un_least)
  15.155  have 10: "Y \<subseteq> x"
  15.156 -  by (metis 2 sup_set_eq Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq 9 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq)
  15.157 +  by (metis 2 Un_upper2 1 Un_upper1 0 9 Un_upper2 1 Un_upper1 0)
  15.158  have 11: "X \<subseteq> x"
  15.159 -  by (metis Un_least sup_set_eq 9 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq 8 9 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq 10)
  15.160 +  by (metis Un_least 9 Un_upper2 1 Un_upper1 0 8 9 Un_upper2 1 Un_upper1 0 10)
  15.161  show "False"
  15.162 -  by (metis 11 6 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq 9 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq)
  15.163 +  by (metis 11 6 Un_upper2 1 Un_upper1 0 9 Un_upper2 1 Un_upper1 0)
  15.164  qed 
  15.165  
  15.166  ML {*AtpWrapper.problem_name := "set__equal_union"*}
  15.167 @@ -238,7 +237,7 @@
  15.168  
  15.169  lemma (*singleton_example_2:*)
  15.170       "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
  15.171 -by (metis Set.subsetI Union_upper insert_code mem_def set_eq_subset)
  15.172 +by (metis Set.subsetI Union_upper insert_iff set_eq_subset)
  15.173  
  15.174  lemma singleton_example_2:
  15.175       "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
    16.1 --- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Thu Sep 24 19:14:18 2009 +0200
    16.2 +++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Fri Sep 25 09:50:31 2009 +0200
    16.3 @@ -140,7 +140,7 @@
    16.4    apply fastsimp
    16.5    
    16.6    apply (erule disjE)
    16.7 -   apply (clarsimp simp add: Un_subset_iff)  
    16.8 +   apply clarsimp
    16.9     apply (drule method_wf_mdecl, assumption+)
   16.10     apply (clarsimp simp add: wf_mdecl_def wf_mhead_def)
   16.11     apply fastsimp
    17.1 --- a/src/HOL/Predicate.thy	Thu Sep 24 19:14:18 2009 +0200
    17.2 +++ b/src/HOL/Predicate.thy	Fri Sep 25 09:50:31 2009 +0200
    17.3 @@ -81,7 +81,7 @@
    17.4  lemma sup2_iff: "sup A B x y \<longleftrightarrow> A x y | B x y"
    17.5    by (simp add: sup_fun_eq sup_bool_eq)
    17.6  
    17.7 -lemma sup_Un_eq [pred_set_conv]: "sup (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
    17.8 +lemma sup_Un_eq: "sup (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
    17.9    by (simp add: sup1_iff expand_fun_eq)
   17.10  
   17.11  lemma sup_Un_eq2 [pred_set_conv]: "sup (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)"
   17.12 @@ -125,7 +125,7 @@
   17.13  lemma inf2_iff: "inf A B x y \<longleftrightarrow> A x y \<and> B x y"
   17.14    by (simp add: inf_fun_eq inf_bool_eq)
   17.15  
   17.16 -lemma inf_Int_eq [pred_set_conv]: "inf (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
   17.17 +lemma inf_Int_eq: "inf (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
   17.18    by (simp add: inf1_iff expand_fun_eq)
   17.19  
   17.20  lemma inf_Int_eq2 [pred_set_conv]: "inf (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)"
    18.1 --- a/src/HOL/Set.thy	Thu Sep 24 19:14:18 2009 +0200
    18.2 +++ b/src/HOL/Set.thy	Fri Sep 25 09:50:31 2009 +0200
    18.3 @@ -652,8 +652,8 @@
    18.4  
    18.5  subsubsection {* Binary union -- Un *}
    18.6  
    18.7 -definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
    18.8 -  sup_set_eq [symmetric]: "A Un B = sup A B"
    18.9 +abbreviation union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
   18.10 +  "op Un \<equiv> sup"
   18.11  
   18.12  notation (xsymbols)
   18.13    union  (infixl "\<union>" 65)
   18.14 @@ -663,7 +663,7 @@
   18.15  
   18.16  lemma Un_def:
   18.17    "A \<union> B = {x. x \<in> A \<or> x \<in> B}"
   18.18 -  by (simp add: sup_fun_eq sup_bool_eq sup_set_eq [symmetric] Collect_def mem_def)
   18.19 +  by (simp add: sup_fun_eq sup_bool_eq Collect_def mem_def)
   18.20  
   18.21  lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)"
   18.22    by (unfold Un_def) blast
   18.23 @@ -689,15 +689,13 @@
   18.24    by (simp add: Collect_def mem_def insert_compr Un_def)
   18.25  
   18.26  lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
   18.27 -  apply (fold sup_set_eq)
   18.28 -  apply (erule mono_sup)
   18.29 -  done
   18.30 +  by (fact mono_sup)
   18.31  
   18.32  
   18.33  subsubsection {* Binary intersection -- Int *}
   18.34  
   18.35 -definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
   18.36 -  inf_set_eq [symmetric]: "A Int B = inf A B"
   18.37 +abbreviation inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
   18.38 +  "op Int \<equiv> inf"
   18.39  
   18.40  notation (xsymbols)
   18.41    inter  (infixl "\<inter>" 70)
   18.42 @@ -707,7 +705,7 @@
   18.43  
   18.44  lemma Int_def:
   18.45    "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
   18.46 -  by (simp add: inf_fun_eq inf_bool_eq inf_set_eq [symmetric] Collect_def mem_def)
   18.47 +  by (simp add: inf_fun_eq inf_bool_eq Collect_def mem_def)
   18.48  
   18.49  lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
   18.50    by (unfold Int_def) blast
   18.51 @@ -725,9 +723,7 @@
   18.52    by simp
   18.53  
   18.54  lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
   18.55 -  apply (fold inf_set_eq)
   18.56 -  apply (erule mono_inf)
   18.57 -  done
   18.58 +  by (fact mono_inf)
   18.59  
   18.60  
   18.61  subsubsection {* Set difference *}
    19.1 --- a/src/HOL/Tools/Function/fundef_lib.ML	Thu Sep 24 19:14:18 2009 +0200
    19.2 +++ b/src/HOL/Tools/Function/fundef_lib.ML	Fri Sep 25 09:50:31 2009 +0200
    19.3 @@ -170,7 +170,7 @@
    19.4   end
    19.5  
    19.6  (* instance for unions *)
    19.7 -fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Set.union}
    19.8 +fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Lattices.sup}
    19.9    (map (fn t => t RS eq_reflection) (@{thms Un_ac} @
   19.10                                       @{thms Un_empty_right} @
   19.11                                       @{thms Un_empty_left})) t
    20.1 --- a/src/HOL/Tools/Function/termination.ML	Thu Sep 24 19:14:18 2009 +0200
    20.2 +++ b/src/HOL/Tools/Function/termination.ML	Fri Sep 25 09:50:31 2009 +0200
    20.3 @@ -145,7 +145,7 @@
    20.4  
    20.5  fun mk_sum_skel rel =
    20.6    let
    20.7 -    val cs = FundefLib.dest_binop_list @{const_name Set.union} rel
    20.8 +    val cs = FundefLib.dest_binop_list @{const_name Lattices.sup} rel
    20.9      fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
   20.10        let
   20.11          val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
   20.12 @@ -233,7 +233,7 @@
   20.13  fun CALLS tac i st =
   20.14    if Thm.no_prems st then all_tac st
   20.15    else case Thm.term_of (Thm.cprem_of st i) of
   20.16 -    (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name Set.union} rel, i) st
   20.17 +    (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name Lattices.sup} rel, i) st
   20.18    |_ => no_tac st
   20.19  
   20.20  type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
   20.21 @@ -293,7 +293,7 @@
   20.22            if null ineqs then
   20.23                Const (@{const_name Set.empty}, fastype_of rel)
   20.24            else
   20.25 -              foldr1 (HOLogic.mk_binop @{const_name Set.union}) (map mk_compr ineqs)
   20.26 +              foldr1 (HOLogic.mk_binop @{const_name Lattices.sup}) (map mk_compr ineqs)
   20.27  
   20.28        fun solve_membership_tac i =
   20.29            (EVERY' (replicate (i - 2) (rtac @{thm UnI2}))  (* pick the right component of the union *)
    21.1 --- a/src/HOL/Tools/inductive_set.ML	Thu Sep 24 19:14:18 2009 +0200
    21.2 +++ b/src/HOL/Tools/inductive_set.ML	Fri Sep 25 09:50:31 2009 +0200
    21.3 @@ -74,8 +74,8 @@
    21.4          in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs))
    21.5            (p (fold (Logic.all o Var) vs t) f)
    21.6          end;
    21.7 -      fun mkop "op &" T x = SOME (Const (@{const_name Set.inter}, T --> T --> T), x)
    21.8 -        | mkop "op |" T x = SOME (Const (@{const_name Set.union}, T --> T --> T), x)
    21.9 +      fun mkop "op &" T x = SOME (Const (@{const_name Lattices.inf}, T --> T --> T), x)
   21.10 +        | mkop "op |" T x = SOME (Const (@{const_name Lattices.sup}, T --> T --> T), x)
   21.11          | mkop _ _ _ = NONE;
   21.12        fun mk_collect p T t =
   21.13          let val U = HOLogic.dest_setT T
    22.1 --- a/src/HOL/UNITY/Follows.thy	Thu Sep 24 19:14:18 2009 +0200
    22.2 +++ b/src/HOL/UNITY/Follows.thy	Fri Sep 25 09:50:31 2009 +0200
    22.3 @@ -1,5 +1,4 @@
    22.4  (*  Title:      HOL/UNITY/Follows
    22.5 -    ID:         $Id$
    22.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    22.7      Copyright   1998  University of Cambridge
    22.8  *)
    22.9 @@ -160,7 +159,7 @@
   22.10  lemma Follows_Un: 
   22.11      "[| F \<in> f' Fols f;  F \<in> g' Fols g |]  
   22.12       ==> F \<in> (%s. (f' s) \<union> (g' s)) Fols (%s. (f s) \<union> (g s))"
   22.13 -apply (simp add: Follows_def Increasing_Un Always_Un del: Un_subset_iff, auto)
   22.14 +apply (simp add: Follows_def Increasing_Un Always_Un del: Un_subset_iff le_sup_iff, auto)
   22.15  apply (rule LeadsTo_Trans)
   22.16  apply (blast intro: Follows_Un_lemma)
   22.17  (*Weakening is used to exchange Un's arguments*)
    23.1 --- a/src/HOL/UNITY/ProgressSets.thy	Thu Sep 24 19:14:18 2009 +0200
    23.2 +++ b/src/HOL/UNITY/ProgressSets.thy	Fri Sep 25 09:50:31 2009 +0200
    23.3 @@ -1,5 +1,4 @@
    23.4  (*  Title:      HOL/UNITY/ProgressSets
    23.5 -    ID:         $Id$
    23.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    23.7      Copyright   2003  University of Cambridge
    23.8  
    23.9 @@ -245,7 +244,7 @@
   23.10    then have "cl C (T\<inter>?r) \<subseteq> ?r"
   23.11      by (blast intro!: subset_wens) 
   23.12    then have cl_subset: "cl C (T\<inter>?r) \<subseteq> T\<inter>?r"
   23.13 -    by (simp add: Int_subset_iff cl_ident TC
   23.14 +    by (simp add: cl_ident TC
   23.15                    subset_trans [OF cl_mono [OF Int_lower1]]) 
   23.16    show ?thesis
   23.17      by (rule cl_subset_in_lattice [OF cl_subset latt]) 
   23.18 @@ -486,7 +485,7 @@
   23.19    shows "closed F T B L"
   23.20  apply (simp add: closed_def, clarify)
   23.21  apply (rule ProgressSets.cl_subset_in_lattice [OF _ lattice])  
   23.22 -apply (simp add: Int_Un_distrib cl_Un [OF lattice] Un_subset_iff 
   23.23 +apply (simp add: Int_Un_distrib cl_Un [OF lattice] 
   23.24                   cl_ident Int_in_lattice [OF TL BL lattice] Un_upper1)
   23.25  apply (subgoal_tac "cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))") 
   23.26   prefer 2 
    25.1 --- a/src/HOL/UNITY/Transformers.thy	Thu Sep 24 19:14:18 2009 +0200
    25.2 +++ b/src/HOL/UNITY/Transformers.thy	Fri Sep 25 09:50:31 2009 +0200
    25.3 @@ -1,5 +1,4 @@
    25.4  (*  Title:      HOL/UNITY/Transformers
    25.5 -    ID:         $Id$
    25.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    25.7      Copyright   2003  University of Cambridge
    25.8  
    25.9 @@ -133,7 +132,7 @@
   25.10  apply (drule constrains_Un [OF Diff_wens_constrains [of F act A]]) 
   25.11  apply (simp add: Un_Int_distrib2 Compl_partition2) 
   25.12  apply (erule constrains_weaken, blast) 
   25.13 -apply (simp add: Un_subset_iff wens_weakening) 
   25.14 +apply (simp add: wens_weakening)
   25.15  done
   25.16  
   25.17  text{*Assertion 4.20 in the thesis.*}
   25.18 @@ -151,7 +150,7 @@
   25.19        "[|T-B \<subseteq> awp F T; act \<in> Acts F|]
   25.20         ==> T \<inter> wens F act B = T \<inter> wens F act (T\<inter>B)"
   25.21  apply (rule equalityI)
   25.22 - apply (simp_all add: Int_lower1 Int_subset_iff) 
   25.23 + apply (simp_all add: Int_lower1) 
   25.24   apply (rule wens_Int_eq_lemma, assumption+) 
   25.25  apply (rule subset_trans [OF _ wens_mono [of "T\<inter>B" B]], auto) 
   25.26  done
   25.27 @@ -176,7 +175,7 @@
   25.28   apply (drule_tac act1=act and A1=X 
   25.29          in constrains_Un [OF Diff_wens_constrains]) 
   25.30   apply (erule constrains_weaken, blast) 
   25.31 - apply (simp add: Un_subset_iff wens_weakening) 
   25.32 + apply (simp add: wens_weakening) 
   25.33  apply (rule constrains_weaken) 
   25.34  apply (rule_tac I=W and A="\<lambda>v. v-B" and A'="\<lambda>v. v" in constrains_UN, blast+)
   25.35  done
   25.36 @@ -229,7 +228,7 @@
   25.37  apply (subgoal_tac "(T \<inter> wens F act B) - B \<subseteq> 
   25.38                      wp act B \<inter> awp F (B \<union> wens F act B) \<inter> awp F T") 
   25.39   apply (rule subset_wens) 
   25.40 - apply (simp add: awp_Join_eq awp_Int_eq Int_subset_iff Un_commute)
   25.41 + apply (simp add: awp_Join_eq awp_Int_eq Un_commute)
   25.42   apply (simp add: awp_def wp_def, blast) 
   25.43  apply (insert wens_subset [of F act B], blast) 
   25.44  done
   25.45 @@ -253,7 +252,7 @@
   25.46   apply (blast dest: wens_mono intro: wens_Join_subset [THEN subsetD], simp)
   25.47  apply (rule equalityI) 
   25.48   prefer 2 apply blast
   25.49 -apply (simp add: Int_lower1 Int_subset_iff) 
   25.50 +apply (simp add: Int_lower1) 
   25.51  apply (frule wens_set_imp_subset) 
   25.52  apply (subgoal_tac "T-X \<subseteq> awp F T")  
   25.53   prefer 2 apply (blast intro: awpF [THEN subsetD]) 
   25.54 @@ -347,7 +346,7 @@
   25.55        "single_valued act
   25.56         ==> wens_single act B \<union> wp act (wens_single act B) = wens_single act B"
   25.57  apply (rule equalityI)
   25.58 - apply (simp_all add: Un_upper1 Un_subset_iff) 
   25.59 + apply (simp_all add: Un_upper1) 
   25.60  apply (simp add: wens_single_def wp_UN_eq, clarify) 
   25.61  apply (rule_tac a="Suc(i)" in UN_I, auto) 
   25.62  done
    26.1 --- a/src/HOL/UNITY/UNITY_Main.thy	Thu Sep 24 19:14:18 2009 +0200
    26.2 +++ b/src/HOL/UNITY/UNITY_Main.thy	Fri Sep 25 09:50:31 2009 +0200
    26.3 @@ -1,13 +1,14 @@
    26.4  (*  Title:      HOL/UNITY/UNITY_Main.thy
    26.5 -    ID:         $Id$
    26.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    26.7      Copyright   2003  University of Cambridge
    26.8  *)
    26.9  
   26.10  header{*Comprehensive UNITY Theory*}
   26.11  
   26.12 -theory UNITY_Main imports Detects PPROD Follows ProgressSets
   26.13 -uses "UNITY_tactics.ML" begin
   26.14 +theory UNITY_Main
   26.15 +imports Detects PPROD Follows ProgressSets
   26.16 +uses "UNITY_tactics.ML"
   26.17 +begin
   26.18  
   26.19  method_setup safety = {*
   26.20      Scan.succeed (fn ctxt =>
    27.1 --- a/src/HOL/UNITY/WFair.thy	Thu Sep 24 19:14:18 2009 +0200
    27.2 +++ b/src/HOL/UNITY/WFair.thy	Fri Sep 25 09:50:31 2009 +0200
    27.3 @@ -113,7 +113,7 @@
    27.4  lemma totalize_transient_iff:
    27.5     "(totalize F \<in> transient A) = (\<exists>act\<in>Acts F. A \<subseteq> Domain act & act``A \<subseteq> -A)"
    27.6  apply (simp add: totalize_def totalize_act_def transient_def 
    27.7 -                 Un_Image Un_subset_iff, safe)
    27.8 +                 Un_Image, safe)
    27.9  apply (blast intro!: rev_bexI)+
   27.10  done
   27.11  
    28.1 --- a/src/HOL/Wellfounded.thy	Thu Sep 24 19:14:18 2009 +0200
    28.2 +++ b/src/HOL/Wellfounded.thy	Fri Sep 25 09:50:31 2009 +0200
    28.3 @@ -267,8 +267,8 @@
    28.4  
    28.5  lemma wfP_SUP:
    28.6    "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (DomainP (r i)) (RangeP (r j)) = bot \<Longrightarrow> wfP (SUPR UNIV r)"
    28.7 -  by (rule wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}", to_pred SUP_UN_eq2 pred_equals_eq])
    28.8 -    (simp_all add: bot_fun_eq bot_bool_eq)
    28.9 +  by (rule wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}", to_pred SUP_UN_eq2])
   28.10 +    (simp_all add: Collect_def)
   28.11  
   28.12  lemma wf_Union: 
   28.13   "[| ALL r:R. wf r;  
    29.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    29.2 +++ b/src/HOL/ex/predicate_compile.ML	Fri Sep 25 09:50:31 2009 +0200
    29.3 @@ -0,0 +1,2182 @@
    29.4 +(* Author: Lukas Bulwahn, TU Muenchen
    29.5 +
    29.6 +(Prototype of) A compiler from predicates specified by intro/elim rules
    29.7 +to equations.
    29.8 +*)
    29.9 +
   29.10 +signature PREDICATE_COMPILE =
   29.11 +sig
   29.12 +  type mode = int list option list * int list
   29.13 +  (*val add_equations_of: bool -> string list -> theory -> theory *)
   29.14 +  val register_predicate : (thm list * thm * int) -> theory -> theory
   29.15 +  val is_registered : theory -> string -> bool
   29.16 + (* val fetch_pred_data : theory -> string -> (thm list * thm * int)  *)
   29.17 +  val predfun_intro_of: theory -> string -> mode -> thm
   29.18 +  val predfun_elim_of: theory -> string -> mode -> thm
   29.19 +  val strip_intro_concl: int -> term -> term * (term list * term list)
   29.20 +  val predfun_name_of: theory -> string -> mode -> string
   29.21 +  val all_preds_of : theory -> string list
   29.22 +  val modes_of: theory -> string -> mode list
   29.23 +  val string_of_mode : mode -> string
   29.24 +  val intros_of: theory -> string -> thm list
   29.25 +  val nparams_of: theory -> string -> int
   29.26 +  val add_intro: thm -> theory -> theory
   29.27 +  val set_elim: thm -> theory -> theory
   29.28 +  val setup: theory -> theory
   29.29 +  val code_pred: string -> Proof.context -> Proof.state
   29.30 +  val code_pred_cmd: string -> Proof.context -> Proof.state
   29.31 +  val print_stored_rules: theory -> unit
   29.32 +  val print_all_modes: theory -> unit
   29.33 +  val do_proofs: bool ref
   29.34 +  val mk_casesrule : Proof.context -> int -> thm list -> term
   29.35 +  val analyze_compr: theory -> term -> term
   29.36 +  val eval_ref: (unit -> term Predicate.pred) option ref
   29.37 +  val add_equations : string list -> theory -> theory
   29.38 +  val code_pred_intros_attrib : attribute
   29.39 +  (* used by Quickcheck_Generator *) 
   29.40 +  (*val funT_of : mode -> typ -> typ
   29.41 +  val mk_if_pred : term -> term
   29.42 +  val mk_Eval : term * term -> term*)
   29.43 +  val mk_tupleT : typ list -> typ
   29.44 +(*  val mk_predT :  typ -> typ *)
   29.45 +  (* temporary for testing of the compilation *)
   29.46 +  datatype indprem = Prem of term list * term | Negprem of term list * term | Sidecond of term |
   29.47 +    GeneratorPrem of term list * term | Generator of (string * typ);
   29.48 +  val prepare_intrs: theory -> string list ->
   29.49 +    (string * typ) list * int * string list * string list * (string * mode list) list *
   29.50 +    (string * (term list * indprem list) list) list * (string * (int option list * int)) list
   29.51 +  datatype compilation_funs = CompilationFuns of {
   29.52 +    mk_predT : typ -> typ,
   29.53 +    dest_predT : typ -> typ,
   29.54 +    mk_bot : typ -> term,
   29.55 +    mk_single : term -> term,
   29.56 +    mk_bind : term * term -> term,
   29.57 +    mk_sup : term * term -> term,
   29.58 +    mk_if : term -> term,
   29.59 +    mk_not : term -> term,
   29.60 +    mk_map : typ -> typ -> term -> term -> term,
   29.61 +    lift_pred : term -> term
   29.62 +  };  
   29.63 +  datatype tmode = Mode of mode * int list * tmode option list;
   29.64 +  type moded_clause = term list * (indprem * tmode) list
   29.65 +  type 'a pred_mode_table = (string * (mode * 'a) list) list
   29.66 +  val infer_modes : bool -> theory -> (string * (int list option list * int list) list) list
   29.67 +    -> (string * (int option list * int)) list -> string list
   29.68 +    -> (string * (term list * indprem list) list) list
   29.69 +    -> (moded_clause list) pred_mode_table
   29.70 +  val infer_modes_with_generator : theory -> (string * (int list option list * int list) list) list
   29.71 +    -> (string * (int option list * int)) list -> string list
   29.72 +    -> (string * (term list * indprem list) list) list
   29.73 +    -> (moded_clause list) pred_mode_table  
   29.74 +  (*val compile_preds : theory -> compilation_funs -> string list -> string list
   29.75 +    -> (string * typ) list -> (moded_clause list) pred_mode_table -> term pred_mode_table
   29.76 +  val rpred_create_definitions :(string * typ) list -> string * mode list
   29.77 +    -> theory -> theory 
   29.78 +  val split_smode : int list -> term list -> (term list * term list) *)
   29.79 +  val print_moded_clauses :
   29.80 +    theory -> (moded_clause list) pred_mode_table -> unit
   29.81 +  val print_compiled_terms : theory -> term pred_mode_table -> unit
   29.82 +  (*val rpred_prove_preds : theory -> term pred_mode_table -> thm pred_mode_table*)
   29.83 +  val rpred_compfuns : compilation_funs
   29.84 +  val dest_funT : typ -> typ * typ
   29.85 + (* val depending_preds_of : theory -> thm list -> string list *)
   29.86 +  val add_quickcheck_equations : string list -> theory -> theory
   29.87 +  val add_sizelim_equations : string list -> theory -> theory
   29.88 +  val is_inductive_predicate : theory -> string -> bool
   29.89 +  val terms_vs : term list -> string list
   29.90 +  val subsets : int -> int -> int list list
   29.91 +  val check_mode_clause : bool -> theory -> string list ->
   29.92 +    (string * mode list) list -> (string * mode list) list -> mode -> (term list * indprem list)
   29.93 +      -> (term list * (indprem * tmode) list) option
   29.94 +  val string_of_moded_prem : theory -> (indprem * tmode) -> string
   29.95 +  val all_modes_of : theory -> (string * mode list) list
   29.96 +  val all_generator_modes_of : theory -> (string * mode list) list
   29.97 +  val compile_clause : compilation_funs -> term option -> (term list -> term) ->
   29.98 +    theory -> string list -> string list -> mode -> term -> moded_clause -> term
   29.99 +  val preprocess_intro : theory -> thm -> thm
  29.100 +  val is_constrt : theory -> term -> bool
  29.101 +  val is_predT : typ -> bool
  29.102 +  val guess_nparams : typ -> int
  29.103 +end;
  29.104 +
  29.105 +structure Predicate_Compile : PREDICATE_COMPILE =
  29.106 +struct
  29.107 +
  29.108 +(** auxiliary **)
  29.109 +
  29.110 +(* debug stuff *)
  29.111 +
  29.112 +fun tracing s = (if ! Toplevel.debug then Output.tracing s else ());
  29.113 +
  29.114 +fun print_tac s = Seq.single; (* (if ! Toplevel.debug then Tactical.print_tac s else Seq.single); *)
  29.115 +fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *)
  29.116 +
  29.117 +val do_proofs = ref true;
  29.118 +
  29.119 +fun mycheat_tac thy i st =
  29.120 +  (Tactic.rtac (SkipProof.make_thm thy (Var (("A", 0), propT))) i) st
  29.121 +
  29.122 +fun remove_last_goal thy st =
  29.123 +  (Tactic.rtac (SkipProof.make_thm thy (Var (("A", 0), propT))) (nprems_of st)) st
  29.124 +
  29.125 +(* reference to preprocessing of InductiveSet package *)
  29.126 +
  29.127 +val ind_set_codegen_preproc = Inductive_Set.codegen_preproc;
  29.128 +
  29.129 +(** fundamentals **)
  29.130 +
  29.131 +(* syntactic operations *)
  29.132 +
  29.133 +fun mk_eq (x, xs) =
  29.134 +  let fun mk_eqs _ [] = []
  29.135 +        | mk_eqs a (b::cs) =
  29.136 +            HOLogic.mk_eq (Free (a, fastype_of b), b) :: mk_eqs a cs
  29.137 +  in mk_eqs x xs end;
  29.138 +
  29.139 +fun mk_tupleT [] = HOLogic.unitT
  29.140 +  | mk_tupleT Ts = foldr1 HOLogic.mk_prodT Ts;
  29.141 +
  29.142 +fun dest_tupleT (Type (@{type_name Product_Type.unit}, [])) = []
  29.143 +  | dest_tupleT (Type (@{type_name "*"}, [T1, T2])) = T1 :: (dest_tupleT T2)
  29.144 +  | dest_tupleT t = [t]
  29.145 +
  29.146 +fun mk_tuple [] = HOLogic.unit
  29.147 +  | mk_tuple ts = foldr1 HOLogic.mk_prod ts;
  29.148 +
  29.149 +fun dest_tuple (Const (@{const_name Product_Type.Unity}, _)) = []
  29.150 +  | dest_tuple (Const (@{const_name Pair}, _) $ t1 $ t2) = t1 :: (dest_tuple t2)
  29.151 +  | dest_tuple t = [t]
  29.152 +
  29.153 +fun mk_scomp (t, u) =
  29.154 +  let
  29.155 +    val T = fastype_of t
  29.156 +    val U = fastype_of u
  29.157 +    val [A] = binder_types T
  29.158 +    val D = body_type U 
  29.159 +  in 
  29.160 +    Const (@{const_name "scomp"}, T --> U --> A --> D) $ t $ u
  29.161 +  end;
  29.162 +
  29.163 +fun dest_funT (Type ("fun",[S, T])) = (S, T)
  29.164 +  | dest_funT T = raise TYPE ("dest_funT", [T], [])
  29.165 + 
  29.166 +fun mk_fun_comp (t, u) =
  29.167 +  let
  29.168 +    val (_, B) = dest_funT (fastype_of t)
  29.169 +    val (C, A) = dest_funT (fastype_of u)
  29.170 +  in
  29.171 +    Const(@{const_name "Fun.comp"}, (A --> B) --> (C --> A) --> C --> B) $ t $ u
  29.172 +  end;
  29.173 +
  29.174 +fun dest_randomT (Type ("fun", [@{typ Random.seed},
  29.175 +  Type ("*", [Type ("*", [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T
  29.176 +  | dest_randomT T = raise TYPE ("dest_randomT", [T], [])
  29.177 +
  29.178 +(* destruction of intro rules *)
  29.179 +
  29.180 +(* FIXME: look for other place where this functionality was used before *)
  29.181 +fun strip_intro_concl nparams intro = let
  29.182 +  val _ $ u = Logic.strip_imp_concl intro
  29.183 +  val (pred, all_args) = strip_comb u
  29.184 +  val (params, args) = chop nparams all_args
  29.185 +in (pred, (params, args)) end
  29.186 +
  29.187 +(** data structures **)
  29.188 +
  29.189 +type smode = int list;
  29.190 +type mode = smode option list * smode;
  29.191 +datatype tmode = Mode of mode * int list * tmode option list;
  29.192 +
  29.193 +fun split_smode is ts =
  29.194 +  let
  29.195 +    fun split_smode' _ _ [] = ([], [])
  29.196 +      | split_smode' is i (t::ts) = (if i mem is then apfst else apsnd) (cons t)
  29.197 +          (split_smode' is (i+1) ts)
  29.198 +  in split_smode' is 1 ts end
  29.199 +
  29.200 +fun split_mode (iss, is) ts =
  29.201 +  let
  29.202 +    val (t1, t2) = chop (length iss) ts 
  29.203 +  in (t1, split_smode is t2) end
  29.204 +
  29.205 +fun string_of_mode (iss, is) = space_implode " -> " (map
  29.206 +  (fn NONE => "X"
  29.207 +    | SOME js => enclose "[" "]" (commas (map string_of_int js)))
  29.208 +       (iss @ [SOME is]));
  29.209 +
  29.210 +fun string_of_tmode (Mode (predmode, termmode, param_modes)) =
  29.211 +  "predmode: " ^ (string_of_mode predmode) ^ 
  29.212 +  (if null param_modes then "" else
  29.213 +    "; " ^ "params: " ^ commas (map (the_default "NONE" o Option.map string_of_tmode) param_modes))
  29.214 +    
  29.215 +datatype indprem = Prem of term list * term | Negprem of term list * term | Sidecond of term |
  29.216 +  GeneratorPrem of term list * term | Generator of (string * typ);
  29.217 +
  29.218 +type moded_clause = term list * (indprem * tmode) list
  29.219 +type 'a pred_mode_table = (string * (mode * 'a) list) list
  29.220 +
  29.221 +datatype predfun_data = PredfunData of {
  29.222 +  name : string,
  29.223 +  definition : thm,
  29.224 +  intro : thm,
  29.225 +  elim : thm
  29.226 +};
  29.227 +
  29.228 +fun rep_predfun_data (PredfunData data) = data;
  29.229 +fun mk_predfun_data (name, definition, intro, elim) =
  29.230 +  PredfunData {name = name, definition = definition, intro = intro, elim = elim}
  29.231 +
  29.232 +datatype function_data = FunctionData of {
  29.233 +  name : string,
  29.234 +  equation : thm option (* is not used at all? *)
  29.235 +};
  29.236 +
  29.237 +fun rep_function_data (FunctionData data) = data;
  29.238 +fun mk_function_data (name, equation) =
  29.239 +  FunctionData {name = name, equation = equation}
  29.240 +
  29.241 +datatype pred_data = PredData of {
  29.242 +  intros : thm list,
  29.243 +  elim : thm option,
  29.244 +  nparams : int,
  29.245 +  functions : (mode * predfun_data) list,
  29.246 +  generators : (mode * function_data) list,
  29.247 +  sizelim_functions : (mode * function_data) list 
  29.248 +};
  29.249 +
  29.250 +fun rep_pred_data (PredData data) = data;
  29.251 +fun mk_pred_data ((intros, elim, nparams), (functions, generators, sizelim_functions)) =
  29.252 +  PredData {intros = intros, elim = elim, nparams = nparams,
  29.253 +    functions = functions, generators = generators, sizelim_functions = sizelim_functions}
  29.254 +fun map_pred_data f (PredData {intros, elim, nparams, functions, generators, sizelim_functions}) =
  29.255 +  mk_pred_data (f ((intros, elim, nparams), (functions, generators, sizelim_functions)))
  29.256 +  
  29.257 +fun eq_option eq (NONE, NONE) = true
  29.258 +  | eq_option eq (SOME x, SOME y) = eq (x, y)
  29.259 +  | eq_option eq _ = false
  29.260 +  
  29.261 +fun eq_pred_data (PredData d1, PredData d2) = 
  29.262 +  eq_list (Thm.eq_thm) (#intros d1, #intros d2) andalso
  29.263 +  eq_option (Thm.eq_thm) (#elim d1, #elim d2) andalso
  29.264 +  #nparams d1 = #nparams d2
  29.265 +  
  29.266 +structure PredData = TheoryDataFun
  29.267 +(
  29.268 +  type T = pred_data Graph.T;
  29.269 +  val empty = Graph.empty;
  29.270 +  val copy = I;
  29.271 +  val extend = I;
  29.272 +  fun merge _ = Graph.merge eq_pred_data;
  29.273 +);
  29.274 +
  29.275 +(* queries *)
  29.276 +
  29.277 +fun lookup_pred_data thy name =
  29.278 +  Option.map rep_pred_data (try (Graph.get_node (PredData.get thy)) name)
  29.279 +
  29.280 +fun the_pred_data thy name = case lookup_pred_data thy name
  29.281 + of NONE => error ("No such predicate " ^ quote name)  
  29.282 +  | SOME data => data;
  29.283 +
  29.284 +val is_registered = is_some oo lookup_pred_data 
  29.285 +
  29.286 +val all_preds_of = Graph.keys o PredData.get
  29.287 +
  29.288 +val intros_of = #intros oo the_pred_data
  29.289 +
  29.290 +fun the_elim_of thy name = case #elim (the_pred_data thy name)
  29.291 + of NONE => error ("No elimination rule for predicate " ^ quote name)
  29.292 +  | SOME thm => thm 
  29.293 +  
  29.294 +val has_elim = is_some o #elim oo the_pred_data;
  29.295 +
  29.296 +val nparams_of = #nparams oo the_pred_data
  29.297 +
  29.298 +val modes_of = (map fst) o #functions oo the_pred_data
  29.299 +
  29.300 +fun all_modes_of thy = map (fn name => (name, modes_of thy name)) (all_preds_of thy) 
  29.301 +
  29.302 +val is_compiled = not o null o #functions oo the_pred_data
  29.303 +
  29.304 +fun lookup_predfun_data thy name mode =
  29.305 +  Option.map rep_predfun_data (AList.lookup (op =)
  29.306 +  (#functions (the_pred_data thy name)) mode)
  29.307 +
  29.308 +fun the_predfun_data thy name mode = case lookup_predfun_data thy name mode
  29.309 +  of NONE => error ("No function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ name)
  29.310 +   | SOME data => data;
  29.311 +
  29.312 +val predfun_name_of = #name ooo the_predfun_data
  29.313 +
  29.314 +val predfun_definition_of = #definition ooo the_predfun_data
  29.315 +
  29.316 +val predfun_intro_of = #intro ooo the_predfun_data
  29.317 +
  29.318 +val predfun_elim_of = #elim ooo the_predfun_data
  29.319 +
  29.320 +fun lookup_generator_data thy name mode = 
  29.321 +  Option.map rep_function_data (AList.lookup (op =)
  29.322 +  (#generators (the_pred_data thy name)) mode)
  29.323 +  
  29.324 +fun the_generator_data thy name mode = case lookup_generator_data thy name mode
  29.325 +  of NONE => error ("No generator defined for mode " ^ string_of_mode mode ^ " of predicate " ^ name)
  29.326 +   | SOME data => data
  29.327 +
  29.328 +val generator_name_of = #name ooo the_generator_data
  29.329 +
  29.330 +val generator_modes_of = (map fst) o #generators oo the_pred_data
  29.331 +
  29.332 +fun all_generator_modes_of thy =
  29.333 +  map (fn name => (name, generator_modes_of thy name)) (all_preds_of thy) 
  29.334 +
  29.335 +fun lookup_sizelim_function_data thy name mode =
  29.336 +  Option.map rep_function_data (AList.lookup (op =)
  29.337 +  (#sizelim_functions (the_pred_data thy name)) mode)
  29.338 +
  29.339 +fun the_sizelim_function_data thy name mode = case lookup_sizelim_function_data thy name mode
  29.340 +  of NONE => error ("No size-limited function defined for mode " ^ string_of_mode mode
  29.341 +    ^ " of predicate " ^ name)
  29.342 +   | SOME data => data
  29.343 +
  29.344 +val sizelim_function_name_of = #name ooo the_sizelim_function_data
  29.345 +
  29.346 +(*val generator_modes_of = (map fst) o #generators oo the_pred_data*)
  29.347 +     
  29.348 +(* diagnostic display functions *)
  29.349 +
  29.350 +fun print_modes modes = Output.tracing ("Inferred modes:\n" ^
  29.351 +  cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
  29.352 +    string_of_mode ms)) modes));
  29.353 +
  29.354 +fun print_pred_mode_table string_of_entry thy pred_mode_table =
  29.355 +  let
  29.356 +    fun print_mode pred (mode, entry) =  "mode : " ^ (string_of_mode mode)
  29.357 +      ^ (string_of_entry pred mode entry)  
  29.358 +    fun print_pred (pred, modes) =
  29.359 +      "predicate " ^ pred ^ ": " ^ cat_lines (map (print_mode pred) modes)
  29.360 +    val _ = Output.tracing (cat_lines (map print_pred pred_mode_table))
  29.361 +  in () end;
  29.362 +
  29.363 +fun string_of_moded_prem thy (Prem (ts, p), tmode) =
  29.364 +    (Syntax.string_of_term_global thy (list_comb (p, ts))) ^
  29.365 +    "(" ^ (string_of_tmode tmode) ^ ")"
  29.366 +  | string_of_moded_prem thy (GeneratorPrem (ts, p), Mode (predmode, is, _)) =
  29.367 +    (Syntax.string_of_term_global thy (list_comb (p, ts))) ^
  29.368 +    "(generator_mode: " ^ (string_of_mode predmode) ^ ")"
  29.369 +  | string_of_moded_prem thy (Generator (v, T), _) =
  29.370 +    "Generator for " ^ v ^ " of Type " ^ (Syntax.string_of_typ_global thy T)
  29.371 +  | string_of_moded_prem thy (Negprem (ts, p), Mode (_, is, _)) =
  29.372 +    (Syntax.string_of_term_global thy (list_comb (p, ts))) ^
  29.373 +    "(negative mode: " ^ (space_implode ", " (map string_of_int is)) ^ ")"
  29.374 +  | string_of_moded_prem thy (Sidecond t, Mode (_, is, _)) =
  29.375 +    (Syntax.string_of_term_global thy t) ^
  29.376 +    "(sidecond mode: " ^ (space_implode ", " (map string_of_int is)) ^ ")"    
  29.377 +  | string_of_moded_prem _ _ = error "string_of_moded_prem: unimplemented"
  29.378 +     
  29.379 +fun print_moded_clauses thy =
  29.380 +  let        
  29.381 +    fun string_of_clause pred mode clauses =
  29.382 +      cat_lines (map (fn (ts, prems) => (space_implode " --> "
  29.383 +        (map (string_of_moded_prem thy) prems)) ^ " --> " ^ pred ^ " "
  29.384 +        ^ (space_implode " " (map (Syntax.string_of_term_global thy) ts))) clauses)
  29.385 +  in print_pred_mode_table string_of_clause thy end;
  29.386 +
  29.387 +fun print_compiled_terms thy =
  29.388 +  print_pred_mode_table (fn _ => fn _ => Syntax.string_of_term_global thy) thy
  29.389 +    
  29.390 +fun print_stored_rules thy =
  29.391 +  let
  29.392 +    val preds = (Graph.keys o PredData.get) thy
  29.393 +    fun print pred () = let
  29.394 +      val _ = writeln ("predicate: " ^ pred)
  29.395 +      val _ = writeln ("number of parameters: " ^ string_of_int (nparams_of thy pred))
  29.396 +      val _ = writeln ("introrules: ")
  29.397 +      val _ = fold (fn thm => fn u => writeln (Display.string_of_thm_global thy thm))
  29.398 +        (rev (intros_of thy pred)) ()
  29.399 +    in
  29.400 +      if (has_elim thy pred) then
  29.401 +        writeln ("elimrule: " ^ Display.string_of_thm_global thy (the_elim_of thy pred))
  29.402 +      else
  29.403 +        writeln ("no elimrule defined")
  29.404 +    end
  29.405 +  in
  29.406 +    fold print preds ()
  29.407 +  end;
  29.408 +
  29.409 +fun print_all_modes thy =
  29.410 +  let
  29.411 +    val _ = writeln ("Inferred modes:")
  29.412 +    fun print (pred, modes) u =
  29.413 +      let
  29.414 +        val _ = writeln ("predicate: " ^ pred)
  29.415 +        val _ = writeln ("modes: " ^ (commas (map string_of_mode modes)))
  29.416 +      in u end  
  29.417 +  in
  29.418 +    fold print (all_modes_of thy) ()
  29.419 +  end
  29.420 +  
  29.421 +(** preprocessing rules **)  
  29.422 +
  29.423 +fun imp_prems_conv cv ct =
  29.424 +  case Thm.term_of ct of
  29.425 +    Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
  29.426 +  | _ => Conv.all_conv ct
  29.427 +
  29.428 +fun Trueprop_conv cv ct =
  29.429 +  case Thm.term_of ct of
  29.430 +    Const ("Trueprop", _) $ _ => Conv.arg_conv cv ct  
  29.431 +  | _ => error "Trueprop_conv"
  29.432 +
  29.433 +fun preprocess_intro thy rule =
  29.434 +  Conv.fconv_rule
  29.435 +    (imp_prems_conv
  29.436 +      (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq})))))
  29.437 +    (Thm.transfer thy rule)
  29.438 +
  29.439 +fun preprocess_elim thy nparams elimrule =
  29.440 +  let
  29.441 +    fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) =
  29.442 +       HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
  29.443 +     | replace_eqs t = t
  29.444 +    val prems = Thm.prems_of elimrule
  29.445 +    val nargs = length (snd (strip_comb (HOLogic.dest_Trueprop (hd prems)))) - nparams
  29.446 +    fun preprocess_case t =
  29.447 +     let
  29.448 +       val params = Logic.strip_params t
  29.449 +       val (assums1, assums2) = chop nargs (Logic.strip_assums_hyp t)
  29.450 +       val assums_hyp' = assums1 @ (map replace_eqs assums2)
  29.451 +     in
  29.452 +       list_all (params, Logic.list_implies (assums_hyp', Logic.strip_assums_concl t))
  29.453 +     end 
  29.454 +    val cases' = map preprocess_case (tl prems)
  29.455 +    val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule)
  29.456 +  in
  29.457 +    Thm.equal_elim
  29.458 +      (Thm.symmetric (Conv.implies_concl_conv (MetaSimplifier.rewrite true [@{thm eq_is_eq}])
  29.459 +         (cterm_of thy elimrule')))
  29.460 +      elimrule
  29.461 +  end;
  29.462 +
  29.463 +(* special case: predicate with no introduction rule *)
  29.464 +fun noclause thy predname elim = let
  29.465 +  val T = (Logic.unvarifyT o Sign.the_const_type thy) predname
  29.466 +  val Ts = binder_types T
  29.467 +  val names = Name.variant_list []
  29.468 +        (map (fn i => "x" ^ (string_of_int i)) (1 upto (length Ts)))
  29.469 +  val vs = map2 (curry Free) names Ts
  29.470 +  val clausehd = HOLogic.mk_Trueprop (list_comb (Const (predname, T), vs))
  29.471 +  val intro_t = Logic.mk_implies (@{prop False}, clausehd)
  29.472 +  val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT))
  29.473 +  val elim_t = Logic.list_implies ([clausehd, Logic.mk_implies (@{prop False}, P)], P)
  29.474 +  val intro = Goal.prove (ProofContext.init thy) names [] intro_t
  29.475 +        (fn {...} => etac @{thm FalseE} 1)
  29.476 +  val elim = Goal.prove (ProofContext.init thy) ("P" :: names) [] elim_t
  29.477 +        (fn {...} => etac elim 1) 
  29.478 +in
  29.479 +  ([intro], elim)
  29.480 +end
  29.481 +
  29.482 +fun fetch_pred_data thy name =
  29.483 +  case try (Inductive.the_inductive (ProofContext.init thy)) name of
  29.484 +    SOME (info as (_, result)) => 
  29.485 +      let
  29.486 +        fun is_intro_of intro =
  29.487 +          let
  29.488 +            val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro))
  29.489 +          in (fst (dest_Const const) = name) end;      
  29.490 +        val intros = ind_set_codegen_preproc thy ((map (preprocess_intro thy))
  29.491 +          (filter is_intro_of (#intrs result)))
  29.492 +        val pre_elim = nth (#elims result) (find_index (fn s => s = name) (#names (fst info)))
  29.493 +        val nparams = length (Inductive.params_of (#raw_induct result))
  29.494 +        val elim = singleton (ind_set_codegen_preproc thy) (preprocess_elim thy nparams pre_elim)
  29.495 +        val (intros, elim) = if null intros then noclause thy name elim else (intros, elim)
  29.496 +      in
  29.497 +        mk_pred_data ((intros, SOME elim, nparams), ([], [], []))
  29.498 +      end                                                                    
  29.499 +  | NONE => error ("No such predicate: " ^ quote name)
  29.500 +  
  29.501 +(* updaters *)
  29.502 +
  29.503 +fun apfst3 f (x, y, z) =  (f x, y, z)
  29.504 +fun apsnd3 f (x, y, z) =  (x, f y, z)
  29.505 +fun aptrd3 f (x, y, z) =  (x, y, f z)
  29.506 +
  29.507 +fun add_predfun name mode data =
  29.508 +  let
  29.509 +    val add = (apsnd o apfst3 o cons) (mode, mk_predfun_data data)
  29.510 +  in PredData.map (Graph.map_node name (map_pred_data add)) end
  29.511 +
  29.512 +fun is_inductive_predicate thy name =
  29.513 +  is_some (try (Inductive.the_inductive (ProofContext.init thy)) name)
  29.514 +
  29.515 +fun depending_preds_of thy (key, value) =
  29.516 +  let
  29.517 +    val intros = (#intros o rep_pred_data) value
  29.518 +  in
  29.519 +    fold Term.add_const_names (map Thm.prop_of intros) []
  29.520 +      |> filter (fn c => (not (c = key)) andalso (is_inductive_predicate thy c orelse is_registered thy c))
  29.521 +  end;
  29.522 +    
  29.523 +    
  29.524 +(* code dependency graph *)    
  29.525 +(*
  29.526 +fun dependencies_of thy name =
  29.527 +  let
  29.528 +    val (intros, elim, nparams) = fetch_pred_data thy name 
  29.529 +    val data = mk_pred_data ((intros, SOME elim, nparams), ([], [], []))
  29.530 +    val keys = depending_preds_of thy intros
  29.531 +  in
  29.532 +    (data, keys)
  29.533 +  end;
  29.534 +*)
  29.535 +(* guessing number of parameters *)
  29.536 +fun find_indexes pred xs =
  29.537 +  let
  29.538 +    fun find is n [] = is
  29.539 +      | find is n (x :: xs) = find (if pred x then (n :: is) else is) (n + 1) xs;
  29.540 +  in rev (find [] 0 xs) end;
  29.541 +
  29.542 +fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = HOLogic.boolT)
  29.543 +  | is_predT _ = false
  29.544 +  
  29.545 +fun guess_nparams T =
  29.546 +  let
  29.547 +    val argTs = binder_types T
  29.548 +    val nparams = fold (curry Int.max)
  29.549 +      (map (fn x => x + 1) (find_indexes is_predT argTs)) 0
  29.550 +  in nparams end;
  29.551 +
  29.552 +fun add_intro thm thy = let
  29.553 +   val (name, T) = dest_Const (fst (strip_intro_concl 0 (prop_of thm)))
  29.554 +   fun cons_intro gr =
  29.555 +     case try (Graph.get_node gr) name of
  29.556 +       SOME pred_data => Graph.map_node name (map_pred_data
  29.557 +         (apfst (fn (intro, elim, nparams) => (thm::intro, elim, nparams)))) gr
  29.558 +     | NONE =>
  29.559 +       let
  29.560 +         val nparams = the_default (guess_nparams T)  (try (#nparams o rep_pred_data o (fetch_pred_data thy)) name)
  29.561 +       in Graph.new_node (name, mk_pred_data (([thm], NONE, nparams), ([], [], []))) gr end;
  29.562 +  in PredData.map cons_intro thy end
  29.563 +
  29.564 +fun set_elim thm = let
  29.565 +    val (name, _) = dest_Const (fst 
  29.566 +      (strip_comb (HOLogic.dest_Trueprop (hd (prems_of thm)))))
  29.567 +    fun set (intros, _, nparams) = (intros, SOME thm, nparams)  
  29.568 +  in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end
  29.569 +
  29.570 +fun set_nparams name nparams = let
  29.571 +    fun set (intros, elim, _ ) = (intros, elim, nparams) 
  29.572 +  in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end
  29.573 +    
  29.574 +fun register_predicate (pre_intros, pre_elim, nparams) thy = let
  29.575 +    val (name, _) = dest_Const (fst (strip_intro_concl nparams (prop_of (hd pre_intros))))
  29.576 +    (* preprocessing *)
  29.577 +    val intros = ind_set_codegen_preproc thy (map (preprocess_intro thy) pre_intros)
  29.578 +    val elim = singleton (ind_set_codegen_preproc thy) (preprocess_elim thy nparams pre_elim)
  29.579 +  in
  29.580 +    PredData.map
  29.581 +      (Graph.new_node (name, mk_pred_data ((intros, SOME elim, nparams), ([], [], [])))) thy
  29.582 +  end
  29.583 +
  29.584 +fun set_generator_name pred mode name = 
  29.585 +  let
  29.586 +    val set = (apsnd o apsnd3 o cons) (mode, mk_function_data (name, NONE))
  29.587 +  in
  29.588 +    PredData.map (Graph.map_node pred (map_pred_data set))
  29.589 +  end
  29.590 +
  29.591 +fun set_sizelim_function_name pred mode name = 
  29.592 +  let
  29.593 +    val set = (apsnd o aptrd3 o cons) (mode, mk_function_data (name, NONE))
  29.594 +  in
  29.595 +    PredData.map (Graph.map_node pred (map_pred_data set))
  29.596 +  end
  29.597 +
  29.598 +(** data structures for generic compilation for different monads **)
  29.599 +
  29.600 +(* maybe rename functions more generic:
  29.601 +  mk_predT -> mk_monadT; dest_predT -> dest_monadT
  29.602 +  mk_single -> mk_return (?)
  29.603 +*)
  29.604 +datatype compilation_funs = CompilationFuns of {
  29.605 +  mk_predT : typ -> typ,
  29.606 +  dest_predT : typ -> typ,
  29.607 +  mk_bot : typ -> term,
  29.608 +  mk_single : term -> term,
  29.609 +  mk_bind : term * term -> term,
  29.610 +  mk_sup : term * term -> term,
  29.611 +  mk_if : term -> term,
  29.612 +  mk_not : term -> term,
  29.613 +(*  funT_of : mode -> typ -> typ, *)
  29.614 +(*  mk_fun_of : theory -> (string * typ) -> mode -> term, *) 
  29.615 +  mk_map : typ -> typ -> term -> term -> term,
  29.616 +  lift_pred : term -> term
  29.617 +};
  29.618 +
  29.619 +fun mk_predT (CompilationFuns funs) = #mk_predT funs
  29.620 +fun dest_predT (CompilationFuns funs) = #dest_predT funs
  29.621 +fun mk_bot (CompilationFuns funs) = #mk_bot funs
  29.622 +fun mk_single (CompilationFuns funs) = #mk_single funs
  29.623 +fun mk_bind (CompilationFuns funs) = #mk_bind funs
  29.624 +fun mk_sup (CompilationFuns funs) = #mk_sup funs
  29.625 +fun mk_if (CompilationFuns funs) = #mk_if funs
  29.626 +fun mk_not (CompilationFuns funs) = #mk_not funs
  29.627 +(*fun funT_of (CompilationFuns funs) = #funT_of funs*)
  29.628 +(*fun mk_fun_of (CompilationFuns funs) = #mk_fun_of funs*)
  29.629 +fun mk_map (CompilationFuns funs) = #mk_map funs
  29.630 +fun lift_pred (CompilationFuns funs) = #lift_pred funs
  29.631 +
  29.632 +fun funT_of compfuns (iss, is) T =
  29.633 +  let
  29.634 +    val Ts = binder_types T
  29.635 +    val (paramTs, (inargTs, outargTs)) = split_mode (iss, is) Ts
  29.636 +    val paramTs' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) iss paramTs 
  29.637 +  in
  29.638 +    (paramTs' @ inargTs) ---> (mk_predT compfuns (mk_tupleT outargTs))
  29.639 +  end;
  29.640 +
  29.641 +fun sizelim_funT_of compfuns (iss, is) T =
  29.642 +  let
  29.643 +    val Ts = binder_types T
  29.644 +    val (paramTs, (inargTs, outargTs)) = split_mode (iss, is) Ts
  29.645 +    val paramTs' = map2 (fn SOME is => sizelim_funT_of compfuns ([], is) | NONE => I) iss paramTs 
  29.646 +  in
  29.647 +    (paramTs' @ inargTs @ [@{typ "code_numeral"}]) ---> (mk_predT compfuns (mk_tupleT outargTs))
  29.648 +  end;  
  29.649 +
  29.650 +fun mk_fun_of compfuns thy (name, T) mode = 
  29.651 +  Const (predfun_name_of thy name mode, funT_of compfuns mode T)
  29.652 +
  29.653 +fun mk_sizelim_fun_of compfuns thy (name, T) mode =
  29.654 +  Const (sizelim_function_name_of thy name mode, sizelim_funT_of compfuns mode T)
  29.655 +  
  29.656 +fun mk_generator_of compfuns thy (name, T) mode = 
  29.657 +  Const (generator_name_of thy name mode, sizelim_funT_of compfuns mode T)
  29.658 +
  29.659 +
  29.660 +structure PredicateCompFuns =
  29.661 +struct
  29.662 +
  29.663 +fun mk_predT T = Type (@{type_name "Predicate.pred"}, [T])
  29.664 +
  29.665 +fun dest_predT (Type (@{type_name "Predicate.pred"}, [T])) = T
  29.666 +  | dest_predT T = raise TYPE ("dest_predT", [T], []);
  29.667 +
  29.668 +fun mk_bot T = Const (@{const_name Orderings.bot}, mk_predT T);
  29.669 +
  29.670 +fun mk_single t =
  29.671 +  let val T = fastype_of t
  29.672 +  in Const(@{const_name Predicate.single}, T --> mk_predT T) $ t end;
  29.673 +
  29.674 +fun mk_bind (x, f) =
  29.675 +  let val T as Type ("fun", [_, U]) = fastype_of f
  29.676 +  in
  29.677 +    Const (@{const_name Predicate.bind}, fastype_of x --> T --> U) $ x $ f
  29.678 +  end;
  29.679 +
  29.680 +val mk_sup = HOLogic.mk_binop @{const_name sup};
  29.681 +
  29.682 +fun mk_if cond = Const (@{const_name Predicate.if_pred},
  29.683 +  HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond;
  29.684 +
  29.685 +fun mk_not t = let val T = mk_predT HOLogic.unitT
  29.686 +  in Const (@{const_name Predicate.not_pred}, T --> T) $ t end
  29.687 +
  29.688 +fun mk_Enum f =
  29.689 +  let val T as Type ("fun", [T', _]) = fastype_of f
  29.690 +  in
  29.691 +    Const (@{const_name Predicate.Pred}, T --> mk_predT T') $ f    
  29.692 +  end;
  29.693 +
  29.694 +fun mk_Eval (f, x) =
  29.695 +  let
  29.696 +    val T = fastype_of x
  29.697 +  in
  29.698 +    Const (@{const_name Predicate.eval}, mk_predT T --> T --> HOLogic.boolT) $ f $ x
  29.699 +  end;
  29.700 +
  29.701 +fun mk_map T1 T2 tf tp = Const (@{const_name Predicate.map},
  29.702 +  (T1 --> T2) --> mk_predT T1 --> mk_predT T2) $ tf $ tp;
  29.703 +
  29.704 +val lift_pred = I
  29.705 +
  29.706 +val compfuns = CompilationFuns {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
  29.707 +  mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not,
  29.708 +  mk_map = mk_map, lift_pred = lift_pred};
  29.709 +
  29.710 +end;
  29.711 +
  29.712 +(* termify_code:
  29.713 +val termT = Type ("Code_Evaluation.term", []);
  29.714 +fun termifyT T = HOLogic.mk_prodT (T, HOLogic.unitT --> termT)
  29.715 +*)
  29.716 +(*
  29.717 +fun lift_random random =
  29.718 +  let
  29.719 +    val T = dest_randomT (fastype_of random)
  29.720 +  in
  29.721 +    mk_scomp (random,
  29.722 +      mk_fun_comp (HOLogic.pair_const (PredicateCompFuns.mk_predT T) @{typ Random.seed},
  29.723 +        mk_fun_comp (Const (@{const_name Predicate.single}, T --> (PredicateCompFuns.mk_predT T)),
  29.724 +          Const (@{const_name "fst"}, HOLogic.mk_prodT (T, @{typ "unit => term"}) --> T)))) 
  29.725 +  end;
  29.726 +*)
  29.727 + 
  29.728 +structure RPredCompFuns =
  29.729 +struct
  29.730 +
  29.731 +fun mk_rpredT T =
  29.732 +  @{typ "Random.seed"} --> HOLogic.mk_prodT (PredicateCompFuns.mk_predT T, @{typ "Random.seed"})
  29.733 +
  29.734 +fun dest_rpredT (Type ("fun", [_,
  29.735 +  Type (@{type_name "*"}, [Type (@{type_name "Predicate.pred"}, [T]), _])])) = T
  29.736 +  | dest_rpredT T = raise TYPE ("dest_rpredT", [T], []); 
  29.737 +
  29.738 +fun mk_bot T = Const(@{const_name RPred.bot}, mk_rpredT T)
  29.739 +
  29.740 +fun mk_single t =
  29.741 +  let
  29.742 +    val T = fastype_of t
  29.743 +  in
  29.744 +    Const (@{const_name RPred.return}, T --> mk_rpredT T) $ t
  29.745 +  end;
  29.746 +
  29.747 +fun mk_bind (x, f) =
  29.748 +  let
  29.749 +    val T as (Type ("fun", [_, U])) = fastype_of f
  29.750 +  in
  29.751 +    Const (@{const_name RPred.bind}, fastype_of x --> T --> U) $ x $ f
  29.752 +  end
  29.753 +
  29.754 +val mk_sup = HOLogic.mk_binop @{const_name RPred.supp}
  29.755 +
  29.756 +fun mk_if cond = Const (@{const_name RPred.if_rpred},
  29.757 +  HOLogic.boolT --> mk_rpredT HOLogic.unitT) $ cond;
  29.758 +
  29.759 +fun mk_not t = error "Negation is not defined for RPred"
  29.760 +
  29.761 +fun mk_map t = error "FIXME" (*FIXME*)
  29.762 +
  29.763 +fun lift_pred t =
  29.764 +  let
  29.765 +    val T = PredicateCompFuns.dest_predT (fastype_of t)
  29.766 +    val lift_predT = PredicateCompFuns.mk_predT T --> mk_rpredT T 
  29.767 +  in
  29.768 +    Const (@{const_name "RPred.lift_pred"}, lift_predT) $ t  
  29.769 +  end;
  29.770 +
  29.771 +val compfuns = CompilationFuns {mk_predT = mk_rpredT, dest_predT = dest_rpredT, mk_bot = mk_bot,
  29.772 +    mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not,
  29.773 +    mk_map = mk_map, lift_pred = lift_pred};
  29.774 +
  29.775 +end;
  29.776 +(* for external use with interactive mode *)
  29.777 +val rpred_compfuns = RPredCompFuns.compfuns;
  29.778 +
  29.779 +fun lift_random random =
  29.780 +  let
  29.781 +    val T = dest_randomT (fastype_of random)
  29.782 +  in
  29.783 +    Const (@{const_name lift_random}, (@{typ Random.seed} -->
  29.784 +      HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) --> 
  29.785 +      RPredCompFuns.mk_rpredT T) $ random
  29.786 +  end;
  29.787 + 
  29.788 +(* Mode analysis *)
  29.789 +
  29.790 +(*** check if a term contains only constructor functions ***)
  29.791 +fun is_constrt thy =
  29.792 +  let
  29.793 +    val cnstrs = flat (maps
  29.794 +      (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
  29.795 +      (Symtab.dest (Datatype.get_all thy)));
  29.796 +    fun check t = (case strip_comb t of
  29.797 +        (Free _, []) => true
  29.798 +      | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of
  29.799 +            (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname' andalso forall check ts
  29.800 +          | _ => false)
  29.801 +      | _ => false)
  29.802 +  in check end;
  29.803 +
  29.804 +(*** check if a type is an equality type (i.e. doesn't contain fun)
  29.805 +  FIXME this is only an approximation ***)
  29.806 +fun is_eqT (Type (s, Ts)) = s <> "fun" andalso forall is_eqT Ts
  29.807 +  | is_eqT _ = true;
  29.808 +
  29.809 +fun term_vs tm = fold_aterms (fn Free (x, T) => cons x | _ => I) tm [];
  29.810 +val terms_vs = distinct (op =) o maps term_vs;
  29.811 +
  29.812 +(** collect all Frees in a term (with duplicates!) **)
  29.813 +fun term_vTs tm =
  29.814 +  fold_aterms (fn Free xT => cons xT | _ => I) tm [];
  29.815 +
  29.816 +(*FIXME this function should not be named merge... make it local instead*)
  29.817 +fun merge xs [] = xs
  29.818 +  | merge [] ys = ys
  29.819 +  | merge (x::xs) (y::ys) = if length x >= length y then x::merge xs (y::ys)
  29.820 +      else y::merge (x::xs) ys;
  29.821 +
  29.822 +fun subsets i j = if i <= j then
  29.823 +       let val is = subsets (i+1) j
  29.824 +       in merge (map (fn ks => i::ks) is) is end
  29.825 +     else [[]];
  29.826 +     
  29.827 +(* FIXME: should be in library - map_prod *)
  29.828 +fun cprod ([], ys) = []
  29.829 +  | cprod (x :: xs, ys) = map (pair x) ys @ cprod (xs, ys);
  29.830 +
  29.831 +fun cprods xss = foldr (map op :: o cprod) [[]] xss;
  29.832 +
  29.833 +
  29.834 +  
  29.835 +(*TODO: cleanup function and put together with modes_of_term *)
  29.836 +(*
  29.837 +fun modes_of_param default modes t = let
  29.838 +    val (vs, t') = strip_abs t
  29.839 +    val b = length vs
  29.840 +    fun mk_modes name args = Option.map (maps (fn (m as (iss, is)) =>
  29.841 +        let
  29.842 +          val (args1, args2) =
  29.843 +            if length args < length iss then
  29.844 +              error ("Too few arguments for inductive predicate " ^ name)
  29.845 +            else chop (length iss) args;
  29.846 +          val k = length args2;
  29.847 +          val perm = map (fn i => (find_index_eq (Bound (b - i)) args2) + 1)
  29.848 +            (1 upto b)  
  29.849 +          val partial_mode = (1 upto k) \\ perm
  29.850 +        in
  29.851 +          if not (partial_mode subset is) then [] else
  29.852 +          let
  29.853 +            val is' = 
  29.854 +            (fold_index (fn (i, j) => if j mem is then cons (i + 1) else I) perm [])
  29.855 +            |> fold (fn i => if i > k then cons (i - k + b) else I) is
  29.856 +              
  29.857 +           val res = map (fn x => Mode (m, is', x)) (cprods (map
  29.858 +            (fn (NONE, _) => [NONE]
  29.859 +              | (SOME js, arg) => map SOME (filter
  29.860 +                  (fn Mode (_, js', _) => js=js') (modes_of_term modes arg)))
  29.861 +                    (iss ~~ args1)))
  29.862 +          in res end
  29.863 +        end)) (AList.lookup op = modes name)
  29.864 +  in case strip_comb t' of
  29.865 +    (Const (name, _), args) => the_default default (mk_modes name args)
  29.866 +    | (Var ((name, _), _), args) => the (mk_modes name args)
  29.867 +    | (Free (name, _), args) => the (mk_modes name args)
  29.868 +    | _ => default end
  29.869 +  
  29.870 +and
  29.871 +*)
  29.872 +fun modes_of_term modes t =
  29.873 +  let
  29.874 +    val ks = 1 upto length (binder_types (fastype_of t));
  29.875 +    val default = [Mode (([], ks), ks, [])];
  29.876 +    fun mk_modes name args = Option.map (maps (fn (m as (iss, is)) =>
  29.877 +        let
  29.878 +          val (args1, args2) =
  29.879 +            if length args < length iss then
  29.880 +              error ("Too few arguments for inductive predicate " ^ name)
  29.881 +            else chop (length iss) args;
  29.882 +          val k = length args2;
  29.883 +          val prfx = 1 upto k
  29.884 +        in
  29.885 +          if not (is_prefix op = prfx is) then [] else
  29.886 +          let val is' = map (fn i => i - k) (List.drop (is, k))
  29.887 +          in map (fn x => Mode (m, is', x)) (cprods (map
  29.888 +            (fn (NONE, _) => [NONE]
  29.889 +              | (SOME js, arg) => map SOME (filter
  29.890 +                  (fn Mode (_, js', _) => js=js') (modes_of_term modes arg)))
  29.891 +                    (iss ~~ args1)))
  29.892 +          end
  29.893 +        end)) (AList.lookup op = modes name)
  29.894 +
  29.895 +  in
  29.896 +    case strip_comb (Envir.eta_contract t) of
  29.897 +      (Const (name, _), args) => the_default default (mk_modes name args)
  29.898 +    | (Var ((name, _), _), args) => the (mk_modes name args)
  29.899 +    | (Free (name, _), args) => the (mk_modes name args)
  29.900 +    | (Abs _, []) => error "Abs at param position" (* modes_of_param default modes t *)
  29.901 +    | _ => default
  29.902 +  end
  29.903 +  
  29.904 +fun select_mode_prem thy modes vs ps =
  29.905 +  find_first (is_some o snd) (ps ~~ map
  29.906 +    (fn Prem (us, t) => find_first (fn Mode (_, is, _) =>
  29.907 +          let
  29.908 +            val (in_ts, out_ts) = split_smode is us;
  29.909 +            val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts;
  29.910 +            val vTs = maps term_vTs out_ts';
  29.911 +            val dupTs = map snd (duplicates (op =) vTs) @
  29.912 +              List.mapPartial (AList.lookup (op =) vTs) vs;
  29.913 +          in
  29.914 +            terms_vs (in_ts @ in_ts') subset vs andalso
  29.915 +            forall (is_eqT o fastype_of) in_ts' andalso
  29.916 +            term_vs t subset vs andalso
  29.917 +            forall is_eqT dupTs
  29.918 +          end)
  29.919 +            (modes_of_term modes t handle Option =>
  29.920 +               error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
  29.921 +      | Negprem (us, t) => find_first (fn Mode (_, is, _) =>
  29.922 +            length us = length is andalso
  29.923 +            terms_vs us subset vs andalso
  29.924 +            term_vs t subset vs)
  29.925 +            (modes_of_term modes t handle Option =>
  29.926 +               error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
  29.927 +      | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], []))
  29.928 +          else NONE
  29.929 +      ) ps);
  29.930 +
  29.931 +fun fold_prem f (Prem (args, _)) = fold f args
  29.932 +  | fold_prem f (Negprem (args, _)) = fold f args
  29.933 +  | fold_prem f (Sidecond t) = f t
  29.934 +
  29.935 +fun all_subsets [] = [[]]
  29.936 +  | all_subsets (x::xs) = let val xss' = all_subsets xs in xss' @ (map (cons x) xss') end
  29.937 +
  29.938 +fun generator vTs v = 
  29.939 +  let
  29.940 +    val T = the (AList.lookup (op =) vTs v)
  29.941 +  in
  29.942 +    (Generator (v, T), Mode (([], []), [], []))
  29.943 +  end;
  29.944 +
  29.945 +fun gen_prem (Prem (us, t)) = GeneratorPrem (us, t) 
  29.946 +  | gen_prem _ = error "gen_prem : invalid input for gen_prem"
  29.947 +
  29.948 +fun param_gen_prem param_vs (p as Prem (us, t as Free (v, _))) =
  29.949 +  if member (op =) param_vs v then
  29.950 +    GeneratorPrem (us, t)
  29.951 +  else p  
  29.952 +  | param_gen_prem param_vs p = p
  29.953 +  
  29.954 +fun check_mode_clause with_generator thy param_vs modes gen_modes (iss, is) (ts, ps) =
  29.955 +  let
  29.956 +    val modes' = modes @ List.mapPartial
  29.957 +      (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
  29.958 +        (param_vs ~~ iss);
  29.959 +    val gen_modes' = gen_modes @ List.mapPartial
  29.960 +      (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
  29.961 +        (param_vs ~~ iss);  
  29.962 +    val vTs = distinct (op =) ((fold o fold_prem) Term.add_frees ps (fold Term.add_frees ts []))
  29.963 +    val prem_vs = distinct (op =) ((fold o fold_prem) Term.add_free_names ps [])
  29.964 +    fun check_mode_prems acc_ps vs [] = SOME (acc_ps, vs)
  29.965 +      | check_mode_prems acc_ps vs ps = (case select_mode_prem thy modes' vs ps of
  29.966 +          NONE =>
  29.967 +            (if with_generator then
  29.968 +              (case select_mode_prem thy gen_modes' vs ps of
  29.969 +                  SOME (p, SOME mode) => check_mode_prems ((gen_prem p, mode) :: acc_ps) 
  29.970 +                  (case p of Prem (us, _) => vs union terms_vs us | _ => vs)
  29.971 +                  (filter_out (equal p) ps)
  29.972 +                | NONE =>
  29.973 +                  let 
  29.974 +                    val all_generator_vs = all_subsets (prem_vs \\ vs) |> sort (int_ord o (pairself length))
  29.975 +                  in
  29.976 +                    case (find_first (fn generator_vs => is_some
  29.977 +                      (select_mode_prem thy modes' (vs union generator_vs) ps)) all_generator_vs) of
  29.978 +                      SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps)
  29.979 +                        (vs union generator_vs) ps
  29.980 +                    | NONE => NONE
  29.981 +                  end)
  29.982 +            else
  29.983 +              NONE)
  29.984 +        | SOME (p, SOME mode) => check_mode_prems ((if with_generator then param_gen_prem param_vs p else p, mode) :: acc_ps) 
  29.985 +            (case p of Prem (us, _) => vs union terms_vs us | _ => vs)
  29.986 +            (filter_out (equal p) ps))
  29.987 +    val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (split_smode is ts));
  29.988 +    val in_vs = terms_vs in_ts;
  29.989 +    val concl_vs = terms_vs ts
  29.990 +  in
  29.991 +    if forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso
  29.992 +    forall (is_eqT o fastype_of) in_ts' then
  29.993 +      case check_mode_prems [] (param_vs union in_vs) ps of
  29.994 +         NONE => NONE
  29.995 +       | SOME (acc_ps, vs) =>
  29.996 +         if with_generator then
  29.997 +           SOME (ts, (rev acc_ps) @ (map (generator vTs) (concl_vs \\ vs))) 
  29.998 +         else
  29.999 +           if concl_vs subset vs then SOME (ts, rev acc_ps) else NONE
 29.1000 +    else NONE
 29.1001 +  end;
 29.1002 +
 29.1003 +fun check_modes_pred with_generator thy param_vs preds modes gen_modes (p, ms) =
 29.1004 +  let val SOME rs = AList.lookup (op =) preds p
 29.1005 +  in (p, List.filter (fn m => case find_index
 29.1006 +    (is_none o check_mode_clause with_generator thy param_vs modes gen_modes m) rs of
 29.1007 +      ~1 => true
 29.1008 +    | i => (Output.tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
 29.1009 +      p ^ " violates mode " ^ string_of_mode m); false)) ms)
 29.1010 +  end;
 29.1011 +
 29.1012 +fun get_modes_pred with_generator thy param_vs preds modes gen_modes (p, ms) =
 29.1013 +  let
 29.1014 +    val SOME rs = AList.lookup (op =) preds p 
 29.1015 +  in
 29.1016 +    (p, map (fn m =>
 29.1017 +      (m, map (the o check_mode_clause with_generator thy param_vs modes gen_modes m) rs)) ms)
 29.1018 +  end;
 29.1019 +  
 29.1020 +fun fixp f (x : (string * mode list) list) =
 29.1021 +  let val y = f x
 29.1022 +  in if x = y then x else fixp f y end;
 29.1023 +
 29.1024 +fun modes_of_arities arities =
 29.1025 +  (map (fn (s, (ks, k)) => (s, cprod (cprods (map
 29.1026 +            (fn NONE => [NONE]
 29.1027 +              | SOME k' => map SOME (subsets 1 k')) ks),
 29.1028 +            subsets 1 k))) arities)
 29.1029 +  
 29.1030 +fun infer_modes with_generator thy extra_modes arities param_vs preds =
 29.1031 +  let
 29.1032 +    val modes =
 29.1033 +      fixp (fn modes =>
 29.1034 +        map (check_modes_pred with_generator thy param_vs preds (modes @ extra_modes) []) modes)
 29.1035 +          (modes_of_arities arities)
 29.1036 +  in
 29.1037 +    map (get_modes_pred with_generator thy param_vs preds (modes @ extra_modes) []) modes
 29.1038 +  end;
 29.1039 +
 29.1040 +fun remove_from rem [] = []
 29.1041 +  | remove_from rem ((k, vs) :: xs) =
 29.1042 +    (case AList.lookup (op =) rem k of
 29.1043 +      NONE => (k, vs)
 29.1044 +    | SOME vs' => (k, vs \\ vs'))
 29.1045 +    :: remove_from rem xs
 29.1046 +    
 29.1047 +fun infer_modes_with_generator thy extra_modes arities param_vs preds =
 29.1048 +  let
 29.1049 +    val prednames = map fst preds
 29.1050 +    val extra_modes = all_modes_of thy
 29.1051 +    val gen_modes = all_generator_modes_of thy
 29.1052 +      |> filter_out (fn (name, _) => member (op =) prednames name)
 29.1053 +    val starting_modes = remove_from extra_modes (modes_of_arities arities) 
 29.1054 +    val modes =
 29.1055 +      fixp (fn modes =>
 29.1056 +        map (check_modes_pred true thy param_vs preds extra_modes (gen_modes @ modes)) modes)
 29.1057 +         starting_modes 
 29.1058 +  in
 29.1059 +    map (get_modes_pred true thy param_vs preds extra_modes (gen_modes @ modes)) modes
 29.1060 +  end;
 29.1061 +
 29.1062 +(* term construction *)
 29.1063 +
 29.1064 +fun mk_v (names, vs) s T = (case AList.lookup (op =) vs s of
 29.1065 +      NONE => (Free (s, T), (names, (s, [])::vs))
 29.1066 +    | SOME xs =>
 29.1067 +        let
 29.1068 +          val s' = Name.variant names s;
 29.1069 +          val v = Free (s', T)
 29.1070 +        in
 29.1071 +          (v, (s'::names, AList.update (op =) (s, v::xs) vs))
 29.1072 +        end);
 29.1073 +
 29.1074 +fun distinct_v (Free (s, T)) nvs = mk_v nvs s T
 29.1075 +  | distinct_v (t $ u) nvs =
 29.1076 +      let
 29.1077 +        val (t', nvs') = distinct_v t nvs;
 29.1078 +        val (u', nvs'') = distinct_v u nvs';
 29.1079 +      in (t' $ u', nvs'') end
 29.1080 +  | distinct_v x nvs = (x, nvs);
 29.1081 +
 29.1082 +fun compile_match thy compfuns eqs eqs' out_ts success_t =
 29.1083 +  let
 29.1084 +    val eqs'' = maps mk_eq eqs @ eqs'
 29.1085 +    val names = fold Term.add_free_names (success_t :: eqs'' @ out_ts) [];
 29.1086 +    val name = Name.variant names "x";
 29.1087 +    val name' = Name.variant (name :: names) "y";
 29.1088 +    val T = mk_tupleT (map fastype_of out_ts);
 29.1089 +    val U = fastype_of success_t;
 29.1090 +    val U' = dest_predT compfuns U;
 29.1091 +    val v = Free (name, T);
 29.1092 +    val v' = Free (name', T);
 29.1093 +  in
 29.1094 +    lambda v (fst (Datatype.make_case
 29.1095 +      (ProofContext.init thy) false [] v
 29.1096 +      [(mk_tuple out_ts,
 29.1097 +        if null eqs'' then success_t
 29.1098 +        else Const (@{const_name HOL.If}, HOLogic.boolT --> U --> U --> U) $
 29.1099 +          foldr1 HOLogic.mk_conj eqs'' $ success_t $
 29.1100 +            mk_bot compfuns U'),
 29.1101 +       (v', mk_bot compfuns U')]))
 29.1102 +  end;
 29.1103 +
 29.1104 +(*FIXME function can be removed*)
 29.1105 +fun mk_funcomp f t =
 29.1106 +  let
 29.1107 +    val names = Term.add_free_names t [];
 29.1108 +    val Ts = binder_types (fastype_of t);
 29.1109 +    val vs = map Free
 29.1110 +      (Name.variant_list names (replicate (length Ts) "x") ~~ Ts)
 29.1111 +  in
 29.1112 +    fold_rev lambda vs (f (list_comb (t, vs)))
 29.1113 +  end;
 29.1114 +(*
 29.1115 +fun compile_param_ext thy compfuns modes (NONE, t) = t
 29.1116 +  | compile_param_ext thy compfuns modes (m as SOME (Mode ((iss, is'), is, ms)), t) =
 29.1117 +      let
 29.1118 +        val (vs, u) = strip_abs t
 29.1119 +        val (ivs, ovs) = split_mode is vs    
 29.1120 +        val (f, args) = strip_comb u
 29.1121 +        val (params, args') = chop (length ms) args
 29.1122 +        val (inargs, outargs) = split_mode is' args'
 29.1123 +        val b = length vs
 29.1124 +        val perm = map (fn i => (find_index_eq (Bound (b - i)) args') + 1) (1 upto b)
 29.1125 +        val outp_perm =
 29.1126 +          snd (split_mode is perm)
 29.1127 +          |> map (fn i => i - length (filter (fn x => x < i) is'))
 29.1128 +        val names = [] -- TODO
 29.1129 +        val out_names = Name.variant_list names (replicate (length outargs) "x")
 29.1130 +        val f' = case f of
 29.1131 +            Const (name, T) =>
 29.1132 +              if AList.defined op = modes name then
 29.1133 +                mk_predfun_of thy compfuns (name, T) (iss, is')
 29.1134 +              else error "compile param: Not an inductive predicate with correct mode"
 29.1135 +          | Free (name, T) => Free (name, param_funT_of compfuns T (SOME is'))
 29.1136 +        val outTs = dest_tupleT (dest_predT compfuns (body_type (fastype_of f')))
 29.1137 +        val out_vs = map Free (out_names ~~ outTs)
 29.1138 +        val params' = map (compile_param thy modes) (ms ~~ params)
 29.1139 +        val f_app = list_comb (f', params' @ inargs)
 29.1140 +        val single_t = (mk_single compfuns (mk_tuple (map (fn i => nth out_vs (i - 1)) outp_perm)))
 29.1141 +        val match_t = compile_match thy compfuns [] [] out_vs single_t
 29.1142 +      in list_abs (ivs,
 29.1143 +        mk_bind compfuns (f_app, match_t))
 29.1144 +      end
 29.1145 +  | compile_param_ext _ _ _ _ = error "compile params"
 29.1146 +*)
 29.1147 +
 29.1148 +fun compile_param size thy compfuns (NONE, t) = t
 29.1149 +  | compile_param size thy compfuns (m as SOME (Mode ((iss, is'), is, ms)), t) =
 29.1150 +   let
 29.1151 +     val (f, args) = strip_comb (Envir.eta_contract t)
 29.1152 +     val (params, args') = chop (length ms) args
 29.1153 +     val params' = map (compile_param size thy compfuns) (ms ~~ params)
 29.1154 +     val mk_fun_of = case size of NONE => mk_fun_of | SOME _ => mk_sizelim_fun_of
 29.1155 +     val funT_of = case size of NONE => funT_of | SOME _ => sizelim_funT_of
 29.1156 +     val f' =
 29.1157 +       case f of
 29.1158 +         Const (name, T) =>
 29.1159 +           mk_fun_of compfuns thy (name, T) (iss, is')
 29.1160 +       | Free (name, T) => Free (name, funT_of compfuns (iss, is') T)
 29.1161 +       | _ => error ("PredicateCompiler: illegal parameter term")
 29.1162 +   in list_comb (f', params' @ args') end
 29.1163 +   
 29.1164 +fun compile_expr size thy ((Mode (mode, is, ms)), t) =
 29.1165 +  case strip_comb t of
 29.1166 +    (Const (name, T), params) =>
 29.1167 +       let
 29.1168 +         val params' = map (compile_param size thy PredicateCompFuns.compfuns) (ms ~~ params)
 29.1169 +         val mk_fun_of = case size of NONE => mk_fun_of | SOME _ => mk_sizelim_fun_of
 29.1170 +       in
 29.1171 +         list_comb (mk_fun_of PredicateCompFuns.compfuns thy (name, T) mode, params')
 29.1172 +       end
 29.1173 +  | (Free (name, T), args) =>
 29.1174 +       let 
 29.1175 +         val funT_of = case size of NONE => funT_of | SOME _ => sizelim_funT_of 
 29.1176 +       in
 29.1177 +         list_comb (Free (name, funT_of PredicateCompFuns.compfuns ([], is) T), args)
 29.1178 +       end;
 29.1179 +       
 29.1180 +fun compile_gen_expr size thy compfuns ((Mode (mode, is, ms)), t) =
 29.1181 +  case strip_comb t of
 29.1182 +    (Const (name, T), params) =>
 29.1183 +      let
 29.1184 +        val params' = map (compile_param size thy compfuns) (ms ~~ params)
 29.1185 +      in
 29.1186 +        list_comb (mk_generator_of compfuns thy (name, T) mode, params')
 29.1187 +      end
 29.1188 +    | (Free (name, T), args) =>
 29.1189 +      list_comb (Free (name, sizelim_funT_of RPredCompFuns.compfuns ([], is) T), args)
 29.1190 +          
 29.1191 +(** specific rpred functions -- move them to the correct place in this file *)
 29.1192 +
 29.1193 +(* uncommented termify code; causes more trouble than expected at first *) 
 29.1194 +(*
 29.1195 +fun mk_valtermify_term (t as Const (c, T)) = HOLogic.mk_prod (t, Abs ("u", HOLogic.unitT, HOLogic.reflect_term t))
 29.1196 +  | mk_valtermify_term (Free (x, T)) = Free (x, termifyT T) 
 29.1197 +  | mk_valtermify_term (t1 $ t2) =
 29.1198 +    let
 29.1199 +      val T = fastype_of t1
 29.1200 +      val (T1, T2) = dest_funT T
 29.1201 +      val t1' = mk_valtermify_term t1
 29.1202 +      val t2' = mk_valtermify_term t2
 29.1203 +    in
 29.1204 +      Const ("Code_Evaluation.valapp", termifyT T --> termifyT T1 --> termifyT T2) $ t1' $ t2'
 29.1205 +    end
 29.1206 +  | mk_valtermify_term _ = error "Not a valid term for mk_valtermify_term"
 29.1207 +*)
 29.1208 +
 29.1209 +fun compile_clause compfuns size final_term thy all_vs param_vs (iss, is) inp (ts, moded_ps) =
 29.1210 +  let
 29.1211 +    fun check_constrt t (names, eqs) =
 29.1212 +      if is_constrt thy t then (t, (names, eqs)) else
 29.1213 +        let
 29.1214 +          val s = Name.variant names "x";
 29.1215 +          val v = Free (s, fastype_of t)
 29.1216 +        in (v, (s::names, HOLogic.mk_eq (v, t)::eqs)) end;
 29.1217 +
 29.1218 +    val (in_ts, out_ts) = split_smode is ts;
 29.1219 +    val (in_ts', (all_vs', eqs)) =
 29.1220 +      fold_map check_constrt in_ts (all_vs, []);
 29.1221 +
 29.1222 +    fun compile_prems out_ts' vs names [] =
 29.1223 +          let
 29.1224 +            val (out_ts'', (names', eqs')) =
 29.1225 +              fold_map check_constrt out_ts' (names, []);
 29.1226 +            val (out_ts''', (names'', constr_vs)) = fold_map distinct_v
 29.1227 +              out_ts'' (names', map (rpair []) vs);
 29.1228 +          in
 29.1229 +          (* termify code:
 29.1230 +            compile_match thy compfuns constr_vs (eqs @ eqs') out_ts'''
 29.1231 +              (mk_single compfuns (mk_tuple (map mk_valtermify_term out_ts)))
 29.1232 +           *)
 29.1233 +            compile_match thy compfuns constr_vs (eqs @ eqs') out_ts'''
 29.1234 +              (final_term out_ts)
 29.1235 +          end
 29.1236 +      | compile_prems out_ts vs names ((p, mode as Mode ((_, is), _, _)) :: ps) =
 29.1237 +          let
 29.1238 +            val vs' = distinct (op =) (flat (vs :: map term_vs out_ts));
 29.1239 +            val (out_ts', (names', eqs)) =
 29.1240 +              fold_map check_constrt out_ts (names, [])
 29.1241 +            val (out_ts'', (names'', constr_vs')) = fold_map distinct_v
 29.1242 +              out_ts' ((names', map (rpair []) vs))
 29.1243 +            val (compiled_clause, rest) = case p of
 29.1244 +               Prem (us, t) =>
 29.1245 +                 let
 29.1246 +                   val (in_ts, out_ts''') = split_smode is us;
 29.1247 +                   val args = case size of
 29.1248 +                     NONE => in_ts
 29.1249 +                   | SOME size_t => in_ts @ [size_t]
 29.1250 +                   val u = lift_pred compfuns
 29.1251 +                     (list_comb (compile_expr size thy (mode, t), args))                     
 29.1252 +                   val rest = compile_prems out_ts''' vs' names'' ps
 29.1253 +                 in
 29.1254 +                   (u, rest)
 29.1255 +                 end
 29.1256 +             | Negprem (us, t) =>
 29.1257 +                 let
 29.1258 +                   val (in_ts, out_ts''') = split_smode is us
 29.1259 +                   val u = lift_pred compfuns
 29.1260 +                     (mk_not PredicateCompFuns.compfuns (list_comb (compile_expr NONE thy (mode, t), in_ts)))
 29.1261 +                   val rest = compile_prems out_ts''' vs' names'' ps
 29.1262 +                 in
 29.1263 +                   (u, rest)
 29.1264 +                 end
 29.1265 +             | Sidecond t =>
 29.1266 +                 let
 29.1267 +                   val rest = compile_prems [] vs' names'' ps;
 29.1268 +                 in
 29.1269 +                   (mk_if compfuns t, rest)
 29.1270 +                 end
 29.1271 +             | GeneratorPrem (us, t) =>
 29.1272 +                 let
 29.1273 +                   val (in_ts, out_ts''') = split_smode is us;
 29.1274 +                   val args = case size of
 29.1275 +                     NONE => in_ts
 29.1276 +                   | SOME size_t => in_ts @ [size_t]
 29.1277 +                   val u = list_comb (compile_gen_expr size thy compfuns (mode, t), args)
 29.1278 +                   val rest = compile_prems out_ts''' vs' names'' ps
 29.1279 +                 in
 29.1280 +                   (u, rest)
 29.1281 +                 end
 29.1282 +             | Generator (v, T) =>
 29.1283 +                 let
 29.1284 +                   val u = lift_random (HOLogic.mk_random T @{term "1::code_numeral"})
 29.1285 +                   val rest = compile_prems [Free (v, T)]  vs' names'' ps;
 29.1286 +                 in
 29.1287 +                   (u, rest)
 29.1288 +                 end
 29.1289 +          in
 29.1290 +            compile_match thy compfuns constr_vs' eqs out_ts'' 
 29.1291 +              (mk_bind compfuns (compiled_clause, rest))
 29.1292 +          end
 29.1293 +    val prem_t = compile_prems in_ts' param_vs all_vs' moded_ps;
 29.1294 +  in
 29.1295 +    mk_bind compfuns (mk_single compfuns inp, prem_t)
 29.1296 +  end
 29.1297 +
 29.1298 +fun compile_pred compfuns mk_fun_of use_size thy all_vs param_vs s T mode moded_cls =
 29.1299 +  let
 29.1300 +    val (Ts1, (Us1, Us2)) = split_mode mode (binder_types T)
 29.1301 +    val funT_of = if use_size then sizelim_funT_of else funT_of 
 29.1302 +    val Ts1' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) (fst mode) Ts1
 29.1303 +    val xnames = Name.variant_list (all_vs @ param_vs)
 29.1304 +      (map (fn i => "x" ^ string_of_int i) (snd mode));
 29.1305 +    val size_name = Name.variant (all_vs @ param_vs @ xnames) "size"
 29.1306 +    (* termify code: val xs = map2 (fn s => fn T => Free (s, termifyT T)) xnames Us1; *)
 29.1307 +    val xs = map2 (fn s => fn T => Free (s, T)) xnames Us1;
 29.1308 +    val params = map2 (fn s => fn T => Free (s, T)) param_vs Ts1'
 29.1309 +    val size = Free (size_name, @{typ "code_numeral"})
 29.1310 +    val decr_size =
 29.1311 +      if use_size then
 29.1312 +        SOME (Const ("HOL.minus_class.minus", @{typ "code_numeral => code_numeral => code_numeral"})
 29.1313 +          $ size $ Const ("HOL.one_class.one", @{typ "Code_Numeral.code_numeral"}))
 29.1314 +      else
 29.1315 +        NONE
 29.1316 +    val cl_ts =
 29.1317 +      map (compile_clause compfuns decr_size (fn out_ts => mk_single compfuns (mk_tuple out_ts))
 29.1318 +        thy all_vs param_vs mode (mk_tuple xs)) moded_cls;
 29.1319 +    val t = foldr1 (mk_sup compfuns) cl_ts
 29.1320 +    val T' = mk_predT compfuns (mk_tupleT Us2)
 29.1321 +    val size_t = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
 29.1322 +      $ HOLogic.mk_eq (size, @{term "0 :: code_numeral"})
 29.1323 +      $ mk_bot compfuns (dest_predT compfuns T') $ t
 29.1324 +    val fun_const = mk_fun_of compfuns thy (s, T) mode
 29.1325 +    val eq = if use_size then
 29.1326 +      (list_comb (fun_const, params @ xs @ [size]), size_t)
 29.1327 +    else
 29.1328 +      (list_comb (fun_const, params @ xs), t)
 29.1329 +  in
 29.1330 +    HOLogic.mk_Trueprop (HOLogic.mk_eq eq)
 29.1331 +  end;
 29.1332 +  
 29.1333 +(* special setup for simpset *)                  
 29.1334 +val HOL_basic_ss' = HOL_basic_ss setSolver 
 29.1335 +  (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
 29.1336 +
 29.1337 +(* Definition of executable functions and their intro and elim rules *)
 29.1338 +
 29.1339 +fun print_arities arities = tracing ("Arities:\n" ^
 29.1340 +  cat_lines (map (fn (s, (ks, k)) => s ^ ": " ^
 29.1341 +    space_implode " -> " (map
 29.1342 +      (fn NONE => "X" | SOME k' => string_of_int k')
 29.1343 +        (ks @ [SOME k]))) arities));
 29.1344 +
 29.1345 +fun mk_Eval_of ((x, T), NONE) names = (x, names)
 29.1346 +  | mk_Eval_of ((x, T), SOME mode) names = let
 29.1347 +  val Ts = binder_types T
 29.1348 +  val argnames = Name.variant_list names
 29.1349 +        (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
 29.1350 +  val args = map Free (argnames ~~ Ts)
 29.1351 +  val (inargs, outargs) = split_smode mode args
 29.1352 +  val r = PredicateCompFuns.mk_Eval (list_comb (x, inargs), mk_tuple outargs)
 29.1353 +  val t = fold_rev lambda args r 
 29.1354 +in
 29.1355 +  (t, argnames @ names)
 29.1356 +end;
 29.1357 +
 29.1358 +fun create_intro_elim_rule (mode as (iss, is)) defthm mode_id funT pred thy =
 29.1359 +let
 29.1360 +  val Ts = binder_types (fastype_of pred)
 29.1361 +  val funtrm = Const (mode_id, funT)
 29.1362 +  val argnames = Name.variant_list []
 29.1363 +        (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
 29.1364 +  val (Ts1, Ts2) = chop (length iss) Ts;
 29.1365 +  val Ts1' = map2 (fn NONE => I | SOME is => funT_of (PredicateCompFuns.compfuns) ([], is)) iss Ts1
 29.1366 +  val args = map Free (argnames ~~ (Ts1' @ Ts2))
 29.1367 +  val (params, ioargs) = chop (length iss) args
 29.1368 +  val (inargs, outargs) = split_smode is ioargs
 29.1369 +  val param_names = Name.variant_list argnames
 29.1370 +    (map (fn i => "p" ^ string_of_int i) (1 upto (length iss)))
 29.1371 +  val param_vs = map Free (param_names ~~ Ts1)
 29.1372 +  val (params', names) = fold_map mk_Eval_of ((params ~~ Ts1) ~~ iss) []
 29.1373 +  val predpropI = HOLogic.mk_Trueprop (list_comb (pred, param_vs @ ioargs))
 29.1374 +  val predpropE = HOLogic.mk_Trueprop (list_comb (pred, params' @ ioargs))
 29.1375 +  val param_eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (param_vs ~~ params')
 29.1376 +  val funargs = params @ inargs
 29.1377 +  val funpropE = HOLogic.mk_Trueprop (PredicateCompFuns.mk_Eval (list_comb (funtrm, funargs),
 29.1378 +                  if null outargs then Free("y", HOLogic.unitT) else mk_tuple outargs))
 29.1379 +  val funpropI = HOLogic.mk_Trueprop (PredicateCompFuns.mk_Eval (list_comb (funtrm, funargs),
 29.1380 +                   mk_tuple outargs))
 29.1381 +  val introtrm = Logic.list_implies (predpropI :: param_eqs, funpropI)
 29.1382 +  val simprules = [defthm, @{thm eval_pred},
 29.1383 +                   @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}]
 29.1384 +  val unfolddef_tac = Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps simprules) 1
 29.1385 +  val introthm = Goal.prove (ProofContext.init thy) (argnames @ param_names @ ["y"]) [] introtrm (fn {...} => unfolddef_tac)
 29.1386 +  val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT));
 29.1387 +  val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predpropE, P)], P)
 29.1388 +  val elimthm = Goal.prove (ProofContext.init thy) (argnames @ param_names @ ["y", "P"]) [] elimtrm (fn {...} => unfolddef_tac)
 29.1389 +in 
 29.1390 +  (introthm, elimthm)
 29.1391 +end;
 29.1392 +
 29.1393 +fun create_constname_of_mode thy prefix name mode = 
 29.1394 +  let
 29.1395 +    fun string_of_mode mode = if null mode then "0"
 29.1396 +      else space_implode "_" (map string_of_int mode)
 29.1397 +    val HOmode = space_implode "_and_"
 29.1398 +      (fold (fn NONE => I | SOME mode => cons (string_of_mode mode)) (fst mode) [])
 29.1399 +  in
 29.1400 +    (Sign.full_bname thy (prefix ^ (Long_Name.base_name name))) ^
 29.1401 +      (if HOmode = "" then "_" else "_for_" ^ HOmode ^ "_yields_") ^ (string_of_mode (snd mode))
 29.1402 +  end;
 29.1403 +  
 29.1404 +fun create_definitions preds (name, modes) thy =
 29.1405 +  let
 29.1406 +    val compfuns = PredicateCompFuns.compfuns
 29.1407 +    val T = AList.lookup (op =) preds name |> the
 29.1408 +    fun create_definition (mode as (iss, is)) thy = let
 29.1409 +      val mode_cname = create_constname_of_mode thy "" name mode
 29.1410 +      val mode_cbasename = Long_Name.base_name mode_cname
 29.1411 +      val Ts = binder_types T
 29.1412 +      val (Ts1, Ts2) = chop (length iss) Ts
 29.1413 +      val (Us1, Us2) =  split_smode is Ts2
 29.1414 +      val Ts1' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) iss Ts1
 29.1415 +      val funT = (Ts1' @ Us1) ---> (mk_predT compfuns (mk_tupleT Us2))
 29.1416 +      val names = Name.variant_list []
 29.1417 +        (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
 29.1418 +      val xs = map Free (names ~~ (Ts1' @ Ts2));                   
 29.1419 +      val (xparams, xargs) = chop (length iss) xs;
 29.1420 +      val (xins, xouts) = split_smode is xargs 
 29.1421 +      val (xparams', names') = fold_map mk_Eval_of ((xparams ~~ Ts1) ~~ iss) names
 29.1422 +      fun mk_split_lambda [] t = lambda (Free (Name.variant names' "x", HOLogic.unitT)) t
 29.1423 +        | mk_split_lambda [x] t = lambda x t
 29.1424 +        | mk_split_lambda xs t =
 29.1425 +        let
 29.1426 +          fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t))
 29.1427 +            | mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t))
 29.1428 +        in
 29.1429 +          mk_split_lambda' xs t
 29.1430 +        end;
 29.1431 +      val predterm = PredicateCompFuns.mk_Enum (mk_split_lambda xouts
 29.1432 +        (list_comb (Const (name, T), xparams' @ xargs)))
 29.1433 +      val lhs = list_comb (Const (mode_cname, funT), xparams @ xins)
 29.1434 +      val def = Logic.mk_equals (lhs, predterm)
 29.1435 +      val ([definition], thy') = thy |>
 29.1436 +        Sign.add_consts_i [(Binding.name mode_cbasename, funT, NoSyn)] |>
 29.1437 +        PureThy.add_defs false [((Binding.name (mode_cbasename ^ "_def"), def), [])]
 29.1438 +      val (intro, elim) =
 29.1439 +        create_intro_elim_rule mode definition mode_cname funT (Const (name, T)) thy'
 29.1440 +      in thy' |> add_predfun name mode (mode_cname, definition, intro, elim)
 29.1441 +        |> PureThy.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd
 29.1442 +        |> PureThy.store_thm (Binding.name (mode_cbasename ^ "E"), elim)  |> snd
 29.1443 +        |> Theory.checkpoint
 29.1444 +      end;
 29.1445 +  in
 29.1446 +    fold create_definition modes thy
 29.1447 +  end;
 29.1448 +
 29.1449 +fun sizelim_create_definitions preds (name, modes) thy =
 29.1450 +  let
 29.1451 +    val T = AList.lookup (op =) preds name |> the
 29.1452 +    fun create_definition mode thy =
 29.1453 +      let
 29.1454 +        val mode_cname = create_constname_of_mode thy "sizelim_" name mode
 29.1455 +        val funT = sizelim_funT_of PredicateCompFuns.compfuns mode T
 29.1456 +      in
 29.1457 +        thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
 29.1458 +        |> set_sizelim_function_name name mode mode_cname 
 29.1459 +      end;
 29.1460 +  in
 29.1461 +    fold create_definition modes thy
 29.1462 +  end;
 29.1463 +    
 29.1464 +fun rpred_create_definitions preds (name, modes) thy =
 29.1465 +  let
 29.1466 +    val T = AList.lookup (op =) preds name |> the
 29.1467 +    fun create_definition mode thy =
 29.1468 +      let
 29.1469 +        val mode_cname = create_constname_of_mode thy "gen_" name mode
 29.1470 +        val funT = sizelim_funT_of RPredCompFuns.compfuns mode T
 29.1471 +      in
 29.1472 +        thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
 29.1473 +        |> set_generator_name name mode mode_cname 
 29.1474 +      end;
 29.1475 +  in
 29.1476 +    fold create_definition modes thy
 29.1477 +  end;
 29.1478 +  
 29.1479 +(* Proving equivalence of term *)
 29.1480 +
 29.1481 +fun is_Type (Type _) = true
 29.1482 +  | is_Type _ = false
 29.1483 +
 29.1484 +(* returns true if t is an application of an datatype constructor *)
 29.1485 +(* which then consequently would be splitted *)
 29.1486 +(* else false *)
 29.1487 +fun is_constructor thy t =
 29.1488 +  if (is_Type (fastype_of t)) then
 29.1489 +    (case Datatype.get_info thy ((fst o dest_Type o fastype_of) t) of
 29.1490 +      NONE => false
 29.1491 +    | SOME info => (let
 29.1492 +      val constr_consts = maps (fn (_, (_, _, constrs)) => map fst constrs) (#descr info)
 29.1493 +      val (c, _) = strip_comb t
 29.1494 +      in (case c of
 29.1495 +        Const (name, _) => name mem_string constr_consts
 29.1496 +        | _ => false) end))
 29.1497 +  else false
 29.1498 +
 29.1499 +(* MAJOR FIXME:  prove_params should be simple
 29.1500 + - different form of introrule for parameters ? *)
 29.1501 +fun prove_param thy (NONE, t) = TRY (rtac @{thm refl} 1)
 29.1502 +  | prove_param thy (m as SOME (Mode (mode, is, ms)), t) =
 29.1503 +  let
 29.1504 +    val  (f, args) = strip_comb (Envir.eta_contract t)
 29.1505 +    val (params, _) = chop (length ms) args
 29.1506 +    val f_tac = case f of
 29.1507 +      Const (name, T) => simp_tac (HOL_basic_ss addsimps 
 29.1508 +         (@{thm eval_pred}::(predfun_definition_of thy name mode)::
 29.1509 +         @{thm "Product_Type.split_conv"}::[])) 1
 29.1510 +    | Free _ => TRY (rtac @{thm refl} 1)
 29.1511 +    | Abs _ => error "prove_param: No valid parameter term"
 29.1512 +  in
 29.1513 +    REPEAT_DETERM (etac @{thm thin_rl} 1)
 29.1514 +    THEN REPEAT_DETERM (rtac @{thm ext} 1)
 29.1515 +    THEN print_tac "prove_param"
 29.1516 +    THEN f_tac
 29.1517 +    THEN print_tac "after simplification in prove_args"
 29.1518 +    THEN (EVERY (map (prove_param thy) (ms ~~ params)))
 29.1519 +    THEN (REPEAT_DETERM (atac 1))
 29.1520 +  end
 29.1521 +
 29.1522 +fun prove_expr thy (Mode (mode, is, ms), t, us) (premposition : int) =
 29.1523 +  case strip_comb t of
 29.1524 +    (Const (name, T), args) =>  
 29.1525 +      let
 29.1526 +        val introrule = predfun_intro_of thy name mode
 29.1527 +        val (args1, args2) = chop (length ms) args
 29.1528 +      in
 29.1529 +        rtac @{thm bindI} 1
 29.1530 +        THEN print_tac "before intro rule:"
 29.1531 +        (* for the right assumption in first position *)
 29.1532 +        THEN rotate_tac premposition 1
 29.1533 +        THEN debug_tac (Display.string_of_thm (ProofContext.init thy) introrule)
 29.1534 +        THEN rtac introrule 1
 29.1535 +        THEN print_tac "after intro rule"
 29.1536 +        (* work with parameter arguments *)
 29.1537 +        THEN (atac 1)
 29.1538 +        THEN (print_tac "parameter goal")
 29.1539 +        THEN (EVERY (map (prove_param thy) (ms ~~ args1)))
 29.1540 +        THEN (REPEAT_DETERM (atac 1))
 29.1541 +      end
 29.1542 +  | _ => rtac @{thm bindI} 1 THEN atac 1
 29.1543 +
 29.1544 +fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st; 
 29.1545 +
 29.1546 +fun SOLVEDALL tac st = FILTER (fn st' => nprems_of st' = 0) tac st
 29.1547 +
 29.1548 +fun prove_match thy (out_ts : term list) = let
 29.1549 +  fun get_case_rewrite t =
 29.1550 +    if (is_constructor thy t) then let
 29.1551 +      val case_rewrites = (#case_rewrites (Datatype.the_info thy
 29.1552 +        ((fst o dest_Type o fastype_of) t)))
 29.1553 +      in case_rewrites @ (flat (map get_case_rewrite (snd (strip_comb t)))) end
 29.1554 +    else []
 29.1555 +  val simprules = @{thm "unit.cases"} :: @{thm "prod.cases"} :: (flat (map get_case_rewrite out_ts))
 29.1556 +(* replace TRY by determining if it necessary - are there equations when calling compile match? *)
 29.1557 +in
 29.1558 +   (* make this simpset better! *)
 29.1559 +  asm_simp_tac (HOL_basic_ss' addsimps simprules) 1
 29.1560 +  THEN print_tac "after prove_match:"
 29.1561 +  THEN (DETERM (TRY (EqSubst.eqsubst_tac (ProofContext.init thy) [0] [@{thm "HOL.if_P"}] 1
 29.1562 +         THEN (REPEAT_DETERM (rtac @{thm conjI} 1 THEN (SOLVED (asm_simp_tac HOL_basic_ss 1))))
 29.1563 +         THEN (SOLVED (asm_simp_tac HOL_basic_ss 1)))))
 29.1564 +  THEN print_tac "after if simplification"
 29.1565 +end;
 29.1566 +
 29.1567 +(* corresponds to compile_fun -- maybe call that also compile_sidecond? *)
 29.1568 +
 29.1569 +fun prove_sidecond thy modes t =
 29.1570 +  let
 29.1571 +    fun preds_of t nameTs = case strip_comb t of 
 29.1572 +      (f as Const (name, T), args) =>
 29.1573 +        if AList.defined (op =) modes name then (name, T) :: nameTs
 29.1574 +          else fold preds_of args nameTs
 29.1575 +      | _ => nameTs
 29.1576 +    val preds = preds_of t []
 29.1577 +    val defs = map
 29.1578 +      (fn (pred, T) => predfun_definition_of thy pred ([], (1 upto (length (binder_types T)))))
 29.1579 +        preds
 29.1580 +  in 
 29.1581 +    (* remove not_False_eq_True when simpset in prove_match is better *)
 29.1582 +    simp_tac (HOL_basic_ss addsimps @{thm not_False_eq_True} :: @{thm eval_pred} :: defs) 1 
 29.1583 +    (* need better control here! *)
 29.1584 +  end
 29.1585 +
 29.1586 +fun prove_clause thy nargs modes (iss, is) (_, clauses) (ts, moded_ps) =
 29.1587 +  let
 29.1588 +    val (in_ts, clause_out_ts) = split_smode is ts;
 29.1589 +    fun prove_prems out_ts [] =
 29.1590 +      (prove_match thy out_ts)
 29.1591 +      THEN asm_simp_tac HOL_basic_ss' 1
 29.1592 +      THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
 29.1593 +    | prove_prems out_ts ((p, mode as Mode ((iss, is), _, param_modes)) :: ps) =
 29.1594 +      let
 29.1595 +        val premposition = (find_index (equal p) clauses) + nargs
 29.1596 +        val rest_tac = (case p of Prem (us, t) =>
 29.1597 +            let
 29.1598 +              val (_, out_ts''') = split_smode is us
 29.1599 +              val rec_tac = prove_prems out_ts''' ps
 29.1600 +            in
 29.1601 +              print_tac "before clause:"
 29.1602 +              THEN asm_simp_tac HOL_basic_ss 1
 29.1603 +              THEN print_tac "before prove_expr:"
 29.1604 +              THEN prove_expr thy (mode, t, us) premposition
 29.1605 +              THEN print_tac "after prove_expr:"
 29.1606 +              THEN rec_tac
 29.1607 +            end
 29.1608 +          | Negprem (us, t) =>
 29.1609 +            let
 29.1610 +              val (_, out_ts''') = split_smode is us
 29.1611 +              val rec_tac = prove_prems out_ts''' ps
 29.1612 +              val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE)
 29.1613 +              val (_, params) = strip_comb t
 29.1614 +            in
 29.1615 +              rtac @{thm bindI} 1
 29.1616 +              THEN (if (is_some name) then
 29.1617 +                  simp_tac (HOL_basic_ss addsimps [predfun_definition_of thy (the name) (iss, is)]) 1
 29.1618 +                  THEN rtac @{thm not_predI} 1
 29.1619 +                  THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1
 29.1620 +                  THEN (REPEAT_DETERM (atac 1))
 29.1621 +                  (* FIXME: work with parameter arguments *)
 29.1622 +                  THEN (EVERY (map (prove_param thy) (param_modes ~~ params)))
 29.1623 +                else
 29.1624 +                  rtac @{thm not_predI'} 1)
 29.1625 +                  THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1
 29.1626 +              THEN rec_tac
 29.1627 +            end
 29.1628 +          | Sidecond t =>
 29.1629 +           rtac @{thm bindI} 1
 29.1630 +           THEN rtac @{thm if_predI} 1
 29.1631 +           THEN print_tac "before sidecond:"
 29.1632 +           THEN prove_sidecond thy modes t
 29.1633 +           THEN print_tac "after sidecond:"
 29.1634 +           THEN prove_prems [] ps)
 29.1635 +      in (prove_match thy out_ts)
 29.1636 +          THEN rest_tac
 29.1637 +      end;
 29.1638 +    val prems_tac = prove_prems in_ts moded_ps
 29.1639 +  in
 29.1640 +    rtac @{thm bindI} 1
 29.1641 +    THEN rtac @{thm singleI} 1
 29.1642 +    THEN prems_tac
 29.1643 +  end;
 29.1644 +
 29.1645 +fun select_sup 1 1 = []
 29.1646 +  | select_sup _ 1 = [rtac @{thm supI1}]
 29.1647 +  | select_sup n i = (rtac @{thm supI2})::(select_sup (n - 1) (i - 1));
 29.1648 +
 29.1649 +fun prove_one_direction thy clauses preds modes pred mode moded_clauses =
 29.1650 +  let
 29.1651 +    val T = the (AList.lookup (op =) preds pred)
 29.1652 +    val nargs = length (binder_types T) - nparams_of thy pred
 29.1653 +    val pred_case_rule = the_elim_of thy pred
 29.1654 +  in
 29.1655 +    REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"}))
 29.1656 +    THEN etac (predfun_elim_of thy pred mode) 1
 29.1657 +    THEN etac pred_case_rule 1
 29.1658 +    THEN (EVERY (map
 29.1659 +           (fn i => EVERY' (select_sup (length moded_clauses) i) i) 
 29.1660 +             (1 upto (length moded_clauses))))
 29.1661 +    THEN (EVERY (map2 (prove_clause thy nargs modes mode) clauses moded_clauses))
 29.1662 +    THEN print_tac "proved one direction"
 29.1663 +  end;
 29.1664 +
 29.1665 +(** Proof in the other direction **)
 29.1666 +
 29.1667 +fun prove_match2 thy out_ts = let
 29.1668 +  fun split_term_tac (Free _) = all_tac
 29.1669 +    | split_term_tac t =
 29.1670 +      if (is_constructor thy t) then let
 29.1671 +        val info = Datatype.the_info thy ((fst o dest_Type o fastype_of) t)
 29.1672 +        val num_of_constrs = length (#case_rewrites info)
 29.1673 +        (* special treatment of pairs -- because of fishing *)
 29.1674 +        val split_rules = case (fst o dest_Type o fastype_of) t of
 29.1675 +          "*" => [@{thm prod.split_asm}] 
 29.1676 +          | _ => PureThy.get_thms thy (((fst o dest_Type o fastype_of) t) ^ ".split_asm")
 29.1677 +        val (_, ts) = strip_comb t
 29.1678 +      in
 29.1679 +        (Splitter.split_asm_tac split_rules 1)
 29.1680 +(*        THEN (Simplifier.asm_full_simp_tac HOL_basic_ss 1)
 29.1681 +          THEN (DETERM (TRY (etac @{thm Pair_inject} 1))) *)
 29.1682 +        THEN (REPEAT_DETERM_N (num_of_constrs - 1) (etac @{thm botE} 1 ORELSE etac @{thm botE} 2))
 29.1683 +        THEN (EVERY (map split_term_tac ts))
 29.1684 +      end
 29.1685 +    else all_tac
 29.1686 +  in
 29.1687 +    split_term_tac (mk_tuple out_ts)
 29.1688 +    THEN (DETERM (TRY ((Splitter.split_asm_tac [@{thm "split_if_asm"}] 1) THEN (etac @{thm botE} 2))))
 29.1689 +  end
 29.1690 +
 29.1691 +(* VERY LARGE SIMILIRATIY to function prove_param 
 29.1692 +-- join both functions
 29.1693 +*)
 29.1694 +(* TODO: remove function *)
 29.1695 +
 29.1696 +fun prove_param2 thy (NONE, t) = all_tac 
 29.1697 +  | prove_param2 thy (m as SOME (Mode (mode, is, ms)), t) = let
 29.1698 +    val  (f, args) = strip_comb (Envir.eta_contract t)
 29.1699 +    val (params, _) = chop (length ms) args
 29.1700 +    val f_tac = case f of
 29.1701 +        Const (name, T) => full_simp_tac (HOL_basic_ss addsimps 
 29.1702 +           (@{thm eval_pred}::(predfun_definition_of thy name mode)
 29.1703 +           :: @{thm "Product_Type.split_conv"}::[])) 1
 29.1704 +      | Free _ => all_tac
 29.1705 +      | _ => error "prove_param2: illegal parameter term"
 29.1706 +  in  
 29.1707 +    print_tac "before simplification in prove_args:"
 29.1708 +    THEN f_tac
 29.1709 +    THEN print_tac "after simplification in prove_args"
 29.1710 +    THEN (EVERY (map (prove_param2 thy) (ms ~~ params)))
 29.1711 +  end
 29.1712 +
 29.1713 +
 29.1714 +fun prove_expr2 thy (Mode (mode, is, ms), t) = 
 29.1715 +  (case strip_comb t of
 29.1716 +    (Const (name, T), args) =>
 29.1717 +      etac @{thm bindE} 1
 29.1718 +      THEN (REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"})))
 29.1719 +      THEN print_tac "prove_expr2-before"
 29.1720 +      THEN (debug_tac (Syntax.string_of_term_global thy
 29.1721 +        (prop_of (predfun_elim_of thy name mode))))
 29.1722 +      THEN (etac (predfun_elim_of thy name mode) 1)
 29.1723 +      THEN print_tac "prove_expr2"
 29.1724 +      THEN (EVERY (map (prove_param2 thy) (ms ~~ args)))
 29.1725 +      THEN print_tac "finished prove_expr2"      
 29.1726 +    | _ => etac @{thm bindE} 1)
 29.1727 +    
 29.1728 +(* FIXME: what is this for? *)
 29.1729 +(* replace defined by has_mode thy pred *)
 29.1730 +(* TODO: rewrite function *)
 29.1731 +fun prove_sidecond2 thy modes t = let
 29.1732 +  fun preds_of t nameTs = case strip_comb t of 
 29.1733 +    (f as Const (name, T), args) =>
 29.1734 +      if AList.defined (op =) modes name then (name, T) :: nameTs
 29.1735 +        else fold preds_of args nameTs
 29.1736 +    | _ => nameTs
 29.1737 +  val preds = preds_of t []
 29.1738 +  val defs = map
 29.1739 +    (fn (pred, T) => predfun_definition_of thy pred ([], (1 upto (length (binder_types T)))))
 29.1740 +      preds
 29.1741 +  in
 29.1742 +   (* only simplify the one assumption *)
 29.1743 +   full_simp_tac (HOL_basic_ss' addsimps @{thm eval_pred} :: defs) 1 
 29.1744 +   (* need better control here! *)
 29.1745 +   THEN print_tac "after sidecond2 simplification"
 29.1746 +   end
 29.1747 +  
 29.1748 +fun prove_clause2 thy modes pred (iss, is) (ts, ps) i =
 29.1749 +  let
 29.1750 +    val pred_intro_rule = nth (intros_of thy pred) (i - 1)
 29.1751 +    val (in_ts, clause_out_ts) = split_smode is ts;
 29.1752 +    fun prove_prems2 out_ts [] =
 29.1753 +      print_tac "before prove_match2 - last call:"
 29.1754 +      THEN prove_match2 thy out_ts
 29.1755 +      THEN print_tac "after prove_match2 - last call:"
 29.1756 +      THEN (etac @{thm singleE} 1)
 29.1757 +      THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1))
 29.1758 +      THEN (asm_full_simp_tac HOL_basic_ss' 1)
 29.1759 +      THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1))
 29.1760 +      THEN (asm_full_simp_tac HOL_basic_ss' 1)
 29.1761 +      THEN SOLVED (print_tac "state before applying intro rule:"
 29.1762 +      THEN (rtac pred_intro_rule 1)
 29.1763 +      (* How to handle equality correctly? *)
 29.1764 +      THEN (print_tac "state before assumption matching")
 29.1765 +      THEN (REPEAT (atac 1 ORELSE 
 29.1766 +         (CHANGED (asm_full_simp_tac HOL_basic_ss' 1)
 29.1767 +          THEN print_tac "state after simp_tac:"))))
 29.1768 +    | prove_prems2 out_ts ((p, mode as Mode ((iss, is), _, param_modes)) :: ps) =
 29.1769 +      let
 29.1770 +        val rest_tac = (case p of
 29.1771 +          Prem (us, t) =>
 29.1772 +          let
 29.1773 +            val (_, out_ts''') = split_smode is us
 29.1774 +            val rec_tac = prove_prems2 out_ts''' ps
 29.1775 +          in
 29.1776 +            (prove_expr2 thy (mode, t)) THEN rec_tac
 29.1777 +          end
 29.1778 +        | Negprem (us, t) =>
 29.1779 +          let
 29.1780 +            val (_, out_ts''') = split_smode is us
 29.1781 +            val rec_tac = prove_prems2 out_ts''' ps
 29.1782 +            val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE)
 29.1783 +            val (_, params) = strip_comb t
 29.1784 +          in
 29.1785 +            print_tac "before neg prem 2"
 29.1786 +            THEN etac @{thm bindE} 1
 29.1787 +            THEN (if is_some name then
 29.1788 +                full_simp_tac (HOL_basic_ss addsimps [predfun_definition_of thy (the name) (iss, is)]) 1 
 29.1789 +                THEN etac @{thm not_predE} 1
 29.1790 +                THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1
 29.1791 +                THEN (EVERY (map (prove_param2 thy) (param_modes ~~ params)))
 29.1792 +              else
 29.1793 +                etac @{thm not_predE'} 1)
 29.1794 +            THEN rec_tac
 29.1795 +          end 
 29.1796 +        | Sidecond t =>
 29.1797 +          etac @{thm bindE} 1
 29.1798 +          THEN etac @{thm if_predE} 1
 29.1799 +          THEN prove_sidecond2 thy modes t 
 29.1800 +          THEN prove_prems2 [] ps)
 29.1801 +      in print_tac "before prove_match2:"
 29.1802 +         THEN prove_match2 thy out_ts
 29.1803 +         THEN print_tac "after prove_match2:"
 29.1804 +         THEN rest_tac
 29.1805 +      end;
 29.1806 +    val prems_tac = prove_prems2 in_ts ps 
 29.1807 +  in
 29.1808 +    print_tac "starting prove_clause2"
 29.1809 +    THEN etac @{thm bindE} 1
 29.1810 +    THEN (etac @{thm singleE'} 1)
 29.1811 +    THEN (TRY (etac @{thm Pair_inject} 1))
 29.1812 +    THEN print_tac "after singleE':"
 29.1813 +    THEN prems_tac
 29.1814 +  end;
 29.1815 + 
 29.1816 +fun prove_other_direction thy modes pred mode moded_clauses =
 29.1817 +  let
 29.1818 +    fun prove_clause clause i =
 29.1819 +      (if i < length moded_clauses then etac @{thm supE} 1 else all_tac)
 29.1820 +      THEN (prove_clause2 thy modes pred mode clause i)
 29.1821 +  in
 29.1822 +    (DETERM (TRY (rtac @{thm unit.induct} 1)))
 29.1823 +     THEN (REPEAT_DETERM (CHANGED (rewtac @{thm split_paired_all})))
 29.1824 +     THEN (rtac (predfun_intro_of thy pred mode) 1)
 29.1825 +     THEN (REPEAT_DETERM (rtac @{thm refl} 2))
 29.1826 +     THEN (EVERY (map2 prove_clause moded_clauses (1 upto (length moded_clauses))))
 29.1827 +  end;
 29.1828 +
 29.1829 +(** proof procedure **)
 29.1830 +
 29.1831 +fun prove_pred thy clauses preds modes pred mode (moded_clauses, compiled_term) =
 29.1832 +  let
 29.1833 +    val ctxt = ProofContext.init thy
 29.1834 +    val clauses = the (AList.lookup (op =) clauses pred)
 29.1835 +  in
 29.1836 +    Goal.prove ctxt (Term.add_free_names compiled_term []) [] compiled_term
 29.1837 +      (if !do_proofs then
 29.1838 +        (fn _ =>
 29.1839 +        rtac @{thm pred_iffI} 1
 29.1840 +        THEN prove_one_direction thy clauses preds modes pred mode moded_clauses
 29.1841 +        THEN print_tac "proved one direction"
 29.1842 +        THEN prove_other_direction thy modes pred mode moded_clauses
 29.1843 +        THEN print_tac "proved other direction")
 29.1844 +       else (fn _ => mycheat_tac thy 1))
 29.1845 +  end;
 29.1846 +
 29.1847 +(* composition of mode inference, definition, compilation and proof *)
 29.1848 +
 29.1849 +(** auxillary combinators for table of preds and modes **)
 29.1850 +
 29.1851 +fun map_preds_modes f preds_modes_table =
 29.1852 +  map (fn (pred, modes) =>
 29.1853 +    (pred, map (fn (mode, value) => (mode, f pred mode value)) modes)) preds_modes_table
 29.1854 +
 29.1855 +fun join_preds_modes table1 table2 =
 29.1856 +  map_preds_modes (fn pred => fn mode => fn value =>
 29.1857 +    (value, the (AList.lookup (op =) (the (AList.lookup (op =) table2 pred)) mode))) table1
 29.1858 +    
 29.1859 +fun maps_modes preds_modes_table =
 29.1860 +  map (fn (pred, modes) =>
 29.1861 +    (pred, map (fn (mode, value) => value) modes)) preds_modes_table  
 29.1862 +    
 29.1863 +fun compile_preds compfuns mk_fun_of use_size thy all_vs param_vs preds moded_clauses =
 29.1864 +  map_preds_modes (fn pred => compile_pred compfuns mk_fun_of use_size thy all_vs param_vs pred
 29.1865 +      (the (AList.lookup (op =) preds pred))) moded_clauses  
 29.1866 +  
 29.1867 +fun prove thy clauses preds modes moded_clauses compiled_terms =
 29.1868 +  map_preds_modes (prove_pred thy clauses preds modes)
 29.1869 +    (join_preds_modes moded_clauses compiled_terms)
 29.1870 +
 29.1871 +fun prove_by_skip thy _ _ _ _ compiled_terms =
 29.1872 +  map_preds_modes (fn pred => fn mode => fn t => Drule.standard (SkipProof.make_thm thy t))
 29.1873 +    compiled_terms
 29.1874 +    
 29.1875 +fun prepare_intrs thy prednames =
 29.1876 +  let
 29.1877 +    val intrs = maps (intros_of thy) prednames
 29.1878 +      |> map (Logic.unvarify o prop_of)
 29.1879 +    val nparams = nparams_of thy (hd prednames)
 29.1880 +    val extra_modes = all_modes_of thy |> filter_out (fn (name, _) => member (op =) prednames name)
 29.1881 +    val preds = distinct (op =) (map (dest_Const o fst o (strip_intro_concl nparams)) intrs)
 29.1882 +    val _ $ u = Logic.strip_imp_concl (hd intrs);
 29.1883 +    val params = List.take (snd (strip_comb u), nparams);
 29.1884 +    val param_vs = maps term_vs params
 29.1885 +    val all_vs = terms_vs intrs
 29.1886 +    fun dest_prem t =
 29.1887 +      (case strip_comb t of
 29.1888 +        (v as Free _, ts) => if v mem params then Prem (ts, v) else Sidecond t
 29.1889 +      | (c as Const (@{const_name Not}, _), [t]) => (case dest_prem t of          
 29.1890 +          Prem (ts, t) => Negprem (ts, t)
 29.1891 +        | Negprem _ => error ("Double negation not allowed in premise: " ^ (Syntax.string_of_term_global thy (c $ t))) 
 29.1892 +        | Sidecond t => Sidecond (c $ t))
 29.1893 +      | (c as Const (s, _), ts) =>
 29.1894 +        if is_registered thy s then
 29.1895 +          let val (ts1, ts2) = chop (nparams_of thy s) ts
 29.1896 +          in Prem (ts2, list_comb (c, ts1)) end
 29.1897 +        else Sidecond t
 29.1898 +      | _ => Sidecond t)
 29.1899 +    fun add_clause intr (clauses, arities) =
 29.1900 +    let
 29.1901 +      val _ $ t = Logic.strip_imp_concl intr;
 29.1902 +      val (Const (name, T), ts) = strip_comb t;
 29.1903 +      val (ts1, ts2) = chop nparams ts;
 29.1904 +      val prems = map (dest_prem o HOLogic.dest_Trueprop) (Logic.strip_imp_prems intr);
 29.1905 +      val (Ts, Us) = chop nparams (binder_types T)
 29.1906 +    in
 29.1907 +      (AList.update op = (name, these (AList.lookup op = clauses name) @
 29.1908 +        [(ts2, prems)]) clauses,
 29.1909 +       AList.update op = (name, (map (fn U => (case strip_type U of
 29.1910 +                 (Rs as _ :: _, Type ("bool", [])) => SOME (length Rs)
 29.1911 +               | _ => NONE)) Ts,
 29.1912 +             length Us)) arities)
 29.1913 +    end;
 29.1914 +    val (clauses, arities) = fold add_clause intrs ([], []);
 29.1915 +  in (preds, nparams, all_vs, param_vs, extra_modes, clauses, arities) end;
 29.1916 +
 29.1917 +(** main function of predicate compiler **)
 29.1918 +
 29.1919 +fun add_equations_of steps prednames thy =
 29.1920 +  let
 29.1921 +    val _ = Output.tracing ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
 29.1922 +    val (preds, nparams, all_vs, param_vs, extra_modes, clauses, arities) =
 29.1923 +      prepare_intrs thy prednames
 29.1924 +    val _ = Output.tracing "Infering modes..."
 29.1925 +    val moded_clauses = #infer_modes steps thy extra_modes arities param_vs clauses 
 29.1926 +    val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
 29.1927 +    val _ = print_modes modes
 29.1928 +    val _ = print_moded_clauses thy moded_clauses
 29.1929 +    val _ = Output.tracing "Defining executable functions..."
 29.1930 +    val thy' = fold (#create_definitions steps preds) modes thy
 29.1931 +      |> Theory.checkpoint
 29.1932 +    val _ = Output.tracing "Compiling equations..."
 29.1933 +    val compiled_terms =
 29.1934 +      (#compile_preds steps) thy' all_vs param_vs preds moded_clauses
 29.1935 +    val _ = print_compiled_terms thy' compiled_terms
 29.1936 +    val _ = Output.tracing "Proving equations..."
 29.1937 +    val result_thms = #prove steps thy' clauses preds (extra_modes @ modes)
 29.1938 +      moded_clauses compiled_terms
 29.1939 +    val qname = #qname steps
 29.1940 +    (* val attrib = gn thy => Attrib.attribute_i thy Code.add_eqn_attrib *)
 29.1941 +    val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute
 29.1942 +      (fn thm => Context.mapping (Code.add_eqn thm) I))))
 29.1943 +    val thy'' = fold (fn (name, result_thms) => fn thy => snd (PureThy.add_thmss
 29.1944 +      [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms),
 29.1945 +        [attrib thy ])] thy))
 29.1946 +      (maps_modes result_thms) thy'
 29.1947 +      |> Theory.checkpoint
 29.1948 +  in
 29.1949 +    thy''
 29.1950 +  end
 29.1951 +
 29.1952 +fun extend' value_of edges_of key (G, visited) =
 29.1953 +  let
 29.1954 +    val (G', v) = case try (Graph.get_node G) key of
 29.1955 +        SOME v => (G, v)
 29.1956 +      | NONE => (Graph.new_node (key, value_of key) G, value_of key)
 29.1957 +    val (G'', visited') = fold (extend' value_of edges_of) (edges_of (key, v) \\ visited)
 29.1958 +      (G', key :: visited) 
 29.1959 +  in
 29.1960 +    (fold (Graph.add_edge o (pair key)) (edges_of (key, v)) G'', visited')
 29.1961 +  end;
 29.1962 +
 29.1963 +fun extend value_of edges_of key G = fst (extend' value_of edges_of key (G, [])) 
 29.1964 +  
 29.1965 +fun gen_add_equations steps names thy =
 29.1966 +  let
 29.1967 +    val thy' = PredData.map (fold (extend (fetch_pred_data thy) (depending_preds_of thy)) names) thy
 29.1968 +      |> Theory.checkpoint;
 29.1969 +    fun strong_conn_of gr keys =
 29.1970 +      Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
 29.1971 +    val scc = strong_conn_of (PredData.get thy') names
 29.1972 +    val thy'' = fold_rev
 29.1973 +      (fn preds => fn thy =>
 29.1974 +        if #are_not_defined steps thy preds then add_equations_of steps preds thy else thy)
 29.1975 +      scc thy' |> Theory.checkpoint
 29.1976 +  in thy'' end
 29.1977 +
 29.1978 +(* different instantiantions of the predicate compiler *)
 29.1979 +
 29.1980 +val add_equations = gen_add_equations
 29.1981 +  {infer_modes = infer_modes false,
 29.1982 +  create_definitions = create_definitions,
 29.1983 +  compile_preds = compile_preds PredicateCompFuns.compfuns mk_fun_of false,
 29.1984 +  prove = prove,
 29.1985 +  are_not_defined = (fn thy => forall (null o modes_of thy)),
 29.1986 +  qname = "equation"}
 29.1987 +
 29.1988 +val add_sizelim_equations = gen_add_equations
 29.1989 +  {infer_modes = infer_modes false,
 29.1990 +  create_definitions = sizelim_create_definitions,
 29.1991 +  compile_preds = compile_preds PredicateCompFuns.compfuns mk_sizelim_fun_of true,
 29.1992 +  prove = prove_by_skip,
 29.1993 +  are_not_defined = (fn thy => fn preds => true), (* TODO *)
 29.1994 +  qname = "sizelim_equation"
 29.1995 +  }
 29.1996 +  
 29.1997 +val add_quickcheck_equations = gen_add_equations
 29.1998 +  {infer_modes = infer_modes_with_generator,
 29.1999 +  create_definitions = rpred_create_definitions,
 29.2000 +  compile_preds = compile_preds RPredCompFuns.compfuns mk_generator_of true,
 29.2001 +  prove = prove_by_skip,
 29.2002 +  are_not_defined = (fn thy => fn preds => true), (* TODO *)
 29.2003 +  qname = "rpred_equation"}
 29.2004 +
 29.2005 +(** user interface **)
 29.2006 +
 29.2007 +(* generation of case rules from user-given introduction rules *)
 29.2008 +
 29.2009 +fun mk_casesrule ctxt nparams introrules =
 29.2010 +  let
 29.2011 +    val intros = map (Logic.unvarify o prop_of) introrules
 29.2012 +    val (pred, (params, args)) = strip_intro_concl nparams (hd intros)
 29.2013 +    val ([propname], ctxt1) = Variable.variant_fixes ["thesis"] ctxt
 29.2014 +    val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT))
 29.2015 +    val (argnames, ctxt2) = Variable.variant_fixes
 29.2016 +      (map (fn i => "a" ^ string_of_int i) (1 upto (length args))) ctxt1
 29.2017 +    val argvs = map2 (curry Free) argnames (map fastype_of args)
 29.2018 +    fun mk_case intro =
 29.2019 +      let
 29.2020 +        val (_, (_, args)) = strip_intro_concl nparams intro
 29.2021 +        val prems = Logic.strip_imp_prems intro
 29.2022 +        val eqprems = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (argvs ~~ args)
 29.2023 +        val frees = (fold o fold_aterms)
 29.2024 +          (fn t as Free _ =>
 29.2025 +              if member (op aconv) params t then I else insert (op aconv) t
 29.2026 +           | _ => I) (args @ prems) []
 29.2027 +      in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) end
 29.2028 +    val assm = HOLogic.mk_Trueprop (list_comb (pred, params @ argvs))
 29.2029 +    val cases = map mk_case intros
 29.2030 +  in Logic.list_implies (assm :: cases, prop) end;
 29.2031 +
 29.2032 +(* code_pred_intro attribute *)
 29.2033 +
 29.2034 +fun attrib f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
 29.2035 +
 29.2036 +val code_pred_intros_attrib = attrib add_intro;
 29.2037 +
 29.2038 +local
 29.2039 +
 29.2040 +(* TODO: make TheoryDataFun to GenericDataFun & remove duplication of local theory and theory *)
 29.2041 +(* TODO: must create state to prove multiple cases *)
 29.2042 +fun generic_code_pred prep_const raw_const lthy =
 29.2043 +  let
 29.2044 +    val thy = ProofContext.theory_of lthy
 29.2045 +    val const = prep_const thy raw_const
 29.2046 +    val lthy' = LocalTheory.theory (PredData.map
 29.2047 +        (extend (fetch_pred_data thy) (depending_preds_of thy) const)) lthy
 29.2048 +      |> LocalTheory.checkpoint
 29.2049 +    val thy' = ProofContext.theory_of lthy'
 29.2050 +    val preds = Graph.all_preds (PredData.get thy') [const] |> filter_out (has_elim thy')
 29.2051 +    fun mk_cases const =
 29.2052 +      let
 29.2053 +        val nparams = nparams_of thy' const
 29.2054 +        val intros = intros_of thy' const
 29.2055 +      in mk_casesrule lthy' nparams intros end  
 29.2056 +    val cases_rules = map mk_cases preds
 29.2057 +    val cases =
 29.2058 +      map (fn case_rule => RuleCases.Case {fixes = [],
 29.2059 +        assumes = [("", Logic.strip_imp_prems case_rule)],
 29.2060 +        binds = [], cases = []}) cases_rules
 29.2061 +    val case_env = map2 (fn p => fn c => (Long_Name.base_name p, SOME c)) preds cases
 29.2062 +    val lthy'' = lthy'
 29.2063 +      |> fold Variable.auto_fixes cases_rules 
 29.2064 +      |> ProofContext.add_cases true case_env
 29.2065 +    fun after_qed thms goal_ctxt =
 29.2066 +      let
 29.2067 +        val global_thms = ProofContext.export goal_ctxt
 29.2068 +          (ProofContext.init (ProofContext.theory_of goal_ctxt)) (map the_single thms)
 29.2069 +      in
 29.2070 +        goal_ctxt |> LocalTheory.theory (fold set_elim global_thms #> add_equations [const])
 29.2071 +      end  
 29.2072 +  in
 29.2073 +    Proof.theorem_i NONE after_qed (map (single o (rpair [])) cases_rules) lthy''
 29.2074 +  end;
 29.2075 +
 29.2076 +structure P = OuterParse
 29.2077 +
 29.2078 +in
 29.2079 +
 29.2080 +val code_pred = generic_code_pred (K I);
 29.2081 +val code_pred_cmd = generic_code_pred Code.read_const
 29.2082 +
 29.2083 +val setup = PredData.put (Graph.empty) #>
 29.2084 +  Attrib.setup @{binding code_pred_intros} (Scan.succeed (attrib add_intro))
 29.2085 +    "adding alternative introduction rules for code generation of inductive predicates"
 29.2086 +(*  Attrib.setup @{binding code_ind_cases} (Scan.succeed add_elim_attrib)
 29.2087 +    "adding alternative elimination rules for code generation of inductive predicates";
 29.2088 +    *)
 29.2089 +  (*FIXME name discrepancy in attribs and ML code*)
 29.2090 +  (*FIXME intros should be better named intro*)
 29.2091 +  (*FIXME why distinguished attribute for cases?*)
 29.2092 +
 29.2093 +val _ = OuterSyntax.local_theory_to_proof "code_pred"
 29.2094 +  "prove equations for predicate specified by intro/elim rules"
 29.2095 +  OuterKeyword.thy_goal (P.term_group >> code_pred_cmd)
 29.2096 +
 29.2097 +end
 29.2098 +
 29.2099 +(*FIXME
 29.2100 +- Naming of auxiliary rules necessary?
 29.2101 +- add default code equations P x y z = P_i_i_i x y z
 29.2102 +*)
 29.2103 +
 29.2104 +(* transformation for code generation *)
 29.2105 +
 29.2106 +val eval_ref = ref (NONE : (unit -> term Predicate.pred) option);
 29.2107 +
 29.2108 +(*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
 29.2109 +fun analyze_compr thy t_compr =
 29.2110 +  let
 29.2111 +    val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
 29.2112 +      | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term_global thy t_compr);
 29.2113 +    val (body, Ts, fp) = HOLogic.strip_psplits split;
 29.2114 +    val (pred as Const (name, T), all_args) = strip_comb body;
 29.2115 +    val (params, args) = chop (nparams_of thy name) all_args;
 29.2116 +    val user_mode = map_filter I (map_index
 29.2117 +      (fn (i, t) => case t of Bound j => if j < length Ts then NONE
 29.2118 +        else SOME (i+1) | _ => SOME (i+1)) args); (*FIXME dangling bounds should not occur*)
 29.2119 +    val modes = filter (fn Mode (_, is, _) => is = user_mode)
 29.2120 +      (modes_of_term (all_modes_of thy) (list_comb (pred, params)));
 29.2121 +    val m = case modes
 29.2122 +     of [] => error ("No mode possible for comprehension "
 29.2123 +                ^ Syntax.string_of_term_global thy t_compr)
 29.2124 +      | [m] => m
 29.2125 +      | m :: _ :: _ => (warning ("Multiple modes possible for comprehension "
 29.2126 +                ^ Syntax.string_of_term_global thy t_compr); m);
 29.2127 +    val (inargs, outargs) = split_smode user_mode args;
 29.2128 +    val t_pred = list_comb (compile_expr NONE thy (m, list_comb (pred, params)), inargs);
 29.2129 +    val t_eval = if null outargs then t_pred else let
 29.2130 +        val outargs_bounds = map (fn Bound i => i) outargs;
 29.2131 +        val outargsTs = map (nth Ts) outargs_bounds;
 29.2132 +        val T_pred = HOLogic.mk_tupleT outargsTs;
 29.2133 +        val T_compr = HOLogic.mk_ptupleT fp Ts;
 29.2134 +        val arrange_bounds = map_index I outargs_bounds
 29.2135 +          |> sort (prod_ord (K EQUAL) int_ord)
 29.2136 +          |> map fst;
 29.2137 +        val arrange = funpow (length outargs_bounds - 1) HOLogic.mk_split
 29.2138 +          (Term.list_abs (map (pair "") outargsTs,
 29.2139 +            HOLogic.mk_ptuple fp T_compr (map Bound arrange_bounds)))
 29.2140 +      in mk_map PredicateCompFuns.compfuns T_pred T_compr arrange t_pred end
 29.2141 +  in t_eval end;
 29.2142 +
 29.2143 +fun eval thy t_compr =
 29.2144 +  let
 29.2145 +    val t = analyze_compr thy t_compr;
 29.2146 +    val T = dest_predT PredicateCompFuns.compfuns (fastype_of t);
 29.2147 +    val t' = mk_map PredicateCompFuns.compfuns T HOLogic.termT (HOLogic.term_of_const T) t;
 29.2148 +  in (T, Code_ML.eval NONE ("Predicate_Compile.eval_ref", eval_ref) Predicate.map thy t' []) end;
 29.2149 +
 29.2150 +fun values ctxt k t_compr =
 29.2151 +  let
 29.2152 +    val thy = ProofContext.theory_of ctxt;
 29.2153 +    val (T, t) = eval thy t_compr;
 29.2154 +    val setT = HOLogic.mk_setT T;
 29.2155 +    val (ts, _) = Predicate.yieldn k t;
 29.2156 +    val elemsT = HOLogic.mk_set T ts;
 29.2157 +  in if k = ~1 orelse length ts < k then elemsT
 29.2158 +    else Const (@{const_name Lattices.sup}, setT --> setT --> setT) $ elemsT $ t_compr
 29.2159 +  end;
 29.2160 +
 29.2161 +fun values_cmd modes k raw_t state =
 29.2162 +  let
 29.2163 +    val ctxt = Toplevel.context_of state;
 29.2164 +    val t = Syntax.read_term ctxt raw_t;
 29.2165 +    val t' = values ctxt k t;
 29.2166 +    val ty' = Term.type_of t';
 29.2167 +    val ctxt' = Variable.auto_fixes t' ctxt;
 29.2168 +    val p = PrintMode.with_modes modes (fn () =>
 29.2169 +      Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
 29.2170 +        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
 29.2171 +  in Pretty.writeln p end;
 29.2172 +
 29.2173 +local structure P = OuterParse in
 29.2174 +
 29.2175 +val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
 29.2176 +
 29.2177 +val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag
 29.2178 +  (opt_modes -- Scan.optional P.nat ~1 -- P.term
 29.2179 +    >> (fn ((modes, k), t) => Toplevel.no_timing o Toplevel.keep
 29.2180 +        (values_cmd modes k t)));
 29.2181 +
 29.2182 +end;
 29.2183 +
 29.2184 +end;
 29.2185 +