theory i131216a__isaU_eq_is_not_assignment
imports Complex_Main (*"../../../iHelp/i"*)
begin
(*SHOWING THAT "=" IS HOL.eq, RATHER THAN PROGRAMMING LANGUAGE ASSIGNMENT*)

(*
You're treating "=" as if it's assignment or definition, such as "val x = 1", but
it's not, it's the application of the function HOL.eq::('a => 'a => bool), which
has been axiomatized to have certain properties, such as substitution.

The expression "f = (%a. a | f a)" is a statement of function equality, and the
pertinent theorem is this:
*)

theorem "(f = g) <-> (!x. f x = g x)" 
by(rule fun_eq_iff)

(*
To prove your theorem wrong, I only need one function of type (bool => bool),  
and I choose (%x. True), with the result that "(%x. True) = (%a. a | (%x. True) a)"
is True by fun_eq_iff. There are only two values, True and False, that need to
be tested to determine whether (%x. True) is equal to (%a. a | (%x. True) a).

Also, this shows that there's no recursion, unless for a particular f, f has
been defined to be recursive. Here, it appears I've defined a recursive function 
named fix_f:
*)

function fix_f :: "bool => bool" where
  "fix_f a = (%x. x | fix_f x) a"
by(auto)

(*
Of note is that the "=" used is still HOL.eq, which can be seen by cntl-clicking 
on it.

You might think that "(fix_f True)" should return "(True | fix_f True)", where
if HOL implements a short-circuited or, it would simplify to "True".

You might think that "(fix_f False)" should be an infinite loop, because
the first iteration will return "(False | fix_f False)", and so on, to infinity.

You can try to use fix_f in theorems, but it's not usable because termination
hasn't been proved.

Your options for defining recursive functions are function, fun, and primrec,
none of which will work for fix_f. The applicable documents are functions.pdf 
and isar-ref.pdf.
*)

function fix_g :: "bool => bool" where
  "fix_g a = (%x. x | fix_g x) a"
by pat_completeness auto
termination by lexicographic_order 
(*ERROR: Unfinished goal "1. False". Could not find lexicographic termination 
  order.*)

fun fix_h :: "bool => bool" where
  "fix_h a = (%x. x | fix_h x) a"
(*ERROR: Same error as for "function".*)

primrec fix_i :: "bool => bool" where
  "fix_i a = (%x. x | fix_i x) a"
(*ERROR: primrec only defines functions that use datatype.*)

 
(*********************************************************************) 
(*SHOWING THAT RECURSIVE FUNCTIONS DON'T GET "COMPUTED" AUTOMATICALLY*)
(*********************************************************************) 

fun sumXp :: "nat => nat" where
  "sumXp 0 = 0"
 |"sumXp n = n + sumXp(n - 1)"

find_theorems "sumXp" 
thm sumXp.simps
(*
Prints the simp rules created for sumXp: sumXp.simps(1), sumXp.simps(2)
*)   
 
value "sumXp 4"  
(*
The code generator prints the successor form of 10. Doing an import of
"~~/src/HOL/Library/Code_Target_Nat" will print 10, but the fact that the
successor form is being used is needed information here.
*)
  
  
theorem "sumXp 4 = 10"
apply(simp) oops
(*
But simp here doesn't do any magic computation, even though sumXp.simps(1)
and sumXp.simps(2) are automatically declared as simp rules.
*)


theorem "(!!f::(nat => nat). !!a. f = (%x. f x) ==> f a = a) ==> False"
by(auto)
(*
EXAMPLE: This example, similar to yours, will be made concrete with sumXp.
*)


theorem "sumXp = (%x. sumXp x)"
by(rule eta_contract_eq)
(*
Checking that the left-hand side will be true.
*)


theorem "sumXp = (%x. sumXp x) ==> sumXp 4 = 10"
using[[simp_trace]]
apply(simp) oops
(*
After simp is applied, the goal is "sumXp 4 = 10". The RHS hasn't been 
simplified any at all. Computations like this are a result of simp rule 
substitutions (rewriting), and simp rules are picky.
*)

theorem "sumXp = (%x. sumXp x) ==> 
  sumXp (Suc (Suc (Suc (Suc 0)))) 
    = (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))"
(*
Happy simp rules make for happy computations...
*)
using[[simp_trace]]
by(simp)
(*
...by means of rewriting. With the right form of natural numbers, the simp
rules can compute what is needed to obtain the necessary "HOL.eq a b == True", 
the rewriting of which can be seen at the end of the simp trace.
*)

(*declare[[simp_trace]]*)
value "sumXp 4"
(*
Going back, I'd like to see if simp_trace can tell me what simp rule "value" is
using to compute `value "sumXp 4"`.

It's using the function Num.nat_of_num, which cntl-clicking will take you to.
It's also using a lot of other rewrite rules.
*)

term "nat_of_num"

theorem "sumXp 4 = 10"
apply(simp add: nat_of_num.simps)
oops
(*
The message is that nat_of_num.simps are duplicate rewrite rules. It will be
easier just to ask what needs to be done to be able to prove a theorem which
uses an expression like "sumXp 4 = 10".
*)
  
(******************************************************************************)
end