Improved proof efficiency of chantyperep instantiation using meson.

Author: simondfoster

Channel_Type.ML

@@ -77,8 +77,8 @@ fun chantyperep_instance name raw_chans thy =
   open Syntax; open HOLogic; open Global_Theory;
   val ty = Syntax.read_typ (Named_Target.theory_init thy) name;
   val tyco = fst (dest_Type ty);
-  val disc_intro_thms = if length raw_chans = 1 then [] else get_thms thy (tyco ^ ".disc");
-  val disc_elim_thms = if length raw_chans = 1 then [] else get_thms thy (tyco ^ ".exhaust_disc");
+  val disc_thms = if length raw_chans = 1 then [] else get_thms thy (tyco ^ ".disc") @ get_thms thy (tyco ^ ".exhaust_disc") 
+                  @ (if length raw_chans = 2 then [] else get_thms thy (tyco ^ ".distinct_disc"));
   val ctx0 = Class.instantiation ([tyco], [], \<^sort>\<open>chantyperep\<close>) thy;
   val chans = map (fn (n, t) => (n, mk_typerep (read_typ ctx0 t))) raw_chans
   val lhs = \<^Const>\<open>chantyperep ty\<close> $ Free ("T", Term.itselfT ty);
@@ -87,10 +87,9 @@ fun chantyperep_instance name raw_chans thy =
   val eq = check_term ctx1 (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)));
   val (_, ctx2) = Specification.definition NONE [] [] ((Binding.empty, @{attributes [chantyperep_defs]}), eq) ctx1;
   val ctx3 = Local_Theory.end_nested ctx2;
-  val ctx4 = fold (Context.proof_map o Named_Theorems.add_thm "Channel_Type.datatype_disc_intros") disc_intro_thms ctx3;
-  val ctx5 = fold (Context.proof_map o Named_Theorems.add_thm "Channel_Type.datatype_disc_elims") disc_elim_thms ctx4;
+  val ctx4 = fold (Context.proof_map o Named_Theorems.add_thm "Channel_Type.datatype_disc_thms") disc_thms ctx3;
   in
-  Class.prove_instantiation_exit (fn _ => NO_CONTEXT_TACTIC ctx5 (Method_Closure.apply_method ctx5 @{method chantyperep_inst} [] [] [] ctx5 [])) ctx5
+  Class.prove_instantiation_exit (fn _ => NO_CONTEXT_TACTIC ctx4 (Method_Closure.apply_method ctx4 @{method chantyperep_inst} [] [] [] ctx4 [])) ctx4
   end;
 
 fun compile_chantype (name, chans) thy =
@@ -100,7 +99,6 @@ fun compile_chantype (name, chans) thy =
     val ctx = Named_Target.theory_init thy;
     val ctrs = map (fn (n, t) => (((Binding.empty, Binding.name (n ^ ctor_suffix)), [(Binding.empty, t)]), Mixfix.NoSyn)) chans 
     val pnames = map fst chans
-    val tyreps = map (mk_typerep o read_typ ctx o snd) chans
     val thypfx = 
       case (Named_Target.locale_of ctx) of
         SOME loc => loc ^ "." |

Channel_Type.thy

@@ -70,11 +70,10 @@ definition set_chan :: "'a chantyperep \<Rightarrow> String.literal \<Rightarrow
 definition set_chans :: "'a chantyperep \<Rightarrow> String.literal set \<Rightarrow> 'a set" where
 "set_chans ct ns = \<Union> (set_chan ct ` ns)" 
 
-named_theorems datatype_disc_elims
-named_theorems datatype_disc_intros 
+named_theorems datatype_disc_thms 
 named_theorems chantyperep_defs
 
-method wf_chantyperep = (force intro: datatype_disc_intros simp add: comp_def wf_chantyperep_def chantyperep_defs)
+method wf_chantyperep = (simp add: comp_def wf_chantyperep_def chantyperep_defs, (meson datatype_disc_thms)?)
 
 lemma foldr_disj_one_True: "foldr (\<or>) Ps False \<Longrightarrow> (\<exists> P\<in>set Ps. P)"
   by (induct Ps, auto)
@@ -102,9 +101,7 @@ class chantyperep =
   fixes chantyperep :: "'a itself \<Rightarrow> 'a raw_chantyperep"
   assumes wf_chantyperep: "wf_chantyperep (chantyperep TYPE('a))"
 
-(* The following method works, but relies too much on auto. It should be optimised *)
-
-method chantyperep_inst = (rule chantyperep_class.intro, (intro_classes)[1], rule_tac class.chantyperep.intro, insert datatype_disc_elims, auto intro!:datatype_disc_intros simp add: comp_def wf_chantyperep_def chantyperep_defs)
+method chantyperep_inst = (rule chantyperep_class.intro, (intro_classes)[1], rule_tac class.chantyperep.intro, wf_chantyperep)
 
 syntax "_chantyperep" :: "type \<Rightarrow> logic" ("CHANTYPEREP'(_')")
 translations "CHANTYPEREP('a)" == "CONST chantyperep TYPE('a)"

Channel_Type_Example.thy

@@ -23,4 +23,15 @@ chantype ch_buffer2 =
   outp2 :: nat
   mod2 :: bool
 
+chantype chbig =
+  a1 :: int
+  a2 :: int
+  a3 :: int
+  a4 :: int
+  a5 :: int
+  a6 :: bool
+  a7 :: bool
+  a8 :: unit
+  a9 :: nat
+
 end