# HG changeset patch
# User bulwahn
# Date 1253715612 -7200
# Node ID 462b1dd67a58ece27415bec063dc6deddca81842
# Parent  b2de450075379800c8cfc5b6c2a69b651f95ac63
added context free grammar example; removed dead code; adapted to work without quick and dirty mode; fixed typo

diff -r b2de45007537 -r 462b1dd67a58 src/HOL/Tools/Predicate_Compile/pred_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Wed Sep 23 16:20:12 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Wed Sep 23 16:20:12 2009 +0200
@@ -108,7 +108,7 @@
       in ((Free (x, T), HOLogic.mk_ptuple paths T (map Free xTs)), nctxt') end
     val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt 
     val t' = Pattern.rewrite_term thy rewr [] t
-    val tac = SkipProof.cheat_tac thy
+    val tac = setmp quick_and_dirty true (SkipProof.cheat_tac thy)
     val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn {...} => tac)
     val th''' = LocalDefs.unfold ctxt [@{thm split_conv}] th''
   in
diff -r b2de45007537 -r 462b1dd67a58 src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML	Wed Sep 23 16:20:12 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML	Wed Sep 23 16:20:12 2009 +0200
@@ -56,7 +56,7 @@
     val ((_, intros), ctxt') = Variable.import true intros ctxt
     val (intros', (local_defs, thy')) = (fold_map o fold_map_atoms)
       (flatten constname) (map prop_of intros) ([], thy)
-    val tac = fn {...} => SkipProof.cheat_tac thy'
+    val tac = fn {...} => setmp quick_and_dirty true (SkipProof.cheat_tac thy')
     val intros'' = map (fn t => Goal.prove ctxt' [] [] t tac) intros'
       |> Variable.export ctxt' ctxt
   in
diff -r b2de45007537 -r 462b1dd67a58 src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Sep 23 16:20:12 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Sep 23 16:20:12 2009 +0200
@@ -36,7 +36,7 @@
     val _ = tracing ("intross: " ^ commas (map (Display.string_of_thm_global thy'') (flat intross)))
     val _ = priority "Replacing functions in introrules..."
     val intross' = burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross
-    val intross'' = burrow (maps remove_pointless_clauses) intross
+    val intross'' = burrow (maps remove_pointless_clauses) intross'
     val thy''' = fold Predicate_Compile_Core.register_intros intross'' thy''
   in
     thy'''
diff -r b2de45007537 -r 462b1dd67a58 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Sep 23 16:20:12 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Sep 23 16:20:12 2009 +0200
@@ -1623,24 +1623,11 @@
 							 val xout = Free (name_out, HOLogic.mk_tupleT Touts)
 							 val xarg = mk_arg xin xout pis T
 						 in (((if null Tins then [] else [xin], if null Touts then [] else [xout]), xarg), name_in :: name_out :: names) end
-						(* HOLogic.strip_tupleT T of
-						[] => 
-							in (Free (vname, T), vname :: names) end
-					| [_] => let val vname = Name.variant names ("x" ^ string_of_int (length Ts1' + i))
-							in (Free (vname, T), vname :: names) end
-					| Ts =>
-						let
-							val vnames = Name.variant_list names
-								(map (fn j => "x" ^ string_of_int (length Ts1' + i) ^ "p" ^ string_of_int j)
-									(1 upto (length Ts)))
-						 in (HOLogic.mk_tuple (map Free (vnames ~~ Ts)), vnames @ names) end *)
-				end
+						 end
    	  val (xinoutargs, names) = fold_map mk_vars ((1 upto (length Ts2)) ~~ Ts2) param_names
       val (xinout, xargs) = split_list xinoutargs
 			val (xins, xouts) = pairself flat (split_list xinout)
-			(*val (xins, xouts) = split_smode is xargs*)
 			val (xparams', names') = fold_map mk_Eval_of ((xparams ~~ Ts1) ~~ iss) names
-			val _ = Output.tracing ("xargs:" ^ commas (map (Syntax.string_of_term_global thy) xargs))
       fun mk_split_lambda [] t = lambda (Free (Name.variant names' "x", HOLogic.unitT)) t
         | mk_split_lambda [x] t = lambda x t
         | mk_split_lambda xs t =
@@ -2107,7 +2094,7 @@
     (join_preds_modes moded_clauses compiled_terms)
 
 fun prove_by_skip thy _ _ _ _ compiled_terms =
-  map_preds_modes (fn pred => fn mode => fn t => Drule.standard (SkipProof.make_thm thy t))
+  map_preds_modes (fn pred => fn mode => fn t => Drule.standard (setmp quick_and_dirty true (SkipProof.make_thm thy) t))
     compiled_terms
     
 fun prepare_intrs thy prednames =
diff -r b2de45007537 -r 462b1dd67a58 src/HOL/ex/Predicate_Compile_ex.thy
--- a/src/HOL/ex/Predicate_Compile_ex.thy	Wed Sep 23 16:20:12 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Wed Sep 23 16:20:12 2009 +0200
@@ -252,4 +252,26 @@
 thm Domain.equation
 
 
+section {* Context Free Grammar *}
+
+datatype alphabet = a | b
+
+inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where
+  "[] \<in> S\<^isub>1"
+| "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
+| "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
+| "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
+| "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
+| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
+
+code_pred (inductify_all) S\<^isub>1p .
+
+thm S\<^isub>1p.equation
+
+code_pred (inductify_all) (rpred) S\<^isub>1p .
+
+thm S\<^isub>1p.rpred_equation
+
+
+
 end
\ No newline at end of file