skip coinduction proofs for indirect-recursive domain definitions
authorhuffman
Fri Mar 05 15:25:59 2010 -0800 (2010-03-05)
changeset 3559920670f5564e9
parent 35597 e4331b99b03f
child 35600 94bd51880746
skip coinduction proofs for indirect-recursive domain definitions
src/HOLCF/Tools/Domain/domain_theorems.ML
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Mar 05 14:50:37 2010 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Mar 05 15:25:59 2010 -0800
     1.3 @@ -440,7 +440,7 @@
     1.4  fun prove_coinduction
     1.5      (comp_dnam, eqs : eq list)
     1.6      (take_lemmas : thm list)
     1.7 -    (thy : theory) : thm * theory =
     1.8 +    (thy : theory) : theory =
     1.9  let
    1.10  
    1.11  val dnames = map (fst o fst) eqs;
    1.12 @@ -580,9 +580,10 @@
    1.13      in pg [] goal (K tacs) end;
    1.14  end; (* local *)
    1.15  
    1.16 -in
    1.17 -  (coind, thy)
    1.18 -end;
    1.19 +in thy |> Sign.add_path comp_dnam
    1.20 +       |> snd o PureThy.add_thmss [((Binding.name "coind", [coind]), [])]
    1.21 +       |> Sign.parent_path
    1.22 +end; (* let *)
    1.23  
    1.24  fun comp_theorems (comp_dnam, eqs: eq list) thy =
    1.25  let
    1.26 @@ -591,8 +592,6 @@
    1.27  val dnames = map (fst o fst) eqs;
    1.28  val comp_dname = Sign.full_bname thy comp_dnam;
    1.29  
    1.30 -val _ = message ("Proving induction properties of domain "^comp_dname^" ...");
    1.31 -
    1.32  (* ----- getting the composite axiom and definitions ------------------------ *)
    1.33  
    1.34  (* Test for indirect recursion *)
    1.35 @@ -603,9 +602,10 @@
    1.36    fun indirect_eq (_, cons) = exists indirect_con cons;
    1.37  in
    1.38    val is_indirect = exists indirect_eq eqs;
    1.39 -  val _ = if is_indirect
    1.40 -          then message "Definition uses indirect recursion."
    1.41 -          else ();
    1.42 +  val _ =
    1.43 +      if is_indirect
    1.44 +      then message "Indirect recursion detected, skipping proofs of (co)induction rules"
    1.45 +      else message ("Proving induction properties of domain "^comp_dname^" ...");
    1.46  end;
    1.47  
    1.48  (* theorems about take *)
    1.49 @@ -638,13 +638,14 @@
    1.50      if is_indirect then thy else
    1.51      prove_induction (comp_dnam, eqs) take_lemmas axs_reach take_rews thy;
    1.52  
    1.53 -val (coind, thy) = prove_coinduction (comp_dnam, eqs) take_lemmas thy;
    1.54 +val thy =
    1.55 +    if is_indirect then thy else
    1.56 +    prove_coinduction (comp_dnam, eqs) take_lemmas thy;
    1.57  
    1.58  in thy |> Sign.add_path comp_dnam
    1.59         |> snd o PureThy.add_thmss [
    1.60             ((Binding.name "take_lemmas", take_lemmas ), []),
    1.61 -           ((Binding.name "reach"      , axs_reach   ), []),
    1.62 -           ((Binding.name "coind"      , [coind]     ), [])]
    1.63 +           ((Binding.name "reach"      , axs_reach   ), [])]
    1.64         |> Sign.parent_path |> pair take_rews
    1.65  end; (* let *)
    1.66  end; (* struct *)