--- a/ProgTutorial/Package/Ind_Code.thy	Thu Mar 19 23:21:26 2009 +0100
+++ b/ProgTutorial/Package/Ind_Code.thy	Sat Mar 21 12:35:03 2009 +0100
@@ -2,9 +2,24 @@
 imports "../Base" "../FirstSteps" Simple_Inductive_Package Ind_Prelims
 begin
 
+datatype trm =
+  Var "string"
+| App "trm" "trm"
+| Lam "string" "trm"
+
+simple_inductive 
+  fresh :: "string \<Rightarrow> trm \<Rightarrow> bool" ("_ \<sharp> _" [100,100] 100)
+where
+  "a\<noteq>b \<Longrightarrow> a\<sharp>Var b"
+| "\<lbrakk>a\<sharp>t; a\<sharp>s\<rbrakk> \<Longrightarrow> a\<sharp>App t s"
+| "a\<sharp>Lam a t"
+| "\<lbrakk>a\<noteq>b; a\<sharp>t\<rbrakk> \<Longrightarrow> a\<sharp>Lam b t"  
+
+
 section {* Code *}
 
 text {*
+  
   @{text [display] "rule ::= \<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}
 
   @{text [display] "orule ::= \<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"}
@@ -533,13 +548,13 @@
 ML {* Logic.strip_assums_hyp *}
 
 ML {*
-fun chop_print_tac ctxt thm =
+fun chop_print_tac m n ctxt thm =
 let
   val [trm] = prems_of thm
   val params = map fst (Logic.strip_params trm)
   val prems  = Logic.strip_assums_hyp trm
-  val (prems1, prems2) = chop (length prems - 3) prems;
-  val (params1, params2) = chop (length params - 2) params;
+  val (prems1, prems2) = chop (length prems - m) prems;
+  val (params1, params2) = chop (length params - n) params;
   val _ = warning (Syntax.string_of_term ctxt trm)
   val _ = warning (commas params)
   val _ = warning (commas (map (Syntax.string_of_term ctxt) prems))
@@ -551,15 +566,58 @@
 end
 *}
 
+ML {* METAHYPS *}
+
+ML {*
+fun chop_print_tac2 ctxt prems =
+let
+  val _ = warning (commas (map (str_of_thm ctxt) prems))
+in
+   all_tac
+end
+*}
 
 lemma intro1:
   shows "\<And>m. odd m \<Longrightarrow> even (Suc m)"
 apply(tactic {* ObjectLogic.rulify_tac 1 *})
 apply(tactic {* rewrite_goals_tac [@{thm even_def}, @{thm odd_def}] *})
 apply(tactic {* REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1) *})
-apply(tactic {* chop_print_tac @{context} *})
+apply(tactic {* chop_print_tac 3 2 @{context} *})
 oops
 
+ML {*
+fun SUBPROOF_test tac ctxt =
+  SUBPROOF (fn {params, prems, context,...} =>
+    let
+      val thy = ProofContext.theory_of context
+    in 
+      tac (params, prems, context) 
+      THEN  Method.insert_tac prems 1
+      THEN  print_tac "SUBPROOF Test"
+      THEN  SkipProof.cheat_tac thy
+    end) ctxt 1
+*}
+
+
+
+
+lemma fresh_App:
+  shows "\<And>a t s. \<lbrakk>a\<sharp>t; a\<sharp>s\<rbrakk> \<Longrightarrow> a\<sharp>App t s"
+apply(tactic {* ObjectLogic.rulify_tac 1 *})
+apply(tactic {* rewrite_goals_tac [@{thm fresh_def}] *})
+apply(tactic {* REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1) *})
+oops
+(*
+apply(tactic {* SUBPROOF_test 
+  (fn (params, prems, ctxt) =>
+   let 
+     val (prems1, prems2) = chop (length prems - 4) prems;
+     val (params1, params2) = chop (length params - 1) params;
+   in
+     rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 2))) 1
+   end) @{context} *})
+*)
+
 ML{*fun subproof2 prem params2 prems2 =  
  SUBPROOF (fn {prems, ...} =>
    let
@@ -717,6 +775,7 @@
   the rules
   \item say that the induction principle is weaker (weaker than
   what the standard inductive package generates)
+  \item say that no conformity test is done
   \end{itemize}
   
 *}