# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1306797442 -3600
# Node ID 32979078bfe9ed6968292fb88449b16cb615ce92
# Parent  036a19936febb47f7eac3e5299ce779e5853601d
functions involving if and case do not throw exceptions anymore; but eqvt_at assumption has now a precondition

diff -r 036a19936feb -r 32979078bfe9 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Thu May 26 06:36:29 2011 +0200
+++ b/Nominal/Ex/Lambda.thy	Tue May 31 00:17:22 2011 +0100
@@ -3,26 +3,6 @@
 begin
 
 
-(* inductive_cases do not simplify with simple equations *)
-atom_decl var
-nominal_datatype expr =
-  eCnst nat
-| eVar nat
-
-inductive 
-  eval :: "expr \<Rightarrow> nat list \<Rightarrow> bool"
-where
-  evCnst1: "eval (eCnst c) [2,1]"
-| evCnst2: "eval (eCnst b) [1,2]"
-| evVar: "eval (eVar n) [1]"
-
-inductive_cases 
-  evInv_Cnst: "eval (eCnst c) [1,2]"
-
-thm evInv_Cnst
-
-
-
 atom_decl name
 
 nominal_datatype lam =
@@ -515,7 +495,59 @@
 apply(simp_all add: permute_pure)
 done
 
-(*
+
+text {* tests of functions containing if and case *}
+
+consts P :: "lam \<Rightarrow> bool"
+
+nominal_primrec  
+  A :: "lam => lam"
+where  
+  "A (App M N) = (if (True \<or> P M) then (A M) else (A N))"
+| "A (Var x) = (Var x)" 
+| "A (App M N) = (if True then M else A N)"
+oops
+
+nominal_primrec  
+  C :: "lam => lam"
+where  
+  "C (App M N) = (case (True \<or> P M) of True \<Rightarrow> (A M) | False \<Rightarrow> (A N))"
+| "C (Var x) = (Var x)" 
+| "C (App M N) = (if True then M else C N)"
+oops
+
+nominal_primrec
+  map_term :: "(lam \<Rightarrow> lam) \<Rightarrow> lam \<Rightarrow> lam"
+where
+  "map_term f (Var x) = f (Var x)"
+| "map_term f (App t1 t2) = App (f t1) (f t2)"
+| "map_term f (Lam [x].t) = Lam [x].(f t)"
+oops
+
+nominal_primrec  
+  A :: "lam => lam"
+where  
+  "A (Lam [x].M) = (Lam [x].M)"
+| "A (Var x) = (Var x)"
+| "A (App M N) = (if True then M else A N)"
+oops
+
+nominal_primrec  
+  B :: "lam => lam"
+where  
+  "B (Lam [x].M) = (Lam [x].M)"
+| "B (Var x) = (Var x)"
+| "B (App M N) = (if True then M else (B N))"
+unfolding eqvt_def
+unfolding B_graph_def
+apply(perm_simp)
+apply(rule allI)
+apply(rule refl)
+oops
+
+text {* not working yet *}
+
+(* not working yet
 nominal_primrec
   trans :: "lam \<Rightarrow> atom list \<Rightarrow> db option"
 where
@@ -524,6 +556,30 @@
 | "trans (Lam [x].t) xs = (trans t (atom x # xs) \<guillemotright>= (\<lambda>db. Some (DBLam db)))"
 *)
 
+(* not working yet
+nominal_primrec
+  CPS :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam"
+where
+  "CPS (Var x) k = Var x"
+| "CPS (App M N) k = CPS M (\<lambda>m. CPS N (\<lambda>n. n))"
+*)
+
+
+(* function tests *)
+
+(* similar problem with function package *)
+function
+  f :: "int list \<Rightarrow> int"
+where
+  "f [] = 0"
+| "f [e] = e"
+| "f (l @ m) = f l + f m"
+apply(simp_all)
+oops
+
+
+
+
 
 
 end
diff -r 036a19936feb -r 32979078bfe9 Nominal/nominal_function.ML
--- a/Nominal/nominal_function.ML	Thu May 26 06:36:29 2011 +0200
+++ b/Nominal/nominal_function.ML	Tue May 31 00:17:22 2011 +0100
@@ -140,7 +140,8 @@
     val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
     val fixes = map (apfst (apfst Binding.name_of)) fixes0;
     val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0;
-    val (eqs, post, sort_cont, cnames) =  empty_preproc nominal_check_defs config ctxt' fixes spec (* nominal *)
+    val (eqs, post, sort_cont, cnames) =  
+      empty_preproc nominal_check_defs config ctxt' fixes spec (* nominal *)
 
     val defname = mk_defname fixes
     val FunctionConfig {partials, default, ...} = config
diff -r 036a19936feb -r 32979078bfe9 Nominal/nominal_function_core.ML
--- a/Nominal/nominal_function_core.ML	Thu May 26 06:36:29 2011 +0200
+++ b/Nominal/nominal_function_core.ML	Tue May 31 00:17:22 2011 +0100
@@ -123,39 +123,34 @@
     |> HOLogic.mk_Trueprop
   end
 
-(* nominal *)
-fun find_calls2 f t = 
-  let
-    fun aux (g $ arg) = aux g #> aux arg #> (if f = g then cons ((g, arg)) else I)
-      | aux (Abs (_, _, t)) = aux t 
-      | aux _ = I
-  in
-    aux t []
-  end 
-
-
+fun mk_eqvt_proof_obligation qs fvar (assms, arg) = 
+  mk_eqvt_at (fvar, arg)
+  |> curry Logic.list_implies assms
+  |> curry Term.list_abs_free qs
+  |> strip_abs_body
 
 (** building proof obligations *)
 
-fun mk_compat_proof_obligations domT ranT fvar f glrs =
+fun mk_compat_proof_obligations lthy domT ranT fvar f RCss glrs =
   let
-    fun mk_impl ((qs, gs, lhs, rhs), (qs', gs', lhs', rhs')) =
+    fun mk_impl (((qs, gs, lhs, rhs), RCs), ((qs', gs', lhs', rhs'), _)) =
       let
         val shift = incr_boundvars (length qs')
-
-        val RCs_rhs  = find_calls2 fvar rhs (* nominal : FIXME : recursive calls should be passed here *)
+     
+        val rc_args = map (fn (_, thms, args) => (map prop_of thms, args)) RCs
+        val tt = map (shift o mk_eqvt_proof_obligation qs fvar) rc_args
       in
         Logic.mk_implies
           (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'),
             HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs'))
         |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
-        |> fold_rev (curry Logic.mk_implies) (map (shift o mk_eqvt_at) RCs_rhs) (* nominal *)
+        |> fold_rev (curry Logic.mk_implies) tt (* nominal *)
         |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs')
         |> curry abstract_over fvar
         |> curry subst_bound f
       end
   in
-    map mk_impl (unordered_pairs glrs)
+    map mk_impl (unordered_pairs (glrs ~~ RCss))
   end
 
 
@@ -268,8 +263,8 @@
 (* if j < i, then turn around *)
 fun get_compat_thm thy cts eqvtsi eqvtsj i j ctxi ctxj =
   let
-    val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
-    val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
+    val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,case_hyp=case_hypi,...} = ctxi
+    val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,case_hyp=case_hypj,...} = ctxj
 
     val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))
   in if j < i then
@@ -278,7 +273,7 @@
     in
       compat         (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
       |> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
-      |> fold Thm.elim_implies (rev eqvtsj) (* nominal *)
+      |> fold Thm.elim_implies eqvtsj (* nominal *)
       |> fold Thm.elim_implies agsj
       |> fold Thm.elim_implies agsi
       |> Thm.elim_implies ((Thm.assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
@@ -289,7 +284,7 @@
     in
       compat        (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
       |> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
-      |> fold Thm.elim_implies (rev eqvtsi)  (* nominal *)
+      |> fold Thm.elim_implies eqvtsi  (* nominal *)
       |> fold Thm.elim_implies agsi
       |> fold Thm.elim_implies agsj
       |> Thm.elim_implies (Thm.assume lhsi_eq_lhsj)
@@ -332,7 +327,7 @@
 fun mk_eqvt_lemma thy ih_eqvt clause =
   let
     val ClauseInfo {cdata=ClauseContext {cqs, ags, case_hyp, ...}, RCs, ...} = clause
-
+     
     local open Conv in
       val ih_conv = arg1_conv o arg_conv o arg_conv
     end
@@ -420,7 +415,7 @@
         (llRI RS ih_intro_case)
         |> fold_rev (Thm.implies_intr o cprop_of) CCas
         |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
-
+ 
     val existence = fold (curry op COMP o prep_RC) RCs lGI
 
     val P = cterm_of thy (mk_eq (y, rhsC))
@@ -431,7 +426,7 @@
 
     fun elim_implies_eta A AB =
       Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single
-
+ 
     val uniqueness = G_cases
       |> Thm.forall_elim (cterm_of thy lhs)
       |> Thm.forall_elim (cterm_of thy y)
@@ -963,7 +958,7 @@
       mk_completeness globals clauses abstract_qglrs |> cert |> Thm.assume
 
     val compat =
-      mk_compat_proof_obligations domT ranT fvar f abstract_qglrs 
+      mk_compat_proof_obligations lthy domT ranT fvar f RCss abstract_qglrs 
       |> map (cert #> Thm.assume)
 
     val G_eqvt = mk_eqvt G |> cert |> Thm.assume