src/HOL/Statespace/DistinctTreeProver.thy
changeset 38838 62f6ba39b3d4
parent 35408 b48ab741683b
child 39557 fe5722fce758
     1.1 --- a/src/HOL/Statespace/DistinctTreeProver.thy	Fri Aug 27 22:09:51 2010 +0200
     1.2 +++ b/src/HOL/Statespace/DistinctTreeProver.thy	Fri Aug 27 22:30:25 2010 +0200
     1.3 @@ -32,17 +32,18 @@
     1.4  subsection {* Distinctness of Nodes *}
     1.5  
     1.6  
     1.7 -consts set_of:: "'a tree \<Rightarrow> 'a set"
     1.8 -primrec 
     1.9 -"set_of Tip = {}"
    1.10 -"set_of (Node l x d r) = (if d then {} else {x}) \<union> set_of l \<union> set_of r"
    1.11 +primrec set_of :: "'a tree \<Rightarrow> 'a set"
    1.12 +where
    1.13 +  "set_of Tip = {}"
    1.14 +| "set_of (Node l x d r) = (if d then {} else {x}) \<union> set_of l \<union> set_of r"
    1.15  
    1.16 -consts all_distinct:: "'a tree \<Rightarrow> bool"
    1.17 -primrec
    1.18 -"all_distinct Tip = True"
    1.19 -"all_distinct (Node l x d r) = ((d \<or> (x \<notin> set_of l \<and> x \<notin> set_of r)) \<and> 
    1.20 -                               set_of l \<inter> set_of r = {} \<and>
    1.21 -                               all_distinct l \<and> all_distinct r)"
    1.22 +primrec all_distinct :: "'a tree \<Rightarrow> bool"
    1.23 +where
    1.24 +  "all_distinct Tip = True"
    1.25 +| "all_distinct (Node l x d r) =
    1.26 +    ((d \<or> (x \<notin> set_of l \<and> x \<notin> set_of r)) \<and> 
    1.27 +      set_of l \<inter> set_of r = {} \<and>
    1.28 +      all_distinct l \<and> all_distinct r)"
    1.29  
    1.30  text {* Given a binary tree @{term "t"} for which 
    1.31  @{const all_distinct} holds, given two different nodes contained in the tree,
    1.32 @@ -99,19 +100,19 @@
    1.33  *}
    1.34  
    1.35  
    1.36 -consts "delete" :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree option"
    1.37 -primrec
    1.38 -"delete x Tip = None"
    1.39 -"delete x (Node l y d r) = (case delete x l of
    1.40 -                              Some l' \<Rightarrow>
    1.41 -                               (case delete x r of 
    1.42 -                                  Some r' \<Rightarrow> Some (Node l' y (d \<or> (x=y)) r')
    1.43 -                                | None \<Rightarrow> Some (Node l' y (d \<or> (x=y)) r))
    1.44 -                             | None \<Rightarrow>
    1.45 -                                (case (delete x r) of 
    1.46 -                                   Some r' \<Rightarrow> Some (Node l y (d \<or> (x=y)) r')
    1.47 -                                 | None \<Rightarrow> if x=y \<and> \<not>d then Some (Node l y True r)
    1.48 -                                           else None))"
    1.49 +primrec delete :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree option"
    1.50 +where
    1.51 +  "delete x Tip = None"
    1.52 +| "delete x (Node l y d r) = (case delete x l of
    1.53 +                                Some l' \<Rightarrow>
    1.54 +                                 (case delete x r of 
    1.55 +                                    Some r' \<Rightarrow> Some (Node l' y (d \<or> (x=y)) r')
    1.56 +                                  | None \<Rightarrow> Some (Node l' y (d \<or> (x=y)) r))
    1.57 +                               | None \<Rightarrow>
    1.58 +                                  (case (delete x r) of 
    1.59 +                                     Some r' \<Rightarrow> Some (Node l y (d \<or> (x=y)) r')
    1.60 +                                   | None \<Rightarrow> if x=y \<and> \<not>d then Some (Node l y True r)
    1.61 +                                             else None))"
    1.62  
    1.63  
    1.64  lemma delete_Some_set_of: "\<And>t'. delete x t = Some t' \<Longrightarrow> set_of t' \<subseteq> set_of t"
    1.65 @@ -293,15 +294,15 @@
    1.66  qed
    1.67  
    1.68  
    1.69 -consts "subtract" :: "'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree option"
    1.70 -primrec
    1.71 -"subtract Tip t = Some t"
    1.72 -"subtract (Node l x b r) t = 
    1.73 -   (case delete x t of
    1.74 -      Some t' \<Rightarrow> (case subtract l t' of 
    1.75 -                   Some t'' \<Rightarrow> subtract r t''
    1.76 -                  | None \<Rightarrow> None)
    1.77 -    | None \<Rightarrow> None)"
    1.78 +primrec subtract :: "'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree option"
    1.79 +where
    1.80 +  "subtract Tip t = Some t"
    1.81 +| "subtract (Node l x b r) t =
    1.82 +     (case delete x t of
    1.83 +        Some t' \<Rightarrow> (case subtract l t' of 
    1.84 +                     Some t'' \<Rightarrow> subtract r t''
    1.85 +                    | None \<Rightarrow> None)
    1.86 +       | None \<Rightarrow> None)"
    1.87  
    1.88  lemma subtract_Some_set_of_res: 
    1.89    "\<And>t\<^isub>2 t. subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> set_of t \<subseteq> set_of t\<^isub>2"