author huffman Fri Mar 05 15:25:59 2010 -0800 (2010-03-05) changeset 35599 20670f5564e9 parent 35597 e4331b99b03f child 35600 94bd51880746
skip coinduction proofs for indirect-recursive domain definitions
```     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 *)
```